From 56df1f808fa2289c3e97d45d84bce8acc8937280 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Thu, 14 Mar 2019 03:45:46 -0400 Subject: Implement Containment mapping (partially) and revisit enum mapping --- .../builder/Logic2VampireLanguageMapper.xtend | 16 +- ...c2VampireLanguageMapper_ContainmentMapper.xtend | 123 ++++++++++++++ .../Logic2VampireLanguageMapper_ScopeMapper.xtend | 25 ++- .../Logic2VampireLanguageMapper_Support.xtend | 30 +++- .../Logic2VampireLanguageMapper_TypeMapper.xtend | 104 ++++++------ .../vampire/reasoner/.VampireSolver.xtendbin | Bin 5892 -> 5892 bytes .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 17817 -> 18129 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3164 bytes ...ampireLanguageMapper_ContainmentMapper.xtendbin | Bin 0 -> 7649 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 8209 -> 8210 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 8916 -> 9263 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 11900 -> 12311 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 9688 -> 10377 bytes .../vampire/reasoner/builder/.gitignore | 2 + .../builder/Logic2VampireLanguageMapper.java | 12 +- ...ic2VampireLanguageMapper_ContainmentMapper.java | 180 +++++++++++++++++++++ .../Logic2VampireLanguageMapper_ScopeMapper.java | 78 +++++---- .../Logic2VampireLanguageMapper_Support.java | 27 +++- .../Logic2VampireLanguageMapper_TypeMapper.java | 99 ++++++++---- .../output/FAMTest/vampireProblem.tptp | 29 ++-- .../dslreasoner/vampire/icse/GeneralTest.xtend | 4 +- .../dslreasoner/vampire/icse/.GeneralTest.xtendbin | Bin 8486 -> 8486 bytes .../ecse/dslreasoner/vampire/icse/GeneralTest.java | 4 +- 23 files changed, 590 insertions(+), 143 deletions(-) create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java 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 1dbc0055..b7ad8f3d 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 @@ -47,6 +47,8 @@ class Logic2VampireLanguageMapper { private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support; @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper( this) + @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ContainmentMapper containmentMapper = new Logic2VampireLanguageMapper_ContainmentMapper( + this) @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper( this) @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper( @@ -80,24 +82,26 @@ class Logic2VampireLanguageMapper { // SCOPE MAPPER scopeMapper.transformScope(config, trace) - trace.constantDefinitions = problem.collectConstantDefinitions + // RELATION MAPPER trace.relationDefinitions = problem.collectRelationDefinitions - problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] + + // CONTAINMENT MAPPER + containmentMapper.transformContainment(problem.containmentHierarchies, trace) + // CONSTANT MAPPER // only transforms definitions + trace.constantDefinitions = problem.collectConstantDefinitions // problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstant(it, trace)] problem.constants.filter(ConstantDefinition).forEach [ this.constantMapper.transformConstantDefinitionSpecification(it, trace) ] - // ////////////////// - // Transform Assertions - // ////////////////// + // ASSERTION MAPPER for (assertion : problem.assertions) { transformAssertion(assertion, trace) } - + // OUTPUT return new TracedOutput(specification, trace) } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend new file mode 100644 index 00000000..0820f47d --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend @@ -0,0 +1,123 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy +import java.util.List +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference + +class Logic2VampireLanguageMapper_ContainmentMapper { + private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE + private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support + val Logic2VampireLanguageMapper base + private val VLSVariable variable = createVLSVariable => [it.name = "A"] + + public new(Logic2VampireLanguageMapper base) { + this.base = base + } + + def public void transformContainment(List hierarchies, + Logic2VampireLanguageMapperTrace trace) { + + // TODO CONSIDER CASE WHERE MULTIPLE CONTAINMMENT HIERARCHIES EXIST + // TEMP + val hierarchy = hierarchies.get(0) + + val containmentListCopy = hierarchy.typesOrderedInHierarchy + val relationsList = hierarchy.containmentRelations + // STEP 1 + // Find root element + for (l : relationsList) { + var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type + containmentListCopy.remove(pointingTo) + for (c : pointingTo.subtypes) { + containmentListCopy.remove(c) + } + } + + // State that there must exist 1 and only 1 root element + val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString + val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate)) + + val contTop = createVLSFofFormula => [ + it.name = support.toIDMultiple("containment_topLevel", topName) + it.fofRole = "axiom" + + it.fofFormula = createVLSUniversalQuantifier => [ + it.variables += support.duplicate(variable) + it.operand = createVLSEquivalent => [ + it.left = topTerm + it.right = createVLSEquality => [ + it.left = support.duplicate(variable) + it.right = createVLSConstant => [ + it.name = "o1" + ] + ] + ] + ] +// it.fofFormula = support.duplicate( +// topTerm, +// createVLSFunctionAsTerm => [ +// it.functor = "o1" +// ] +// ) + ] + trace.specification.formulas += contTop + + // STEP 2 + // for each edge, if the pointedTo element exists,the edge must exist also + val varA = createVLSVariable => [it.name = "A"] + val varB = createVLSVariable => [it.name = "B"] + val varList = newArrayList(varB, varA) + + for (l : relationsList) { + val relName = (l as RelationDeclaration).lookup(trace.rel2Predicate).constant.toString + val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type + val toType = (l.parameters.get(1) as ComplexTypeReference).referred as Type + + val relFormula = createVLSFofFormula => [ + it.name = support.toIDMultiple("containment", relName) + it.fofRole = "axiom" + + it.fofFormula = createVLSUniversalQuantifier => [ + it.variables += support.duplicate(varA) + it.operand = createVLSImplies => [ + it.left = support.duplicate(toType.lookup(trace.type2Predicate), varA) + it.right = createVLSExistentialQuantifier => [ + it.variables += support.duplicate(varB) + it.operand = createVLSAnd => [ + it.left = support.duplicate(fromType.lookup(trace.type2Predicate), varB) + it.right = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), + varList) + ] + ] + + createVLSEquality => [ + it.left = support.duplicate(variable) + it.right = createVLSConstant => [ + it.name = "o1" + ] + ] + ] + ] + ] + trace.specification.formulas += relFormula + var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type + containmentListCopy.remove(pointingTo) + for (c : pointingTo.subtypes) { + containmentListCopy.remove(c) + } + } + + // STEP 3 + // Ensure that an objct only has 1 parent + // STEP 4 + // Ensure that there are no cycles in the hierarchy (maybe same as for step3?) + } +} 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 5c5eaff3..548deda4 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 @@ -10,6 +10,8 @@ import java.util.Map import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* import java.util.HashMap +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm +import java.util.List class Logic2VampireLanguageMapper_ScopeMapper { private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE @@ -24,7 +26,8 @@ class Logic2VampireLanguageMapper_ScopeMapper { def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { // TODO HANDLE ERRORS RELATED TO MAX > MIN -// TODO HANDLE ERROR RELATED TO SUM(MIN TYPES) > MAX OBJECTS +// TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS +// TODO HANDLE // TODO NOT SPECIFIED MEANS =0 ? // 1. make a list of constants equaling the min number of specified objects val GLOBAL_MIN = config.typeScopes.minNewElements @@ -34,18 +37,22 @@ class Logic2VampireLanguageMapper_ScopeMapper { // Handling Minimum_General if (GLOBAL_MIN != 0) { - getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) // fix last param + getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) + for(i : trace.uniqueInstances){ + localInstances.add(support.duplicate(i)) + } + makeFofFormula(localInstances, trace, true, null) } // Handling Maximum_General if (GLOBAL_MAX != 0) { - getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true) // fix last param - makeFofFormula(localInstances, trace, false, null) + getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true) + makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null) } // Handling Minimum_Specific - var i = 0 + var i = 1 var minNum = -1 var Map startPoints = new HashMap for (t : config.typeScopes.minNewElementsByType.keySet) { @@ -106,13 +113,17 @@ class Logic2VampireLanguageMapper_ScopeMapper { def protected void makeFofFormula(ArrayList list, Logic2VampireLanguageMapperTrace trace, boolean minimum, Type type) { var nm = "" - var VLSFunction tm = null + var VLSTerm tm = null if (type === null) { nm = "object" tm = support.topLevelTypeFunc } else { nm = type.lookup(trace.type2Predicate).constant.toString - tm = support.duplicate(type.lookup(trace.type2Predicate)) + tm = createVLSAnd => [ + it.left = support.duplicate(type.lookup(trace.type2Predicate)) + it.right = support.topLevelTypeFunc + ] +// tm = support.duplicate(type.lookup(trace.type2Predicate)) } val name = nm val term = tm 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 021cb0ea..8d00d3e7 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 @@ -37,11 +37,11 @@ class Logic2VampireLanguageMapper_Support { def protected VLSVariable duplicate(VLSVariable term) { return createVLSVariable => [it.name = term.name] } - + def protected VLSFunctionAsTerm duplicate(VLSFunctionAsTerm term) { return createVLSFunctionAsTerm => [it.functor = term.functor] } - + def protected VLSConstant duplicate(VLSConstant term) { return createVLSConstant => [it.name = term.name] } @@ -61,14 +61,23 @@ class Logic2VampireLanguageMapper_Support { it.terms += duplicate(v) ] } - + + def protected VLSFunction duplicate(VLSFunction term, List vars) { + return createVLSFunction => [ + it.constant = term.constant + for (v : vars) { + it.terms += duplicate(v) + } + ] + } + def protected VLSFunction duplicate(VLSFunction term, VLSFunctionAsTerm v) { return createVLSFunction => [ it.constant = term.constant it.terms += duplicate(v) ] } - + def protected VLSConstant toConstant(VLSFunctionAsTerm term) { return createVLSConstant => [ it.name = term.functor @@ -84,6 +93,13 @@ class Logic2VampireLanguageMapper_Support { ] } + def protected VLSFunction topLevelTypeFunc(VLSVariable v) { + return createVLSFunction => [ + it.constant = "object" + it.terms += duplicate(v) + ] + } + def protected VLSFunction topLevelTypeFunc(VLSFunctionAsTerm v) { return createVLSFunction => [ it.constant = "object" @@ -173,14 +189,16 @@ class Logic2VampireLanguageMapper_Support { */ // QUANTIFIERS + VARIABLES def protected VLSTerm createQuantifiedExpression(Logic2VampireLanguageMapper mapper, - QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map variables, boolean isUniversal) { + QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map variables, + boolean isUniversal) { val variableMap = expression.quantifiedVariables.toInvertedMap [ v | createVLSVariable => [it.name = toIDMultiple("V", v.name)] ] val typedefs = new ArrayList for (variable : expression.quantifiedVariables) { - val eq = duplicate((variable.range as ComplexTypeReference).referred.lookup(trace.type2Predicate), variable.lookup(variableMap)) + val eq = duplicate((variable.range as ComplexTypeReference).referred.lookup(trace.type2Predicate), + variable.lookup(variableMap)) typedefs.add(eq) } if (isUniversal) { diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend index e12180fa..4c4247ce 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend @@ -1,12 +1,12 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd 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.VampireLanguageFactory import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage import java.util.ArrayList @@ -14,7 +14,6 @@ import java.util.Collection import java.util.List import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* -import java.util.Collections class Logic2VampireLanguageMapper_TypeMapper { private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE @@ -28,10 +27,8 @@ class Logic2VampireLanguageMapper_TypeMapper { def protected 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"] + var globalCounter = 0 // 1. Each type (class) is a predicate with a single variable as input for (type : types) { @@ -39,94 +36,109 @@ class Logic2VampireLanguageMapper_TypeMapper { it.constant = support.toIDMultiple("t", type.name.split(" ").get(0)) it.terms += support.duplicate(variable) ] -// typeTrace.type2Predicate.put(type, typePred) trace.type2Predicate.put(type, typePred) } // 2. Map each ENUM type definition to fof formula for (type : types.filter(TypeDefinition)) { + + // Create a VLSFunction for each Enum Element val List orElems = newArrayList for (e : type.elements) { val enumElemPred = createVLSFunction => [ val splitName = e.name.split(" ") - if( splitName.length > 2) { + if (splitName.length > 2) { it.constant = support.toIDMultiple("e", splitName.get(0), splitName.get(2)) - } - else { + } else { it.constant = support.toIDMultiple("e", splitName.get(0)) } it.terms += support.duplicate(variable) ] -// typeTrace.element2Predicate.put(e, enumElemPred) trace.element2Predicate.put(e, enumElemPred) - orElems.add(enumElemPred) } + // Similar to InheritanceHierarchy for the Enum + val List possibleNots = newArrayList + val List typeDefs = newArrayList + + for (t1 : type.elements) { + for (t2 : type.elements) { + if (t1 == t2) { + val fct = support.duplicate(t2.lookup(trace.element2Predicate), variable) + possibleNots.add(fct) + } else { + val op = support.duplicate(t2.lookup(trace.element2Predicate), variable) + val negFct = createVLSUnaryNegation => [ + it.operand = op + ] + possibleNots.add(negFct) + } + } + typeDefs.add(support.unfoldAnd(possibleNots)) + possibleNots.clear + } + + // Implement Enum Inheritence Hierarchy val res = createVLSFofFormula => [ it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0)) - // below is temporary solution it.fofRole = "axiom" it.fofFormula = createVLSUniversalQuantifier => [ it.variables += support.duplicate(variable) it.operand = createVLSEquivalent => [ it.left = type.lookup(trace.type2Predicate) - it.right = support.unfoldOr(orElems) + it.right = createVLSAnd => [ + it.left = support.topLevelTypeFunc(variable) + it.right = support.unfoldOr(typeDefs) + ] +// it.right = support.unfoldOr((typeDefs)) + ] ] - ] trace.specification.formulas += res - // Create objects for the enum elements - val List enumScopeElems = newArrayList - for (var i = 0; i < type.elements.length; i++) { + for (var i = globalCounter; i < globalCounter+type.elements.length; i++) { + // Create objects for the enum elements val num = i + 1 val cstTerm = createVLSFunctionAsTerm => [ it.functor = "eo" + num ] val cst = support.toConstant(cstTerm) trace.uniqueInstances.add(cst) - val fct = support.duplicate(type.elements.get(i).lookup(trace.element2Predicate), cstTerm) - enumScopeElems.add(fct) - - //For paradox Only - for (var j = 0; j < type.elements.length; j++) { - if(j != i) { - val op = support.duplicate(type.elements.get(j).lookup(trace.element2Predicate), cstTerm) - val negFct = createVLSUnaryNegation => [ - it.operand = op + + val index = i + val enumScope = createVLSFofFormula => [ + it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0), + type.elements.get(index).name.split(" ").get(0)) + it.fofRole = "axiom" + it.fofFormula = createVLSUniversalQuantifier => [ + it.variables += support.duplicate(variable) + it.operand = createVLSEquivalent => [ + it.left = createVLSEquality => [ + it.left = support.duplicate(variable) + it.right = support.duplicate(support.toConstant(cstTerm)) + ] + it.right = support.duplicate(type.elements.get(index).lookup(trace.element2Predicate), + variable) ] - enumScopeElems.add(negFct) - } - } - //End Paradox -// enumScopeElems.add(support.topLevelTypeFunc(cstTerm)) + ] + ] + + trace.specification.formulas += enumScope + } - - - - val enumScope = createVLSFofFormula => [ - it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0)) - // below is temporary solution - it.fofRole = "axiom" - it.fofFormula = support.unfoldAnd(enumScopeElems) - ] - - trace.specification.formulas += enumScope + globalCounter+=type.elements.size } // HIERARCHY HANDLER // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates // and store in a map -// println(types.filter[!isIsAbstract]) - for (t1 : types.filter[!isIsAbstract].filter(TypeDeclaration)) { + 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 || 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 => [ trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ it.operand = support.duplicate(t2.lookup(trace.type2Predicate)) ]) 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 052e0175..8e50f399 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 1296bf9e..99ba52b8 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/.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 fd625384..7b01a284 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_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin new file mode 100644 index 00000000..9f455fdd Binary files /dev/null and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.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 978571d2..0b91349d 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 b98f0332..07e249ce 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 8238a89e..115249ba 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 f64a218b..2e86d0c7 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/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore index ec8107e8..8a9aa4bb 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore @@ -38,3 +38,5 @@ /.VampireSolutionModel.java._trace /.VampireCallerWithTimeout.java._trace /.Logic2VampireLanguageMapper_ScopeMapper.java._trace +/.Logic2VampireLanguageMapper_Containment.java._trace +/.Logic2VampireLanguageMapper_ContainmentMapper.java._trace 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 afe77bbe..36a727b2 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 @@ -3,6 +3,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ConstantMapper; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ContainmentMapper; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_RelationMapper; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ScopeMapper; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; @@ -82,6 +83,9 @@ public class Logic2VampireLanguageMapper { @Accessors(AccessorType.PUBLIC_GETTER) private final Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper(this); + @Accessors(AccessorType.PUBLIC_GETTER) + private final Logic2VampireLanguageMapper_ContainmentMapper containmentMapper = new Logic2VampireLanguageMapper_ContainmentMapper(this); + @Accessors(AccessorType.PUBLIC_GETTER) private final Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(this); @@ -114,12 +118,13 @@ public class Logic2VampireLanguageMapper { this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace); } this.scopeMapper.transformScope(config, trace); - trace.constantDefinitions = this.collectConstantDefinitions(problem); trace.relationDefinitions = this.collectRelationDefinitions(problem); final Consumer _function_3 = (Relation it) -> { this.relationMapper.transformRelation(it, trace); }; problem.getRelations().forEach(_function_3); + this.containmentMapper.transformContainment(problem.getContainmentHierarchies(), trace); + trace.constantDefinitions = this.collectConstantDefinitions(problem); final Consumer _function_4 = (ConstantDefinition it) -> { this.constantMapper.transformConstantDefinitionSpecification(it, trace); }; @@ -427,6 +432,11 @@ public class Logic2VampireLanguageMapper { return this.constantMapper; } + @Pure + public Logic2VampireLanguageMapper_ContainmentMapper getContainmentMapper() { + return this.containmentMapper; + } + @Pure public Logic2VampireLanguageMapper_RelationMapper getRelationMapper() { return this.relationMapper; diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java new file mode 100644 index 00000000..da0e5615 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java @@ -0,0 +1,180 @@ +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.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; +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.Relation; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; +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.logicproblem.ContainmentHierarchy; +import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; +import java.util.ArrayList; +import java.util.List; +import org.eclipse.emf.common.util.EList; +import org.eclipse.xtext.xbase.lib.CollectionLiterals; +import org.eclipse.xtext.xbase.lib.Extension; +import org.eclipse.xtext.xbase.lib.ObjectExtensions; +import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; + +@SuppressWarnings("all") +public class Logic2VampireLanguageMapper_ContainmentMapper { + @Extension + private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; + + private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); + + private final Logic2VampireLanguageMapper base; + + private final VLSVariable variable = ObjectExtensions.operator_doubleArrow(this.factory.createVLSVariable(), ((Procedure1) (VLSVariable it) -> { + it.setName("A"); + })); + + public Logic2VampireLanguageMapper_ContainmentMapper(final Logic2VampireLanguageMapper base) { + this.base = base; + } + + public void transformContainment(final List hierarchies, final Logic2VampireLanguageMapperTrace trace) { + final ContainmentHierarchy hierarchy = hierarchies.get(0); + final EList containmentListCopy = hierarchy.getTypesOrderedInHierarchy(); + final EList relationsList = hierarchy.getContainmentRelations(); + for (final Relation l : relationsList) { + { + TypeReference _get = l.getParameters().get(1); + Type _referred = ((ComplexTypeReference) _get).getReferred(); + Type pointingTo = ((Type) _referred); + containmentListCopy.remove(pointingTo); + EList _subtypes = pointingTo.getSubtypes(); + for (final Type c : _subtypes) { + containmentListCopy.remove(c); + } + } + } + final String topName = CollectionsUtil.lookup(containmentListCopy.get(0), trace.type2Predicate).getConstant().toString(); + final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.lookup(containmentListCopy.get(0), trace.type2Predicate)); + VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); + final Procedure1 _function = (VLSFofFormula it) -> { + it.setName(this.support.toIDMultiple("containment_topLevel", topName)); + it.setFofRole("axiom"); + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { + EList _variables = it_1.getVariables(); + VLSVariable _duplicate = this.support.duplicate(this.variable); + _variables.add(_duplicate); + VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); + final Procedure1 _function_2 = (VLSEquivalent it_2) -> { + it_2.setLeft(topTerm); + VLSEquality _createVLSEquality = this.factory.createVLSEquality(); + final Procedure1 _function_3 = (VLSEquality it_3) -> { + it_3.setLeft(this.support.duplicate(this.variable)); + VLSConstant _createVLSConstant = this.factory.createVLSConstant(); + final Procedure1 _function_4 = (VLSConstant it_4) -> { + it_4.setName("o1"); + }; + VLSConstant _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function_4); + it_3.setRight(_doubleArrow); + }; + VLSEquality _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_3); + it_2.setRight(_doubleArrow); + }; + VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_2); + it_1.setOperand(_doubleArrow); + }; + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); + it.setFofFormula(_doubleArrow); + }; + final VLSFofFormula contTop = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); + EList _formulas = trace.specification.getFormulas(); + _formulas.add(contTop); + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function_1 = (VLSVariable it) -> { + it.setName("A"); + }; + final VLSVariable varA = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_1); + VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); + final Procedure1 _function_2 = (VLSVariable it) -> { + it.setName("B"); + }; + final VLSVariable varB = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_2); + final ArrayList varList = CollectionLiterals.newArrayList(varB, varA); + for (final Relation l_1 : relationsList) { + { + final String relName = CollectionsUtil.lookup(((RelationDeclaration) l_1), trace.rel2Predicate).getConstant().toString(); + TypeReference _get = l_1.getParameters().get(0); + Type _referred = ((ComplexTypeReference) _get).getReferred(); + final Type fromType = ((Type) _referred); + TypeReference _get_1 = l_1.getParameters().get(1); + Type _referred_1 = ((ComplexTypeReference) _get_1).getReferred(); + final Type toType = ((Type) _referred_1); + VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); + final Procedure1 _function_3 = (VLSFofFormula it) -> { + it.setName(this.support.toIDMultiple("containment", relName)); + it.setFofRole("axiom"); + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_4 = (VLSUniversalQuantifier it_1) -> { + EList _variables = it_1.getVariables(); + VLSVariable _duplicate = this.support.duplicate(varA); + _variables.add(_duplicate); + VLSImplies _createVLSImplies = this.factory.createVLSImplies(); + final Procedure1 _function_5 = (VLSImplies it_2) -> { + it_2.setLeft(this.support.duplicate(CollectionsUtil.lookup(toType, trace.type2Predicate), varA)); + VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); + final Procedure1 _function_6 = (VLSExistentialQuantifier it_3) -> { + EList _variables_1 = it_3.getVariables(); + VLSVariable _duplicate_1 = this.support.duplicate(varB); + _variables_1.add(_duplicate_1); + VLSAnd _createVLSAnd = this.factory.createVLSAnd(); + final Procedure1 _function_7 = (VLSAnd it_4) -> { + it_4.setLeft(this.support.duplicate(CollectionsUtil.lookup(fromType, trace.type2Predicate), varB)); + it_4.setRight(this.support.duplicate(CollectionsUtil.lookup(((RelationDeclaration) l_1), trace.rel2Predicate), varList)); + }; + VLSAnd _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSAnd, _function_7); + it_3.setOperand(_doubleArrow); + }; + VLSExistentialQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSExistentialQuantifier, _function_6); + it_2.setRight(_doubleArrow); + VLSEquality _createVLSEquality = this.factory.createVLSEquality(); + final Procedure1 _function_7 = (VLSEquality it_3) -> { + it_3.setLeft(this.support.duplicate(this.variable)); + VLSConstant _createVLSConstant = this.factory.createVLSConstant(); + final Procedure1 _function_8 = (VLSConstant it_4) -> { + it_4.setName("o1"); + }; + VLSConstant _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function_8); + it_3.setRight(_doubleArrow_1); + }; + ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_7); + }; + VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_5); + it_1.setOperand(_doubleArrow); + }; + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); + it.setFofFormula(_doubleArrow); + }; + final VLSFofFormula relFormula = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_3); + EList _formulas_1 = trace.specification.getFormulas(); + _formulas_1.add(relFormula); + TypeReference _get_2 = l_1.getParameters().get(1); + Type _referred_2 = ((ComplexTypeReference) _get_2).getReferred(); + Type pointingTo = ((Type) _referred_2); + containmentListCopy.remove(pointingTo); + EList _subtypes = pointingTo.getSubtypes(); + for (final Type c : _subtypes) { + containmentListCopy.remove(c); + } + } + } + } +} 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 1950cad0..d2a6bff2 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 @@ -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.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; @@ -48,16 +49,19 @@ public class Logic2VampireLanguageMapper_ScopeMapper { public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { final int GLOBAL_MIN = config.typeScopes.minNewElements; final int GLOBAL_MAX = config.typeScopes.maxNewElements; - final ArrayList localInstances = CollectionLiterals.newArrayList(); + final ArrayList localInstances = CollectionLiterals.newArrayList(); if ((GLOBAL_MIN != 0)) { this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false); + for (final VLSConstant i : trace.uniqueInstances) { + localInstances.add(this.support.duplicate(i)); + } this.makeFofFormula(localInstances, trace, true, null); } if ((GLOBAL_MAX != 0)) { this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true); - this.makeFofFormula(localInstances, trace, false, null); + this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); } - int i = 0; + int i_1 = 1; int minNum = (-1); Map startPoints = new HashMap(); Set _keySet = config.typeScopes.minNewElementsByType.keySet(); @@ -65,10 +69,10 @@ public class Logic2VampireLanguageMapper_ScopeMapper { { minNum = (CollectionsUtil.lookup(t, config.typeScopes.minNewElementsByType)).intValue(); if ((minNum != 0)) { - this.getInstanceConstants((i + minNum), i, localInstances, trace, true, false); - startPoints.put(t, Integer.valueOf(i)); - int _i = i; - i = (_i + minNum); + this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false); + startPoints.put(t, Integer.valueOf(i_1)); + int _i = i_1; + i_1 = (_i + minNum); this.makeFofFormula(localInstances, trace, true, t); } } @@ -83,8 +87,8 @@ public class Logic2VampireLanguageMapper_ScopeMapper { this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); } if (((maxNum).intValue() != minNum)) { - int instEndInd = Math.min(GLOBAL_MAX, ((i + (maxNum).intValue()) - minNum)); - this.getInstanceConstants(instEndInd, i, localInstances, trace, false, false); + int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + (maxNum).intValue()) - minNum)); + this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false); this.makeFofFormula(localInstances, trace, false, t_1); } } @@ -126,18 +130,24 @@ public class Logic2VampireLanguageMapper_ScopeMapper { protected void makeFofFormula(final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean minimum, final Type type) { String nm = ""; - VLSFunction tm = null; + VLSTerm tm = null; if ((type == null)) { nm = "object"; tm = this.support.topLevelTypeFunc(); } else { nm = CollectionsUtil.lookup(type, trace.type2Predicate).getConstant().toString(); - tm = this.support.duplicate(CollectionsUtil.lookup(type, trace.type2Predicate)); + VLSAnd _createVLSAnd = this.factory.createVLSAnd(); + final Procedure1 _function = (VLSAnd it) -> { + it.setLeft(this.support.duplicate(CollectionsUtil.lookup(type, trace.type2Predicate))); + it.setRight(this.support.topLevelTypeFunc()); + }; + VLSAnd _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSAnd, _function); + tm = _doubleArrow; } final String name = nm; - final VLSFunction term = tm; + final VLSTerm term = tm; VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function = (VLSFofFormula it) -> { + final Procedure1 _function_1 = (VLSFofFormula it) -> { String _xifexpression = null; if (minimum) { _xifexpression = "min"; @@ -147,53 +157,53 @@ public class Logic2VampireLanguageMapper_ScopeMapper { it.setName(this.support.toIDMultiple("typeScope", _xifexpression, name)); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { + final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { EList _variables = it_1.getVariables(); VLSVariable _duplicate = this.support.duplicate(this.variable); _variables.add(_duplicate); VLSImplies _createVLSImplies = this.factory.createVLSImplies(); - final Procedure1 _function_2 = (VLSImplies it_2) -> { + final Procedure1 _function_3 = (VLSImplies it_2) -> { if (minimum) { - final Function1 _function_3 = (VLSTerm i) -> { + final Function1 _function_4 = (VLSTerm i) -> { VLSEquality _createVLSEquality = this.factory.createVLSEquality(); - final Procedure1 _function_4 = (VLSEquality it_3) -> { + final Procedure1 _function_5 = (VLSEquality it_3) -> { VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_5 = (VLSVariable it_4) -> { + final Procedure1 _function_6 = (VLSVariable it_4) -> { it_4.setName(this.variable.getName()); }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_5); - it_3.setLeft(_doubleArrow); + VLSVariable _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_6); + it_3.setLeft(_doubleArrow_1); it_3.setRight(i); }; - return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_4); + return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_5); }; - it_2.setLeft(this.support.unfoldOr(ListExtensions.map(list, _function_3))); + it_2.setLeft(this.support.unfoldOr(ListExtensions.map(list, _function_4))); it_2.setRight(term); } else { it_2.setLeft(term); - final Function1 _function_4 = (VLSTerm i) -> { + final Function1 _function_5 = (VLSTerm i) -> { VLSEquality _createVLSEquality = this.factory.createVLSEquality(); - final Procedure1 _function_5 = (VLSEquality it_3) -> { + final Procedure1 _function_6 = (VLSEquality it_3) -> { VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_6 = (VLSVariable it_4) -> { + final Procedure1 _function_7 = (VLSVariable it_4) -> { it_4.setName(this.variable.getName()); }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_6); - it_3.setLeft(_doubleArrow); + VLSVariable _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_7); + it_3.setLeft(_doubleArrow_1); it_3.setRight(i); }; - return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_5); + return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_6); }; - it_2.setRight(this.support.unfoldOr(ListExtensions.map(list, _function_4))); + it_2.setRight(this.support.unfoldOr(ListExtensions.map(list, _function_5))); } }; - VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_2); - it_1.setOperand(_doubleArrow); + VLSImplies _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_3); + it_1.setOperand(_doubleArrow_1); }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); - it.setFofFormula(_doubleArrow); + VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); + it.setFofFormula(_doubleArrow_1); }; - final VLSFofFormula cstDec = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); + final VLSFofFormula cstDec = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_1); EList _formulas = trace.specification.getFormulas(); _formulas.add(cstDec); } 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 e2ff7a0e..119d01f1 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 @@ -104,6 +104,19 @@ public class Logic2VampireLanguageMapper_Support { return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); } + protected VLSFunction duplicate(final VLSFunction term, final List vars) { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function = (VLSFunction it) -> { + it.setConstant(term.getConstant()); + for (final VLSVariable v : vars) { + EList _terms = it.getTerms(); + VLSVariable _duplicate = this.duplicate(v); + _terms.add(_duplicate); + } + }; + return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); + } + protected VLSFunction duplicate(final VLSFunction term, final VLSFunctionAsTerm v) { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function = (VLSFunction it) -> { @@ -138,6 +151,17 @@ public class Logic2VampireLanguageMapper_Support { return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); } + protected VLSFunction topLevelTypeFunc(final VLSVariable v) { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function = (VLSFunction it) -> { + it.setConstant("object"); + EList _terms = it.getTerms(); + VLSVariable _duplicate = this.duplicate(v); + _terms.add(_duplicate); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); + } + protected VLSFunction topLevelTypeFunc(final VLSFunctionAsTerm v) { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function = (VLSFunction it) -> { @@ -284,7 +308,8 @@ public class Logic2VampireLanguageMapper_Support { for (final Variable variable : _quantifiedVariables) { { TypeReference _range = variable.getRange(); - final VLSFunction eq = this.duplicate(CollectionsUtil.lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate), CollectionsUtil.lookup(variable, variableMap)); + final VLSFunction eq = this.duplicate(CollectionsUtil.lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate), + CollectionsUtil.lookup(variable, variableMap)); typedefs.add(eq); } } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java index b8d74f36..ec759ebf 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java @@ -3,8 +3,10 @@ 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.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; @@ -18,7 +20,6 @@ import com.google.common.base.Objects; import com.google.common.collect.Iterables; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; @@ -56,6 +57,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { it.setName("A"); }; final VLSVariable variable = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); + int globalCounter = 0; for (final Type type : types) { { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); @@ -92,7 +94,31 @@ public class Logic2VampireLanguageMapper_TypeMapper { }; final VLSFunction enumElemPred = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); trace.element2Predicate.put(e, enumElemPred); - orElems.add(enumElemPred); + } + } + final List possibleNots = CollectionLiterals.newArrayList(); + final List typeDefs = CollectionLiterals.newArrayList(); + EList _elements_1 = type_1.getElements(); + for (final DefinedElement t1 : _elements_1) { + { + EList _elements_2 = type_1.getElements(); + for (final DefinedElement t2 : _elements_2) { + boolean _equals = Objects.equal(t1, t2); + if (_equals) { + final VLSFunction fct = this.support.duplicate(CollectionsUtil.lookup(t2, trace.element2Predicate), variable); + possibleNots.add(fct); + } else { + final VLSFunction op = this.support.duplicate(CollectionsUtil.lookup(t2, trace.element2Predicate), variable); + VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); + final Procedure1 _function_1 = (VLSUnaryNegation it) -> { + it.setOperand(op); + }; + final VLSUnaryNegation negFct = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_1); + possibleNots.add(negFct); + } + } + typeDefs.add(this.support.unfoldAnd(possibleNots)); + possibleNots.clear(); } } VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); @@ -107,7 +133,13 @@ public class Logic2VampireLanguageMapper_TypeMapper { VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); final Procedure1 _function_3 = (VLSEquivalent it_2) -> { it_2.setLeft(CollectionsUtil.lookup(type_1, trace.type2Predicate)); - it_2.setRight(this.support.unfoldOr(orElems)); + VLSAnd _createVLSAnd = this.factory.createVLSAnd(); + final Procedure1 _function_4 = (VLSAnd it_3) -> { + it_3.setLeft(this.support.topLevelTypeFunc(variable)); + it_3.setRight(this.support.unfoldOr(typeDefs)); + }; + VLSAnd _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSAnd, _function_4); + it_2.setRight(_doubleArrow); }; VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_3); it_1.setOperand(_doubleArrow); @@ -118,8 +150,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { final VLSFofFormula res = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_1); EList _formulas = trace.specification.getFormulas(); _formulas.add(res); - final List enumScopeElems = CollectionLiterals.newArrayList(); - for (int i = 0; (i < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); i++) { + for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) { { final int num = (i + 1); VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); @@ -129,38 +160,50 @@ public class Logic2VampireLanguageMapper_TypeMapper { final VLSFunctionAsTerm cstTerm = ObjectExtensions.operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); final VLSConstant cst = this.support.toConstant(cstTerm); trace.uniqueInstances.add(cst); - final VLSFunction fct = this.support.duplicate(CollectionsUtil.lookup(type_1.getElements().get(i), trace.element2Predicate), cstTerm); - enumScopeElems.add(fct); - for (int j = 0; (j < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); j++) { - if ((j != i)) { - final VLSFunction op = this.support.duplicate(CollectionsUtil.lookup(type_1.getElements().get(j), trace.element2Predicate), cstTerm); - VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); - final Procedure1 _function_3 = (VLSUnaryNegation it) -> { - it.setOperand(op); + final int index = i; + VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); + final Procedure1 _function_3 = (VLSFofFormula it) -> { + it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0], + type_1.getElements().get(index).getName().split(" ")[0])); + it.setFofRole("axiom"); + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_4 = (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_5 = (VLSEquivalent it_2) -> { + VLSEquality _createVLSEquality = this.factory.createVLSEquality(); + final Procedure1 _function_6 = (VLSEquality it_3) -> { + it_3.setLeft(this.support.duplicate(variable)); + it_3.setRight(this.support.duplicate(this.support.toConstant(cstTerm))); + }; + VLSEquality _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_6); + it_2.setLeft(_doubleArrow); + it_2.setRight(this.support.duplicate(CollectionsUtil.lookup(type_1.getElements().get(index), trace.element2Predicate), variable)); }; - final VLSUnaryNegation negFct = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_3); - enumScopeElems.add(negFct); - } - } + VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_5); + it_1.setOperand(_doubleArrow); + }; + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); + it.setFofFormula(_doubleArrow); + }; + final VLSFofFormula enumScope = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_3); + EList _formulas_1 = trace.specification.getFormulas(); + _formulas_1.add(enumScope); } } - VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); - final Procedure1 _function_2 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0])); - it.setFofRole("axiom"); - it.setFofFormula(this.support.unfoldAnd(enumScopeElems)); - }; - final VLSFofFormula enumScope = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_2); - EList _formulas_1 = trace.specification.getFormulas(); - _formulas_1.add(enumScope); + int _globalCounter = globalCounter; + int _size = type_1.getElements().size(); + globalCounter = (_globalCounter + _size); } } final Function1 _function_1 = (Type it) -> { boolean _isIsAbstract = it.isIsAbstract(); return Boolean.valueOf((!_isIsAbstract)); }; - Iterable _filter_1 = Iterables.filter(IterableExtensions.filter(types, _function_1), TypeDeclaration.class); - for (final TypeDeclaration t1 : _filter_1) { + Iterable _filter_1 = IterableExtensions.filter(types, _function_1); + for (final Type t1 : _filter_1) { { for (final Type t2 : types) { if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) { 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 265e7762..3109ccc2 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,14 +1,16 @@ % This is an initial Test Comment -fof ( typeDef_FunctionType , axiom , ! [ A ] : ( t_FunctionType ( A ) <=> ( e_Root_FunctionType ( A ) | ( e_Intermediate_FunctionType ( A ) | e_Leaf_FunctionType ( A ) ) ) ) ) . -fof ( enumScope_FunctionType , axiom , e_Root_FunctionType ( eo1 ) & ( ~ e_Intermediate_FunctionType ( eo1 ) & ( ~ e_Leaf_FunctionType ( eo1 ) & ( e_Intermediate_FunctionType ( eo2 ) & ( ~ e_Root_FunctionType ( eo2 ) & ( ~ e_Leaf_FunctionType ( eo2 ) & ( e_Leaf_FunctionType ( eo3 ) & ( ~ e_Root_FunctionType ( eo3 ) & ~ e_Intermediate_FunctionType ( eo3 ) ) ) ) ) ) ) ) ) . -fof ( inheritanceHierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalInput ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( t_Function ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalData ( A ) & ( t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( t_InformationLink ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . -fof ( typeScope_min_object , axiom , ! [ A ] : ( ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = o5 | A = o6 ) ) ) ) ) => object ( A ) ) ) . -fof ( typeScope_max_object , axiom , ! [ A ] : ( object ( A ) => ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = o5 | ( A = o6 | ( A = o7 | A = o8 ) ) ) ) ) ) ) ) ) . -fof ( typeScope_min_t_FunctionalOutput , axiom , ! [ A ] : ( A = o1 => t_FunctionalOutput ( A ) ) ) . -fof ( typeScope_min_t_Function , axiom , ! [ A ] : ( ( A = o2 | ( A = o3 | A = o4 ) ) => t_Function ( A ) ) ) . -fof ( typeScope_min_t_FunctionalInterface , axiom , ! [ A ] : ( ( A = o5 | A = o6 ) => t_FunctionalInterface ( A ) ) ) . -fof ( typeScope_max_t_FunctionalOutput , axiom , ! [ A ] : ( t_FunctionalOutput ( A ) => ( A = o1 | ( A = o7 | A = o8 ) ) ) ) . -fof ( typeScope_max_t_Function , axiom , ! [ A ] : ( t_Function ( A ) => ( A = o2 | ( A = o3 | ( A = o4 | ( A = o7 | A = o8 ) ) ) ) ) ) . +fof ( typeDef_FunctionType , axiom , ! [ A ] : ( t_FunctionType ( A ) <=> ( object ( A ) & ( ( e_Root_FunctionType ( A ) & ( ~ e_Intermediate_FunctionType ( A ) & ~ e_Leaf_FunctionType ( A ) ) ) | ( ( ~ e_Root_FunctionType ( A ) & ( e_Intermediate_FunctionType ( A ) & ~ e_Leaf_FunctionType ( A ) ) ) | ( ~ e_Root_FunctionType ( A ) & ( ~ e_Intermediate_FunctionType ( A ) & e_Leaf_FunctionType ( A ) ) ) ) ) ) ) ) . +fof ( enumScope_FunctionType_Root , axiom , ! [ A ] : ( A = eo1 <=> e_Root_FunctionType ( A ) ) ) . +fof ( enumScope_FunctionType_Intermediate , axiom , ! [ A ] : ( A = eo2 <=> e_Intermediate_FunctionType ( A ) ) ) . +fof ( enumScope_FunctionType_Leaf , axiom , ! [ A ] : ( A = eo3 <=> e_Leaf_FunctionType ( A ) ) ) . +fof ( inheritanceHierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_FAMTerminator ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . +fof ( typeScope_min_object , axiom , ! [ A ] : ( ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = o5 | ( A = o6 | ( A = eo1 | ( A = eo2 | A = eo3 ) ) ) ) ) ) ) ) => object ( A ) ) ) . +fof ( typeScope_max_object , axiom , ! [ A ] : ( object ( A ) => ( A = eo1 | ( A = eo2 | ( A = eo3 | ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = o5 | ( A = o6 | ( A = o7 | A = o8 ) ) ) ) ) ) ) ) ) ) ) ) . +fof ( typeScope_min_t_FunctionalInterface , axiom , ! [ A ] : ( ( A = o2 | A = o3 ) => ( t_FunctionalInterface ( A ) & object ( A ) ) ) ) . +fof ( typeScope_min_t_Function , axiom , ! [ A ] : ( A = o4 => ( t_Function ( A ) & object ( A ) ) ) ) . +fof ( typeScope_min_t_FunctionalOutput , axiom , ! [ A ] : ( ( A = o5 | ( A = o6 | A = o7 ) ) => ( t_FunctionalOutput ( A ) & object ( A ) ) ) ) . +fof ( typeScope_max_t_Function , axiom , ! [ A ] : ( ( t_Function ( A ) & object ( A ) ) => ( A = o4 | A = o8 ) ) ) . +fof ( typeScope_max_t_FunctionalOutput , axiom , ! [ A ] : ( ( t_FunctionalOutput ( A ) & object ( A ) ) => ( A = o5 | ( A = o6 | ( A = o7 | A = o8 ) ) ) ) ) . fof ( typeUniqueness , axiom , eo1 != eo2 & ( eo1 != eo3 & ( eo2 != eo3 & ( eo1 != o1 & ( eo2 != o1 & ( eo3 != o1 & ( eo1 != o2 & ( eo2 != o2 & ( eo3 != o2 & ( o1 != o2 & ( eo1 != o3 & ( eo2 != o3 & ( eo3 != o3 & ( o1 != o3 & ( o2 != o3 & ( eo1 != o4 & ( eo2 != o4 & ( eo3 != o4 & ( o1 != o4 & ( o2 != o4 & ( o3 != o4 & ( eo1 != o5 & ( eo2 != o5 & ( eo3 != o5 & ( o1 != o5 & ( o2 != o5 & ( o3 != o5 & ( o4 != o5 & ( eo1 != o6 & ( eo2 != o6 & ( eo3 != o6 & ( o1 != o6 & ( o2 != o6 & ( o3 != o6 & ( o4 != o6 & ( o5 != o6 & ( eo1 != o7 & ( eo2 != o7 & ( eo3 != o7 & ( o1 != o7 & ( o2 != o7 & ( o3 != o7 & ( o4 != o7 & ( o5 != o7 & ( o6 != o7 & ( eo1 != o8 & ( eo2 != o8 & ( eo3 != o8 & ( o1 != o8 & ( o2 != o8 & ( o3 != o8 & ( o4 != o8 & ( o5 != o8 & ( o6 != o8 & o7 != o8 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . fof ( compliance_interface_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) . fof ( compliance_model_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_model_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalArchitectureModel ( V_1 ) ) ) ) . @@ -25,6 +27,13 @@ fof ( compliance_outgoingLinks_FunctionalOutput , axiom , ! [ V_0 , V_1 ] : ( r_ fof ( compliance_terminator_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( r_terminator_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FAMTerminator ( V_1 ) ) ) ) . fof ( compliance_interface_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) . fof ( compliance_type_Function , axiom , ! [ V_0 , V_1 ] : ( r_type_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionType ( V_1 ) ) ) ) . +fof ( containment_topLevel_t_FunctionalArchitectureModel , axiom , ! [ A ] : ( t_FunctionalArchitectureModel ( A ) <=> A = o1 ) ) . +fof ( containment_r_interface_FunctionalElement , axiom , ! [ A ] : ( t_FunctionalInterface ( A ) => ? [ B ] : ( t_FunctionalElement ( B ) & r_interface_FunctionalElement ( B , A ) ) ) ) . +fof ( containment_r_rootElements_FunctionalArchitectureModel , axiom , ! [ A ] : ( t_FunctionalElement ( A ) => ? [ B ] : ( t_FunctionalArchitectureModel ( B ) & r_rootElements_FunctionalArchitectureModel ( B , A ) ) ) ) . +fof ( containment_r_subElements_Function , axiom , ! [ A ] : ( t_FunctionalElement ( A ) => ? [ B ] : ( t_Function ( B ) & r_subElements_Function ( B , A ) ) ) ) . +fof ( containment_r_data_FunctionalInterface , axiom , ! [ A ] : ( t_FunctionalData ( A ) => ? [ B ] : ( t_FunctionalInterface ( B ) & r_data_FunctionalInterface ( B , A ) ) ) ) . +fof ( containment_r_outgoingLinks_FunctionalOutput , axiom , ! [ A ] : ( t_InformationLink ( A ) => ? [ B ] : ( t_FunctionalOutput ( B ) & r_outgoingLinks_FunctionalOutput ( B , A ) ) ) ) . +fof ( containment_r_terminator_FunctionalData , axiom , ! [ A ] : ( t_FAMTerminator ( A ) => ? [ B ] : ( t_FunctionalData ( B ) & r_terminator_FunctionalData ( B , A ) ) ) ) . fof ( upperMultiplicity_interface_FunctionalElement , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalElement ( V_src ) & ( t_FunctionalInterface ( V_trg_1 ) & t_FunctionalInterface ( V_trg_2 ) ) ) => ( ( r_interface_FunctionalElement ( V_src , V_trg_1 ) & r_interface_FunctionalElement ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . fof ( lowerMultiplicity_model_FunctionalElement , axiom , ! [ V_src ] : ( t_FunctionalElement ( V_src ) => ? [ V_trg_1 ] : ( t_FunctionalArchitectureModel ( V_trg_1 ) & r_model_FunctionalElement ( V_src , V_trg_1 ) ) ) ) . fof ( upperMultiplicity_model_FunctionalElement , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalElement ( V_src ) & ( t_FunctionalArchitectureModel ( V_trg_1 ) & t_FunctionalArchitectureModel ( V_trg_2 ) ) ) => ( ( r_model_FunctionalElement ( V_src , V_trg_1 ) & r_model_FunctionalElement ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend index b67a867a..86c9092a 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend @@ -65,13 +65,13 @@ class GeneralTest { // Minimum Scope typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace, list2MapMin.get(Function.simpleName) - ), 3) + ), 1) typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace, list2MapMin.get(functionalarchitecture.FunctionalInterface.simpleName) ), 2) typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace, list2MapMin.get(FunctionalOutput.simpleName) - ), 1) + ), 3) // Maximum Scope typeMapMax.put(ecore2Logic.TypeofEClass( 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 ff2a8e18..ce6042ea 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/icse/GeneralTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java index 7d3be50d..13a0e74a 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java @@ -85,13 +85,13 @@ public class GeneralTest { final Map list2MapMax = IterableExtensions.toMap(metamodel.getClasses(), _function_1); typeMapMin.put( ecore2Logic.TypeofEClass(modelGenerationProblem.getTrace(), - list2MapMin.get(Function.class.getSimpleName())), Integer.valueOf(3)); + list2MapMin.get(Function.class.getSimpleName())), Integer.valueOf(1)); typeMapMin.put( ecore2Logic.TypeofEClass(modelGenerationProblem.getTrace(), list2MapMin.get(functionalarchitecture.FunctionalInterface.class.getSimpleName())), Integer.valueOf(2)); typeMapMin.put( ecore2Logic.TypeofEClass(modelGenerationProblem.getTrace(), - list2MapMin.get(FunctionalOutput.class.getSimpleName())), Integer.valueOf(1)); + list2MapMin.get(FunctionalOutput.class.getSimpleName())), Integer.valueOf(3)); typeMapMax.put( ecore2Logic.TypeofEClass( modelGenerationProblem.getTrace(), -- cgit v1.2.3-54-g00ecf