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 ++++--- .../.VampireAnalyzerConfiguration.xtendbin | Bin 2382 -> 2399 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 5941 -> 5941 bytes .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 18004 -> 18006 bytes .../.Logic2VampireLanguageMapperTrace.xtendbin | Bin 3137 -> 3137 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3164 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 8246 -> 8245 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 5890 -> 6090 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 9766 -> 10536 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 3223 -> 3223 bytes ...geMapper_TypeMapperTrace_FilteredTypes.xtendbin | Bin 2643 -> 2643 bytes ...anguageMapper_TypeMapper_FilteredTypes.xtendbin | Bin 9048 -> 8978 bytes .../reasoner/builder/.Vampire2LogicMapper.xtendbin | Bin 1720 -> 1720 bytes .../reasoner/builder/.VampireHandler.xtendbin | Bin 4908 -> 4908 bytes ...ModelInterpretation_TypeInterpretation.xtendbin | Bin 1491 -> 1491 bytes ...ation_TypeInterpretation_FilteredTypes.xtendbin | Bin 1688 -> 1688 bytes .../builder/Logic2VampireLanguageMapper.java | 2 +- ...Logic2VampireLanguageMapper_RelationMapper.java | 6 +- .../Logic2VampireLanguageMapper_ScopeMapper.java | 73 ++++++++++++--------- .../Logic2VampireLanguageMapper_Support.java | 36 +++++++++- ...ireLanguageMapper_TypeMapper_FilteredTypes.java | 46 +++++-------- 25 files changed, 167 insertions(+), 125 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner') 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)) diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin index 9a2a1b15..4a4eedf5 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin index ce05b92c..55f0ac1e 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin index 379d0683..e91f89cc 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin index 76dd192f..154ff393 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin index 936ab9ca..5d6ad730 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin index e0f442f5..7c787543 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin index 493ff288..34f3b285 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin index 13281767..f8d6cd3f 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin index 1a777880..7b2b11f8 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin index e8658e7b..7e8336e2 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin index aec1688a..a2229dba 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin index e77b9866..d82649ff 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin index 100a52b8..030a0be9 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin index 231c1995..87203ed8 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin index b67a307c..65689b0c 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java index 89c9637e..6643576f 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java @@ -273,7 +273,7 @@ public class Logic2VampireLanguageMapper { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function = (VLSFunction it) -> { TypeReference _range = instanceOf.getRange(); - it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); + it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); EList _terms = it.getTerms(); VLSTerm _transformTerm = this.transformTerm(instanceOf.getValue(), trace, variables); _terms.add(_transformTerm); diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java index 561402a7..bce50fcc 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java @@ -61,7 +61,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_1 = (VLSFunction it) -> { TypeReference _range = variable.getRange(); - it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); + it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); EList _terms = it.getTerms(); VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); final Procedure1 _function_2 = (VLSVariable it_1) -> { @@ -75,7 +75,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction(); final Procedure1 _function_2 = (VLSFunction it) -> { TypeReference _range = variable.getRange(); - it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); + it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); EList _terms = it.getTerms(); VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); final Procedure1 _function_3 = (VLSVariable it_1) -> { @@ -215,7 +215,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_1 = (VLSFunction it) -> { TypeReference _get = r.getParameters().get((i).intValue()); - it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _get).getReferred().getName())); + it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _get).getReferred().getName())); EList _terms = it.getTerms(); VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); final Procedure1 _function_2 = (VLSVariable it_1) -> { diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java index 86d8b648..8967839d 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java @@ -51,42 +51,53 @@ public class Logic2VampireLanguageMapper_ScopeMapper { instances.add(cst); } } - VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function_1 = (VLSFofFormula it) -> { - it.setName("typeScope"); - it.setFofRole("axiom"); - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); - VLSVariable _duplicate = this.support.duplicate(variable); - _variables.add(_duplicate); - VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); - final Procedure1 _function_3 = (VLSEquivalent it_2) -> { - it_2.setLeft(this.support.topLevelTypeFunc()); - final Function1 _function_4 = (VLSConstant i) -> { - VLSEquality _createVLSEquality = this.factory.createVLSEquality(); - final Procedure1 _function_5 = (VLSEquality it_3) -> { - VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); - final Procedure1 _function_6 = (VLSVariable it_4) -> { - it_4.setName(variable.getName()); + if ((config.typeScopes.minNewElements != 0)) { + VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); + final Procedure1 _function_1 = (VLSFofFormula it) -> { + it.setName("typeScope"); + it.setFofRole("axiom"); + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { + EList _variables = it_1.getVariables(); + VLSVariable _duplicate = this.support.duplicate(variable); + _variables.add(_duplicate); + VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); + final Procedure1 _function_3 = (VLSEquivalent it_2) -> { + it_2.setLeft(this.support.topLevelTypeFunc()); + final Function1 _function_4 = (VLSConstant i) -> { + VLSEquality _createVLSEquality = this.factory.createVLSEquality(); + final Procedure1 _function_5 = (VLSEquality it_3) -> { + VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); + final Procedure1 _function_6 = (VLSVariable it_4) -> { + it_4.setName(variable.getName()); + }; + VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_6); + it_3.setLeft(_doubleArrow); + it_3.setRight(i); }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_6); - it_3.setLeft(_doubleArrow); - it_3.setRight(i); + return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_5); }; - return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_5); + it_2.setRight(this.support.unfoldOr(ListExtensions.map(instances, _function_4))); }; - it_2.setRight(this.support.unfoldOr(ListExtensions.map(instances, _function_4))); + VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_3); + it_1.setOperand(_doubleArrow); }; - VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_3); - it_1.setOperand(_doubleArrow); + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); + it.setFofFormula(_doubleArrow); }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); - it.setFofFormula(_doubleArrow); - }; - final VLSFofFormula cstDec = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_1); - EList _formulas = trace.specification.getFormulas(); - _formulas.add(cstDec); + final VLSFofFormula cstDec = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_1); + EList _formulas = trace.specification.getFormulas(); + _formulas.add(cstDec); + VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); + final Procedure1 _function_2 = (VLSFofFormula it) -> { + it.setName("typeUniqueness"); + it.setFofRole("axiom"); + it.setFofFormula(this.support.establishUniqueness(instances)); + }; + final VLSFofFormula uniqueness = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_2); + EList _formulas_1 = trace.specification.getFormulas(); + _formulas_1.add(uniqueness); + } } public void transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java index b111732f..dfe624be 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java @@ -3,6 +3,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; @@ -25,6 +26,7 @@ import java.util.List; import java.util.Map; import org.eclipse.emf.common.util.EList; import org.eclipse.xtend2.lib.StringConcatenation; +import org.eclipse.xtext.xbase.lib.CollectionLiterals; import org.eclipse.xtext.xbase.lib.Conversions; import org.eclipse.xtext.xbase.lib.ExclusiveRange; import org.eclipse.xtext.xbase.lib.Extension; @@ -73,6 +75,36 @@ public class Logic2VampireLanguageMapper_Support { return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); } + public VLSTerm establishUniqueness(final List terms) { + final List eqs = CollectionLiterals.newArrayList(); + List _subList = terms.subList(1, ((Object[])Conversions.unwrapArray(terms, Object.class)).length); + for (final VLSConstant t1 : _subList) { + List _subList_1 = terms.subList(0, terms.indexOf(t1)); + for (final VLSConstant t2 : _subList_1) { + { + VLSInequality _createVLSInequality = this.factory.createVLSInequality(); + final Procedure1 _function = (VLSInequality it) -> { + VLSConstant _createVLSConstant = this.factory.createVLSConstant(); + final Procedure1 _function_1 = (VLSConstant it_1) -> { + it_1.setName(t2.getName()); + }; + VLSConstant _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function_1); + it.setLeft(_doubleArrow); + VLSConstant _createVLSConstant_1 = this.factory.createVLSConstant(); + final Procedure1 _function_2 = (VLSConstant it_1) -> { + it_1.setName(t1.getName()); + }; + VLSConstant _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSConstant_1, _function_2); + it.setRight(_doubleArrow_1); + }; + final VLSInequality eq = ObjectExtensions.operator_doubleArrow(_createVLSInequality, _function); + eqs.add(eq); + } + } + } + return this.unfoldAnd(eqs); + } + protected VLSTerm unfoldAnd(final List operands) { int _size = operands.size(); boolean _equals = (_size == 1); @@ -180,7 +212,7 @@ public class Logic2VampireLanguageMapper_Support { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_1 = (VLSFunction it) -> { TypeReference _range = variable.getRange(); - it.setConstant(this.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); + it.setConstant(this.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); EList _terms = it.getTerms(); VLSVariable _createVLSVariable = this.factory.createVLSVariable(); final Procedure1 _function_2 = (VLSVariable it_1) -> { @@ -229,7 +261,7 @@ public class Logic2VampireLanguageMapper_Support { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_1 = (VLSFunction it) -> { TypeReference _range = variable.getRange(); - it.setConstant(this.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); + it.setConstant(this.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); EList _terms = it.getTerms(); VLSVariable _createVLSVariable = this.factory.createVLSVariable(); final Procedure1 _function_2 = (VLSVariable it_1) -> { diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java index 71e98871..1e845d94 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java @@ -115,47 +115,39 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log return Boolean.valueOf((!_isIsAbstract)); }; Iterable _filter_1 = IterableExtensions.filter(types, _function_1); - for (final Type type_2 : _filter_1) { + for (final Type t1 : _filter_1) { { - for (final Type type2 : types) { - if ((Objects.equal(type_2, type2) || this.dfsSupertypeCheck(type_2, type2))) { + for (final Type t2 : types) { + if ((Objects.equal(t1, t2) || this.dfsSupertypeCheck(t1, t2))) { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_2 = (VLSFunction it) -> { - it.setConstant(CollectionsUtil.lookup(type2, typeTrace.type2Predicate).getConstant()); + it.setConstant(CollectionsUtil.lookup(t2, typeTrace.type2Predicate).getConstant()); EList _terms = it.getTerms(); - VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); - final Procedure1 _function_3 = (VLSVariable it_1) -> { - it_1.setName("A"); - }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_3); - _terms.add(_doubleArrow); + VLSVariable _duplicate = this.support.duplicate(variable); + _terms.add(_duplicate); }; VLSFunction _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_2); - typeTrace.type2PossibleNot.put(type2, _doubleArrow); + typeTrace.type2PossibleNot.put(t2, _doubleArrow); } else { VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); final Procedure1 _function_3 = (VLSUnaryNegation it) -> { VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction(); final Procedure1 _function_4 = (VLSFunction it_1) -> { - it_1.setConstant(CollectionsUtil.lookup(type2, typeTrace.type2Predicate).getConstant()); + it_1.setConstant(CollectionsUtil.lookup(t2, typeTrace.type2Predicate).getConstant()); EList _terms = it_1.getTerms(); - VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); - final Procedure1 _function_5 = (VLSVariable it_2) -> { - it_2.setName("A"); - }; - VLSVariable _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_5); - _terms.add(_doubleArrow_1); + VLSVariable _duplicate = this.support.duplicate(variable); + _terms.add(_duplicate); }; VLSFunction _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSFunction_1, _function_4); it.setOperand(_doubleArrow_1); }; VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_3); - typeTrace.type2PossibleNot.put(type2, _doubleArrow_1); + typeTrace.type2PossibleNot.put(t2, _doubleArrow_1); } } Collection _values = typeTrace.type2PossibleNot.values(); ArrayList _arrayList = new ArrayList(_values); - typeTrace.type2And.put(type_2, this.support.unfoldAnd(_arrayList)); + typeTrace.type2And.put(t1, this.support.unfoldAnd(_arrayList)); typeTrace.type2PossibleNot.clear(); } } @@ -166,21 +158,17 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_3 = (VLSUniversalQuantifier it_1) -> { EList _variables = it_1.getVariables(); - VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); - final Procedure1 _function_4 = (VLSVariable it_2) -> { - it_2.setName("A"); - }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_4); - _variables.add(_doubleArrow); + VLSVariable _duplicate = this.support.duplicate(variable); + _variables.add(_duplicate); VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); - final Procedure1 _function_5 = (VLSEquivalent it_2) -> { + final Procedure1 _function_4 = (VLSEquivalent it_2) -> { it_2.setLeft(this.support.topLevelTypeFunc()); Collection _values = typeTrace.type2And.values(); ArrayList _arrayList = new ArrayList(_values); it_2.setRight(this.support.unfoldOr(_arrayList)); }; - VLSEquivalent _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_5); - it_1.setOperand(_doubleArrow_1); + VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_4); + it_1.setOperand(_doubleArrow); }; VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_3); it.setFofFormula(_doubleArrow); -- cgit v1.2.3-54-g00ecf