diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-05 21:33:28 -0500 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:22:40 -0400 |
commit | 3d92a0eb813309993892a978482b2858179034f7 (patch) | |
tree | 12203a71c02430b0f8fb93dafbd4aa68be60f8b1 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java | |
parent | Implement type scope handling (diff) | |
download | VIATRA-Generator-3d92a0eb813309993892a978482b2858179034f7.tar.gz VIATRA-Generator-3d92a0eb813309993892a978482b2858179034f7.tar.zst VIATRA-Generator-3d92a0eb813309993892a978482b2858179034f7.zip |
Partially improve coding style (leaving for soccer)
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java | 218 |
1 files changed, 93 insertions, 125 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java index bce50fcc..4f5c6acc 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java | |||
@@ -15,6 +15,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | |||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | 15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; |
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; |
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | 20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; |
20 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 21 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
@@ -44,17 +45,84 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
44 | this.base = base; | 45 | this.base = base; |
45 | } | 46 | } |
46 | 47 | ||
47 | public void _transformRelation(final RelationDefinition r, final Logic2VampireLanguageMapperTrace trace) { | 48 | public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) { |
49 | final List<VLSVariable> relVar2VLS = new ArrayList<VLSVariable>(); | ||
50 | final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>(); | ||
51 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | ||
52 | int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
53 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); | ||
54 | for (final Integer i : _doubleDotLessThan) { | ||
55 | { | ||
56 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
57 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
58 | it.setName(this.support.toIDMultiple("V", i.toString())); | ||
59 | }; | ||
60 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
61 | relVar2VLS.add(v); | ||
62 | TypeReference _get = r.getParameters().get((i).intValue()); | ||
63 | final Type relType = ((ComplexTypeReference) _get).getReferred(); | ||
64 | final VLSFunction varTypeComply = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(relType, trace.type2Predicate), v); | ||
65 | relVar2TypeDecComply.add(varTypeComply); | ||
66 | } | ||
67 | } | ||
68 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
69 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
70 | final String[] nameArray = r.getName().split(" "); | ||
71 | it.setName(this.support.toIDMultiple("compliance", nameArray[0], | ||
72 | nameArray[2])); | ||
73 | it.setFofRole("axiom"); | ||
74 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
75 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | ||
76 | for (final VLSVariable v : relVar2VLS) { | ||
77 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
78 | VLSVariable _duplicate = this.support.duplicate(v); | ||
79 | _variables.add(_duplicate); | ||
80 | } | ||
81 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
82 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | ||
83 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
84 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { | ||
85 | it_3.setConstant(this.support.toIDMultiple("rel", r.getName())); | ||
86 | int _length_1 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
87 | ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(0, _length_1, true); | ||
88 | for (final Integer i_1 : _doubleDotLessThan_1) { | ||
89 | { | ||
90 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
91 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> { | ||
92 | it_4.setName(relVar2VLS.get((i_1).intValue()).getName()); | ||
93 | }; | ||
94 | final VLSVariable v_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4); | ||
95 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
96 | _terms.add(v_1); | ||
97 | } | ||
98 | } | ||
99 | }; | ||
100 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3); | ||
101 | it_2.setLeft(_doubleArrow); | ||
102 | it_2.setRight(this.support.unfoldAnd(relVar2TypeDecComply)); | ||
103 | }; | ||
104 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | ||
105 | it_1.setOperand(_doubleArrow); | ||
106 | }; | ||
107 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
108 | it.setFofFormula(_doubleArrow); | ||
109 | }; | ||
110 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
111 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
112 | _formulas.add(comply); | ||
113 | } | ||
114 | |||
115 | public void _transformRelation(final RelationDefinition reldef, final Logic2VampireLanguageMapperTrace trace) { | ||
48 | final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); | 116 | final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); |
49 | final Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap<Variable, VLSFunction>(); | 117 | final Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap<Variable, VLSFunction>(); |
50 | final Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap<Variable, VLSFunction>(); | 118 | final Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap<Variable, VLSFunction>(); |
51 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | 119 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); |
52 | EList<Variable> _variables = r.getVariables(); | 120 | EList<Variable> _variables = reldef.getVariables(); |
53 | for (final Variable variable : _variables) { | 121 | for (final Variable variable : _variables) { |
54 | { | 122 | { |
55 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 123 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); |
56 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | 124 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { |
57 | it.setName(this.support.toIDMultiple("Var", variable.getName())); | 125 | it.setName(this.support.toIDMultiple("V", variable.getName())); |
58 | }; | 126 | }; |
59 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | 127 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); |
60 | relationVar2VLS.put(variable, v); | 128 | relationVar2VLS.put(variable, v); |
@@ -63,56 +131,39 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
63 | TypeReference _range = variable.getRange(); | 131 | TypeReference _range = variable.getRange(); |
64 | it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); | 132 | it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); |
65 | EList<VLSTerm> _terms = it.getTerms(); | 133 | EList<VLSTerm> _terms = it.getTerms(); |
66 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | 134 | VLSVariable _duplicate = this.support.duplicate(v); |
67 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | 135 | _terms.add(_duplicate); |
68 | it_1.setName(this.support.toIDMultiple("Var", variable.getName())); | ||
69 | }; | ||
70 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); | ||
71 | _terms.add(_doubleArrow); | ||
72 | }; | 136 | }; |
73 | final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | 137 | final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); |
74 | relationVar2TypeDecComply.put(variable, varTypeComply); | 138 | relationVar2TypeDecComply.put(variable, varTypeComply); |
75 | VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction(); | 139 | relationVar2TypeDecRes.put(variable, this.support.duplicate(varTypeComply)); |
76 | final Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> { | ||
77 | TypeReference _range = variable.getRange(); | ||
78 | it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); | ||
79 | EList<VLSTerm> _terms = it.getTerms(); | ||
80 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
81 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it_1) -> { | ||
82 | it_1.setName(this.support.toIDMultiple("Var", variable.getName())); | ||
83 | }; | ||
84 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_3); | ||
85 | _terms.add(_doubleArrow); | ||
86 | }; | ||
87 | final VLSFunction varTypeRes = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction_1, _function_2); | ||
88 | relationVar2TypeDecRes.put(variable, varTypeRes); | ||
89 | } | 140 | } |
90 | } | 141 | } |
91 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 142 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
92 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 143 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { |
93 | it.setName(this.support.toIDMultiple("compliance", r.getName())); | 144 | final String[] nameArray = reldef.getName().split(" "); |
145 | int _length = nameArray.length; | ||
146 | int _minus = (_length - 2); | ||
147 | int _length_1 = nameArray.length; | ||
148 | int _minus_1 = (_length_1 - 1); | ||
149 | it.setName(this.support.toIDMultiple("compliance", nameArray[_minus], | ||
150 | nameArray[_minus_1])); | ||
94 | it.setFofRole("axiom"); | 151 | it.setFofRole("axiom"); |
95 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 152 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
96 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | 153 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { |
97 | EList<Variable> _variables_1 = r.getVariables(); | 154 | EList<Variable> _variables_1 = reldef.getVariables(); |
98 | for (final Variable variable_1 : _variables_1) { | 155 | for (final Variable variable_1 : _variables_1) { |
99 | { | 156 | EList<VLSVariable> _variables_2 = it_1.getVariables(); |
100 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 157 | VLSVariable _duplicate = this.support.duplicate(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS)); |
101 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_2) -> { | 158 | _variables_2.add(_duplicate); |
102 | it_2.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS).getName()); | ||
103 | }; | ||
104 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2); | ||
105 | EList<VLSVariable> _variables_2 = it_1.getVariables(); | ||
106 | _variables_2.add(v); | ||
107 | } | ||
108 | } | 159 | } |
109 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | 160 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); |
110 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | 161 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { |
111 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 162 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
112 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { | 163 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { |
113 | it_3.setConstant(this.support.toIDMultiple("rel", r.getName())); | 164 | it_3.setConstant(this.support.toIDMultiple("rel", reldef.getName())); |
114 | EList<Variable> _variables_2 = r.getVariables(); | 165 | EList<Variable> _variables_3 = reldef.getVariables(); |
115 | for (final Variable variable_2 : _variables_2) { | 166 | for (final Variable variable_2 : _variables_3) { |
116 | { | 167 | { |
117 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 168 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); |
118 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> { | 169 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> { |
@@ -139,11 +190,11 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
139 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | 190 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); |
140 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 191 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
141 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | 192 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { |
142 | it.setName(this.support.toIDMultiple("relation", r.getName())); | 193 | it.setName(this.support.toIDMultiple("relation", reldef.getName())); |
143 | it.setFofRole("axiom"); | 194 | it.setFofRole("axiom"); |
144 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 195 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
145 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | 196 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { |
146 | EList<Variable> _variables_1 = r.getVariables(); | 197 | EList<Variable> _variables_1 = reldef.getVariables(); |
147 | for (final Variable variable_1 : _variables_1) { | 198 | for (final Variable variable_1 : _variables_1) { |
148 | { | 199 | { |
149 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 200 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); |
@@ -164,8 +215,8 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
164 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_3) -> { | 215 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_3) -> { |
165 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 216 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
166 | final Procedure1<VLSFunction> _function_5 = (VLSFunction it_4) -> { | 217 | final Procedure1<VLSFunction> _function_5 = (VLSFunction it_4) -> { |
167 | it_4.setConstant(this.support.toIDMultiple("rel", r.getName())); | 218 | it_4.setConstant(this.support.toIDMultiple("rel", reldef.getName())); |
168 | EList<Variable> _variables_2 = r.getVariables(); | 219 | EList<Variable> _variables_2 = reldef.getVariables(); |
169 | for (final Variable variable_2 : _variables_2) { | 220 | for (final Variable variable_2 : _variables_2) { |
170 | { | 221 | { |
171 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 222 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); |
@@ -180,7 +231,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
180 | }; | 231 | }; |
181 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5); | 232 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5); |
182 | it_3.setLeft(_doubleArrow); | 233 | it_3.setLeft(_doubleArrow); |
183 | it_3.setRight(this.base.transformTerm(r.getValue(), trace, relationVar2VLS)); | 234 | it_3.setRight(this.base.transformTerm(reldef.getValue(), trace, relationVar2VLS)); |
184 | }; | 235 | }; |
185 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); | 236 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); |
186 | it_2.setRight(_doubleArrow); | 237 | it_2.setRight(_doubleArrow); |
@@ -198,89 +249,6 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
198 | _formulas_1.add(res); | 249 | _formulas_1.add(res); |
199 | } | 250 | } |
200 | 251 | ||
201 | public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) { | ||
202 | final List<VLSVariable> relationVar2VLS = new ArrayList<VLSVariable>(); | ||
203 | final List<VLSFunction> relationVar2TypeDecComply = new ArrayList<VLSFunction>(); | ||
204 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | ||
205 | int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
206 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); | ||
207 | for (final Integer i : _doubleDotLessThan) { | ||
208 | { | ||
209 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
210 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
211 | it.setName(this.support.toIDMultiple("Var", i.toString())); | ||
212 | }; | ||
213 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
214 | relationVar2VLS.add(v); | ||
215 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
216 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
217 | TypeReference _get = r.getParameters().get((i).intValue()); | ||
218 | it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _get).getReferred().getName())); | ||
219 | EList<VLSTerm> _terms = it.getTerms(); | ||
220 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
221 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | ||
222 | it_1.setName(this.support.toIDMultiple("Var", i.toString())); | ||
223 | }; | ||
224 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); | ||
225 | _terms.add(_doubleArrow); | ||
226 | }; | ||
227 | final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
228 | relationVar2TypeDecComply.add(varTypeComply); | ||
229 | } | ||
230 | } | ||
231 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
232 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
233 | it.setName(this.support.toIDMultiple("compliance", r.getName())); | ||
234 | it.setFofRole("axiom"); | ||
235 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
236 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | ||
237 | int _length_1 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
238 | ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(0, _length_1, true); | ||
239 | for (final Integer i_1 : _doubleDotLessThan_1) { | ||
240 | { | ||
241 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
242 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_2) -> { | ||
243 | it_2.setName(relationVar2VLS.get((i_1).intValue()).getName()); | ||
244 | }; | ||
245 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2); | ||
246 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
247 | _variables.add(v); | ||
248 | } | ||
249 | } | ||
250 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
251 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | ||
252 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
253 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { | ||
254 | it_3.setConstant(this.support.toIDMultiple("rel", r.getName())); | ||
255 | int _length_2 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
256 | ExclusiveRange _doubleDotLessThan_2 = new ExclusiveRange(0, _length_2, true); | ||
257 | for (final Integer i_2 : _doubleDotLessThan_2) { | ||
258 | { | ||
259 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
260 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> { | ||
261 | it_4.setName(relationVar2VLS.get((i_2).intValue()).getName()); | ||
262 | }; | ||
263 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4); | ||
264 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
265 | _terms.add(v); | ||
266 | } | ||
267 | } | ||
268 | }; | ||
269 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3); | ||
270 | it_2.setLeft(_doubleArrow); | ||
271 | it_2.setRight(this.support.unfoldAnd(relationVar2TypeDecComply)); | ||
272 | }; | ||
273 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | ||
274 | it_1.setOperand(_doubleArrow); | ||
275 | }; | ||
276 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
277 | it.setFofFormula(_doubleArrow); | ||
278 | }; | ||
279 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
280 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
281 | _formulas.add(comply); | ||
282 | } | ||
283 | |||
284 | public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) { | 252 | public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) { |
285 | if (r instanceof RelationDeclaration) { | 253 | if (r instanceof RelationDeclaration) { |
286 | _transformRelation((RelationDeclaration)r, trace); | 254 | _transformRelation((RelationDeclaration)r, trace); |