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 --- .../Logic2VampireLanguageMapper_TypeMapper.java | 18 ++++++------------ 1 file changed, 6 insertions(+), 12 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java') 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