From f1245cf2bf0447566dd69798d20d7ae6b64b6a19 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Wed, 6 Mar 2019 17:46:15 -0500 Subject: Fix Enum handling for Paradox Integration --- .../builder/Logic2VampireLanguageMapper_TypeMapper.xtend | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill') 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 f2a7b3f2..ee6365dd 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 @@ -90,7 +90,7 @@ class Logic2VampireLanguageMapper_TypeMapper { trace.specification.formulas += res // Create objects for the enum elements - val List enumScopeElems = newArrayList + val List enumScopeElems = newArrayList for (var i = 0; i < type.elements.length; i++) { val num = i + 1 val cstTerm = createVLSFunctionAsTerm => [ @@ -100,6 +100,18 @@ class Logic2VampireLanguageMapper_TypeMapper { trace.uniqueInstances.add(cst) val fct = support.duplicate(type.elements.get(i).lookup(trace.element2Predicate), cstTerm) enumScopeElems.add(fct) + + //For paradox Only + for (var j = 0; j < type.elements.length; j++) { + if(j != i) { + val op = support.duplicate(type.elements.get(j).lookup(trace.element2Predicate), cstTerm) + val negFct = createVLSUnaryNegation => [ + it.operand = op + ] + enumScopeElems.add(negFct) + } + } + //End Paradox // enumScopeElems.add(support.topLevelTypeFunc(cstTerm)) } -- cgit v1.2.3-54-g00ecf