From f1245cf2bf0447566dd69798d20d7ae6b64b6a19 Mon Sep 17 00:00:00 2001
From: ArenBabikian <aren.babikian@mail.mcgill.ca>
Date: Wed, 6 Mar 2019 17:46:15 -0500
Subject: Fix Enum handling for Paradox Integration

---
 .../Logic2VampireLanguageMapper_TypeMapper.xtend      |  14 +++++++++++++-
 .../.Logic2VampireLanguageMapper_TypeMapper.xtendbin  | Bin 9388 -> 9592 bytes
 .../Logic2VampireLanguageMapper_TypeMapper.java       |  13 ++++++++++++-
 3 files changed, 25 insertions(+), 2 deletions(-)

(limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner')

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
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_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();
-- 
cgit v1.2.3-54-g00ecf