diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-09-11 15:34:03 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-09-11 15:34:03 -0400 |
commit | ce5aafc07151275363735013c261cacf3d7b6431 (patch) | |
tree | 96e13919940dba3d2cb5b81000579a5613615a73 /Solvers | |
parent | VAMPIRE: Implement wf constraint handling (diff) | |
download | VIATRA-Generator-ce5aafc07151275363735013c261cacf3d7b6431.tar.gz VIATRA-Generator-ce5aafc07151275363735013c261cacf3d7b6431.tar.zst VIATRA-Generator-ce5aafc07151275363735013c261cacf3d7b6431.zip |
VAMPIRE: fix model generation
Diffstat (limited to 'Solvers')
8 files changed, 34 insertions, 21 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 14926280..b617912d 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 | |||
@@ -265,7 +265,11 @@ class Logic2VampireLanguageMapper { | |||
265 | def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred, | 265 | def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred, |
266 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | 266 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, |
267 | Map<Variable, VLSVariable> variables) { | 267 | Map<Variable, VLSVariable> variables) { |
268 | typeMapper.transformReference(referred, trace) | 268 | val name = referred.lookup(trace.definedElement2String) |
269 | return createVLSConstant => [ | ||
270 | it.name = name | ||
271 | ] | ||
272 | // typeMapper.transformReference(referred, trace) | ||
269 | } | 273 | } |
270 | 274 | ||
271 | def dispatch protected VLSTerm transformSymbolicReference(ConstantDeclaration constant, | 275 | def dispatch protected VLSTerm transformSymbolicReference(ConstantDeclaration constant, |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend index d2a01e0e..38c99a89 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend | |||
@@ -138,9 +138,9 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
138 | val cstTerm = createVLSFunctionAsTerm => [ | 138 | val cstTerm = createVLSFunctionAsTerm => [ |
139 | it.functor = "eo" + num | 139 | it.functor = "eo" + num |
140 | ] | 140 | ] |
141 | if (isNotEnum) { | 141 | // if (isNotEnum) { |
142 | trace.definedElement2String.put(type.elements.get(index),cstTerm.functor) | 142 | trace.definedElement2String.put(type.elements.get(index),cstTerm.functor) |
143 | } | 143 | // } |
144 | 144 | ||
145 | val cst = support.toConstant(cstTerm) | 145 | val cst = support.toConstant(cstTerm) |
146 | trace.uniqueInstances.add(cst) | 146 | trace.uniqueInstances.add(cst) |
@@ -249,8 +249,13 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
249 | } | 249 | } |
250 | 250 | ||
251 | def protected transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) { | 251 | def protected transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) { |
252 | createVLSDoubleQuote => [ | 252 | |
253 | it.value = "\"a" + referred.name + "\"" | 253 | // createVLSDoubleQuote => [ |
254 | // it.value = "\"a" + referred.name + "\"" | ||
255 | // ] | ||
256 | |||
257 | createVLSConstant => [ | ||
258 | it.name = referred.name | ||
254 | ] | 259 | ] |
255 | } | 260 | } |
256 | 261 | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend index ef77b6ca..9eb47f41 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend | |||
@@ -246,7 +246,12 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
246 | return declaration.lookup(this.type2DefinedElement) | 246 | return declaration.lookup(this.type2DefinedElement) |
247 | } | 247 | } |
248 | 248 | ||
249 | def private dispatch getElementsDispatch(TypeDefinition declaration) { return declaration.elements } | 249 | def private dispatch getElementsDispatch(TypeDefinition declaration) { |
250 | println("~~" + declaration) | ||
251 | println(declaration.elements) | ||
252 | println() | ||
253 | return declaration.elements | ||
254 | } | ||
250 | 255 | ||
251 | override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { | 256 | override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { |
252 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 257 | throw new UnsupportedOperationException("TODO: auto-generated method stub") |
@@ -260,12 +265,12 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
260 | for (real : realRelations) { | 265 | for (real : realRelations) { |
261 | if (real.contains(node1) && real.contains(node2)) { | 266 | if (real.contains(node1) && real.contains(node2)) { |
262 | println(" true") | 267 | println(" true") |
263 | TimeUnit.SECONDS.sleep(1) | 268 | TimeUnit.MILLISECONDS.sleep(10) |
264 | return true | 269 | return true |
265 | } | 270 | } |
266 | } | 271 | } |
267 | println(" false") | 272 | println(" false") |
268 | TimeUnit.SECONDS.sleep(1) | 273 | TimeUnit.MILLISECONDS.sleep(10) |
269 | return false | 274 | return false |
270 | } | 275 | } |
271 | 276 | ||
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 b1e3b95d..8ce1beed 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/.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 803b5fed..f7259e75 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_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 7e8b1703..116b2d15 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.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java index f8a65187..c8961c6e 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 | |||
@@ -283,7 +283,12 @@ public class Logic2VampireLanguageMapper { | |||
283 | } | 283 | } |
284 | 284 | ||
285 | protected VLSTerm _transformSymbolicReference(final DefinedElement referred, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 285 | protected VLSTerm _transformSymbolicReference(final DefinedElement referred, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { |
286 | return this.typeMapper.transformReference(referred, trace); | 286 | final String name = CollectionsUtil.<DefinedElement, String>lookup(referred, trace.definedElement2String); |
287 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
288 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { | ||
289 | it.setName(name); | ||
290 | }; | ||
291 | return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function); | ||
287 | } | 292 | } |
288 | 293 | ||
289 | protected VLSTerm _transformSymbolicReference(final ConstantDeclaration constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 294 | protected VLSTerm _transformSymbolicReference(final ConstantDeclaration constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java index c8888eb0..72fea6d3 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java | |||
@@ -5,7 +5,6 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage | |||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; |
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; |
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | 9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | 10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; |
@@ -177,9 +176,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
177 | it.setFunctor(("eo" + Integer.valueOf(num))); | 176 | it.setFunctor(("eo" + Integer.valueOf(num))); |
178 | }; | 177 | }; |
179 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_3); | 178 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_3); |
180 | if (isNotEnum) { | 179 | trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor()); |
181 | trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor()); | ||
182 | } | ||
183 | final VLSConstant cst = this.support.toConstant(cstTerm); | 180 | final VLSConstant cst = this.support.toConstant(cstTerm); |
184 | trace.uniqueInstances.add(cst); | 181 | trace.uniqueInstances.add(cst); |
185 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 182 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
@@ -328,15 +325,12 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
328 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | 325 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); |
329 | } | 326 | } |
330 | 327 | ||
331 | protected VLSDoubleQuote transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) { | 328 | protected VLSConstant transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) { |
332 | VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote(); | 329 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); |
333 | final Procedure1<VLSDoubleQuote> _function = (VLSDoubleQuote it) -> { | 330 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { |
334 | String _name = referred.getName(); | 331 | it.setName(referred.getName()); |
335 | String _plus = ("\"a" + _name); | ||
336 | String _plus_1 = (_plus + "\""); | ||
337 | it.setValue(_plus_1); | ||
338 | }; | 332 | }; |
339 | return ObjectExtensions.<VLSDoubleQuote>operator_doubleArrow(_createVLSDoubleQuote, _function); | 333 | return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function); |
340 | } | 334 | } |
341 | 335 | ||
342 | protected void getTypeInterpreter() { | 336 | protected void getTypeInterpreter() { |