Fix Enum handling for Paradox Integration

4 files changed, 26 insertions, 3 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();

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
index c492b66d..a3b9c865 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
@@ -1,6 +1,6 @@
 % This is an initial Test Comment

 fof ( typeDef_FunctionType , axiom , ! [ A ] : ( t_FunctionType ( A ) <=> ( e_Root_FunctionType ( A ) | ( e_Intermediate_FunctionType ( A ) | e_Leaf_FunctionType ( A ) ) ) ) ) .

-fof ( enumScope_FunctionType , axiom , e_Root_FunctionType ( eo1 ) & ( e_Intermediate_FunctionType ( eo2 ) & e_Leaf_FunctionType ( eo3 ) ) ) .

+fof ( enumScope_FunctionType , axiom , e_Root_FunctionType ( eo1 ) & ( ~ e_Intermediate_FunctionType ( eo1 ) & ( ~ e_Leaf_FunctionType ( eo1 ) & ( e_Intermediate_FunctionType ( eo2 ) & ( ~ e_Root_FunctionType ( eo2 ) & ( ~ e_Leaf_FunctionType ( eo2 ) & ( e_Leaf_FunctionType ( eo3 ) & ( ~ e_Root_FunctionType ( eo3 ) & ~ e_Intermediate_FunctionType ( eo3 ) ) ) ) ) ) ) ) ) .

 fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_FunctionalData ( A ) & ( t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ( t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ~ t_Function ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInput ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & t_Function ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .

 fof ( typeScope , axiom , ! [ A ] : ( ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | A = o5 ) ) ) ) => object ( A ) ) ) .

 fof ( typeUniqueness , axiom , eo1 != eo2 & ( eo1 != eo3 & ( eo2 != eo3 & ( eo1 != o1 & ( eo2 != o1 & ( eo3 != o1 & ( eo1 != o2 & ( eo2 != o2 & ( eo3 != o2 & ( o1 != o2 & ( eo1 != o3 & ( eo2 != o3 & ( eo3 != o3 & ( o1 != o3 & ( o2 != o3 & ( eo1 != o4 & ( eo2 != o4 & ( eo3 != o4 & ( o1 != o4 & ( o2 != o4 & ( o3 != o4 & ( eo1 != o5 & ( eo2 != o5 & ( eo3 != o5 & ( o1 != o5 & ( o2 != o5 & ( o3 != o5 & o4 != o5 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .