From ce5aafc07151275363735013c261cacf3d7b6431 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Wed, 11 Sep 2019 15:34:03 -0400 Subject: VAMPIRE: fix model generation --- .../reasoner/builder/Logic2VampireLanguageMapper.xtend | 6 +++++- .../builder/Logic2VampireLanguageMapper_TypeMapper.xtend | 13 +++++++++---- .../reasoner/builder/VampireModelInterpretation.xtend | 11 ++++++++--- 3 files changed, 22 insertions(+), 8 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner') 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 { def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred, List parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, Map variables) { - typeMapper.transformReference(referred, trace) + val name = referred.lookup(trace.definedElement2String) + return createVLSConstant => [ + it.name = name + ] +// typeMapper.transformReference(referred, trace) } 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 { val cstTerm = createVLSFunctionAsTerm => [ it.functor = "eo" + num ] - if (isNotEnum) { +// if (isNotEnum) { trace.definedElement2String.put(type.elements.get(index),cstTerm.functor) - } +// } val cst = support.toConstant(cstTerm) trace.uniqueInstances.add(cst) @@ -249,8 +249,13 @@ class Logic2VampireLanguageMapper_TypeMapper { } def protected transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) { - createVLSDoubleQuote => [ - it.value = "\"a" + referred.name + "\"" + +// createVLSDoubleQuote => [ +// it.value = "\"a" + referred.name + "\"" +// ] + + createVLSConstant => [ + it.name = referred.name ] } 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 { return declaration.lookup(this.type2DefinedElement) } - def private dispatch getElementsDispatch(TypeDefinition declaration) { return declaration.elements } + def private dispatch getElementsDispatch(TypeDefinition declaration) { + println("~~" + declaration) + println(declaration.elements) + println() + return declaration.elements + } override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { throw new UnsupportedOperationException("TODO: auto-generated method stub") @@ -260,12 +265,12 @@ class VampireModelInterpretation implements LogicModelInterpretation { for (real : realRelations) { if (real.contains(node1) && real.contains(node2)) { println(" true") - TimeUnit.SECONDS.sleep(1) + TimeUnit.MILLISECONDS.sleep(10) return true } } println(" false") - TimeUnit.SECONDS.sleep(1) + TimeUnit.MILLISECONDS.sleep(10) return false } -- cgit v1.2.3-54-g00ecf