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 --- .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 17989 -> 18099 bytes ...Logic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 10676 -> 10717 bytes ....Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 11170 -> 11037 bytes .../builder/Logic2VampireLanguageMapper.java | 7 ++++++- .../Logic2VampireLanguageMapper_TypeMapper.java | 18 ++++++------------ 5 files changed, 12 insertions(+), 13 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca') 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin 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 { } protected VLSTerm _transformSymbolicReference(final DefinedElement referred, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - return this.typeMapper.transformReference(referred, trace); + final String name = CollectionsUtil.lookup(referred, trace.definedElement2String); + VLSConstant _createVLSConstant = this.factory.createVLSConstant(); + final Procedure1 _function = (VLSConstant it) -> { + it.setName(name); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function); } protected VLSTerm _transformSymbolicReference(final ConstantDeclaration constant, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map 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 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; @@ -177,9 +176,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { it.setFunctor(("eo" + Integer.valueOf(num))); }; final VLSFunctionAsTerm cstTerm = ObjectExtensions.operator_doubleArrow(_createVLSFunctionAsTerm, _function_3); - if (isNotEnum) { - trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor()); - } + trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor()); final VLSConstant cst = this.support.toConstant(cstTerm); trace.uniqueInstances.add(cst); VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); @@ -328,15 +325,12 @@ public class Logic2VampireLanguageMapper_TypeMapper { throw new UnsupportedOperationException("TODO: auto-generated method stub"); } - protected VLSDoubleQuote transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) { - VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote(); - final Procedure1 _function = (VLSDoubleQuote it) -> { - String _name = referred.getName(); - String _plus = ("\"a" + _name); - String _plus_1 = (_plus + "\""); - it.setValue(_plus_1); + protected VLSConstant transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) { + VLSConstant _createVLSConstant = this.factory.createVLSConstant(); + final Procedure1 _function = (VLSConstant it) -> { + it.setName(referred.getName()); }; - return ObjectExtensions.operator_doubleArrow(_createVLSDoubleQuote, _function); + return ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function); } protected void getTypeInterpreter() { -- cgit v1.2.3-54-g00ecf