Implement Enum handling and study hierarchy handling

1 files changed, 13 insertions, 11 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
index 8967839d..15ba78c9 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
@@ -5,13 +5,14 @@ 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.VLSConstant;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality;

-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies;

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration;

-import java.util.List;

+import java.util.ArrayList;

 import org.eclipse.emf.common.util.EList;

 import org.eclipse.xtext.xbase.lib.CollectionLiterals;

 import org.eclipse.xtext.xbase.lib.Extension;

@@ -39,7 +40,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
       it.setName("A");

     };

     final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);

-    final List<VLSConstant> instances = CollectionLiterals.<VLSConstant>newArrayList();

+    final ArrayList<VLSTerm> localInstances = CollectionLiterals.<VLSTerm>newArrayList();

     for (int i = 0; (i < config.typeScopes.minNewElements); i++) {

       {

         final int num = (i + 1);

@@ -48,7 +49,8 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
           it.setName(("o" + Integer.valueOf(num)));

         };

         final VLSConstant cst = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_1);

-        instances.add(cst);

+        trace.uniqueInstances.add(cst);

+        localInstances.add(cst);

       }

     }

     if ((config.typeScopes.minNewElements != 0)) {

@@ -61,10 +63,9 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
           EList<VLSVariable> _variables = it_1.getVariables();

           VLSVariable _duplicate = this.support.duplicate(variable);

           _variables.add(_duplicate);

-          VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

-          final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> {

-            it_2.setLeft(this.support.topLevelTypeFunc());

-            final Function1<VLSConstant, VLSEquality> _function_4 = (VLSConstant i) -> {

+          VLSImplies _createVLSImplies = this.factory.createVLSImplies();

+          final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> {

+            final Function1<VLSTerm, VLSEquality> _function_4 = (VLSTerm i) -> {

               VLSEquality _createVLSEquality = this.factory.createVLSEquality();

               final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> {

                 VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();

@@ -77,9 +78,10 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
               };

               return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5);

             };

-            it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSConstant, VLSEquality>map(instances, _function_4)));

+            it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(localInstances, _function_4)));

+            it_2.setRight(this.support.topLevelTypeFunc());

           };

-          VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3);

+          VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3);

           it_1.setOperand(_doubleArrow);

         };

         VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2);

@@ -92,7 +94,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
       final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> {

         it.setName("typeUniqueness");

         it.setFofRole("axiom");

-        it.setFofFormula(this.support.establishUniqueness(instances));

+        it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances));

       };

       final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_2);

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