1 files changed, 71 insertions, 28 deletions

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 b8d74f36..ec759ebf 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
@@ -3,8 +3,10 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;

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

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

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

+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.VLSFunction;

@@ -18,7 +20,6 @@ import com.google.common.base.Objects;
 import com.google.common.collect.Iterables;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;

-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition;

 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage;

 import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;

@@ -56,6 +57,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
         it.setName("A");

       };

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

+      int globalCounter = 0;

       for (final Type type : types) {

         {

           VLSFunction _createVLSFunction = this.factory.createVLSFunction();

@@ -92,7 +94,31 @@ public class Logic2VampireLanguageMapper_TypeMapper {
               };

               final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);

               trace.element2Predicate.put(e, enumElemPred);

-              orElems.add(enumElemPred);

+            }

+          }

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

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

+          EList<DefinedElement> _elements_1 = type_1.getElements();

+          for (final DefinedElement t1 : _elements_1) {

+            {

+              EList<DefinedElement> _elements_2 = type_1.getElements();

+              for (final DefinedElement t2 : _elements_2) {

+                boolean _equals = Objects.equal(t1, t2);

+                if (_equals) {

+                  final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable);

+                  possibleNots.add(fct);

+                } else {

+                  final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable);

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

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

+                    it.setOperand(op);

+                  };

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

+                  possibleNots.add(negFct);

+                }

+              }

+              typeDefs.add(this.support.unfoldAnd(possibleNots));

+              possibleNots.clear();

             }

           }

           VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

@@ -107,7 +133,13 @@ public class Logic2VampireLanguageMapper_TypeMapper {
               VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

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

                 it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate));

-                it_2.setRight(this.support.unfoldOr(orElems));

+                VLSAnd _createVLSAnd = this.factory.createVLSAnd();

+                final Procedure1<VLSAnd> _function_4 = (VLSAnd it_3) -> {

+                  it_3.setLeft(this.support.topLevelTypeFunc(variable));

+                  it_3.setRight(this.support.unfoldOr(typeDefs));

+                };

+                VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_4);

+                it_2.setRight(_doubleArrow);

               };

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

               it_1.setOperand(_doubleArrow);

@@ -118,8 +150,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<VLSTerm> enumScopeElems = CollectionLiterals.<VLSTerm>newArrayList();

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

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

             {

               final int num = (i + 1);

               VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm();

@@ -129,38 +160,50 @@ public class Logic2VampireLanguageMapper_TypeMapper {
               final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2);

               final VLSConstant cst = this.support.toConstant(cstTerm);

               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 int index = i;

+              VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

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

+                it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0], 

+                  type_1.getElements().get(index).getName().split(" ")[0]));

+                it.setFofRole("axiom");

+                VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

+                final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> {

+                  EList<VLSVariable> _variables = it_1.getVariables();

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

+                  _variables.add(_duplicate);

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

+                  final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> {

+                    VLSEquality _createVLSEquality = this.factory.createVLSEquality();

+                    final Procedure1<VLSEquality> _function_6 = (VLSEquality it_3) -> {

+                      it_3.setLeft(this.support.duplicate(variable));

+                      it_3.setRight(this.support.duplicate(this.support.toConstant(cstTerm)));

+                    };

+                    VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_6);

+                    it_2.setLeft(_doubleArrow);

+                    it_2.setRight(this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(index), trace.element2Predicate), variable));

                   };

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

-                  enumScopeElems.add(negFct);

-                }

-              }

+                  VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_5);

+                  it_1.setOperand(_doubleArrow);

+                };

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

+                it.setFofFormula(_doubleArrow);

+              };

+              final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_3);

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

+              _formulas_1.add(enumScope);

             }

           }

-          VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

-          final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> {

-            it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0]));

-            it.setFofRole("axiom");

-            it.setFofFormula(this.support.unfoldAnd(enumScopeElems));

-          };

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

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

-          _formulas_1.add(enumScope);

+          int _globalCounter = globalCounter;

+          int _size = type_1.getElements().size();

+          globalCounter = (_globalCounter + _size);

         }

       }

       final Function1<Type, Boolean> _function_1 = (Type it) -> {

         boolean _isIsAbstract = it.isIsAbstract();

         return Boolean.valueOf((!_isIsAbstract));

       };

-      Iterable<TypeDeclaration> _filter_1 = Iterables.<TypeDeclaration>filter(IterableExtensions.<Type>filter(types, _function_1), TypeDeclaration.class);

-      for (final TypeDeclaration t1 : _filter_1) {

+      Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1);

+      for (final Type t1 : _filter_1) {

         {

           for (final Type t2 : types) {

             if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) {