From 89929078ca93c74a80ad70d58934d5d6d43d0e4f Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Tue, 5 Mar 2019 21:33:28 -0500 Subject: Partially improve coding style (leaving for soccer) --- .../builder/Logic2VampireLanguageMapperTrace.xtend | 30 ++- ...ogic2VampireLanguageMapper_RelationMapper.xtend | 159 +++++++-------- .../Logic2VampireLanguageMapper_Support.xtend | 42 +++- ...reLanguageMapper_TypeMapper_FilteredTypes.xtend | 71 +++---- .../.VampireAnalyzerConfiguration.xtendbin | Bin 2399 -> 2399 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 5941 -> 5941 bytes .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 18006 -> 18008 bytes .../.Logic2VampireLanguageMapperTrace.xtendbin | Bin 3137 -> 3708 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3164 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 8245 -> 8177 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 6090 -> 6096 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 10536 -> 11367 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 3223 -> 3223 bytes ...geMapper_TypeMapperTrace_FilteredTypes.xtendbin | Bin 2643 -> 2643 bytes ...anguageMapper_TypeMapper_FilteredTypes.xtendbin | Bin 8978 -> 8565 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/Logic2VampireLanguageMapperTrace.java | 12 ++ ...Logic2VampireLanguageMapper_RelationMapper.java | 218 +++++++++------------ .../Logic2VampireLanguageMapper_Support.java | 54 ++++- ...ireLanguageMapper_TypeMapper_FilteredTypes.java | 75 ++----- .../output/FAMTest/vampireProblem.tptp | 38 ++-- .../dslreasoner/vampire/icse/.EcoreTest.xtendbin | Bin 6358 -> 6358 bytes .../dslreasoner/vampire/icse/.GeneralTest.xtendbin | Bin 7655 -> 7655 bytes .../vampire/test/.MedicalSystem.xtendbin | Bin 4997 -> 4997 bytes .../dslreasoner/vampire/test/.VampireTest.xtendbin | Bin 6500 -> 6500 bytes 28 files changed, 349 insertions(+), 350 deletions(-) diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend index 135b3f07..3c672f4b 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend @@ -1,15 +1,17 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable import java.util.HashMap import java.util.Map @@ -22,17 +24,29 @@ class Logic2VampireLanguageMapperTrace { public var VampireModel specification public var VLSFofFormula logicLanguageBody public var VLSTerm formula -//NOT NEEDED //public var VLSFunction constantDec + //Necessary containers public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace + public val Map type2Predicate = new HashMap; + public val Map element2Predicate = new HashMap + public val Map type2PossibleNot = new HashMap + public val Map type2And = new HashMap + + public var Map constantDefinitions + public var Map relationDefinitions + public var Map rel2Predicate = new HashMap + + +//NOT NEEDED //public var VLSFunction constantDec + + + //NOT NEEDED //public val Map constantDeclaration2LanguageField = new HashMap //public val Map constantDefinition2Function = new HashMap - public var Map constantDefinitions - public var Map relationDefinitions public val Map relationVar2VLS = new HashMap public val Map relationVar2TypeDec = new HashMap 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 6f3b13ef..23b57701 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 @@ -24,52 +24,97 @@ class Logic2VampireLanguageMapper_RelationMapper { this.base = base } - def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace) { + def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace) { // 1. store all variables in support wrt their name // 1.1 if variable has type, creating list of type declarations + val List relVar2VLS = new ArrayList + val List relVar2TypeDecComply = new ArrayList + val typedefs = new ArrayList + + for (i : 0 ..< r.parameters.length) { + + val v = createVLSVariable => [ + it.name = support.toIDMultiple("V", i.toString) + ] + relVar2VLS.add(v) + + val relType = (r.parameters.get(i) as ComplexTypeReference).referred + val varTypeComply = support.duplicate(relType.lookup(trace.type2Predicate), v) + relVar2TypeDecComply.add(varTypeComply) + + } + + val comply = createVLSFofFormula => [ + val nameArray = r.name.split(" ") + it.name = support.toIDMultiple("compliance", nameArray.get(0), + nameArray.get(2)) + it.fofRole = "axiom" + it.fofFormula = createVLSUniversalQuantifier => [ + + for (v : relVar2VLS) { + it.variables += support.duplicate(v) + } + + it.operand = createVLSImplies => [ + it.left = createVLSFunction => [ + it.constant = support.toIDMultiple("rel", r.name) + + for (i : 0 ..< r.parameters.length) { + val v = createVLSVariable => [ + it.name = relVar2VLS.get(i).name + ] + it.terms += v + } + + ] + it.right = support.unfoldAnd(relVar2TypeDecComply) + ] + ] + ] + + // trace.relationDefinition2Predicate.put(r,res) + trace.specification.formulas += comply + } + + def dispatch public void transformRelation(RelationDefinition reldef, Logic2VampireLanguageMapperTrace trace) { + + // 1. store all variables in support wrt their name + // 1.1 if variable has type, creating list of type declarations +// val VLSVariable variable = createVLSVariable => [it.name = "A"] val Map relationVar2VLS = new HashMap val Map relationVar2TypeDecComply = new HashMap val Map relationVar2TypeDecRes = new HashMap val typedefs = new ArrayList - for (variable : r.variables) { + + for (variable : reldef.variables) { val v = createVLSVariable => [ - it.name = support.toIDMultiple("Var", variable.name) + it.name = support.toIDMultiple("V", variable.name) ] relationVar2VLS.put(variable, v) val varTypeComply = createVLSFunction => [ it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) - it.terms += createVLSVariable => [ - it.name = support.toIDMultiple("Var", variable.name) - ] + it.terms += support.duplicate(v) ] relationVar2TypeDecComply.put(variable, varTypeComply) - - val varTypeRes = createVLSFunction => [ - it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) - it.terms += createVLSVariable => [ - it.name = support.toIDMultiple("Var", variable.name) - ] - ] - relationVar2TypeDecRes.put(variable, varTypeRes) + relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply)) } val comply = createVLSFofFormula => [ - it.name = support.toIDMultiple("compliance", r.name) + val nameArray = reldef.name.split(" ") + it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2), + nameArray.get(nameArray.length - 1)) it.fofRole = "axiom" it.fofFormula = createVLSUniversalQuantifier => [ - for (variable : r.variables) { - val v = createVLSVariable => [ - it.name = variable.lookup(relationVar2VLS).name - ] - it.variables += v + for (variable : reldef.variables) { + it.variables += support.duplicate(variable.lookup(relationVar2VLS)) } it.operand = createVLSImplies => [ it.left = createVLSFunction => [ - it.constant = support.toIDMultiple("rel", r.name) - for (variable : r.variables) { + it.constant = support.toIDMultiple("rel", reldef.name) + for (variable : reldef.variables) { val v = createVLSVariable => [ it.name = variable.lookup(relationVar2VLS).name ] @@ -82,10 +127,10 @@ class Logic2VampireLanguageMapper_RelationMapper { ] val res = createVLSFofFormula => [ - it.name = support.toIDMultiple("relation", r.name) + it.name = support.toIDMultiple("relation", reldef.name) it.fofRole = "axiom" it.fofFormula = createVLSUniversalQuantifier => [ - for (variable : r.variables) { + for (variable : reldef.variables) { val v = createVLSVariable => [ it.name = variable.lookup(relationVar2VLS).name ] @@ -96,8 +141,8 @@ class Logic2VampireLanguageMapper_RelationMapper { it.left = support.unfoldAnd(new ArrayList(relationVar2TypeDecRes.values)) it.right = createVLSEquivalent => [ it.left = createVLSFunction => [ - it.constant = support.toIDMultiple("rel", r.name) - for (variable : r.variables) { + it.constant = support.toIDMultiple("rel", reldef.name) + for (variable : reldef.variables) { val v = createVLSVariable => [ it.name = variable.lookup(relationVar2VLS).name ] @@ -105,7 +150,7 @@ class Logic2VampireLanguageMapper_RelationMapper { } ] - it.right = base.transformTerm(r.value, trace, relationVar2VLS) + it.right = base.transformTerm(reldef.value, trace, relationVar2VLS) ] ] @@ -119,65 +164,5 @@ class Logic2VampireLanguageMapper_RelationMapper { trace.specification.formulas += res; } - - def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace) { - - // 1. store all variables in support wrt their name - // 1.1 if variable has type, creating list of type declarations - val List relationVar2VLS = new ArrayList - val List relationVar2TypeDecComply = new ArrayList - val typedefs = new ArrayList - - for (i : 0.. [ - it.name = support.toIDMultiple("Var", i.toString) - ] - relationVar2VLS.add(v) - - val varTypeComply = createVLSFunction => [ - it.constant = support.toIDMultiple("t", (r.parameters.get(i) as ComplexTypeReference).referred.name) - it.terms += createVLSVariable => [ - it.name = support.toIDMultiple("Var", i.toString) - ] - ] - relationVar2TypeDecComply.add(varTypeComply) - - } - - - val comply = createVLSFofFormula => [ - it.name = support.toIDMultiple("compliance", r.name) - it.fofRole = "axiom" - it.fofFormula = createVLSUniversalQuantifier => [ - - for (i : 0.. [ - it.name = relationVar2VLS.get(i).name - ] - it.variables += v - - } - - it.operand = createVLSImplies => [ - it.left = createVLSFunction => [ - it.constant = support.toIDMultiple("rel", r.name) - - for (i : 0.. [ - it.name = relationVar2VLS.get(i).name - ] - it.terms += v - } - - ] - it.right = support.unfoldAnd(relationVar2TypeDecComply) - ] - ] - ] - - // trace.relationDefinition2Predicate.put(r,res) - trace.specification.formulas += comply - } } 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 06ec585c..090cf916 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 @@ -1,20 +1,21 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable import java.util.ArrayList 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 @@ -28,10 +29,28 @@ class Logic2VampireLanguageMapper_Support { ids.split("\\s+").join("_") } + //Term Handling //TODO Make more general - def protected VLSVariable duplicate(VLSVariable vrbl) { - return createVLSVariable => [it.name = vrbl.name] + def protected VLSVariable duplicate(VLSVariable term) { + return createVLSVariable => [it.name = term.name] + } + + def protected VLSFunction duplicate(VLSFunction term) { + return createVLSFunction => [ + it.constant = term.constant + for ( v : term.terms){ + it.terms += duplicate(v as VLSVariable) + } + ] } + + def protected VLSFunction duplicate(VLSFunction term, VLSVariable v) { + return createVLSFunction => [ + it.constant = term.constant + it.terms += duplicate(v) + ] + } + def protected VLSFunction topLevelTypeFunc() { return createVLSFunction => [ @@ -175,6 +194,21 @@ class Logic2VampireLanguageMapper_Support { ] } + + def protected boolean dfsSupertypeCheck(Type type, Type type2) { + // There is surely a better way to do this + if (type.supertypes.isEmpty) + return false + else { + if (type.supertypes.contains(type2)) + return true + else { + for (supertype : type.supertypes) { + if(dfsSupertypeCheck(supertype, type2)) return true + } + } + } + } 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 88e1e23a..ea72940e 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 @@ -22,21 +22,20 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp LogicproblemPackage.eINSTANCE.class } - override transformTypes(Collection types, Collection elements, - Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) { - val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes - trace.typeMapperTrace = typeTrace - - // The variable + override transformTypes(Collection types, Collection elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) { + +// val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes +// trace.typeMapperTrace = typeTrace val VLSVariable variable = createVLSVariable => [it.name = "A"] // 1. Each type (class) is a predicate with a single variable as input for (type : types) { val typePred = createVLSFunction => [ - it.constant = support.toIDMultiple("t", type.name) + it.constant = support.toIDMultiple("t", type.name.split(" ").get(0)) it.terms += support.duplicate(variable) ] - typeTrace.type2Predicate.put(type, typePred) +// typeTrace.type2Predicate.put(type, typePred) + trace.type2Predicate.put(type, typePred) } // 2. Map each ENUM type definition to fof formula @@ -44,15 +43,16 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp val List orElems = newArrayList for (e : type.elements) { val enumElemPred = createVLSFunction => [ - it.constant = support.toIDMultiple("e", e.name, type.name) + it.constant = support.toIDMultiple("e", e.name.split(" ").get(0), e.name.split(" ").get(2)) it.terms += support.duplicate(variable) ] - typeTrace.element2Predicate.put(e, enumElemPred) +// typeTrace.element2Predicate.put(e, enumElemPred) + trace.element2Predicate.put(e, enumElemPred) orElems.add(enumElemPred) } val res = createVLSFofFormula => [ - it.name = support.toIDMultiple("typeDef", type.name) + it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0)) // below is temporary solution it.fofRole = "axiom" it.fofFormula = createVLSUniversalQuantifier => [ @@ -62,7 +62,8 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp // it.constant = type.lookup(typeTrace.type2Predicate).constant // it.terms += createVLSVariable => [it.name = "A"] // ] - it.left = type.lookup(typeTrace.type2Predicate) +// it.left = type.lookup(typeTrace.type2Predicate) + it.left = type.lookup(trace.type2Predicate) it.right = support.unfoldOr(orElems) @@ -92,31 +93,23 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp 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 (t1 == t2 || dfsSupertypeCheck(t1, t2)) { - typeTrace.type2PossibleNot.put(t2, createVLSFunction => [ - it.constant = t2.lookup(typeTrace.type2Predicate).constant - it.terms += support.duplicate(variable) - ]) + if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) { +// typeTrace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(typeTrace.type2Predicate))) + trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate))) } else { - typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ - it.operand = createVLSFunction => [ - it.constant = t2.lookup(typeTrace.type2Predicate).constant - it.terms += support.duplicate(variable) - ] +// typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ + trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ + it.operand = support.duplicate(t2.lookup(trace.type2Predicate)) ]) } -// typeTrace.type2PossibleNot.put(type2, type2.lookup(typeTrace.type2Predicate)) } - typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList(typeTrace.type2PossibleNot.values))) -// typeTrace.type2And.put(type, type.lookup(typeTrace.type2Predicate) ) - typeTrace.type2PossibleNot.clear +// typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList(typeTrace.type2PossibleNot.values))) +// typeTrace.type2PossibleNot.clear + trace.type2And.put(t1, support.unfoldAnd(new ArrayList(trace.type2PossibleNot.values))) + trace.type2PossibleNot.clear } // 5. create fof function that is an or with all the elements in map - - - - val hierarch = createVLSFofFormula => [ it.name = "hierarchyHandler" it.fofRole = "axiom" @@ -124,7 +117,8 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp it.variables += support.duplicate(variable) it.operand = createVLSEquivalent => [ it.left = support.topLevelTypeFunc - it.right = support.unfoldOr(new ArrayList(typeTrace.type2And.values)) +// it.right = support.unfoldOr(new ArrayList(typeTrace.type2And.values)) + it.right = support.unfoldOr(new ArrayList(trace.type2And.values)) ] ] ] @@ -133,21 +127,6 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp } - def boolean dfsSupertypeCheck(Type type, Type type2) { - // There is surely a better way to do this - if (type.supertypes.isEmpty) - return false - else { - if (type.supertypes.contains(type2)) - return true - else { - for (supertype : type.supertypes) { - if(dfsSupertypeCheck(supertype, type2)) return true - } - } - } - } - override transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) { throw new UnsupportedOperationException("TODO: auto-generated method stub") 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 4a4eedf5..bda7463e 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 55f0ac1e..a062fcec 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 e91f89cc..5fc0da27 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 154ff393..562b9bbf 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 5d6ad730..dd7bdf86 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 7c787543..496d27b3 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 34f3b285..4a03f2ce 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 f8d6cd3f..511f4a1f 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 7b2b11f8..37e9480c 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 7e8336e2..f473c4bc 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 a2229dba..e53791d6 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 d82649ff..1b112c56 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 030a0be9..c8284658 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 87203ed8..89d4c657 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 65689b0c..3c98bd64 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/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java index 855815f8..2b491209 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java @@ -8,8 +8,10 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; import java.util.HashMap; import java.util.Map; @@ -24,10 +26,20 @@ public class Logic2VampireLanguageMapperTrace { public Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace; + public final Map type2Predicate = new HashMap(); + + public final Map element2Predicate = new HashMap(); + + public final Map type2PossibleNot = new HashMap(); + + public final Map type2And = new HashMap(); + public Map constantDefinitions; public Map relationDefinitions; + public Map rel2Predicate = new HashMap(); + public final Map relationVar2VLS = new HashMap(); public final Map relationVar2TypeDec = new HashMap(); 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 bce50fcc..4f5c6acc 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 @@ -15,6 +15,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; @@ -44,17 +45,84 @@ public class Logic2VampireLanguageMapper_RelationMapper { this.base = base; } - public void _transformRelation(final RelationDefinition r, final Logic2VampireLanguageMapperTrace trace) { + public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) { + final List relVar2VLS = new ArrayList(); + final List relVar2TypeDecComply = new ArrayList(); + final ArrayList typedefs = new ArrayList(); + int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; + ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); + for (final Integer i : _doubleDotLessThan) { + { + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function = (VLSVariable it) -> { + it.setName(this.support.toIDMultiple("V", i.toString())); + }; + final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); + relVar2VLS.add(v); + TypeReference _get = r.getParameters().get((i).intValue()); + final Type relType = ((ComplexTypeReference) _get).getReferred(); + final VLSFunction varTypeComply = this.support.duplicate(CollectionsUtil.lookup(relType, trace.type2Predicate), v); + relVar2TypeDecComply.add(varTypeComply); + } + } + VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); + final Procedure1 _function = (VLSFofFormula it) -> { + final String[] nameArray = r.getName().split(" "); + it.setName(this.support.toIDMultiple("compliance", nameArray[0], + nameArray[2])); + it.setFofRole("axiom"); + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { + for (final VLSVariable v : relVar2VLS) { + EList _variables = it_1.getVariables(); + VLSVariable _duplicate = this.support.duplicate(v); + _variables.add(_duplicate); + } + VLSImplies _createVLSImplies = this.factory.createVLSImplies(); + final Procedure1 _function_2 = (VLSImplies it_2) -> { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function_3 = (VLSFunction it_3) -> { + it_3.setConstant(this.support.toIDMultiple("rel", r.getName())); + int _length_1 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; + ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(0, _length_1, true); + for (final Integer i_1 : _doubleDotLessThan_1) { + { + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function_4 = (VLSVariable it_4) -> { + it_4.setName(relVar2VLS.get((i_1).intValue()).getName()); + }; + final VLSVariable v_1 = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_4); + EList _terms = it_3.getTerms(); + _terms.add(v_1); + } + } + }; + VLSFunction _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_3); + it_2.setLeft(_doubleArrow); + it_2.setRight(this.support.unfoldAnd(relVar2TypeDecComply)); + }; + VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_2); + it_1.setOperand(_doubleArrow); + }; + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); + it.setFofFormula(_doubleArrow); + }; + final VLSFofFormula comply = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); + EList _formulas = trace.specification.getFormulas(); + _formulas.add(comply); + } + + public void _transformRelation(final RelationDefinition reldef, final Logic2VampireLanguageMapperTrace trace) { final Map relationVar2VLS = new HashMap(); final Map relationVar2TypeDecComply = new HashMap(); final Map relationVar2TypeDecRes = new HashMap(); final ArrayList typedefs = new ArrayList(); - EList _variables = r.getVariables(); + EList _variables = reldef.getVariables(); for (final Variable variable : _variables) { { VLSVariable _createVLSVariable = this.factory.createVLSVariable(); final Procedure1 _function = (VLSVariable it) -> { - it.setName(this.support.toIDMultiple("Var", variable.getName())); + it.setName(this.support.toIDMultiple("V", variable.getName())); }; final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); relationVar2VLS.put(variable, v); @@ -63,56 +131,39 @@ public class Logic2VampireLanguageMapper_RelationMapper { TypeReference _range = variable.getRange(); 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) -> { - it_1.setName(this.support.toIDMultiple("Var", variable.getName())); - }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_2); - _terms.add(_doubleArrow); + VLSVariable _duplicate = this.support.duplicate(v); + _terms.add(_duplicate); }; final VLSFunction varTypeComply = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); relationVar2TypeDecComply.put(variable, varTypeComply); - VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction(); - final Procedure1 _function_2 = (VLSFunction it) -> { - TypeReference _range = variable.getRange(); - 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) -> { - it_1.setName(this.support.toIDMultiple("Var", variable.getName())); - }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_3); - _terms.add(_doubleArrow); - }; - final VLSFunction varTypeRes = ObjectExtensions.operator_doubleArrow(_createVLSFunction_1, _function_2); - relationVar2TypeDecRes.put(variable, varTypeRes); + relationVar2TypeDecRes.put(variable, this.support.duplicate(varTypeComply)); } } VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); final Procedure1 _function = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("compliance", r.getName())); + final String[] nameArray = reldef.getName().split(" "); + int _length = nameArray.length; + int _minus = (_length - 2); + int _length_1 = nameArray.length; + int _minus_1 = (_length_1 - 1); + it.setName(this.support.toIDMultiple("compliance", nameArray[_minus], + nameArray[_minus_1])); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { - EList _variables_1 = r.getVariables(); + EList _variables_1 = reldef.getVariables(); for (final Variable variable_1 : _variables_1) { - { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_2 = (VLSVariable it_2) -> { - it_2.setName(CollectionsUtil.lookup(variable_1, relationVar2VLS).getName()); - }; - final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_2); - EList _variables_2 = it_1.getVariables(); - _variables_2.add(v); - } + EList _variables_2 = it_1.getVariables(); + VLSVariable _duplicate = this.support.duplicate(CollectionsUtil.lookup(variable_1, relationVar2VLS)); + _variables_2.add(_duplicate); } VLSImplies _createVLSImplies = this.factory.createVLSImplies(); final Procedure1 _function_2 = (VLSImplies it_2) -> { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_3 = (VLSFunction it_3) -> { - it_3.setConstant(this.support.toIDMultiple("rel", r.getName())); - EList _variables_2 = r.getVariables(); - for (final Variable variable_2 : _variables_2) { + it_3.setConstant(this.support.toIDMultiple("rel", reldef.getName())); + EList _variables_3 = reldef.getVariables(); + for (final Variable variable_2 : _variables_3) { { VLSVariable _createVLSVariable = this.factory.createVLSVariable(); final Procedure1 _function_4 = (VLSVariable it_4) -> { @@ -139,11 +190,11 @@ public class Logic2VampireLanguageMapper_RelationMapper { final VLSFofFormula comply = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); final Procedure1 _function_1 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("relation", r.getName())); + it.setName(this.support.toIDMultiple("relation", reldef.getName())); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { - EList _variables_1 = r.getVariables(); + EList _variables_1 = reldef.getVariables(); for (final Variable variable_1 : _variables_1) { { VLSVariable _createVLSVariable = this.factory.createVLSVariable(); @@ -164,8 +215,8 @@ public class Logic2VampireLanguageMapper_RelationMapper { final Procedure1 _function_4 = (VLSEquivalent it_3) -> { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_5 = (VLSFunction it_4) -> { - it_4.setConstant(this.support.toIDMultiple("rel", r.getName())); - EList _variables_2 = r.getVariables(); + it_4.setConstant(this.support.toIDMultiple("rel", reldef.getName())); + EList _variables_2 = reldef.getVariables(); for (final Variable variable_2 : _variables_2) { { VLSVariable _createVLSVariable = this.factory.createVLSVariable(); @@ -180,7 +231,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { }; VLSFunction _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_5); it_3.setLeft(_doubleArrow); - it_3.setRight(this.base.transformTerm(r.getValue(), trace, relationVar2VLS)); + it_3.setRight(this.base.transformTerm(reldef.getValue(), trace, relationVar2VLS)); }; VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_4); it_2.setRight(_doubleArrow); @@ -198,89 +249,6 @@ public class Logic2VampireLanguageMapper_RelationMapper { _formulas_1.add(res); } - public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) { - final List relationVar2VLS = new ArrayList(); - final List relationVar2TypeDecComply = new ArrayList(); - final ArrayList typedefs = new ArrayList(); - int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; - ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); - for (final Integer i : _doubleDotLessThan) { - { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function = (VLSVariable it) -> { - it.setName(this.support.toIDMultiple("Var", i.toString())); - }; - final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); - relationVar2VLS.add(v); - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_1 = (VLSFunction it) -> { - TypeReference _get = r.getParameters().get((i).intValue()); - 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) -> { - it_1.setName(this.support.toIDMultiple("Var", i.toString())); - }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_2); - _terms.add(_doubleArrow); - }; - final VLSFunction varTypeComply = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); - relationVar2TypeDecComply.add(varTypeComply); - } - } - VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("compliance", r.getName())); - it.setFofRole("axiom"); - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { - int _length_1 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; - ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(0, _length_1, true); - for (final Integer i_1 : _doubleDotLessThan_1) { - { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_2 = (VLSVariable it_2) -> { - it_2.setName(relationVar2VLS.get((i_1).intValue()).getName()); - }; - final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_2); - EList _variables = it_1.getVariables(); - _variables.add(v); - } - } - VLSImplies _createVLSImplies = this.factory.createVLSImplies(); - final Procedure1 _function_2 = (VLSImplies it_2) -> { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_3 = (VLSFunction it_3) -> { - it_3.setConstant(this.support.toIDMultiple("rel", r.getName())); - int _length_2 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; - ExclusiveRange _doubleDotLessThan_2 = new ExclusiveRange(0, _length_2, true); - for (final Integer i_2 : _doubleDotLessThan_2) { - { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_4 = (VLSVariable it_4) -> { - it_4.setName(relationVar2VLS.get((i_2).intValue()).getName()); - }; - final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_4); - EList _terms = it_3.getTerms(); - _terms.add(v); - } - } - }; - VLSFunction _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_3); - it_2.setLeft(_doubleArrow); - it_2.setRight(this.support.unfoldAnd(relationVar2TypeDecComply)); - }; - VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_2); - it_1.setOperand(_doubleArrow); - }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); - it.setFofFormula(_doubleArrow); - }; - final VLSFofFormula comply = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); - EList _formulas = trace.specification.getFormulas(); - _formulas.add(comply); - } - public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) { if (r instanceof RelationDeclaration) { _transformRelation((RelationDeclaration)r, 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 dfe624be..35497eab 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 @@ -17,6 +17,7 @@ import com.google.common.collect.Iterables; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; import java.util.ArrayList; @@ -52,14 +53,39 @@ public class Logic2VampireLanguageMapper_Support { return IterableExtensions.join(((Iterable)Conversions.doWrapArray(ids.split("\\s+"))), "_"); } - protected VLSVariable duplicate(final VLSVariable vrbl) { + protected VLSVariable duplicate(final VLSVariable term) { VLSVariable _createVLSVariable = this.factory.createVLSVariable(); final Procedure1 _function = (VLSVariable it) -> { - it.setName(vrbl.getName()); + it.setName(term.getName()); }; return ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); } + protected VLSFunction duplicate(final VLSFunction term) { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function = (VLSFunction it) -> { + it.setConstant(term.getConstant()); + EList _terms = term.getTerms(); + for (final VLSTerm v : _terms) { + EList _terms_1 = it.getTerms(); + VLSVariable _duplicate = this.duplicate(((VLSVariable) v)); + _terms_1.add(_duplicate); + } + }; + return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); + } + + protected VLSFunction duplicate(final VLSFunction term, final VLSVariable v) { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function = (VLSFunction it) -> { + it.setConstant(term.getConstant()); + EList _terms = it.getTerms(); + VLSVariable _duplicate = this.duplicate(v); + _terms.add(_duplicate); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); + } + protected VLSFunction topLevelTypeFunc() { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function = (VLSFunction it) -> { @@ -287,6 +313,30 @@ public class Logic2VampireLanguageMapper_Support { return _xblockexpression; } + protected boolean dfsSupertypeCheck(final Type type, final Type type2) { + boolean _xifexpression = false; + boolean _isEmpty = type.getSupertypes().isEmpty(); + if (_isEmpty) { + return false; + } else { + boolean _xifexpression_1 = false; + boolean _contains = type.getSupertypes().contains(type2); + if (_contains) { + return true; + } else { + EList _supertypes = type.getSupertypes(); + for (final Type supertype : _supertypes) { + boolean _dfsSupertypeCheck = this.dfsSupertypeCheck(supertype, type2); + if (_dfsSupertypeCheck) { + return true; + } + } + } + _xifexpression = _xifexpression_1; + } + return _xifexpression; + } + protected HashMap withAddition(final Map map1, final Map map2) { HashMap _hashMap = new HashMap(map1); final Procedure1> _function = (HashMap it) -> { 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 1e845d94..b582fb96 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 @@ -4,7 +4,6 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; @@ -46,8 +45,6 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log @Override public void transformTypes(final Collection types, final Collection elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { - final Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes(); - trace.typeMapperTrace = typeTrace; VLSVariable _createVLSVariable = this.factory.createVLSVariable(); final Procedure1 _function = (VLSVariable it) -> { it.setName("A"); @@ -57,13 +54,13 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_1 = (VLSFunction it) -> { - it.setConstant(this.support.toIDMultiple("t", type.getName())); + it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0])); EList _terms = it.getTerms(); VLSVariable _duplicate = this.support.duplicate(variable); _terms.add(_duplicate); }; final VLSFunction typePred = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); - typeTrace.type2Predicate.put(type, typePred); + trace.type2Predicate.put(type, typePred); } } Iterable _filter = Iterables.filter(types, TypeDefinition.class); @@ -75,19 +72,19 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_1 = (VLSFunction it) -> { - it.setConstant(this.support.toIDMultiple("e", e.getName(), type_1.getName())); + it.setConstant(this.support.toIDMultiple("e", e.getName().split(" ")[0], e.getName().split(" ")[2])); EList _terms = it.getTerms(); VLSVariable _duplicate = this.support.duplicate(variable); _terms.add(_duplicate); }; final VLSFunction enumElemPred = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); - typeTrace.element2Predicate.put(e, enumElemPred); + trace.element2Predicate.put(e, enumElemPred); orElems.add(enumElemPred); } } VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); final Procedure1 _function_1 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("typeDef", type_1.getName())); + it.setName(this.support.toIDMultiple("typeDef", type_1.getName().split(" ")[0])); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { @@ -96,7 +93,7 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log _variables.add(_duplicate); VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); final Procedure1 _function_3 = (VLSEquivalent it_2) -> { - it_2.setLeft(CollectionsUtil.lookup(type_1, typeTrace.type2Predicate)); + it_2.setLeft(CollectionsUtil.lookup(type_1, trace.type2Predicate)); it_2.setRight(this.support.unfoldOr(orElems)); }; VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_3); @@ -118,37 +115,21 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log for (final Type t1 : _filter_1) { { 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(t2, typeTrace.type2Predicate).getConstant()); - EList _terms = it.getTerms(); - VLSVariable _duplicate = this.support.duplicate(variable); - _terms.add(_duplicate); - }; - VLSFunction _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_2); - typeTrace.type2PossibleNot.put(t2, _doubleArrow); + if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) { + trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.lookup(t2, trace.type2Predicate))); } 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(t2, typeTrace.type2Predicate).getConstant()); - EList _terms = it_1.getTerms(); - VLSVariable _duplicate = this.support.duplicate(variable); - _terms.add(_duplicate); - }; - VLSFunction _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSFunction_1, _function_4); - it.setOperand(_doubleArrow_1); + final Procedure1 _function_2 = (VLSUnaryNegation it) -> { + it.setOperand(this.support.duplicate(CollectionsUtil.lookup(t2, trace.type2Predicate))); }; - VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_3); - typeTrace.type2PossibleNot.put(t2, _doubleArrow_1); + VLSUnaryNegation _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_2); + trace.type2PossibleNot.put(t2, _doubleArrow); } } - Collection _values = typeTrace.type2PossibleNot.values(); + Collection _values = trace.type2PossibleNot.values(); ArrayList _arrayList = new ArrayList(_values); - typeTrace.type2And.put(t1, this.support.unfoldAnd(_arrayList)); - typeTrace.type2PossibleNot.clear(); + trace.type2And.put(t1, this.support.unfoldAnd(_arrayList)); + trace.type2PossibleNot.clear(); } } VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); @@ -163,7 +144,7 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); final Procedure1 _function_4 = (VLSEquivalent it_2) -> { it_2.setLeft(this.support.topLevelTypeFunc()); - Collection _values = typeTrace.type2And.values(); + Collection _values = trace.type2And.values(); ArrayList _arrayList = new ArrayList(_values); it_2.setRight(this.support.unfoldOr(_arrayList)); }; @@ -178,30 +159,6 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log _formulas.add(hierarch); } - public boolean dfsSupertypeCheck(final Type type, final Type type2) { - boolean _xifexpression = false; - boolean _isEmpty = type.getSupertypes().isEmpty(); - if (_isEmpty) { - return false; - } else { - boolean _xifexpression_1 = false; - boolean _contains = type.getSupertypes().contains(type2); - if (_contains) { - return true; - } else { - EList _supertypes = type.getSupertypes(); - for (final Type supertype : _supertypes) { - boolean _dfsSupertypeCheck = this.dfsSupertypeCheck(supertype, type2); - if (_dfsSupertypeCheck) { - return true; - } - } - } - _xifexpression = _xifexpression_1; - } - return _xifexpression; - } - @Override public List transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { throw new UnsupportedOperationException("TODO: auto-generated method stub"); diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp index 1f220d6f..865b3155 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp @@ -1,25 +1,25 @@ % This is an initial Test Comment -fof ( typeDef_FunctionType_enum , axiom , ! [ A ] : ( t_FunctionType_enum ( A ) <=> ( e_Root_literal_FunctionType_FunctionType_enum ( A ) | ( e_Intermediate_literal_FunctionType_FunctionType_enum ( A ) | e_Leaf_literal_FunctionType_FunctionType_enum ( A ) ) ) ) ) . -fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( t_FunctionalData_class ( A ) & ( t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . +fof ( typeDef_FunctionType , axiom , ! [ A ] : ( t_FunctionType ( A ) <=> ( e_Root_FunctionType ( A ) | ( e_Intermediate_FunctionType ( A ) | e_Leaf_FunctionType ( A ) ) ) ) ) . +fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( t_FunctionalData ( A ) & ( t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . fof ( typeScope , axiom , ! [ A ] : ( object ( A ) <=> ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | A = o5 ) ) ) ) ) ) . fof ( typeUniqueness , axiom , o1 != o2 & ( o1 != o3 & ( o2 != o3 & ( o1 != o4 & ( o2 != o4 & ( o3 != o4 & ( o1 != o5 & ( o2 != o5 & ( o3 != o5 & o4 != o5 ) ) ) ) ) ) ) ) ) . -fof ( compliance_interface_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalElement ( Var_0 , Var_1 ) => ( t_FunctionalElement_class ( Var_0 ) & t_FunctionalInterface_class ( Var_1 ) ) ) ) . -fof ( compliance_model_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_model_reference_FunctionalElement ( Var_0 , Var_1 ) => ( t_FunctionalElement_class ( Var_0 ) & t_FunctionalArchitectureModel_class ( Var_1 ) ) ) ) . -fof ( compliance_parent_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_parent_reference_FunctionalElement ( Var_0 , Var_1 ) => ( t_FunctionalElement_class ( Var_0 ) & t_Function_class ( Var_1 ) ) ) ) . -fof ( compliance_rootElements_reference_FunctionalArchitectureModel , axiom , ! [ Var_0 , Var_1 ] : ( rel_rootElements_reference_FunctionalArchitectureModel ( Var_0 , Var_1 ) => ( t_FunctionalArchitectureModel_class ( Var_0 ) & t_FunctionalElement_class ( Var_1 ) ) ) ) . -fof ( compliance_subElements_reference_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_subElements_reference_Function ( Var_0 , Var_1 ) => ( t_Function_class ( Var_0 ) & t_FunctionalElement_class ( Var_1 ) ) ) ) . -fof ( compliance_data_reference_FAMTerminator , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FAMTerminator ( Var_0 , Var_1 ) => ( t_FAMTerminator_class ( Var_0 ) & t_FunctionalData_class ( Var_1 ) ) ) ) . -fof ( compliance_from_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_from_reference_InformationLink ( Var_0 , Var_1 ) => ( t_InformationLink_class ( Var_0 ) & t_FunctionalOutput_class ( Var_1 ) ) ) ) . -fof ( compliance_to_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_to_reference_InformationLink ( Var_0 , Var_1 ) => ( t_InformationLink_class ( Var_0 ) & t_FunctionalInput_class ( Var_1 ) ) ) ) . -fof ( compliance_data_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( t_FunctionalInterface_class ( Var_0 ) & t_FunctionalData_class ( Var_1 ) ) ) ) . -fof ( compliance_element_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_element_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( t_FunctionalInterface_class ( Var_0 ) & t_FunctionalElement_class ( Var_1 ) ) ) ) . -fof ( compliance_IncomingLinks_reference_FunctionalInput , axiom , ! [ Var_0 , Var_1 ] : ( rel_IncomingLinks_reference_FunctionalInput ( Var_0 , Var_1 ) => ( t_FunctionalInput_class ( Var_0 ) & t_InformationLink_class ( Var_1 ) ) ) ) . -fof ( compliance_outgoingLinks_reference_FunctionalOutput , axiom , ! [ Var_0 , Var_1 ] : ( rel_outgoingLinks_reference_FunctionalOutput ( Var_0 , Var_1 ) => ( t_FunctionalOutput_class ( Var_0 ) & t_InformationLink_class ( Var_1 ) ) ) ) . -fof ( compliance_terminator_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_terminator_reference_FunctionalData ( Var_0 , Var_1 ) => ( t_FunctionalData_class ( Var_0 ) & t_FAMTerminator_class ( Var_1 ) ) ) ) . -fof ( compliance_interface_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalData ( Var_0 , Var_1 ) => ( t_FunctionalData_class ( Var_0 ) & t_FunctionalInterface_class ( Var_1 ) ) ) ) . -fof ( compliance_type_attribute_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_type_attribute_Function ( Var_0 , Var_1 ) => ( t_Function_class ( Var_0 ) & t_FunctionType_enum ( Var_1 ) ) ) ) . -fof ( compliance_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ Var_parameter_T , Var_parameter_I ] : ( rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( Var_parameter_T , Var_parameter_I ) => ( t_FAMTerminator_class ( Var_parameter_T ) & t_InformationLink_class ( Var_parameter_I ) ) ) ) . -fof ( relation_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ Var_parameter_T , Var_parameter_I ] : ( ( t_FAMTerminator_class ( Var_parameter_T ) & t_InformationLink_class ( Var_parameter_I ) ) => ( rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( Var_parameter_T , Var_parameter_I ) <=> ( ? [ Var_variable_Out ] : ( t_FunctionalOutput_class ( Var_variable_Out ) & ( rel_outgoingLinks_reference_FunctionalOutput ( Var_variable_Out , Var_parameter_I ) & rel_terminator_reference_FunctionalData ( Var_variable_Out , Var_parameter_T ) ) ) | ? [ Var_variable_In ] : ( t_FunctionalInput_class ( Var_variable_In ) & ( rel_to_reference_InformationLink ( Var_parameter_I , Var_variable_In ) & rel_terminator_reference_FunctionalData ( Var_variable_In , Var_parameter_T ) ) ) ) ) ) ) . +fof ( compliance_interface_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( rel_interface_reference_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) . +fof ( compliance_model_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( rel_model_reference_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalArchitectureModel ( V_1 ) ) ) ) . +fof ( compliance_parent_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( rel_parent_reference_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_Function ( V_1 ) ) ) ) . +fof ( compliance_rootElements_FunctionalArchitectureModel , axiom , ! [ V_0 , V_1 ] : ( rel_rootElements_reference_FunctionalArchitectureModel ( V_0 , V_1 ) => ( t_FunctionalArchitectureModel ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) . +fof ( compliance_subElements_Function , axiom , ! [ V_0 , V_1 ] : ( rel_subElements_reference_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) . +fof ( compliance_data_FAMTerminator , axiom , ! [ V_0 , V_1 ] : ( rel_data_reference_FAMTerminator ( V_0 , V_1 ) => ( t_FAMTerminator ( V_0 ) & t_FunctionalData ( V_1 ) ) ) ) . +fof ( compliance_from_InformationLink , axiom , ! [ V_0 , V_1 ] : ( rel_from_reference_InformationLink ( V_0 , V_1 ) => ( t_InformationLink ( V_0 ) & t_FunctionalOutput ( V_1 ) ) ) ) . +fof ( compliance_to_InformationLink , axiom , ! [ V_0 , V_1 ] : ( rel_to_reference_InformationLink ( V_0 , V_1 ) => ( t_InformationLink ( V_0 ) & t_FunctionalInput ( V_1 ) ) ) ) . +fof ( compliance_data_FunctionalInterface , axiom , ! [ V_0 , V_1 ] : ( rel_data_reference_FunctionalInterface ( V_0 , V_1 ) => ( t_FunctionalInterface ( V_0 ) & t_FunctionalData ( V_1 ) ) ) ) . +fof ( compliance_element_FunctionalInterface , axiom , ! [ V_0 , V_1 ] : ( rel_element_reference_FunctionalInterface ( V_0 , V_1 ) => ( t_FunctionalInterface ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) . +fof ( compliance_IncomingLinks_FunctionalInput , axiom , ! [ V_0 , V_1 ] : ( rel_IncomingLinks_reference_FunctionalInput ( V_0 , V_1 ) => ( t_FunctionalInput ( V_0 ) & t_InformationLink ( V_1 ) ) ) ) . +fof ( compliance_outgoingLinks_FunctionalOutput , axiom , ! [ V_0 , V_1 ] : ( rel_outgoingLinks_reference_FunctionalOutput ( V_0 , V_1 ) => ( t_FunctionalOutput ( V_0 ) & t_InformationLink ( V_1 ) ) ) ) . +fof ( compliance_terminator_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( rel_terminator_reference_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FAMTerminator ( V_1 ) ) ) ) . +fof ( compliance_interface_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( rel_interface_reference_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) . +fof ( compliance_type_Function , axiom , ! [ V_0 , V_1 ] : ( rel_type_attribute_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionType ( V_1 ) ) ) ) . +fof ( compliance_queries_terminatorAndInformation , axiom , ! [ V_parameter_T , V_parameter_I ] : ( rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( V_parameter_T , V_parameter_I ) => ( t_FAMTerminator_class ( V_parameter_T ) & t_InformationLink_class ( V_parameter_I ) ) ) ) . +fof ( relation_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ V_parameter_T , V_parameter_I ] : ( ( t_FAMTerminator_class ( V_parameter_T ) & t_InformationLink_class ( V_parameter_I ) ) => ( rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( V_parameter_T , V_parameter_I ) <=> ( ? [ Var_variable_Out ] : ( t_FunctionalOutput_class ( Var_variable_Out ) & ( rel_outgoingLinks_reference_FunctionalOutput ( Var_variable_Out , V_parameter_I ) & rel_terminator_reference_FunctionalData ( Var_variable_Out , V_parameter_T ) ) ) | ? [ Var_variable_In ] : ( t_FunctionalInput_class ( Var_variable_In ) & ( rel_to_reference_InformationLink ( V_parameter_I , Var_variable_In ) & rel_terminator_reference_FunctionalData ( Var_variable_In , V_parameter_T ) ) ) ) ) ) ) . fof ( upperMultiplicity_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_FunctionalInterface_class ( Var_trg_1 ) & t_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . fof ( lowerMultiplicity_model_FunctionalElement , axiom , ! [ Var_src ] : ( t_FunctionalElement_class ( Var_src ) => ? [ Var_trg_1 ] : ( t_FunctionalArchitectureModel_class ( Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) ) ) ) . fof ( upperMultiplicity_model_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_FunctionalArchitectureModel_class ( Var_trg_1 ) & t_FunctionalArchitectureModel_class ( Var_trg_2 ) ) ) => ( ( rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin index 59a3bc01..2cd47088 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin differ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin index ebca0881..b4d3bda8 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin differ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin index e9359697..ece511d9 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin differ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin index 1f7b3ee7..a7cea425 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin differ -- cgit v1.2.3-54-g00ecf