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 | |
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)
29 files changed, 146 insertions, 292 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 | } |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin index bda7463e..4828107b 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin | |||
Binary files differ | |||
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 a062fcec..64061f82 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 5fc0da27..f0cd1c7c 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 562b9bbf..7d15db96 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 dd7bdf86..8fed8f56 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 496d27b3..a40e27e4 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 4a03f2ce..4b6b4a1e 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 511f4a1f..c3035658 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 37e9480c..2e21736e 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/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin index f473c4bc..e870dabc 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_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/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin index e53791d6..ed198ef6 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_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/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin index 1b112c56..83697125 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 c8284658..063650c5 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 89d4c657..e36d2270 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 3c98bd64..5e5be153 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/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java index 6643576f..dc2cd5ec 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 | |||
@@ -50,6 +50,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | |||
50 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration; | 50 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration; |
51 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue; | 51 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue; |
52 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; | 52 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; |
53 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
53 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | 54 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; |
54 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | 55 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; |
55 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | 56 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; |
@@ -262,18 +263,18 @@ public class Logic2VampireLanguageMapper { | |||
262 | } | 263 | } |
263 | 264 | ||
264 | protected VLSTerm _transformTerm(final Forall forall, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 265 | protected VLSTerm _transformTerm(final Forall forall, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { |
265 | return this.support.createUniversallyQuantifiedExpression(this, forall, trace, variables); | 266 | return this.support.createQuantifiedExpression(this, forall, trace, variables, true); |
266 | } | 267 | } |
267 | 268 | ||
268 | protected VLSTerm _transformTerm(final Exists exists, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 269 | protected VLSTerm _transformTerm(final Exists exists, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { |
269 | return this.support.createExistentiallyQuantifiedExpression(this, exists, trace, variables); | 270 | return this.support.createQuantifiedExpression(this, exists, trace, variables, false); |
270 | } | 271 | } |
271 | 272 | ||
272 | protected VLSTerm _transformTerm(final InstanceOf instanceOf, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 273 | protected VLSTerm _transformTerm(final InstanceOf instanceOf, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { |
273 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 274 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
274 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | 275 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { |
275 | TypeReference _range = instanceOf.getRange(); | 276 | TypeReference _range = instanceOf.getRange(); |
276 | it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); | 277 | it.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate).getConstant()); |
277 | EList<VLSTerm> _terms = it.getTerms(); | 278 | EList<VLSTerm> _terms = it.getTerms(); |
278 | VLSTerm _transformTerm = this.transformTerm(instanceOf.getValue(), trace, variables); | 279 | VLSTerm _transformTerm = this.transformTerm(instanceOf.getValue(), trace, variables); |
279 | _terms.add(_transformTerm); | 280 | _terms.add(_transformTerm); |
@@ -303,12 +304,7 @@ public class Logic2VampireLanguageMapper { | |||
303 | } | 304 | } |
304 | 305 | ||
305 | protected VLSTerm _transformSymbolicReference(final Variable variable, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 306 | protected VLSTerm _transformSymbolicReference(final Variable variable, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { |
306 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 307 | return this.support.duplicate(CollectionsUtil.<Variable, VLSVariable>lookup(variable, variables)); |
307 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
308 | it.setName(this.support.toID(CollectionsUtil.<Variable, VLSVariable>lookup(variable, variables).getName())); | ||
309 | }; | ||
310 | final VLSVariable res = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
311 | return res; | ||
312 | } | 308 | } |
313 | 309 | ||
314 | protected VLSTerm _transformSymbolicReference(final FunctionDeclaration function, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 310 | protected VLSTerm _transformSymbolicReference(final FunctionDeclaration function, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { |
@@ -359,7 +355,7 @@ public class Logic2VampireLanguageMapper { | |||
359 | protected VLSTerm _transformSymbolicReference(final Relation relation, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 355 | protected VLSTerm _transformSymbolicReference(final Relation relation, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { |
360 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 356 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
361 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | 357 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { |
362 | it.setConstant(this.support.toIDMultiple("rel", relation.getName())); | 358 | it.setConstant(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) relation), trace.rel2Predicate).getConstant()); |
363 | EList<VLSTerm> _terms = it.getTerms(); | 359 | EList<VLSTerm> _terms = it.getTerms(); |
364 | final Function1<Term, VLSTerm> _function_1 = (Term p) -> { | 360 | final Function1<Term, VLSTerm> _function_1 = (Term p) -> { |
365 | return this.transformTerm(p, trace, variables); | 361 | return this.transformTerm(p, trace, variables); |
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 4f5c6acc..d5745333 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 | |||
@@ -48,7 +48,6 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
48 | public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) { | 48 | public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) { |
49 | final List<VLSVariable> relVar2VLS = new ArrayList<VLSVariable>(); | 49 | final List<VLSVariable> relVar2VLS = new ArrayList<VLSVariable>(); |
50 | final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>(); | 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; | 51 | int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; |
53 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); | 52 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); |
54 | for (final Integer i : _doubleDotLessThan) { | 53 | for (final Integer i : _doubleDotLessThan) { |
@@ -68,8 +67,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
68 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 67 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
69 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 68 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { |
70 | final String[] nameArray = r.getName().split(" "); | 69 | final String[] nameArray = r.getName().split(" "); |
71 | it.setName(this.support.toIDMultiple("compliance", nameArray[0], | 70 | it.setName(this.support.toIDMultiple("compliance", nameArray[0], nameArray[2])); |
72 | nameArray[2])); | ||
73 | it.setFofRole("axiom"); | 71 | it.setFofRole("axiom"); |
74 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 72 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
75 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | 73 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { |
@@ -82,23 +80,16 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
82 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | 80 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { |
83 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 81 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
84 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { | 82 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { |
85 | it_3.setConstant(this.support.toIDMultiple("rel", r.getName())); | 83 | it_3.setConstant(this.support.toIDMultiple("r", nameArray[0], nameArray[2])); |
86 | int _length_1 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | 84 | for (final VLSVariable v_1 : relVar2VLS) { |
87 | ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(0, _length_1, true); | 85 | EList<VLSTerm> _terms = it_3.getTerms(); |
88 | for (final Integer i_1 : _doubleDotLessThan_1) { | 86 | VLSVariable _duplicate_1 = this.support.duplicate(v_1); |
89 | { | 87 | _terms.add(_duplicate_1); |
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 | } | 88 | } |
99 | }; | 89 | }; |
100 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3); | 90 | final VLSFunction rel = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3); |
101 | it_2.setLeft(_doubleArrow); | 91 | trace.rel2Predicate.put(r, rel); |
92 | it_2.setLeft(this.support.duplicate(rel)); | ||
102 | it_2.setRight(this.support.unfoldAnd(relVar2TypeDecComply)); | 93 | it_2.setRight(this.support.unfoldAnd(relVar2TypeDecComply)); |
103 | }; | 94 | }; |
104 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | 95 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); |
@@ -139,9 +130,9 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
139 | relationVar2TypeDecRes.put(variable, this.support.duplicate(varTypeComply)); | 130 | relationVar2TypeDecRes.put(variable, this.support.duplicate(varTypeComply)); |
140 | } | 131 | } |
141 | } | 132 | } |
133 | final String[] nameArray = reldef.getName().split(" "); | ||
142 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 134 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
143 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 135 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { |
144 | final String[] nameArray = reldef.getName().split(" "); | ||
145 | int _length = nameArray.length; | 136 | int _length = nameArray.length; |
146 | int _minus = (_length - 2); | 137 | int _minus = (_length - 2); |
147 | int _length_1 = nameArray.length; | 138 | int _length_1 = nameArray.length; |
@@ -190,7 +181,12 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
190 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | 181 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); |
191 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 182 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
192 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | 183 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { |
193 | it.setName(this.support.toIDMultiple("relation", reldef.getName())); | 184 | int _length = nameArray.length; |
185 | int _minus = (_length - 2); | ||
186 | int _length_1 = nameArray.length; | ||
187 | int _minus_1 = (_length_1 - 1); | ||
188 | it.setName(this.support.toIDMultiple("relation", nameArray[_minus], | ||
189 | nameArray[_minus_1])); | ||
194 | it.setFofRole("axiom"); | 190 | it.setFofRole("axiom"); |
195 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 191 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
196 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | 192 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { |
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 35497eab..72ca44e9 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 | |||
@@ -20,6 +20,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; | |||
20 | 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.TypeReference; | 21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; |
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | 22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; |
23 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
23 | import java.util.ArrayList; | 24 | import java.util.ArrayList; |
24 | import java.util.Collection; | 25 | import java.util.Collection; |
25 | import java.util.HashMap; | 26 | import java.util.HashMap; |
@@ -220,13 +221,13 @@ public class Logic2VampireLanguageMapper_Support { | |||
220 | * ids.map[it.split("\\s+").join("'")].join("'") | 221 | * ids.map[it.split("\\s+").join("'")].join("'") |
221 | * } | 222 | * } |
222 | */ | 223 | */ |
223 | protected VLSTerm createUniversallyQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 224 | protected VLSTerm createQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables, final boolean isUniversal) { |
224 | VLSUniversalQuantifier _xblockexpression = null; | 225 | VLSTerm _xblockexpression = null; |
225 | { | 226 | { |
226 | final Function1<Variable, VLSVariable> _function = (Variable v) -> { | 227 | final Function1<Variable, VLSVariable> _function = (Variable v) -> { |
227 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 228 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); |
228 | final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> { | 229 | final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> { |
229 | it.setName(this.toIDMultiple("Var", v.getName())); | 230 | it.setName(this.toIDMultiple("V", v.getName())); |
230 | }; | 231 | }; |
231 | return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1); | 232 | return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1); |
232 | }; | 233 | }; |
@@ -235,80 +236,43 @@ public class Logic2VampireLanguageMapper_Support { | |||
235 | EList<Variable> _quantifiedVariables = expression.getQuantifiedVariables(); | 236 | EList<Variable> _quantifiedVariables = expression.getQuantifiedVariables(); |
236 | for (final Variable variable : _quantifiedVariables) { | 237 | for (final Variable variable : _quantifiedVariables) { |
237 | { | 238 | { |
238 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 239 | TypeReference _range = variable.getRange(); |
239 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | 240 | final VLSFunction eq = this.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate), CollectionsUtil.<Variable, VLSVariable>lookup(variable, variableMap)); |
240 | TypeReference _range = variable.getRange(); | ||
241 | it.setConstant(this.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); | ||
242 | EList<VLSTerm> _terms = it.getTerms(); | ||
243 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
244 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | ||
245 | it_1.setName(this.toIDMultiple("Var", variable.getName())); | ||
246 | }; | ||
247 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2); | ||
248 | _terms.add(_doubleArrow); | ||
249 | }; | ||
250 | final VLSFunction eq = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
251 | typedefs.add(eq); | 241 | typedefs.add(eq); |
252 | } | 242 | } |
253 | } | 243 | } |
254 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 244 | VLSTerm _xifexpression = null; |
255 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it) -> { | 245 | if (isUniversal) { |
256 | EList<VLSVariable> _variables = it.getVariables(); | 246 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
257 | Collection<VLSVariable> _values = variableMap.values(); | 247 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it) -> { |
258 | Iterables.<VLSVariable>addAll(_variables, _values); | 248 | EList<VLSVariable> _variables = it.getVariables(); |
259 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | 249 | Collection<VLSVariable> _values = variableMap.values(); |
260 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_1) -> { | 250 | Iterables.<VLSVariable>addAll(_variables, _values); |
261 | it_1.setLeft(this.unfoldAnd(typedefs)); | 251 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); |
262 | it_1.setRight(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); | 252 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_1) -> { |
263 | }; | 253 | it_1.setLeft(this.unfoldAnd(typedefs)); |
264 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | 254 | it_1.setRight(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); |
265 | it.setOperand(_doubleArrow); | 255 | }; |
266 | }; | 256 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); |
267 | _xblockexpression = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | 257 | it.setOperand(_doubleArrow); |
268 | } | ||
269 | return _xblockexpression; | ||
270 | } | ||
271 | |||
272 | protected VLSTerm createExistentiallyQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
273 | VLSExistentialQuantifier _xblockexpression = null; | ||
274 | { | ||
275 | final Function1<Variable, VLSVariable> _function = (Variable v) -> { | ||
276 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
277 | final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> { | ||
278 | it.setName(this.toIDMultiple("Var", v.getName())); | ||
279 | }; | 258 | }; |
280 | return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1); | 259 | _xifexpression = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); |
281 | }; | 260 | } else { |
282 | final Map<Variable, VLSVariable> variableMap = IterableExtensions.<Variable, VLSVariable>toInvertedMap(expression.getQuantifiedVariables(), _function); | 261 | VLSExistentialQuantifier _xblockexpression_1 = null; |
283 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | ||
284 | EList<Variable> _quantifiedVariables = expression.getQuantifiedVariables(); | ||
285 | for (final Variable variable : _quantifiedVariables) { | ||
286 | { | 262 | { |
287 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 263 | typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); |
288 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | 264 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); |
289 | TypeReference _range = variable.getRange(); | 265 | final Procedure1<VLSExistentialQuantifier> _function_2 = (VLSExistentialQuantifier it) -> { |
290 | it.setConstant(this.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); | 266 | EList<VLSVariable> _variables = it.getVariables(); |
291 | EList<VLSTerm> _terms = it.getTerms(); | 267 | Collection<VLSVariable> _values = variableMap.values(); |
292 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 268 | Iterables.<VLSVariable>addAll(_variables, _values); |
293 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | 269 | it.setOperand(this.unfoldAnd(typedefs)); |
294 | it_1.setName(this.toIDMultiple("Var", variable.getName())); | ||
295 | }; | ||
296 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2); | ||
297 | _terms.add(_doubleArrow); | ||
298 | }; | 270 | }; |
299 | final VLSFunction eq = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | 271 | _xblockexpression_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_2); |
300 | typedefs.add(eq); | ||
301 | } | 272 | } |
273 | _xifexpression = _xblockexpression_1; | ||
302 | } | 274 | } |
303 | typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); | 275 | _xblockexpression = _xifexpression; |
304 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | ||
305 | final Procedure1<VLSExistentialQuantifier> _function_1 = (VLSExistentialQuantifier it) -> { | ||
306 | EList<VLSVariable> _variables = it.getVariables(); | ||
307 | Collection<VLSVariable> _values = variableMap.values(); | ||
308 | Iterables.<VLSVariable>addAll(_variables, _values); | ||
309 | it.setOperand(this.unfoldAnd(typedefs)); | ||
310 | }; | ||
311 | _xblockexpression = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_1); | ||
312 | } | 276 | } |
313 | return _xblockexpression; | 277 | return _xblockexpression; |
314 | } | 278 | } |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem index a0b5d6ea..85e09a0a 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem | |||
@@ -1,5 +1,5 @@ | |||
1 | <?xml version="1.0" encoding="ASCII"?> | 1 | <?xml version="1.0" encoding="ASCII"?> |
2 | <language:LogicProblem xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:ecore2logicannotations="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language/ecore2logicannotation" xmlns:language="http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" xmlns:language_1="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" xmlns:viatra2logicannotations="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language/viatra2logicannotation"> | 2 | <language:LogicProblem xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:ecore2logicannotations="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language/ecore2logicannotation" xmlns:language="http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" xmlns:language_1="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language"> |
3 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalElement class" subtypes="//@types.2" isAbstract="true"/> | 3 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalElement class" subtypes="//@types.2" isAbstract="true"/> |
4 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalArchitectureModel class"/> | 4 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalArchitectureModel class"/> |
5 | <types xsi:type="language_1:TypeDeclaration" name="Function class" supertypes="//@types.0"/> | 5 | <types xsi:type="language_1:TypeDeclaration" name="Function class" supertypes="//@types.0"/> |
@@ -494,22 +494,6 @@ | |||
494 | </expression> | 494 | </expression> |
495 | </value> | 495 | </value> |
496 | </assertions> | 496 | </assertions> |
497 | <assertions name="errorpattern ca mcgill ecse dslreasoner vampire queries terminatorAndInformation" annotations="//@annotations.20"> | ||
498 | <value xsi:type="language_1:Forall"> | ||
499 | <quantifiedVariables name="p0"> | ||
500 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/> | ||
501 | </quantifiedVariables> | ||
502 | <quantifiedVariables name="p1"> | ||
503 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/> | ||
504 | </quantifiedVariables> | ||
505 | <expression xsi:type="language_1:Not"> | ||
506 | <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15"> | ||
507 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@quantifiedVariables.0"/> | ||
508 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@quantifiedVariables.1"/> | ||
509 | </operand> | ||
510 | </expression> | ||
511 | </value> | ||
512 | </assertions> | ||
513 | <relations xsi:type="language_1:RelationDeclaration" name="interface reference FunctionalElement"> | 497 | <relations xsi:type="language_1:RelationDeclaration" name="interface reference FunctionalElement"> |
514 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/> | 498 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/> |
515 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.5"/> | 499 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.5"/> |
@@ -570,48 +554,6 @@ | |||
570 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | 554 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> |
571 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/> | 555 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/> |
572 | </relations> | 556 | </relations> |
573 | <relations xsi:type="language_1:RelationDefinition" name="pattern ca mcgill ecse dslreasoner vampire queries terminatorAndInformation" annotations="//@annotations.19"> | ||
574 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/> | ||
575 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/> | ||
576 | <variables name="parameter T"> | ||
577 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/> | ||
578 | </variables> | ||
579 | <variables name="parameter I"> | ||
580 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/> | ||
581 | </variables> | ||
582 | <value xsi:type="language_1:Or"> | ||
583 | <operands xsi:type="language_1:Exists"> | ||
584 | <quantifiedVariables name="variable Out"> | ||
585 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.7"/> | ||
586 | </quantifiedVariables> | ||
587 | <expression xsi:type="language_1:And"> | ||
588 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.11"> | ||
589 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.0/@quantifiedVariables.0"/> | ||
590 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.1"/> | ||
591 | </operands> | ||
592 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12"> | ||
593 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.0/@quantifiedVariables.0"/> | ||
594 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.0"/> | ||
595 | </operands> | ||
596 | </expression> | ||
597 | </operands> | ||
598 | <operands xsi:type="language_1:Exists"> | ||
599 | <quantifiedVariables name="variable In"> | ||
600 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.6"/> | ||
601 | </quantifiedVariables> | ||
602 | <expression xsi:type="language_1:And"> | ||
603 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.7"> | ||
604 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.1"/> | ||
605 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.1/@quantifiedVariables.0"/> | ||
606 | </operands> | ||
607 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12"> | ||
608 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.1/@quantifiedVariables.0"/> | ||
609 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.0"/> | ||
610 | </operands> | ||
611 | </expression> | ||
612 | </operands> | ||
613 | </value> | ||
614 | </relations> | ||
615 | <elements name="Root literal FunctionType" definedInType="//@types.9"/> | 557 | <elements name="Root literal FunctionType" definedInType="//@types.9"/> |
616 | <elements name="Intermediate literal FunctionType" definedInType="//@types.9"/> | 558 | <elements name="Intermediate literal FunctionType" definedInType="//@types.9"/> |
617 | <elements name="Leaf literal FunctionType" definedInType="//@types.9"/> | 559 | <elements name="Leaf literal FunctionType" definedInType="//@types.9"/> |
@@ -635,6 +577,4 @@ | |||
635 | <annotations xsi:type="ecore2logicannotations:InverseRelationAssertion" target="//@assertions.16" inverseA="//@relations.8" inverseB="//@relations.13"/> | 577 | <annotations xsi:type="ecore2logicannotations:InverseRelationAssertion" target="//@assertions.16" inverseA="//@relations.8" inverseB="//@relations.13"/> |
636 | <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.17" relation="//@relations.14" lower="1"/> | 578 | <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.17" relation="//@relations.14" lower="1"/> |
637 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.18" relation="//@relations.14" upper="1"/> | 579 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.18" relation="//@relations.14" upper="1"/> |
638 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.15" patternFullyQualifiedName="ca.mcgill.ecse.dslreasoner.vampire.queries.terminatorAndInformation"/> | ||
639 | <annotations xsi:type="viatra2logicannotations:TransformedViatraWellformednessConstraint" target="//@assertions.19" query="//@annotations.19"/> | ||
640 | </language:LogicProblem> | 580 | </language:LogicProblem> |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp index 865b3155..4bc4628b 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp | |||
@@ -1,42 +1,39 @@ | |||
1 | % This is an initial Test Comment | 1 | % This is an initial Test Comment |
2 | fof ( typeDef_FunctionType , axiom , ! [ A ] : ( t_FunctionType ( A ) <=> ( e_Root_FunctionType ( A ) | ( e_Intermediate_FunctionType ( A ) | e_Leaf_FunctionType ( A ) ) ) ) ) . | 2 | fof ( typeDef_FunctionType , axiom , ! [ A ] : ( t_FunctionType ( A ) <=> ( e_Root_FunctionType ( A ) | ( e_Intermediate_FunctionType ( A ) | e_Leaf_FunctionType ( A ) ) ) ) ) . |
3 | fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( t_FunctionalData ( A ) & ( t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalInterface ( A ) & ~ t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_InformationLink ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalInterface ( A ) & t_FAMTerminator ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . | 3 | fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_Function ( A ) & ( ~ t_FunctionType ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalData ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_Function ( A ) & ( t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalData ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_Function ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalData ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_Function ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionalInput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ( t_FunctionalData ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_Function ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalData ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_Function ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalData ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_Function ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( t_InformationLink ( A ) & ( ~ t_FunctionalData ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_Function ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ( t_FunctionalData ( A ) & t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . |
4 | fof ( typeScope , axiom , ! [ A ] : ( object ( A ) <=> ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | A = o5 ) ) ) ) ) ) . | 4 | fof ( typeScope , axiom , ! [ A ] : ( object ( A ) <=> ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | A = o5 ) ) ) ) ) ) . |
5 | fof ( typeUniqueness , axiom , o1 != o2 & ( o1 != o3 & ( o2 != o3 & ( o1 != o4 & ( o2 != o4 & ( o3 != o4 & ( o1 != o5 & ( o2 != o5 & ( o3 != o5 & o4 != o5 ) ) ) ) ) ) ) ) ) . | 5 | fof ( typeUniqueness , axiom , o1 != o2 & ( o1 != o3 & ( o2 != o3 & ( o1 != o4 & ( o2 != o4 & ( o3 != o4 & ( o1 != o5 & ( o2 != o5 & ( o3 != o5 & o4 != o5 ) ) ) ) ) ) ) ) ) . |
6 | fof ( compliance_interface_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( rel_interface_reference_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) . | 6 | fof ( compliance_interface_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) . |
7 | fof ( compliance_model_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( rel_model_reference_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalArchitectureModel ( V_1 ) ) ) ) . | 7 | fof ( compliance_model_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_model_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalArchitectureModel ( V_1 ) ) ) ) . |
8 | fof ( compliance_parent_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( rel_parent_reference_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_Function ( V_1 ) ) ) ) . | 8 | fof ( compliance_parent_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_parent_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_Function ( V_1 ) ) ) ) . |
9 | fof ( compliance_rootElements_FunctionalArchitectureModel , axiom , ! [ V_0 , V_1 ] : ( rel_rootElements_reference_FunctionalArchitectureModel ( V_0 , V_1 ) => ( t_FunctionalArchitectureModel ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) . | 9 | fof ( compliance_rootElements_FunctionalArchitectureModel , axiom , ! [ V_0 , V_1 ] : ( r_rootElements_FunctionalArchitectureModel ( V_0 , V_1 ) => ( t_FunctionalArchitectureModel ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) . |
10 | fof ( compliance_subElements_Function , axiom , ! [ V_0 , V_1 ] : ( rel_subElements_reference_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) . | 10 | fof ( compliance_subElements_Function , axiom , ! [ V_0 , V_1 ] : ( r_subElements_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) . |
11 | fof ( compliance_data_FAMTerminator , axiom , ! [ V_0 , V_1 ] : ( rel_data_reference_FAMTerminator ( V_0 , V_1 ) => ( t_FAMTerminator ( V_0 ) & t_FunctionalData ( V_1 ) ) ) ) . | 11 | fof ( compliance_data_FAMTerminator , axiom , ! [ V_0 , V_1 ] : ( r_data_FAMTerminator ( V_0 , V_1 ) => ( t_FAMTerminator ( V_0 ) & t_FunctionalData ( V_1 ) ) ) ) . |
12 | fof ( compliance_from_InformationLink , axiom , ! [ V_0 , V_1 ] : ( rel_from_reference_InformationLink ( V_0 , V_1 ) => ( t_InformationLink ( V_0 ) & t_FunctionalOutput ( V_1 ) ) ) ) . | 12 | fof ( compliance_from_InformationLink , axiom , ! [ V_0 , V_1 ] : ( r_from_InformationLink ( V_0 , V_1 ) => ( t_InformationLink ( V_0 ) & t_FunctionalOutput ( V_1 ) ) ) ) . |
13 | fof ( compliance_to_InformationLink , axiom , ! [ V_0 , V_1 ] : ( rel_to_reference_InformationLink ( V_0 , V_1 ) => ( t_InformationLink ( V_0 ) & t_FunctionalInput ( V_1 ) ) ) ) . | 13 | fof ( compliance_to_InformationLink , axiom , ! [ V_0 , V_1 ] : ( r_to_InformationLink ( V_0 , V_1 ) => ( t_InformationLink ( V_0 ) & t_FunctionalInput ( V_1 ) ) ) ) . |
14 | fof ( compliance_data_FunctionalInterface , axiom , ! [ V_0 , V_1 ] : ( rel_data_reference_FunctionalInterface ( V_0 , V_1 ) => ( t_FunctionalInterface ( V_0 ) & t_FunctionalData ( V_1 ) ) ) ) . | 14 | fof ( compliance_data_FunctionalInterface , axiom , ! [ V_0 , V_1 ] : ( r_data_FunctionalInterface ( V_0 , V_1 ) => ( t_FunctionalInterface ( V_0 ) & t_FunctionalData ( V_1 ) ) ) ) . |
15 | fof ( compliance_element_FunctionalInterface , axiom , ! [ V_0 , V_1 ] : ( rel_element_reference_FunctionalInterface ( V_0 , V_1 ) => ( t_FunctionalInterface ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) . | 15 | fof ( compliance_element_FunctionalInterface , axiom , ! [ V_0 , V_1 ] : ( r_element_FunctionalInterface ( V_0 , V_1 ) => ( t_FunctionalInterface ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) . |
16 | fof ( compliance_IncomingLinks_FunctionalInput , axiom , ! [ V_0 , V_1 ] : ( rel_IncomingLinks_reference_FunctionalInput ( V_0 , V_1 ) => ( t_FunctionalInput ( V_0 ) & t_InformationLink ( V_1 ) ) ) ) . | 16 | fof ( compliance_IncomingLinks_FunctionalInput , axiom , ! [ V_0 , V_1 ] : ( r_IncomingLinks_FunctionalInput ( V_0 , V_1 ) => ( t_FunctionalInput ( V_0 ) & t_InformationLink ( V_1 ) ) ) ) . |
17 | fof ( compliance_outgoingLinks_FunctionalOutput , axiom , ! [ V_0 , V_1 ] : ( rel_outgoingLinks_reference_FunctionalOutput ( V_0 , V_1 ) => ( t_FunctionalOutput ( V_0 ) & t_InformationLink ( V_1 ) ) ) ) . | 17 | fof ( compliance_outgoingLinks_FunctionalOutput , axiom , ! [ V_0 , V_1 ] : ( r_outgoingLinks_FunctionalOutput ( V_0 , V_1 ) => ( t_FunctionalOutput ( V_0 ) & t_InformationLink ( V_1 ) ) ) ) . |
18 | fof ( compliance_terminator_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( rel_terminator_reference_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FAMTerminator ( V_1 ) ) ) ) . | 18 | fof ( compliance_terminator_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( r_terminator_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FAMTerminator ( V_1 ) ) ) ) . |
19 | fof ( compliance_interface_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( rel_interface_reference_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) . | 19 | fof ( compliance_interface_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) . |
20 | fof ( compliance_type_Function , axiom , ! [ V_0 , V_1 ] : ( rel_type_attribute_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionType ( V_1 ) ) ) ) . | 20 | fof ( compliance_type_Function , axiom , ! [ V_0 , V_1 ] : ( r_type_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionType ( V_1 ) ) ) ) . |
21 | fof ( compliance_queries_terminatorAndInformation , axiom , ! [ V_parameter_T , V_parameter_I ] : ( rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( V_parameter_T , V_parameter_I ) => ( t_FAMTerminator_class ( V_parameter_T ) & t_InformationLink_class ( V_parameter_I ) ) ) ) . | 21 | fof ( upperMultiplicity_interface_FunctionalElement , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalElement ( V_src ) & ( t_FunctionalInterface ( V_trg_1 ) & t_FunctionalInterface ( V_trg_2 ) ) ) => ( ( r_interface_FunctionalElement ( V_src , V_trg_1 ) & r_interface_FunctionalElement ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . |
22 | fof ( relation_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ V_parameter_T , V_parameter_I ] : ( ( t_FAMTerminator_class ( V_parameter_T ) & t_InformationLink_class ( V_parameter_I ) ) => ( rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( V_parameter_T , V_parameter_I ) <=> ( ? [ Var_variable_Out ] : ( t_FunctionalOutput_class ( Var_variable_Out ) & ( rel_outgoingLinks_reference_FunctionalOutput ( Var_variable_Out , V_parameter_I ) & rel_terminator_reference_FunctionalData ( Var_variable_Out , V_parameter_T ) ) ) | ? [ Var_variable_In ] : ( t_FunctionalInput_class ( Var_variable_In ) & ( rel_to_reference_InformationLink ( V_parameter_I , Var_variable_In ) & rel_terminator_reference_FunctionalData ( Var_variable_In , V_parameter_T ) ) ) ) ) ) ) . | 22 | fof ( lowerMultiplicity_model_FunctionalElement , axiom , ! [ V_src ] : ( t_FunctionalElement ( V_src ) => ? [ V_trg_1 ] : ( t_FunctionalArchitectureModel ( V_trg_1 ) & r_model_FunctionalElement ( V_src , V_trg_1 ) ) ) ) . |
23 | fof ( upperMultiplicity_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_FunctionalInterface_class ( Var_trg_1 ) & t_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . | 23 | fof ( upperMultiplicity_model_FunctionalElement , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalElement ( V_src ) & ( t_FunctionalArchitectureModel ( V_trg_1 ) & t_FunctionalArchitectureModel ( V_trg_2 ) ) ) => ( ( r_model_FunctionalElement ( V_src , V_trg_1 ) & r_model_FunctionalElement ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . |
24 | fof ( lowerMultiplicity_model_FunctionalElement , axiom , ! [ Var_src ] : ( t_FunctionalElement_class ( Var_src ) => ? [ Var_trg_1 ] : ( t_FunctionalArchitectureModel_class ( Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) ) ) ) . | 24 | fof ( upperMultiplicity_parent_FunctionalElement , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalElement ( V_src ) & ( t_Function ( V_trg_1 ) & t_Function ( V_trg_2 ) ) ) => ( ( r_parent_FunctionalElement ( V_src , V_trg_1 ) & r_parent_FunctionalElement ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . |
25 | fof ( upperMultiplicity_model_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_FunctionalArchitectureModel_class ( Var_trg_1 ) & t_FunctionalArchitectureModel_class ( Var_trg_2 ) ) ) => ( ( rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . | 25 | fof ( upperMultiplicity_data_FAMTerminator , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FAMTerminator ( V_src ) & ( t_FunctionalData ( V_trg_1 ) & t_FunctionalData ( V_trg_2 ) ) ) => ( ( r_data_FAMTerminator ( V_src , V_trg_1 ) & r_data_FAMTerminator ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . |
26 | fof ( upperMultiplicity_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_Function_class ( Var_trg_1 ) & t_Function_class ( Var_trg_2 ) ) ) => ( ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_parent_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . | 26 | fof ( upperMultiplicity_from_InformationLink , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_InformationLink ( V_src ) & ( t_FunctionalOutput ( V_trg_1 ) & t_FunctionalOutput ( V_trg_2 ) ) ) => ( ( r_from_InformationLink ( V_src , V_trg_1 ) & r_from_InformationLink ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . |
27 | fof ( upperMultiplicity_data_FAMTerminator , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FAMTerminator_class ( Var_src ) & ( t_FunctionalData_class ( Var_trg_1 ) & t_FunctionalData_class ( Var_trg_2 ) ) ) => ( ( rel_data_reference_FAMTerminator ( Var_src , Var_trg_1 ) & rel_data_reference_FAMTerminator ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . | 27 | fof ( lowerMultiplicity_to_InformationLink , axiom , ! [ V_src ] : ( t_InformationLink ( V_src ) => ? [ V_trg_1 ] : ( t_FunctionalInput ( V_trg_1 ) & r_to_InformationLink ( V_src , V_trg_1 ) ) ) ) . |
28 | fof ( upperMultiplicity_from_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_InformationLink_class ( Var_src ) & ( t_FunctionalOutput_class ( Var_trg_1 ) & t_FunctionalOutput_class ( Var_trg_2 ) ) ) => ( ( rel_from_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_from_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . | 28 | fof ( upperMultiplicity_to_InformationLink , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_InformationLink ( V_src ) & ( t_FunctionalInput ( V_trg_1 ) & t_FunctionalInput ( V_trg_2 ) ) ) => ( ( r_to_InformationLink ( V_src , V_trg_1 ) & r_to_InformationLink ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . |
29 | fof ( lowerMultiplicity_to_InformationLink , axiom , ! [ Var_src ] : ( t_InformationLink_class ( Var_src ) => ? [ Var_trg_1 ] : ( t_FunctionalInput_class ( Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) ) ) ) . | 29 | fof ( upperMultiplicity_element_FunctionalInterface , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalInterface ( V_src ) & ( t_FunctionalElement ( V_trg_1 ) & t_FunctionalElement ( V_trg_2 ) ) ) => ( ( r_element_FunctionalInterface ( V_src , V_trg_1 ) & r_element_FunctionalInterface ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . |
30 | fof ( upperMultiplicity_to_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_InformationLink_class ( Var_src ) & ( t_FunctionalInput_class ( Var_trg_1 ) & t_FunctionalInput_class ( Var_trg_2 ) ) ) => ( ( rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . | 30 | fof ( upperMultiplicity_terminator_FunctionalData , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalData ( V_src ) & ( t_FAMTerminator ( V_trg_1 ) & t_FAMTerminator ( V_trg_2 ) ) ) => ( ( r_terminator_FunctionalData ( V_src , V_trg_1 ) & r_terminator_FunctionalData ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . |
31 | fof ( upperMultiplicity_element_FunctionalInterface , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalInterface_class ( Var_src ) & ( t_FunctionalElement_class ( Var_trg_1 ) & t_FunctionalElement_class ( Var_trg_2 ) ) ) => ( ( rel_element_reference_FunctionalInterface ( Var_src , Var_trg_1 ) & rel_element_reference_FunctionalInterface ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . | 31 | fof ( upperMultiplicity_interface_FunctionalData , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalData ( V_src ) & ( t_FunctionalInterface ( V_trg_1 ) & t_FunctionalInterface ( V_trg_2 ) ) ) => ( ( r_interface_FunctionalData ( V_src , V_trg_1 ) & r_interface_FunctionalData ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . |
32 | fof ( upperMultiplicity_terminator_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalData_class ( Var_src ) & ( t_FAMTerminator_class ( Var_trg_1 ) & t_FAMTerminator_class ( Var_trg_2 ) ) ) => ( ( rel_terminator_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_terminator_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . | 32 | fof ( oppositeReference_interface_FunctionalElement , axiom , ! [ V_src , V_trg ] : ( ( t_FunctionalElement ( V_src ) & t_FunctionalInterface ( V_trg ) ) => ( r_interface_FunctionalElement ( V_src , V_trg ) <=> r_element_FunctionalInterface ( V_trg , V_src ) ) ) ) . |
33 | fof ( upperMultiplicity_interface_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalData_class ( Var_src ) & ( t_FunctionalInterface_class ( Var_trg_1 ) & t_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . | 33 | fof ( oppositeReference_parent_FunctionalElement , axiom , ! [ V_src , V_trg ] : ( ( t_FunctionalElement ( V_src ) & t_Function ( V_trg ) ) => ( r_parent_FunctionalElement ( V_src , V_trg ) <=> r_subElements_Function ( V_trg , V_src ) ) ) ) . |
34 | fof ( oppositeReference_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( t_FunctionalElement_class ( Var_src ) & t_FunctionalInterface_class ( Var_trg ) ) => ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_element_reference_FunctionalInterface ( Var_trg , Var_src ) ) ) ) . | 34 | fof ( oppositeReference_data_FAMTerminator , axiom , ! [ V_src , V_trg ] : ( ( t_FAMTerminator ( V_src ) & t_FunctionalData ( V_trg ) ) => ( r_data_FAMTerminator ( V_src , V_trg ) <=> r_terminator_FunctionalData ( V_trg , V_src ) ) ) ) . |
35 | fof ( oppositeReference_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( t_FunctionalElement_class ( Var_src ) & t_Function_class ( Var_trg ) ) => ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_subElements_reference_Function ( Var_trg , Var_src ) ) ) ) . | 35 | fof ( oppositeReference_from_InformationLink , axiom , ! [ V_src , V_trg ] : ( ( t_InformationLink ( V_src ) & t_FunctionalOutput ( V_trg ) ) => ( r_from_InformationLink ( V_src , V_trg ) <=> r_outgoingLinks_FunctionalOutput ( V_trg , V_src ) ) ) ) . |
36 | fof ( oppositeReference_data_FAMTerminator , axiom , ! [ Var_src , Var_trg ] : ( ( t_FAMTerminator_class ( Var_src ) & t_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FAMTerminator ( Var_src , Var_trg ) <=> rel_terminator_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) . | 36 | fof ( oppositeReference_to_InformationLink , axiom , ! [ V_src , V_trg ] : ( ( t_InformationLink ( V_src ) & t_FunctionalInput ( V_trg ) ) => ( r_to_InformationLink ( V_src , V_trg ) <=> r_IncomingLinks_FunctionalInput ( V_trg , V_src ) ) ) ) . |
37 | fof ( oppositeReference_from_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( t_InformationLink_class ( Var_src ) & t_FunctionalOutput_class ( Var_trg ) ) => ( rel_from_reference_InformationLink ( Var_src , Var_trg ) <=> rel_outgoingLinks_reference_FunctionalOutput ( Var_trg , Var_src ) ) ) ) . | 37 | fof ( oppositeReference_data_FunctionalInterface , axiom , ! [ V_src , V_trg ] : ( ( t_FunctionalInterface ( V_src ) & t_FunctionalData ( V_trg ) ) => ( r_data_FunctionalInterface ( V_src , V_trg ) <=> r_interface_FunctionalData ( V_trg , V_src ) ) ) ) . |
38 | fof ( oppositeReference_to_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( t_InformationLink_class ( Var_src ) & t_FunctionalInput_class ( Var_trg ) ) => ( rel_to_reference_InformationLink ( Var_src , Var_trg ) <=> rel_IncomingLinks_reference_FunctionalInput ( Var_trg , Var_src ) ) ) ) . | 38 | fof ( lowerMultiplicity_type_Function , axiom , ! [ V_src ] : ( t_Function ( V_src ) => ? [ V_trg_1 ] : ( t_FunctionType ( V_trg_1 ) & r_type_Function ( V_src , V_trg_1 ) ) ) ) . |
39 | fof ( oppositeReference_data_FunctionalInterface , axiom , ! [ Var_src , Var_trg ] : ( ( t_FunctionalInterface_class ( Var_src ) & t_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FunctionalInterface ( Var_src , Var_trg ) <=> rel_interface_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) . | 39 | fof ( upperMultiplicity_type_Function , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_Function ( V_src ) & ( t_FunctionType ( V_trg_1 ) & t_FunctionType ( V_trg_2 ) ) ) => ( ( r_type_Function ( V_src , V_trg_1 ) & r_type_Function ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . |
40 | fof ( lowerMultiplicity_type_Function , axiom , ! [ Var_src ] : ( t_Function_class ( Var_src ) => ? [ Var_trg_1 ] : ( t_FunctionType_enum ( Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_1 ) ) ) ) . | ||
41 | fof ( upperMultiplicity_type_Function , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_Function_class ( Var_src ) & ( t_FunctionType_enum ( Var_trg_1 ) & t_FunctionType_enum ( Var_trg_2 ) ) ) => ( ( rel_type_attribute_Function ( Var_src , Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . | ||
42 | fof ( errorpattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ Var_p0 , Var_p1 ] : ( ( t_FAMTerminator_class ( Var_p0 ) & t_InformationLink_class ( Var_p1 ) ) => ~ rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( Var_p0 , Var_p1 ) ) ) . | ||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend index 8a60f486..20ad6119 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend | |||
@@ -39,8 +39,9 @@ class GeneralTest { | |||
39 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic | 39 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic |
40 | 40 | ||
41 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) | 41 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) |
42 | var problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output | 42 | var problem = modelGenerationProblem.output |
43 | problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output | 43 | // problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output |
44 | // problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output | ||
44 | 45 | ||
45 | workspace.writeModel(problem, "Fam.logicproblem") | 46 | workspace.writeModel(problem, "Fam.logicproblem") |
46 | 47 | ||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin index 2cd47088..6d33db67 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin index b4d3bda8..9f3d423f 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java index 2401e710..5e4df399 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java | |||
@@ -15,7 +15,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | |||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | 15 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; |
16 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; | 16 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; |
17 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; | 17 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; |
18 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration; | ||
19 | import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor; | 18 | import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor; |
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic; | 19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic; |
21 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; | 20 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; |
@@ -59,9 +58,7 @@ public class GeneralTest { | |||
59 | final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); | 58 | final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); |
60 | Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); | 59 | Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); |
61 | final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); | 60 | final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); |
62 | LogicProblem problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput(); | 61 | LogicProblem problem = modelGenerationProblem.getOutput(); |
63 | Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration(); | ||
64 | problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, _viatra2LogicConfiguration).getOutput(); | ||
65 | workspace.writeModel(problem, "Fam.logicproblem"); | 62 | workspace.writeModel(problem, "Fam.logicproblem"); |
66 | InputOutput.<String>println("Problem created"); | 63 | InputOutput.<String>println("Problem created"); |
67 | LogicResult solution = null; | 64 | LogicResult solution = null; |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin index ece511d9..4212d100 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin index a7cea425..d00afe64 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin | |||
Binary files differ | |||