diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-06 02:59:19 -0500 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:22:42 -0400 |
commit | 54431d1418fd4133a49605b804c10dd523c4c30d (patch) | |
tree | 57447af926e347e0ea31953c73f23d33297734d5 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder | |
parent | Partially improve coding style (leaving for soccer) (diff) | |
download | VIATRA-Generator-54431d1418fd4133a49605b804c10dd523c4c30d.tar.gz VIATRA-Generator-54431d1418fd4133a49605b804c10dd523c4c30d.tar.zst VIATRA-Generator-54431d1418fd4133a49605b804c10dd523c4c30d.zip |
Continue improving code style (need sleep)
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder')
3 files changed, 51 insertions, 88 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend index 54c44c72..81af24e5 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend | |||
@@ -40,6 +40,7 @@ import java.util.Map | |||
40 | import org.eclipse.xtend.lib.annotations.Accessors | 40 | import org.eclipse.xtend.lib.annotations.Accessors |
41 | 41 | ||
42 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 42 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
43 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
43 | 44 | ||
44 | class Logic2VampireLanguageMapper { | 45 | class Logic2VampireLanguageMapper { |
45 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | 46 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
@@ -227,18 +228,18 @@ class Logic2VampireLanguageMapper { | |||
227 | // | 228 | // |
228 | def dispatch protected VLSTerm transformTerm(Forall forall, Logic2VampireLanguageMapperTrace trace, | 229 | def dispatch protected VLSTerm transformTerm(Forall forall, Logic2VampireLanguageMapperTrace trace, |
229 | Map<Variable, VLSVariable> variables) { | 230 | Map<Variable, VLSVariable> variables) { |
230 | support.createUniversallyQuantifiedExpression(this, forall, trace, variables) | 231 | support.createQuantifiedExpression(this, forall, trace, variables, true) |
231 | } | 232 | } |
232 | 233 | ||
233 | def dispatch protected VLSTerm transformTerm(Exists exists, Logic2VampireLanguageMapperTrace trace, | 234 | def dispatch protected VLSTerm transformTerm(Exists exists, Logic2VampireLanguageMapperTrace trace, |
234 | Map<Variable, VLSVariable> variables) { | 235 | Map<Variable, VLSVariable> variables) { |
235 | support.createExistentiallyQuantifiedExpression(this, exists, trace, variables) | 236 | support.createQuantifiedExpression(this, exists, trace, variables, false) |
236 | } | 237 | } |
237 | 238 | ||
238 | def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace, | 239 | def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace, |
239 | Map<Variable, VLSVariable> variables) { | 240 | Map<Variable, VLSVariable> variables) { |
240 | return createVLSFunction => [ | 241 | return createVLSFunction => [ |
241 | it.constant = support.toIDMultiple("t", (instanceOf.range as ComplexTypeReference).referred.name) | 242 | it.constant = (instanceOf.range as ComplexTypeReference).referred.lookup(trace.type2Predicate).constant |
242 | it.terms += instanceOf.value.transformTerm(trace, variables) | 243 | it.terms += instanceOf.value.transformTerm(trace, variables) |
243 | ] | 244 | ] |
244 | } | 245 | } |
@@ -292,13 +293,8 @@ class Logic2VampireLanguageMapper { | |||
292 | Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | 293 | Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { |
293 | 294 | ||
294 | // cannot treat variable as function (constant) because of name ID not being the same | 295 | // cannot treat variable as function (constant) because of name ID not being the same |
295 | // below does not work | ||
296 | val res = createVLSVariable => [ | ||
297 | // it.name = support.toIDMultiple("Var", variable.lookup(variables).name) | ||
298 | it.name = support.toID(variable.lookup(variables).name) | ||
299 | ] | ||
300 | // no need for potprocessing cuz booleans are supported | 296 | // no need for potprocessing cuz booleans are supported |
301 | return res | 297 | return support.duplicate(variable.lookup(variables)) |
302 | } | 298 | } |
303 | 299 | ||
304 | // TODO | 300 | // TODO |
@@ -383,7 +379,7 @@ class Logic2VampireLanguageMapper { | |||
383 | // it.params += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] | 379 | // it.params += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] |
384 | // ] | 380 | // ] |
385 | return createVLSFunction => [ | 381 | return createVLSFunction => [ |
386 | it.constant = support.toIDMultiple("rel", relation.name) | 382 | it.constant = (relation as RelationDeclaration).lookup(trace.rel2Predicate).constant |
387 | it.terms += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] | 383 | it.terms += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] |
388 | ] | 384 | ] |
389 | } | 385 | } |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend index 23b57701..deb24778 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend | |||
@@ -30,15 +30,13 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
30 | // 1.1 if variable has type, creating list of type declarations | 30 | // 1.1 if variable has type, creating list of type declarations |
31 | val List<VLSVariable> relVar2VLS = new ArrayList | 31 | val List<VLSVariable> relVar2VLS = new ArrayList |
32 | val List<VLSFunction> relVar2TypeDecComply = new ArrayList | 32 | val List<VLSFunction> relVar2TypeDecComply = new ArrayList |
33 | val typedefs = new ArrayList<VLSTerm> | ||
34 | |||
35 | for (i : 0 ..< r.parameters.length) { | 33 | for (i : 0 ..< r.parameters.length) { |
36 | 34 | ||
37 | val v = createVLSVariable => [ | 35 | val v = createVLSVariable => [ |
38 | it.name = support.toIDMultiple("V", i.toString) | 36 | it.name = support.toIDMultiple("V", i.toString) |
39 | ] | 37 | ] |
40 | relVar2VLS.add(v) | 38 | relVar2VLS.add(v) |
41 | 39 | ||
42 | val relType = (r.parameters.get(i) as ComplexTypeReference).referred | 40 | val relType = (r.parameters.get(i) as ComplexTypeReference).referred |
43 | val varTypeComply = support.duplicate(relType.lookup(trace.type2Predicate), v) | 41 | val varTypeComply = support.duplicate(relType.lookup(trace.type2Predicate), v) |
44 | relVar2TypeDecComply.add(varTypeComply) | 42 | relVar2TypeDecComply.add(varTypeComply) |
@@ -47,33 +45,26 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
47 | 45 | ||
48 | val comply = createVLSFofFormula => [ | 46 | val comply = createVLSFofFormula => [ |
49 | val nameArray = r.name.split(" ") | 47 | val nameArray = r.name.split(" ") |
50 | it.name = support.toIDMultiple("compliance", nameArray.get(0), | 48 | it.name = support.toIDMultiple("compliance", nameArray.get(0), nameArray.get(2)) |
51 | nameArray.get(2)) | ||
52 | it.fofRole = "axiom" | 49 | it.fofRole = "axiom" |
53 | it.fofFormula = createVLSUniversalQuantifier => [ | 50 | it.fofFormula = createVLSUniversalQuantifier => [ |
54 | |||
55 | for (v : relVar2VLS) { | 51 | for (v : relVar2VLS) { |
56 | it.variables += support.duplicate(v) | 52 | it.variables += support.duplicate(v) |
57 | } | 53 | } |
58 | |||
59 | it.operand = createVLSImplies => [ | 54 | it.operand = createVLSImplies => [ |
60 | it.left = createVLSFunction => [ | 55 | val rel = createVLSFunction => [ |
61 | it.constant = support.toIDMultiple("rel", r.name) | 56 | it.constant = support.toIDMultiple("r", nameArray.get(0), nameArray.get(2)) |
62 | 57 | for (v : relVar2VLS) { | |
63 | for (i : 0 ..< r.parameters.length) { | 58 | it.terms += support.duplicate(v) |
64 | val v = createVLSVariable => [ | ||
65 | it.name = relVar2VLS.get(i).name | ||
66 | ] | ||
67 | it.terms += v | ||
68 | } | 59 | } |
69 | |||
70 | ] | 60 | ] |
61 | trace.rel2Predicate.put(r, rel) | ||
62 | it.left = support.duplicate(rel) | ||
71 | it.right = support.unfoldAnd(relVar2TypeDecComply) | 63 | it.right = support.unfoldAnd(relVar2TypeDecComply) |
72 | ] | 64 | ] |
73 | ] | 65 | ] |
74 | ] | 66 | ] |
75 | 67 | ||
76 | // trace.relationDefinition2Predicate.put(r,res) | ||
77 | trace.specification.formulas += comply | 68 | trace.specification.formulas += comply |
78 | } | 69 | } |
79 | 70 | ||
@@ -100,9 +91,8 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
100 | relationVar2TypeDecComply.put(variable, varTypeComply) | 91 | relationVar2TypeDecComply.put(variable, varTypeComply) |
101 | relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply)) | 92 | relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply)) |
102 | } | 93 | } |
103 | 94 | val nameArray = reldef.name.split(" ") | |
104 | val comply = createVLSFofFormula => [ | 95 | val comply = createVLSFofFormula => [ |
105 | val nameArray = reldef.name.split(" ") | ||
106 | it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2), | 96 | it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2), |
107 | nameArray.get(nameArray.length - 1)) | 97 | nameArray.get(nameArray.length - 1)) |
108 | it.fofRole = "axiom" | 98 | it.fofRole = "axiom" |
@@ -127,7 +117,8 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
127 | ] | 117 | ] |
128 | 118 | ||
129 | val res = createVLSFofFormula => [ | 119 | val res = createVLSFofFormula => [ |
130 | it.name = support.toIDMultiple("relation", reldef.name) | 120 | it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2), |
121 | nameArray.get(nameArray.length - 1)) | ||
131 | it.fofRole = "axiom" | 122 | it.fofRole = "axiom" |
132 | it.fofFormula = createVLSUniversalQuantifier => [ | 123 | it.fofFormula = createVLSUniversalQuantifier => [ |
133 | for (variable : reldef.variables) { | 124 | for (variable : reldef.variables) { |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend index 090cf916..d3595a73 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend | |||
@@ -17,6 +17,8 @@ import java.util.List | |||
17 | import java.util.Map | 17 | import java.util.Map |
18 | import org.eclipse.emf.common.util.EList | 18 | import org.eclipse.emf.common.util.EList |
19 | 19 | ||
20 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
21 | |||
20 | class Logic2VampireLanguageMapper_Support { | 22 | class Logic2VampireLanguageMapper_Support { |
21 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | 23 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
22 | 24 | ||
@@ -29,28 +31,27 @@ class Logic2VampireLanguageMapper_Support { | |||
29 | ids.split("\\s+").join("_") | 31 | ids.split("\\s+").join("_") |
30 | } | 32 | } |
31 | 33 | ||
32 | //Term Handling | 34 | // Term Handling |
33 | //TODO Make more general | 35 | // TODO Make more general |
34 | def protected VLSVariable duplicate(VLSVariable term) { | 36 | def protected VLSVariable duplicate(VLSVariable term) { |
35 | return createVLSVariable => [it.name = term.name] | 37 | return createVLSVariable => [it.name = term.name] |
36 | } | 38 | } |
37 | 39 | ||
38 | def protected VLSFunction duplicate(VLSFunction term) { | 40 | def protected VLSFunction duplicate(VLSFunction term) { |
39 | return createVLSFunction => [ | 41 | return createVLSFunction => [ |
40 | it.constant = term.constant | 42 | it.constant = term.constant |
41 | for ( v : term.terms){ | 43 | for (v : term.terms) { |
42 | it.terms += duplicate(v as VLSVariable) | 44 | it.terms += duplicate(v as VLSVariable) |
43 | } | 45 | } |
44 | ] | 46 | ] |
45 | } | 47 | } |
46 | 48 | ||
47 | def protected VLSFunction duplicate(VLSFunction term, VLSVariable v) { | 49 | def protected VLSFunction duplicate(VLSFunction term, VLSVariable v) { |
48 | return createVLSFunction => [ | 50 | return createVLSFunction => [ |
49 | it.constant = term.constant | 51 | it.constant = term.constant |
50 | it.terms += duplicate(v) | 52 | it.terms += duplicate(v) |
51 | ] | 53 | ] |
52 | } | 54 | } |
53 | |||
54 | 55 | ||
55 | def protected VLSFunction topLevelTypeFunc() { | 56 | def protected VLSFunction topLevelTypeFunc() { |
56 | return createVLSFunction => [ | 57 | return createVLSFunction => [ |
@@ -60,24 +61,22 @@ class Logic2VampireLanguageMapper_Support { | |||
60 | ] | 61 | ] |
61 | ] | 62 | ] |
62 | } | 63 | } |
63 | 64 | ||
64 | //TODO Make more general | 65 | // TODO Make more general |
65 | def establishUniqueness(List<VLSConstant> terms) { | 66 | def establishUniqueness(List<VLSConstant> terms) { |
66 | val List<VLSInequality> eqs = newArrayList | 67 | val List<VLSInequality> eqs = newArrayList |
67 | for (t1 : terms.subList(1, terms.length)){ | 68 | for (t1 : terms.subList(1, terms.length)) { |
68 | for (t2 : terms.subList(0, terms.indexOf(t1))){ | 69 | for (t2 : terms.subList(0, terms.indexOf(t1))) { |
69 | val eq = createVLSInequality => [ | 70 | val eq = createVLSInequality => [ |
70 | //TEMP | 71 | // TEMP |
71 | it.left = createVLSConstant => [it.name = t2.name] | 72 | it.left = createVLSConstant => [it.name = t2.name] |
72 | it.right = createVLSConstant => [it.name = t1.name] | 73 | it.right = createVLSConstant => [it.name = t1.name] |
73 | //TEMP | 74 | // TEMP |
74 | ] | 75 | ] |
75 | eqs.add(eq) | 76 | eqs.add(eq) |
76 | } | 77 | } |
77 | } | 78 | } |
78 | |||
79 | return unfoldAnd(eqs) | 79 | return unfoldAnd(eqs) |
80 | |||
81 | } | 80 | } |
82 | 81 | ||
83 | // Support Functions | 82 | // Support Functions |
@@ -108,6 +107,7 @@ class Logic2VampireLanguageMapper_Support { | |||
108 | throw new UnsupportedOperationException('''Logic operator with 0 operands!''') // TEMP | 107 | throw new UnsupportedOperationException('''Logic operator with 0 operands!''') // TEMP |
109 | } | 108 | } |
110 | 109 | ||
110 | // can delete below | ||
111 | def protected VLSTerm unfoldDistinctTerms(Logic2VampireLanguageMapper m, EList<Term> operands, | 111 | def protected VLSTerm unfoldDistinctTerms(Logic2VampireLanguageMapper m, EList<Term> operands, |
112 | Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | 112 | Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { |
113 | if (operands.size == 1) { | 113 | if (operands.size == 1) { |
@@ -143,58 +143,36 @@ class Logic2VampireLanguageMapper_Support { | |||
143 | * } | 143 | * } |
144 | */ | 144 | */ |
145 | // QUANTIFIERS + VARIABLES | 145 | // QUANTIFIERS + VARIABLES |
146 | def protected VLSTerm createUniversallyQuantifiedExpression(Logic2VampireLanguageMapper mapper, | 146 | def protected VLSTerm createQuantifiedExpression(Logic2VampireLanguageMapper mapper, |
147 | QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | 147 | QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables, boolean isUniversal) { |
148 | val variableMap = expression.quantifiedVariables.toInvertedMap [ v | | 148 | val variableMap = expression.quantifiedVariables.toInvertedMap [ v | |
149 | createVLSVariable => [it.name = toIDMultiple("Var", v.name)] | 149 | createVLSVariable => [it.name = toIDMultiple("V", v.name)] |
150 | ] | 150 | ] |
151 | 151 | ||
152 | val typedefs = new ArrayList<VLSTerm> | 152 | val typedefs = new ArrayList<VLSTerm> |
153 | for (variable : expression.quantifiedVariables) { | 153 | for (variable : expression.quantifiedVariables) { |
154 | val eq = createVLSFunction => [ | 154 | val eq = duplicate((variable.range as ComplexTypeReference).referred.lookup(trace.type2Predicate), variable.lookup(variableMap)) |
155 | it.constant = toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) | ||
156 | it.terms += createVLSVariable => [ | ||
157 | it.name = toIDMultiple("Var", variable.name) | ||
158 | ] | ||
159 | |||
160 | ] | ||
161 | typedefs.add(eq) | 155 | typedefs.add(eq) |
162 | } | 156 | } |
163 | 157 | if (isUniversal) { | |
164 | createVLSUniversalQuantifier => [ | 158 | createVLSUniversalQuantifier => [ |
165 | it.variables += variableMap.values | 159 | it.variables += variableMap.values |
166 | it.operand = createVLSImplies => [ | 160 | it.operand = createVLSImplies => [ |
167 | it.left = unfoldAnd(typedefs) | 161 | it.left = unfoldAnd(typedefs) |
168 | it.right = mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap)) | 162 | it.right = mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap)) |
163 | ] | ||
169 | ] | 164 | ] |
170 | ] | 165 | } else { |
171 | } | 166 | typedefs.add(mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap))) |
167 | createVLSExistentialQuantifier => [ | ||
168 | it.variables += variableMap.values | ||
169 | it.operand = unfoldAnd(typedefs) | ||
172 | 170 | ||
173 | def protected VLSTerm createExistentiallyQuantifiedExpression(Logic2VampireLanguageMapper mapper, | ||
174 | QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | ||
175 | val variableMap = expression.quantifiedVariables.toInvertedMap [ v | | ||
176 | createVLSVariable => [it.name = toIDMultiple("Var", v.name)] | ||
177 | ] | ||
178 | |||
179 | val typedefs = new ArrayList<VLSTerm> | ||
180 | for (variable : expression.quantifiedVariables) { | ||
181 | val eq = createVLSFunction => [ | ||
182 | it.constant = toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) | ||
183 | it.terms += createVLSVariable => [ | ||
184 | it.name = toIDMultiple("Var", variable.name) | ||
185 | ] | ||
186 | ] | 171 | ] |
187 | typedefs.add(eq) | ||
188 | } | 172 | } |
189 | 173 | ||
190 | typedefs.add(mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap))) | ||
191 | createVLSExistentialQuantifier => [ | ||
192 | it.variables += variableMap.values | ||
193 | it.operand = unfoldAnd(typedefs) | ||
194 | |||
195 | ] | ||
196 | } | 174 | } |
197 | 175 | ||
198 | def protected boolean dfsSupertypeCheck(Type type, Type type2) { | 176 | def protected boolean dfsSupertypeCheck(Type type, Type type2) { |
199 | // There is surely a better way to do this | 177 | // There is surely a better way to do this |
200 | if (type.supertypes.isEmpty) | 178 | if (type.supertypes.isEmpty) |
@@ -213,7 +191,5 @@ class Logic2VampireLanguageMapper_Support { | |||
213 | def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) { | 191 | def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) { |
214 | new HashMap(map1) => [putAll(map2)] | 192 | new HashMap(map1) => [putAll(map2)] |
215 | } | 193 | } |
216 | |||
217 | |||
218 | 194 | ||
219 | } | 195 | } |