diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-06 17:26:43 -0500 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-06 17:26:43 -0500 |
commit | 5c4471e3a4cd273bf68eb2ccc1d91f99b5c8c7bc (patch) | |
tree | 7a2481581a3bc14a672f6e1f7965573853e62c04 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java | |
parent | Restructure Vampire Reasoner project (diff) | |
download | VIATRA-Generator-5c4471e3a4cd273bf68eb2ccc1d91f99b5c8c7bc.tar.gz VIATRA-Generator-5c4471e3a4cd273bf68eb2ccc1d91f99b5c8c7bc.tar.zst VIATRA-Generator-5c4471e3a4cd273bf68eb2ccc1d91f99b5c8c7bc.zip |
Implement Enum handling and study hierarchy handling
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java | 24 |
1 files changed, 13 insertions, 11 deletions
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(); |