diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder')
15 files changed, 97 insertions, 15 deletions
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 2c091b47..00ebca4b 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/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin index b05fd2c1..9641858d 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin | |||
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 7f6519eb..2b51fe5d 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_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 d30eebe5..75482abc 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 921b79bd..c394f878 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 6b8d1dc0..1ec5da80 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 83e57283..e85b5240 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/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin index 5a0087bc..c000d128 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin index 7d090297..5eb63977 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin index c8ab54c2..501dbfb4 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin index 3306fa73..621c888a 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java index 2b491209..24df5fcd 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java | |||
@@ -1,6 +1,7 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace; | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace; |
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | 5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; |
@@ -14,7 +15,9 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | |||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | 15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; |
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; |
16 | import java.util.HashMap; | 17 | import java.util.HashMap; |
18 | import java.util.List; | ||
17 | import java.util.Map; | 19 | import java.util.Map; |
20 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
18 | 21 | ||
19 | @SuppressWarnings("all") | 22 | @SuppressWarnings("all") |
20 | public class Logic2VampireLanguageMapperTrace { | 23 | public class Logic2VampireLanguageMapperTrace { |
@@ -34,6 +37,8 @@ public class Logic2VampireLanguageMapperTrace { | |||
34 | 37 | ||
35 | public final Map<Type, VLSTerm> type2And = new HashMap<Type, VLSTerm>(); | 38 | public final Map<Type, VLSTerm> type2And = new HashMap<Type, VLSTerm>(); |
36 | 39 | ||
40 | public final List<VLSConstant> uniqueInstances = CollectionLiterals.<VLSConstant>newArrayList(); | ||
41 | |||
37 | public Map<ConstantDeclaration, ConstantDefinition> constantDefinitions; | 42 | public Map<ConstantDeclaration, ConstantDefinition> constantDefinitions; |
38 | 43 | ||
39 | public Map<RelationDeclaration, RelationDefinition> relationDefinitions; | 44 | public Map<RelationDeclaration, RelationDefinition> relationDefinitions; |
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 8967839d..15ba78c9 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 | |||
@@ -5,13 +5,14 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage | |||
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.VLSConstant; | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; |
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | 11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | 12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; |
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | 13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; | 14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; |
14 | import java.util.List; | 15 | import java.util.ArrayList; |
15 | import org.eclipse.emf.common.util.EList; | 16 | import org.eclipse.emf.common.util.EList; |
16 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 17 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
17 | import org.eclipse.xtext.xbase.lib.Extension; | 18 | import org.eclipse.xtext.xbase.lib.Extension; |
@@ -39,7 +40,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
39 | it.setName("A"); | 40 | it.setName("A"); |
40 | }; | 41 | }; |
41 | final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | 42 | final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); |
42 | final List<VLSConstant> instances = CollectionLiterals.<VLSConstant>newArrayList(); | 43 | final ArrayList<VLSTerm> localInstances = CollectionLiterals.<VLSTerm>newArrayList(); |
43 | for (int i = 0; (i < config.typeScopes.minNewElements); i++) { | 44 | for (int i = 0; (i < config.typeScopes.minNewElements); i++) { |
44 | { | 45 | { |
45 | final int num = (i + 1); | 46 | final int num = (i + 1); |
@@ -48,7 +49,8 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
48 | it.setName(("o" + Integer.valueOf(num))); | 49 | it.setName(("o" + Integer.valueOf(num))); |
49 | }; | 50 | }; |
50 | final VLSConstant cst = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_1); | 51 | final VLSConstant cst = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_1); |
51 | instances.add(cst); | 52 | trace.uniqueInstances.add(cst); |
53 | localInstances.add(cst); | ||
52 | } | 54 | } |
53 | } | 55 | } |
54 | if ((config.typeScopes.minNewElements != 0)) { | 56 | if ((config.typeScopes.minNewElements != 0)) { |
@@ -61,10 +63,9 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
61 | EList<VLSVariable> _variables = it_1.getVariables(); | 63 | EList<VLSVariable> _variables = it_1.getVariables(); |
62 | VLSVariable _duplicate = this.support.duplicate(variable); | 64 | VLSVariable _duplicate = this.support.duplicate(variable); |
63 | _variables.add(_duplicate); | 65 | _variables.add(_duplicate); |
64 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 66 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); |
65 | final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> { | 67 | final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> { |
66 | it_2.setLeft(this.support.topLevelTypeFunc()); | 68 | final Function1<VLSTerm, VLSEquality> _function_4 = (VLSTerm i) -> { |
67 | final Function1<VLSConstant, VLSEquality> _function_4 = (VLSConstant i) -> { | ||
68 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | 69 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); |
69 | final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> { | 70 | final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> { |
70 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | 71 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); |
@@ -77,9 +78,10 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
77 | }; | 78 | }; |
78 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5); | 79 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5); |
79 | }; | 80 | }; |
80 | it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSConstant, VLSEquality>map(instances, _function_4))); | 81 | it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(localInstances, _function_4))); |
82 | it_2.setRight(this.support.topLevelTypeFunc()); | ||
81 | }; | 83 | }; |
82 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3); | 84 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3); |
83 | it_1.setOperand(_doubleArrow); | 85 | it_1.setOperand(_doubleArrow); |
84 | }; | 86 | }; |
85 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | 87 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); |
@@ -92,7 +94,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
92 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { | 94 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { |
93 | it.setName("typeUniqueness"); | 95 | it.setName("typeUniqueness"); |
94 | it.setFofRole("axiom"); | 96 | it.setFofRole("axiom"); |
95 | it.setFofFormula(this.support.establishUniqueness(instances)); | 97 | it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances)); |
96 | }; | 98 | }; |
97 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_2); | 99 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_2); |
98 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | 100 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); |
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 72ca44e9..e2ff7a0e 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 | |||
@@ -6,6 +6,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; | |||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; |
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | 10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; |
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality; | 11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality; |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr; | 12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr; |
@@ -62,6 +63,22 @@ public class Logic2VampireLanguageMapper_Support { | |||
62 | return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | 63 | return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); |
63 | } | 64 | } |
64 | 65 | ||
66 | protected VLSFunctionAsTerm duplicate(final VLSFunctionAsTerm term) { | ||
67 | VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); | ||
68 | final Procedure1<VLSFunctionAsTerm> _function = (VLSFunctionAsTerm it) -> { | ||
69 | it.setFunctor(term.getFunctor()); | ||
70 | }; | ||
71 | return ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function); | ||
72 | } | ||
73 | |||
74 | protected VLSConstant duplicate(final VLSConstant term) { | ||
75 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
76 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { | ||
77 | it.setName(term.getName()); | ||
78 | }; | ||
79 | return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function); | ||
80 | } | ||
81 | |||
65 | protected VLSFunction duplicate(final VLSFunction term) { | 82 | protected VLSFunction duplicate(final VLSFunction term) { |
66 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 83 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
67 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | 84 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { |
@@ -87,6 +104,25 @@ public class Logic2VampireLanguageMapper_Support { | |||
87 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | 104 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); |
88 | } | 105 | } |
89 | 106 | ||
107 | protected VLSFunction duplicate(final VLSFunction term, final VLSFunctionAsTerm v) { | ||
108 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
109 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
110 | it.setConstant(term.getConstant()); | ||
111 | EList<VLSTerm> _terms = it.getTerms(); | ||
112 | VLSFunctionAsTerm _duplicate = this.duplicate(v); | ||
113 | _terms.add(_duplicate); | ||
114 | }; | ||
115 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
116 | } | ||
117 | |||
118 | protected VLSConstant toConstant(final VLSFunctionAsTerm term) { | ||
119 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
120 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { | ||
121 | it.setName(term.getFunctor()); | ||
122 | }; | ||
123 | return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function); | ||
124 | } | ||
125 | |||
90 | protected VLSFunction topLevelTypeFunc() { | 126 | protected VLSFunction topLevelTypeFunc() { |
91 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 127 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
92 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | 128 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { |
@@ -102,6 +138,17 @@ public class Logic2VampireLanguageMapper_Support { | |||
102 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | 138 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); |
103 | } | 139 | } |
104 | 140 | ||
141 | protected VLSFunction topLevelTypeFunc(final VLSFunctionAsTerm v) { | ||
142 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
143 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
144 | it.setConstant("object"); | ||
145 | EList<VLSTerm> _terms = it.getTerms(); | ||
146 | VLSFunctionAsTerm _duplicate = this.duplicate(v); | ||
147 | _terms.add(_duplicate); | ||
148 | }; | ||
149 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
150 | } | ||
151 | |||
105 | public VLSTerm establishUniqueness(final List<VLSConstant> terms) { | 152 | public VLSTerm establishUniqueness(final List<VLSConstant> terms) { |
106 | final List<VLSInequality> eqs = CollectionLiterals.<VLSInequality>newArrayList(); | 153 | final List<VLSInequality> eqs = CollectionLiterals.<VLSInequality>newArrayList(); |
107 | List<VLSConstant> _subList = terms.subList(1, ((Object[])Conversions.unwrapArray(terms, Object.class)).length); | 154 | List<VLSConstant> _subList = terms.subList(1, ((Object[])Conversions.unwrapArray(terms, Object.class)).length); |
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 d3dddcfc..f776371b 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,10 +3,12 @@ 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.VLSConstant; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; |
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | 9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | 10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | 12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; | 13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; |
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | 14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; |
@@ -16,6 +18,7 @@ import com.google.common.base.Objects; | |||
16 | import com.google.common.collect.Iterables; | 18 | import com.google.common.collect.Iterables; |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | 20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; |
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration; | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; | 22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; |
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; | 23 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; |
21 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 24 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
@@ -24,6 +27,7 @@ import java.util.Collection; | |||
24 | import java.util.List; | 27 | import java.util.List; |
25 | import org.eclipse.emf.common.util.EList; | 28 | import org.eclipse.emf.common.util.EList; |
26 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 29 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
30 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
27 | import org.eclipse.xtext.xbase.lib.Extension; | 31 | import org.eclipse.xtext.xbase.lib.Extension; |
28 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | 32 | import org.eclipse.xtext.xbase.lib.Functions.Function1; |
29 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | 33 | import org.eclipse.xtext.xbase.lib.IterableExtensions; |
@@ -107,14 +111,38 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
107 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); | 111 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); |
108 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 112 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); |
109 | _formulas.add(res); | 113 | _formulas.add(res); |
114 | final List<VLSFunction> enumScopeElems = CollectionLiterals.<VLSFunction>newArrayList(); | ||
115 | for (int i = 0; (i < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); i++) { | ||
116 | { | ||
117 | final int num = (i + 1); | ||
118 | VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); | ||
119 | final Procedure1<VLSFunctionAsTerm> _function_2 = (VLSFunctionAsTerm it) -> { | ||
120 | it.setFunctor(("eo" + Integer.valueOf(num))); | ||
121 | }; | ||
122 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); | ||
123 | final VLSConstant cst = this.support.toConstant(cstTerm); | ||
124 | trace.uniqueInstances.add(cst); | ||
125 | final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(i), trace.element2Predicate), cstTerm); | ||
126 | enumScopeElems.add(fct); | ||
127 | } | ||
128 | } | ||
129 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
130 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { | ||
131 | it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0])); | ||
132 | it.setFofRole("axiom"); | ||
133 | it.setFofFormula(this.support.unfoldAnd(enumScopeElems)); | ||
134 | }; | ||
135 | final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_2); | ||
136 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
137 | _formulas_1.add(enumScope); | ||
110 | } | 138 | } |
111 | } | 139 | } |
112 | final Function1<Type, Boolean> _function_1 = (Type it) -> { | 140 | final Function1<Type, Boolean> _function_1 = (Type it) -> { |
113 | boolean _isIsAbstract = it.isIsAbstract(); | 141 | boolean _isIsAbstract = it.isIsAbstract(); |
114 | return Boolean.valueOf((!_isIsAbstract)); | 142 | return Boolean.valueOf((!_isIsAbstract)); |
115 | }; | 143 | }; |
116 | Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1); | 144 | Iterable<TypeDeclaration> _filter_1 = Iterables.<TypeDeclaration>filter(IterableExtensions.<Type>filter(types, _function_1), TypeDeclaration.class); |
117 | for (final Type t1 : _filter_1) { | 145 | for (final TypeDeclaration t1 : _filter_1) { |
118 | { | 146 | { |
119 | for (final Type t2 : types) { | 147 | for (final Type t2 : types) { |
120 | if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) { | 148 | if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) { |
@@ -147,8 +175,8 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
147 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> { | 175 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> { |
148 | it_2.setLeft(this.support.topLevelTypeFunc()); | 176 | it_2.setLeft(this.support.topLevelTypeFunc()); |
149 | Collection<VLSTerm> _values = trace.type2And.values(); | 177 | Collection<VLSTerm> _values = trace.type2And.values(); |
150 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | 178 | final ArrayList<VLSTerm> reversedList = new ArrayList<VLSTerm>(_values); |
151 | it_2.setRight(this.support.unfoldOr(_arrayList)); | 179 | it_2.setRight(this.support.unfoldOr(reversedList)); |
152 | }; | 180 | }; |
153 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); | 181 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); |
154 | it_1.setOperand(_doubleArrow); | 182 | it_1.setOperand(_doubleArrow); |