From f019f3ec81976f8e05d0c7458aba2f29b18461d0 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Tue, 5 Mar 2019 13:37:02 -0500 Subject: Implement type scope handling --- .../builder/Logic2VampireLanguageMapper.xtend | 2 +- ...ogic2VampireLanguageMapper_RelationMapper.xtend | 6 +- .../Logic2VampireLanguageMapper_ScopeMapper.xtend | 69 +++++++++------------- .../Logic2VampireLanguageMapper_Support.xtend | 28 ++++++++- ...reLanguageMapper_TypeMapper_FilteredTypes.xtend | 24 ++++---- 5 files changed, 70 insertions(+), 59 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill') diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend index e2c15b75..54c44c72 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend @@ -238,7 +238,7 @@ class Logic2VampireLanguageMapper { def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace, Map variables) { return createVLSFunction => [ - it.constant = support.toIDMultiple("type", (instanceOf.range as ComplexTypeReference).referred.name) + it.constant = support.toIDMultiple("t", (instanceOf.range as ComplexTypeReference).referred.name) it.terms += instanceOf.value.transformTerm(trace, variables) ] } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend index 60653a42..6f3b13ef 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend @@ -39,7 +39,7 @@ class Logic2VampireLanguageMapper_RelationMapper { relationVar2VLS.put(variable, v) val varTypeComply = createVLSFunction => [ - it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) + it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) it.terms += createVLSVariable => [ it.name = support.toIDMultiple("Var", variable.name) ] @@ -47,7 +47,7 @@ class Logic2VampireLanguageMapper_RelationMapper { relationVar2TypeDecComply.put(variable, varTypeComply) val varTypeRes = createVLSFunction => [ - it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) + it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) it.terms += createVLSVariable => [ it.name = support.toIDMultiple("Var", variable.name) ] @@ -136,7 +136,7 @@ class Logic2VampireLanguageMapper_RelationMapper { relationVar2VLS.add(v) val varTypeComply = createVLSFunction => [ - it.constant = support.toIDMultiple("type", (r.parameters.get(i) as ComplexTypeReference).referred.name) + it.constant = support.toIDMultiple("t", (r.parameters.get(i) as ComplexTypeReference).referred.name) it.terms += createVLSVariable => [ it.name = support.toIDMultiple("Var", i.toString) ] diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend index 84aa521d..4b7ea3d0 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend @@ -18,7 +18,6 @@ class Logic2VampireLanguageMapper_ScopeMapper { def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { val VLSVariable variable = createVLSVariable => [it.name = "A"] - // 1. make a list of constants equaling the min number of specified objects val List instances = newArrayList for (var i = 0; i < config.typeScopes.minNewElements; i++) { @@ -28,47 +27,37 @@ class Logic2VampireLanguageMapper_ScopeMapper { ] instances.add(cst) } - - - // TODO: specify for the max - - // 2. Create initial fof formula to specify the number of elems - val cstDec = createVLSFofFormula => [ - it.name = "typeScope" - it.fofRole = "axiom" - it.fofFormula = createVLSUniversalQuantifier => [ - it.variables += support.duplicate(variable) - // check below - it.operand = createVLSEquivalent => [ - it.left = support.topLevelTypeFunc - it.right = support.unfoldOr(instances.map [ i | - createVLSEquality => [ - it.left = createVLSVariable => [it.name = variable.name] - it.right = i - ] - ]) + // TODO: specify for the max + if (config.typeScopes.minNewElements != 0) { + // 2. Create initial fof formula to specify the number of elems + val cstDec = createVLSFofFormula => [ + it.name = "typeScope" + it.fofRole = "axiom" + it.fofFormula = createVLSUniversalQuantifier => [ + it.variables += support.duplicate(variable) + // check below + it.operand = createVLSEquivalent => [ + it.left = support.topLevelTypeFunc + it.right = support.unfoldOr(instances.map [ i | + createVLSEquality => [ + it.left = createVLSVariable => [it.name = variable.name] + it.right = i + ] + ]) + ] ] ] - ] - trace.specification.formulas += cstDec - - - // TODO: specify for scope per type - - - - // 3. Specify uniqueness of elements - val uniqueness = createVLSFofFormula => [ - it.name = "typeUniqueness" - it.fofRole = "axiom" - it.fofFormula = support.unfoldOr(instances.map [ i | - createVLSEquality => [ - it.left = createVLSVariable => [it.name = variable.name] - it.right = i - ] - ]) - ] - trace.specification.formulas += cstDec + trace.specification.formulas += cstDec + + // TODO: specify for scope per type + // 3. Specify uniqueness of elements + val uniqueness = createVLSFofFormula => [ + it.name = "typeUniqueness" + it.fofRole = "axiom" + it.fofFormula = support.establishUniqueness(instances) + ] + trace.specification.formulas += uniqueness + } } } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend index e69f0d51..06ec585c 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend @@ -13,6 +13,8 @@ import java.util.HashMap import java.util.List import java.util.Map import org.eclipse.emf.common.util.EList +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality class Logic2VampireLanguageMapper_Support { private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE @@ -26,6 +28,7 @@ class Logic2VampireLanguageMapper_Support { ids.split("\\s+").join("_") } + //TODO Make more general def protected VLSVariable duplicate(VLSVariable vrbl) { return createVLSVariable => [it.name = vrbl.name] } @@ -38,6 +41,25 @@ class Logic2VampireLanguageMapper_Support { ] ] } + + //TODO Make more general + def establishUniqueness(List terms) { + val List eqs = newArrayList + for (t1 : terms.subList(1, terms.length)){ + for (t2 : terms.subList(0, terms.indexOf(t1))){ + val eq = createVLSInequality => [ + //TEMP + it.left = createVLSConstant => [it.name = t2.name] + it.right = createVLSConstant => [it.name = t1.name] + //TEMP + ] + eqs.add(eq) + } + } + + return unfoldAnd(eqs) + + } // Support Functions // booleans @@ -111,7 +133,7 @@ class Logic2VampireLanguageMapper_Support { val typedefs = new ArrayList for (variable : expression.quantifiedVariables) { val eq = createVLSFunction => [ - it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) + it.constant = toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) it.terms += createVLSVariable => [ it.name = toIDMultiple("Var", variable.name) ] @@ -138,7 +160,7 @@ class Logic2VampireLanguageMapper_Support { val typedefs = new ArrayList for (variable : expression.quantifiedVariables) { val eq = createVLSFunction => [ - it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) + it.constant = toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) it.terms += createVLSVariable => [ it.name = toIDMultiple("Var", variable.name) ] @@ -157,5 +179,7 @@ class Logic2VampireLanguageMapper_Support { def protected withAddition(Map map1, Map map2) { new HashMap(map1) => [putAll(map2)] } + + } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend index eed10656..88e1e23a 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend @@ -89,27 +89,25 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates // and store in a map -// val List type2PossibleNot = new ArrayList -// val List type2And = new ArrayList - for (type : types.filter[!isIsAbstract]) { - for (type2 : types) { + for (t1 : types.filter[!isIsAbstract]) { + for (t2 : types) { // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes - if (type == type2 || dfsSupertypeCheck(type, type2)) { - typeTrace.type2PossibleNot.put(type2, createVLSFunction => [ - it.constant = type2.lookup(typeTrace.type2Predicate).constant - it.terms += createVLSVariable => [it.name = "A"] + if (t1 == t2 || dfsSupertypeCheck(t1, t2)) { + typeTrace.type2PossibleNot.put(t2, createVLSFunction => [ + it.constant = t2.lookup(typeTrace.type2Predicate).constant + it.terms += support.duplicate(variable) ]) } else { - typeTrace.type2PossibleNot.put(type2, createVLSUnaryNegation => [ + typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ it.operand = createVLSFunction => [ - it.constant = type2.lookup(typeTrace.type2Predicate).constant - it.terms += createVLSVariable => [it.name = "A"] + it.constant = t2.lookup(typeTrace.type2Predicate).constant + it.terms += support.duplicate(variable) ] ]) } // typeTrace.type2PossibleNot.put(type2, type2.lookup(typeTrace.type2Predicate)) } - typeTrace.type2And.put(type, support.unfoldAnd(new ArrayList(typeTrace.type2PossibleNot.values))) + typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList(typeTrace.type2PossibleNot.values))) // typeTrace.type2And.put(type, type.lookup(typeTrace.type2Predicate) ) typeTrace.type2PossibleNot.clear } @@ -123,7 +121,7 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp it.name = "hierarchyHandler" it.fofRole = "axiom" it.fofFormula = createVLSUniversalQuantifier => [ - it.variables += createVLSVariable => [it.name = "A"] + it.variables += support.duplicate(variable) it.operand = createVLSEquivalent => [ it.left = support.topLevelTypeFunc it.right = support.unfoldOr(new ArrayList(typeTrace.type2And.values)) -- cgit v1.2.3-54-g00ecf