diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire')
14 files changed, 334 insertions, 64 deletions
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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 @@ | |||
38 | /.VampireSolutionModel.java._trace | 38 | /.VampireSolutionModel.java._trace |
39 | /.VampireCallerWithTimeout.java._trace | 39 | /.VampireCallerWithTimeout.java._trace |
40 | /.Logic2VampireLanguageMapper_ScopeMapper.java._trace | 40 | /.Logic2VampireLanguageMapper_ScopeMapper.java._trace |
41 | /.Logic2VampireLanguageMapper_Containment.java._trace | ||
42 | /.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; | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ConstantMapper; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ConstantMapper; |
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ContainmentMapper; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_RelationMapper; | 7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_RelationMapper; |
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ScopeMapper; | 8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ScopeMapper; |
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | 9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; |
@@ -83,6 +84,9 @@ public class Logic2VampireLanguageMapper { | |||
83 | private final Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper(this); | 84 | private final Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper(this); |
84 | 85 | ||
85 | @Accessors(AccessorType.PUBLIC_GETTER) | 86 | @Accessors(AccessorType.PUBLIC_GETTER) |
87 | private final Logic2VampireLanguageMapper_ContainmentMapper containmentMapper = new Logic2VampireLanguageMapper_ContainmentMapper(this); | ||
88 | |||
89 | @Accessors(AccessorType.PUBLIC_GETTER) | ||
86 | private final Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(this); | 90 | private final Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(this); |
87 | 91 | ||
88 | @Accessors(AccessorType.PUBLIC_GETTER) | 92 | @Accessors(AccessorType.PUBLIC_GETTER) |
@@ -114,12 +118,13 @@ public class Logic2VampireLanguageMapper { | |||
114 | this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace); | 118 | this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace); |
115 | } | 119 | } |
116 | this.scopeMapper.transformScope(config, trace); | 120 | this.scopeMapper.transformScope(config, trace); |
117 | trace.constantDefinitions = this.collectConstantDefinitions(problem); | ||
118 | trace.relationDefinitions = this.collectRelationDefinitions(problem); | 121 | trace.relationDefinitions = this.collectRelationDefinitions(problem); |
119 | final Consumer<Relation> _function_3 = (Relation it) -> { | 122 | final Consumer<Relation> _function_3 = (Relation it) -> { |
120 | this.relationMapper.transformRelation(it, trace); | 123 | this.relationMapper.transformRelation(it, trace); |
121 | }; | 124 | }; |
122 | problem.getRelations().forEach(_function_3); | 125 | problem.getRelations().forEach(_function_3); |
126 | this.containmentMapper.transformContainment(problem.getContainmentHierarchies(), trace); | ||
127 | trace.constantDefinitions = this.collectConstantDefinitions(problem); | ||
123 | final Consumer<ConstantDefinition> _function_4 = (ConstantDefinition it) -> { | 128 | final Consumer<ConstantDefinition> _function_4 = (ConstantDefinition it) -> { |
124 | this.constantMapper.transformConstantDefinitionSpecification(it, trace); | 129 | this.constantMapper.transformConstantDefinitionSpecification(it, trace); |
125 | }; | 130 | }; |
@@ -428,6 +433,11 @@ public class Logic2VampireLanguageMapper { | |||
428 | } | 433 | } |
429 | 434 | ||
430 | @Pure | 435 | @Pure |
436 | public Logic2VampireLanguageMapper_ContainmentMapper getContainmentMapper() { | ||
437 | return this.containmentMapper; | ||
438 | } | ||
439 | |||
440 | @Pure | ||
431 | public Logic2VampireLanguageMapper_RelationMapper getRelationMapper() { | 441 | public Logic2VampireLanguageMapper_RelationMapper getRelationMapper() { |
432 | return this.relationMapper; | 442 | return this.relationMapper; |
433 | } | 443 | } |
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | ||
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy; | ||
23 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
24 | import java.util.ArrayList; | ||
25 | import java.util.List; | ||
26 | import org.eclipse.emf.common.util.EList; | ||
27 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
28 | import org.eclipse.xtext.xbase.lib.Extension; | ||
29 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
30 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
31 | |||
32 | @SuppressWarnings("all") | ||
33 | public class Logic2VampireLanguageMapper_ContainmentMapper { | ||
34 | @Extension | ||
35 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
36 | |||
37 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
38 | |||
39 | private final Logic2VampireLanguageMapper base; | ||
40 | |||
41 | private final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(this.factory.createVLSVariable(), ((Procedure1<VLSVariable>) (VLSVariable it) -> { | ||
42 | it.setName("A"); | ||
43 | })); | ||
44 | |||
45 | public Logic2VampireLanguageMapper_ContainmentMapper(final Logic2VampireLanguageMapper base) { | ||
46 | this.base = base; | ||
47 | } | ||
48 | |||
49 | public void transformContainment(final List<ContainmentHierarchy> hierarchies, final Logic2VampireLanguageMapperTrace trace) { | ||
50 | final ContainmentHierarchy hierarchy = hierarchies.get(0); | ||
51 | final EList<Type> containmentListCopy = hierarchy.getTypesOrderedInHierarchy(); | ||
52 | final EList<Relation> relationsList = hierarchy.getContainmentRelations(); | ||
53 | for (final Relation l : relationsList) { | ||
54 | { | ||
55 | TypeReference _get = l.getParameters().get(1); | ||
56 | Type _referred = ((ComplexTypeReference) _get).getReferred(); | ||
57 | Type pointingTo = ((Type) _referred); | ||
58 | containmentListCopy.remove(pointingTo); | ||
59 | EList<Type> _subtypes = pointingTo.getSubtypes(); | ||
60 | for (final Type c : _subtypes) { | ||
61 | containmentListCopy.remove(c); | ||
62 | } | ||
63 | } | ||
64 | } | ||
65 | final String topName = CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate).getConstant().toString(); | ||
66 | final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate)); | ||
67 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
68 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
69 | it.setName(this.support.toIDMultiple("containment_topLevel", topName)); | ||
70 | it.setFofRole("axiom"); | ||
71 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
72 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | ||
73 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
74 | VLSVariable _duplicate = this.support.duplicate(this.variable); | ||
75 | _variables.add(_duplicate); | ||
76 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
77 | final Procedure1<VLSEquivalent> _function_2 = (VLSEquivalent it_2) -> { | ||
78 | it_2.setLeft(topTerm); | ||
79 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
80 | final Procedure1<VLSEquality> _function_3 = (VLSEquality it_3) -> { | ||
81 | it_3.setLeft(this.support.duplicate(this.variable)); | ||
82 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
83 | final Procedure1<VLSConstant> _function_4 = (VLSConstant it_4) -> { | ||
84 | it_4.setName("o1"); | ||
85 | }; | ||
86 | VLSConstant _doubleArrow = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_4); | ||
87 | it_3.setRight(_doubleArrow); | ||
88 | }; | ||
89 | VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_3); | ||
90 | it_2.setRight(_doubleArrow); | ||
91 | }; | ||
92 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_2); | ||
93 | it_1.setOperand(_doubleArrow); | ||
94 | }; | ||
95 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
96 | it.setFofFormula(_doubleArrow); | ||
97 | }; | ||
98 | final VLSFofFormula contTop = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
99 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
100 | _formulas.add(contTop); | ||
101 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
102 | final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> { | ||
103 | it.setName("A"); | ||
104 | }; | ||
105 | final VLSVariable varA = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1); | ||
106 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
107 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it) -> { | ||
108 | it.setName("B"); | ||
109 | }; | ||
110 | final VLSVariable varB = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); | ||
111 | final ArrayList<VLSVariable> varList = CollectionLiterals.<VLSVariable>newArrayList(varB, varA); | ||
112 | for (final Relation l_1 : relationsList) { | ||
113 | { | ||
114 | final String relName = CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate).getConstant().toString(); | ||
115 | TypeReference _get = l_1.getParameters().get(0); | ||
116 | Type _referred = ((ComplexTypeReference) _get).getReferred(); | ||
117 | final Type fromType = ((Type) _referred); | ||
118 | TypeReference _get_1 = l_1.getParameters().get(1); | ||
119 | Type _referred_1 = ((ComplexTypeReference) _get_1).getReferred(); | ||
120 | final Type toType = ((Type) _referred_1); | ||
121 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
122 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { | ||
123 | it.setName(this.support.toIDMultiple("containment", relName)); | ||
124 | it.setFofRole("axiom"); | ||
125 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
126 | final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> { | ||
127 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
128 | VLSVariable _duplicate = this.support.duplicate(varA); | ||
129 | _variables.add(_duplicate); | ||
130 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
131 | final Procedure1<VLSImplies> _function_5 = (VLSImplies it_2) -> { | ||
132 | it_2.setLeft(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate), varA)); | ||
133 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | ||
134 | final Procedure1<VLSExistentialQuantifier> _function_6 = (VLSExistentialQuantifier it_3) -> { | ||
135 | EList<VLSVariable> _variables_1 = it_3.getVariables(); | ||
136 | VLSVariable _duplicate_1 = this.support.duplicate(varB); | ||
137 | _variables_1.add(_duplicate_1); | ||
138 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); | ||
139 | final Procedure1<VLSAnd> _function_7 = (VLSAnd it_4) -> { | ||
140 | it_4.setLeft(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(fromType, trace.type2Predicate), varB)); | ||
141 | it_4.setRight(this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate), varList)); | ||
142 | }; | ||
143 | VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_7); | ||
144 | it_3.setOperand(_doubleArrow); | ||
145 | }; | ||
146 | VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_6); | ||
147 | it_2.setRight(_doubleArrow); | ||
148 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
149 | final Procedure1<VLSEquality> _function_7 = (VLSEquality it_3) -> { | ||
150 | it_3.setLeft(this.support.duplicate(this.variable)); | ||
151 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
152 | final Procedure1<VLSConstant> _function_8 = (VLSConstant it_4) -> { | ||
153 | it_4.setName("o1"); | ||
154 | }; | ||
155 | VLSConstant _doubleArrow_1 = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_8); | ||
156 | it_3.setRight(_doubleArrow_1); | ||
157 | }; | ||
158 | ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7); | ||
159 | }; | ||
160 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_5); | ||
161 | it_1.setOperand(_doubleArrow); | ||
162 | }; | ||
163 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); | ||
164 | it.setFofFormula(_doubleArrow); | ||
165 | }; | ||
166 | final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_3); | ||
167 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
168 | _formulas_1.add(relFormula); | ||
169 | TypeReference _get_2 = l_1.getParameters().get(1); | ||
170 | Type _referred_2 = ((ComplexTypeReference) _get_2).getReferred(); | ||
171 | Type pointingTo = ((Type) _referred_2); | ||
172 | containmentListCopy.remove(pointingTo); | ||
173 | EList<Type> _subtypes = pointingTo.getSubtypes(); | ||
174 | for (final Type c : _subtypes) { | ||
175 | containmentListCopy.remove(c); | ||
176 | } | ||
177 | } | ||
178 | } | ||
179 | } | ||
180 | } | ||
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; | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; |
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | 9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; |
@@ -48,16 +49,19 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
48 | public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { | 49 | public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { |
49 | final int GLOBAL_MIN = config.typeScopes.minNewElements; | 50 | final int GLOBAL_MIN = config.typeScopes.minNewElements; |
50 | final int GLOBAL_MAX = config.typeScopes.maxNewElements; | 51 | final int GLOBAL_MAX = config.typeScopes.maxNewElements; |
51 | final ArrayList<Object> localInstances = CollectionLiterals.<Object>newArrayList(); | 52 | final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList(); |
52 | if ((GLOBAL_MIN != 0)) { | 53 | if ((GLOBAL_MIN != 0)) { |
53 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false); | 54 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false); |
55 | for (final VLSConstant i : trace.uniqueInstances) { | ||
56 | localInstances.add(this.support.duplicate(i)); | ||
57 | } | ||
54 | this.makeFofFormula(localInstances, trace, true, null); | 58 | this.makeFofFormula(localInstances, trace, true, null); |
55 | } | 59 | } |
56 | if ((GLOBAL_MAX != 0)) { | 60 | if ((GLOBAL_MAX != 0)) { |
57 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true); | 61 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true); |
58 | this.makeFofFormula(localInstances, trace, false, null); | 62 | this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); |
59 | } | 63 | } |
60 | int i = 0; | 64 | int i_1 = 1; |
61 | int minNum = (-1); | 65 | int minNum = (-1); |
62 | Map<Type, Integer> startPoints = new HashMap<Type, Integer>(); | 66 | Map<Type, Integer> startPoints = new HashMap<Type, Integer>(); |
63 | Set<Type> _keySet = config.typeScopes.minNewElementsByType.keySet(); | 67 | Set<Type> _keySet = config.typeScopes.minNewElementsByType.keySet(); |
@@ -65,10 +69,10 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
65 | { | 69 | { |
66 | minNum = (CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType)).intValue(); | 70 | minNum = (CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType)).intValue(); |
67 | if ((minNum != 0)) { | 71 | if ((minNum != 0)) { |
68 | this.getInstanceConstants((i + minNum), i, localInstances, trace, true, false); | 72 | this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false); |
69 | startPoints.put(t, Integer.valueOf(i)); | 73 | startPoints.put(t, Integer.valueOf(i_1)); |
70 | int _i = i; | 74 | int _i = i_1; |
71 | i = (_i + minNum); | 75 | i_1 = (_i + minNum); |
72 | this.makeFofFormula(localInstances, trace, true, t); | 76 | this.makeFofFormula(localInstances, trace, true, t); |
73 | } | 77 | } |
74 | } | 78 | } |
@@ -83,8 +87,8 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
83 | this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); | 87 | this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); |
84 | } | 88 | } |
85 | if (((maxNum).intValue() != minNum)) { | 89 | if (((maxNum).intValue() != minNum)) { |
86 | int instEndInd = Math.min(GLOBAL_MAX, ((i + (maxNum).intValue()) - minNum)); | 90 | int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + (maxNum).intValue()) - minNum)); |
87 | this.getInstanceConstants(instEndInd, i, localInstances, trace, false, false); | 91 | this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false); |
88 | this.makeFofFormula(localInstances, trace, false, t_1); | 92 | this.makeFofFormula(localInstances, trace, false, t_1); |
89 | } | 93 | } |
90 | } | 94 | } |
@@ -126,18 +130,24 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
126 | 130 | ||
127 | protected void makeFofFormula(final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean minimum, final Type type) { | 131 | protected void makeFofFormula(final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean minimum, final Type type) { |
128 | String nm = ""; | 132 | String nm = ""; |
129 | VLSFunction tm = null; | 133 | VLSTerm tm = null; |
130 | if ((type == null)) { | 134 | if ((type == null)) { |
131 | nm = "object"; | 135 | nm = "object"; |
132 | tm = this.support.topLevelTypeFunc(); | 136 | tm = this.support.topLevelTypeFunc(); |
133 | } else { | 137 | } else { |
134 | nm = CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate).getConstant().toString(); | 138 | nm = CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate).getConstant().toString(); |
135 | tm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate)); | 139 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); |
140 | final Procedure1<VLSAnd> _function = (VLSAnd it) -> { | ||
141 | it.setLeft(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate))); | ||
142 | it.setRight(this.support.topLevelTypeFunc()); | ||
143 | }; | ||
144 | VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function); | ||
145 | tm = _doubleArrow; | ||
136 | } | 146 | } |
137 | final String name = nm; | 147 | final String name = nm; |
138 | final VLSFunction term = tm; | 148 | final VLSTerm term = tm; |
139 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 149 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
140 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 150 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { |
141 | String _xifexpression = null; | 151 | String _xifexpression = null; |
142 | if (minimum) { | 152 | if (minimum) { |
143 | _xifexpression = "min"; | 153 | _xifexpression = "min"; |
@@ -147,53 +157,53 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
147 | it.setName(this.support.toIDMultiple("typeScope", _xifexpression, name)); | 157 | it.setName(this.support.toIDMultiple("typeScope", _xifexpression, name)); |
148 | it.setFofRole("axiom"); | 158 | it.setFofRole("axiom"); |
149 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 159 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
150 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | 160 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { |
151 | EList<VLSVariable> _variables = it_1.getVariables(); | 161 | EList<VLSVariable> _variables = it_1.getVariables(); |
152 | VLSVariable _duplicate = this.support.duplicate(this.variable); | 162 | VLSVariable _duplicate = this.support.duplicate(this.variable); |
153 | _variables.add(_duplicate); | 163 | _variables.add(_duplicate); |
154 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | 164 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); |
155 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | 165 | final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> { |
156 | if (minimum) { | 166 | if (minimum) { |
157 | final Function1<VLSTerm, VLSEquality> _function_3 = (VLSTerm i) -> { | 167 | final Function1<VLSTerm, VLSEquality> _function_4 = (VLSTerm i) -> { |
158 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | 168 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); |
159 | final Procedure1<VLSEquality> _function_4 = (VLSEquality it_3) -> { | 169 | final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> { |
160 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 170 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); |
161 | final Procedure1<VLSVariable> _function_5 = (VLSVariable it_4) -> { | 171 | final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> { |
162 | it_4.setName(this.variable.getName()); | 172 | it_4.setName(this.variable.getName()); |
163 | }; | 173 | }; |
164 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_5); | 174 | VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6); |
165 | it_3.setLeft(_doubleArrow); | 175 | it_3.setLeft(_doubleArrow_1); |
166 | it_3.setRight(i); | 176 | it_3.setRight(i); |
167 | }; | 177 | }; |
168 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_4); | 178 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5); |
169 | }; | 179 | }; |
170 | it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_3))); | 180 | it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_4))); |
171 | it_2.setRight(term); | 181 | it_2.setRight(term); |
172 | } else { | 182 | } else { |
173 | it_2.setLeft(term); | 183 | it_2.setLeft(term); |
174 | final Function1<VLSTerm, VLSEquality> _function_4 = (VLSTerm i) -> { | 184 | final Function1<VLSTerm, VLSEquality> _function_5 = (VLSTerm i) -> { |
175 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | 185 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); |
176 | final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> { | 186 | final Procedure1<VLSEquality> _function_6 = (VLSEquality it_3) -> { |
177 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 187 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); |
178 | final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> { | 188 | final Procedure1<VLSVariable> _function_7 = (VLSVariable it_4) -> { |
179 | it_4.setName(this.variable.getName()); | 189 | it_4.setName(this.variable.getName()); |
180 | }; | 190 | }; |
181 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6); | 191 | VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_7); |
182 | it_3.setLeft(_doubleArrow); | 192 | it_3.setLeft(_doubleArrow_1); |
183 | it_3.setRight(i); | 193 | it_3.setRight(i); |
184 | }; | 194 | }; |
185 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5); | 195 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_6); |
186 | }; | 196 | }; |
187 | it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_4))); | 197 | it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_5))); |
188 | } | 198 | } |
189 | }; | 199 | }; |
190 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | 200 | VLSImplies _doubleArrow_1 = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3); |
191 | it_1.setOperand(_doubleArrow); | 201 | it_1.setOperand(_doubleArrow_1); |
192 | }; | 202 | }; |
193 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | 203 | VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); |
194 | it.setFofFormula(_doubleArrow); | 204 | it.setFofFormula(_doubleArrow_1); |
195 | }; | 205 | }; |
196 | final VLSFofFormula cstDec = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | 206 | final VLSFofFormula cstDec = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); |
197 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 207 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); |
198 | _formulas.add(cstDec); | 208 | _formulas.add(cstDec); |
199 | } | 209 | } |
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 { | |||
104 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | 104 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); |
105 | } | 105 | } |
106 | 106 | ||
107 | protected VLSFunction duplicate(final VLSFunction term, final List<VLSVariable> vars) { | ||
108 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
109 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
110 | it.setConstant(term.getConstant()); | ||
111 | for (final VLSVariable v : vars) { | ||
112 | EList<VLSTerm> _terms = it.getTerms(); | ||
113 | VLSVariable _duplicate = this.duplicate(v); | ||
114 | _terms.add(_duplicate); | ||
115 | } | ||
116 | }; | ||
117 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
118 | } | ||
119 | |||
107 | protected VLSFunction duplicate(final VLSFunction term, final VLSFunctionAsTerm v) { | 120 | protected VLSFunction duplicate(final VLSFunction term, final VLSFunctionAsTerm v) { |
108 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 121 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
109 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | 122 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { |
@@ -138,6 +151,17 @@ public class Logic2VampireLanguageMapper_Support { | |||
138 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | 151 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); |
139 | } | 152 | } |
140 | 153 | ||
154 | protected VLSFunction topLevelTypeFunc(final VLSVariable v) { | ||
155 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
156 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
157 | it.setConstant("object"); | ||
158 | EList<VLSTerm> _terms = it.getTerms(); | ||
159 | VLSVariable _duplicate = this.duplicate(v); | ||
160 | _terms.add(_duplicate); | ||
161 | }; | ||
162 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
163 | } | ||
164 | |||
141 | protected VLSFunction topLevelTypeFunc(final VLSFunctionAsTerm v) { | 165 | protected VLSFunction topLevelTypeFunc(final VLSFunctionAsTerm v) { |
142 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 166 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
143 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | 167 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { |
@@ -284,7 +308,8 @@ public class Logic2VampireLanguageMapper_Support { | |||
284 | for (final Variable variable : _quantifiedVariables) { | 308 | for (final Variable variable : _quantifiedVariables) { |
285 | { | 309 | { |
286 | TypeReference _range = variable.getRange(); | 310 | TypeReference _range = variable.getRange(); |
287 | final VLSFunction eq = this.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate), CollectionsUtil.<Variable, VLSVariable>lookup(variable, variableMap)); | 311 | final VLSFunction eq = this.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate), |
312 | CollectionsUtil.<Variable, VLSVariable>lookup(variable, variableMap)); | ||
288 | typedefs.add(eq); | 313 | typedefs.add(eq); |
289 | } | 314 | } |
290 | } | 315 | } |
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; | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | 10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | 11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; |
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | 12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; |
@@ -18,7 +20,6 @@ import com.google.common.base.Objects; | |||
18 | import com.google.common.collect.Iterables; | 20 | import com.google.common.collect.Iterables; |
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | 21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; |
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | 22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; |
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration; | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; | 23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; |
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; | 24 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; |
24 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 25 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
@@ -56,6 +57,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
56 | it.setName("A"); | 57 | it.setName("A"); |
57 | }; | 58 | }; |
58 | final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | 59 | final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); |
60 | int globalCounter = 0; | ||
59 | for (final Type type : types) { | 61 | for (final Type type : types) { |
60 | { | 62 | { |
61 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 63 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
@@ -92,7 +94,31 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
92 | }; | 94 | }; |
93 | final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | 95 | final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); |
94 | trace.element2Predicate.put(e, enumElemPred); | 96 | trace.element2Predicate.put(e, enumElemPred); |
95 | orElems.add(enumElemPred); | 97 | } |
98 | } | ||
99 | final List<VLSTerm> possibleNots = CollectionLiterals.<VLSTerm>newArrayList(); | ||
100 | final List<VLSTerm> typeDefs = CollectionLiterals.<VLSTerm>newArrayList(); | ||
101 | EList<DefinedElement> _elements_1 = type_1.getElements(); | ||
102 | for (final DefinedElement t1 : _elements_1) { | ||
103 | { | ||
104 | EList<DefinedElement> _elements_2 = type_1.getElements(); | ||
105 | for (final DefinedElement t2 : _elements_2) { | ||
106 | boolean _equals = Objects.equal(t1, t2); | ||
107 | if (_equals) { | ||
108 | final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable); | ||
109 | possibleNots.add(fct); | ||
110 | } else { | ||
111 | final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable); | ||
112 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
113 | final Procedure1<VLSUnaryNegation> _function_1 = (VLSUnaryNegation it) -> { | ||
114 | it.setOperand(op); | ||
115 | }; | ||
116 | final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_1); | ||
117 | possibleNots.add(negFct); | ||
118 | } | ||
119 | } | ||
120 | typeDefs.add(this.support.unfoldAnd(possibleNots)); | ||
121 | possibleNots.clear(); | ||
96 | } | 122 | } |
97 | } | 123 | } |
98 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 124 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
@@ -107,7 +133,13 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
107 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 133 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
108 | final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> { | 134 | final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> { |
109 | it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate)); | 135 | it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate)); |
110 | it_2.setRight(this.support.unfoldOr(orElems)); | 136 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); |
137 | final Procedure1<VLSAnd> _function_4 = (VLSAnd it_3) -> { | ||
138 | it_3.setLeft(this.support.topLevelTypeFunc(variable)); | ||
139 | it_3.setRight(this.support.unfoldOr(typeDefs)); | ||
140 | }; | ||
141 | VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_4); | ||
142 | it_2.setRight(_doubleArrow); | ||
111 | }; | 143 | }; |
112 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3); | 144 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3); |
113 | it_1.setOperand(_doubleArrow); | 145 | it_1.setOperand(_doubleArrow); |
@@ -118,8 +150,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
118 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); | 150 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); |
119 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 151 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); |
120 | _formulas.add(res); | 152 | _formulas.add(res); |
121 | final List<VLSTerm> enumScopeElems = CollectionLiterals.<VLSTerm>newArrayList(); | 153 | for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) { |
122 | for (int i = 0; (i < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); i++) { | ||
123 | { | 154 | { |
124 | final int num = (i + 1); | 155 | final int num = (i + 1); |
125 | VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); | 156 | VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); |
@@ -129,38 +160,50 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
129 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); | 160 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); |
130 | final VLSConstant cst = this.support.toConstant(cstTerm); | 161 | final VLSConstant cst = this.support.toConstant(cstTerm); |
131 | trace.uniqueInstances.add(cst); | 162 | trace.uniqueInstances.add(cst); |
132 | final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(i), trace.element2Predicate), cstTerm); | 163 | final int index = i; |
133 | enumScopeElems.add(fct); | 164 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
134 | for (int j = 0; (j < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); j++) { | 165 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { |
135 | if ((j != i)) { | 166 | it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0], |
136 | final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(j), trace.element2Predicate), cstTerm); | 167 | type_1.getElements().get(index).getName().split(" ")[0])); |
137 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | 168 | it.setFofRole("axiom"); |
138 | final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> { | 169 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
139 | it.setOperand(op); | 170 | final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> { |
171 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
172 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
173 | _variables.add(_duplicate); | ||
174 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
175 | final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> { | ||
176 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
177 | final Procedure1<VLSEquality> _function_6 = (VLSEquality it_3) -> { | ||
178 | it_3.setLeft(this.support.duplicate(variable)); | ||
179 | it_3.setRight(this.support.duplicate(this.support.toConstant(cstTerm))); | ||
180 | }; | ||
181 | VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_6); | ||
182 | it_2.setLeft(_doubleArrow); | ||
183 | it_2.setRight(this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(index), trace.element2Predicate), variable)); | ||
140 | }; | 184 | }; |
141 | final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3); | 185 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_5); |
142 | enumScopeElems.add(negFct); | 186 | it_1.setOperand(_doubleArrow); |
143 | } | 187 | }; |
144 | } | 188 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); |
189 | it.setFofFormula(_doubleArrow); | ||
190 | }; | ||
191 | final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_3); | ||
192 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
193 | _formulas_1.add(enumScope); | ||
145 | } | 194 | } |
146 | } | 195 | } |
147 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 196 | int _globalCounter = globalCounter; |
148 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { | 197 | int _size = type_1.getElements().size(); |
149 | it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0])); | 198 | globalCounter = (_globalCounter + _size); |
150 | it.setFofRole("axiom"); | ||
151 | it.setFofFormula(this.support.unfoldAnd(enumScopeElems)); | ||
152 | }; | ||
153 | final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_2); | ||
154 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
155 | _formulas_1.add(enumScope); | ||
156 | } | 199 | } |
157 | } | 200 | } |
158 | final Function1<Type, Boolean> _function_1 = (Type it) -> { | 201 | final Function1<Type, Boolean> _function_1 = (Type it) -> { |
159 | boolean _isIsAbstract = it.isIsAbstract(); | 202 | boolean _isIsAbstract = it.isIsAbstract(); |
160 | return Boolean.valueOf((!_isIsAbstract)); | 203 | return Boolean.valueOf((!_isIsAbstract)); |
161 | }; | 204 | }; |
162 | Iterable<TypeDeclaration> _filter_1 = Iterables.<TypeDeclaration>filter(IterableExtensions.<Type>filter(types, _function_1), TypeDeclaration.class); | 205 | Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1); |
163 | for (final TypeDeclaration t1 : _filter_1) { | 206 | for (final Type t1 : _filter_1) { |
164 | { | 207 | { |
165 | for (final Type t2 : types) { | 208 | for (final Type t2 : types) { |
166 | if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) { | 209 | if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) { |