Fix Enum handling for Paradox Integration

3 files changed, 25 insertions, 2 deletions

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<VLSFunction> enumScopeElems = newArrayList
+                        val List<VLSTerm> 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))
                         }
                         
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 e85b5240..8a6f30f9 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
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 f776371b..c101aa4c 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
@@ -111,7 +111,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
           final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1);

           EList<VLSFofFormula> _formulas = trace.specification.getFormulas();

           _formulas.add(res);

-          final List<VLSFunction> enumScopeElems = CollectionLiterals.<VLSFunction>newArrayList();

+          final List<VLSTerm> enumScopeElems = CollectionLiterals.<VLSTerm>newArrayList();

           for (int i = 0; (i < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); i++) {

             {

               final int num = (i + 1);

@@ -124,6 +124,17 @@ public class Logic2VampireLanguageMapper_TypeMapper {
               trace.uniqueInstances.add(cst);

               final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(i), trace.element2Predicate), cstTerm);

               enumScopeElems.add(fct);

+              for (int j = 0; (j < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); j++) {

+                if ((j != i)) {

+                  final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(j), trace.element2Predicate), cstTerm);

+                  VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();

+                  final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> {

+                    it.setOperand(op);

+                  };

+                  final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3);

+                  enumScopeElems.add(negFct);

+                }

+              }

             }

           }

           VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();