VAMPIRE: add to #40. I am tired

Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend

@@ -30,6 +30,8 @@ class Logic2VampireLanguageMapperTrace {
 	//Necessary containers
 	public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace
 
+	public var Map<DefinedElement, String> definedElement2String = new HashMap
+
 	public val Map<Type, VLSFunction> type2Predicate = new HashMap;
 	public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap
 	public val Map<Type, VLSTerm> type2PossibleNot = new HashMap

Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend

@@ -14,10 +14,11 @@ import java.util.List
 import java.util.Map
 
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
 
 class Logic2VampireLanguageMapper_ContainmentMapper {
-	private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
-	private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
+	val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
+	val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
 	val Logic2VampireLanguageMapper base
 	private val VLSVariable variable = createVLSVariable => [it.name = "A"]
 
@@ -34,6 +35,8 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
 
 		val containmentListCopy = hierarchy.typesOrderedInHierarchy
 		val relationsList = hierarchy.containmentRelations
+		val toRemove = newArrayList
+
 		// STEP 1
 		// Find root element
 		for (l : relationsList) {
@@ -46,16 +49,51 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
 			}
 		}
 
-		for (c : containmentListCopy) {
-			if(c.isIsAbstract) {
-				containmentListCopy.remove(c)
-			}
-		}
-
+//		OLD
+//		for (c : containmentListCopy) {
+//			if(c.isIsAbstract) {
+//				toRemove.add(c)
+//			}
+//		}
 		// State that there must exist 1 and only 1 root element
-		val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString
-		val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate))
+//		val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString
+//		val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate))
 
+		var topTermVar = containmentListCopy.get(0)
+		for (l : relationsList) {
+			var pointingFrom = (l.parameters.get(0) as ComplexTypeReference).referred as Type
+			if(containmentListCopy.contains(pointingFrom)) {
+				//The correct topTerm will be identified
+				topTermVar = pointingFrom
+			}
+		}
+
+		val topName = topTermVar.lookup(trace.type2Predicate).constant.toString
+		val topTerm = support.duplicate(topTermVar.lookup(trace.type2Predicate))
+
+
+
+		var topLvlIsInInitModel = false
+		var topLvlString = ""
+		for ( c : topTermVar.subtypes) {
+			if (c.class.simpleName.equals("TypeDefinitionImpl") ) {
+
+				for (d : (c as TypeDefinition).elements) {
+				if (trace.definedElement2String.containsKey(d)) {
+					topLvlIsInInitModel = true
+					topLvlString = d.lookup(trace.definedElement2String)
+				}
+			}
+
+			}
+
+
+		}
+		val topInIM = topLvlIsInInitModel
+		val topStr = topLvlString
+		print(topInIM)
+		print(topStr)
+
 		val contTop = createVLSFofFormula => [
 			it.name = support.toIDMultiple("containment_topLevel", topName)
 			it.fofRole = "axiom"
@@ -67,7 +105,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
 					it.right = createVLSEquality => [
 						it.left = support.duplicate(variable)
 						it.right = createVLSConstant => [
-							it.name = "o1"
+							it.name = if (topInIM) topStr else "o1"
 						]
 					]
 				]

Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend

@@ -30,6 +30,7 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 //		TODO HANDLE 
 		// 1. make a list of constants equaling the min number of specified objects
 		//These numbers do not include enums or initial model elements
+
 		val GLOBAL_MIN = config.typeScopes.minNewElements
 		val GLOBAL_MAX = config.typeScopes.maxNewElements
 

Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend

@@ -33,14 +33,24 @@ class Logic2VampireLanguageMapper_TypeMapper {
 		// 1. Each type (class) is a predicate with a single variable as input
 		for (type : types) {
 			val typePred = createVLSFunction => [
-				it.constant = support.toIDMultiple("t", type.name.split(" ").get(0))
+				if(type.name.split(" ").length == 3) {
+					it.constant = support.toIDMultiple("t", type.name.split(" ").get(0), type.name.split(" ").get(2))
+				}
+				else {
+					it.constant = support.toIDMultiple("t", type.name.split(" ").get(0))
+				}
 				it.terms += support.duplicate(variable)
 			]
 			trace.type2Predicate.put(type, typePred)
 		}
 
 		// 2. Map each ENUM type definition to fof formula
+		//    This also Handles initial Model stuff
 		for (type : types.filter(TypeDefinition)) {
+
+			//Detect if is an Enum
+			//Otherwise, it is a defined element (from initial model)
+			val isNotEnum = type.supertypes.length == 1 && type.supertypes.get(0).isIsAbstract
 
 			// Create a VLSFunction for each Enum Element
 			val List<VLSFunction> orElems = newArrayList
@@ -104,15 +114,20 @@ class Logic2VampireLanguageMapper_TypeMapper {
 			for (var i = globalCounter; i < globalCounter + type.elements.length; i++) {
 				// Create objects for the enum elements
 				val num = i + 1
+				val index = i-globalCounter
+
 				val cstTerm = createVLSFunctionAsTerm => [
 					it.functor = "eo" + num
 				]
+				if (isNotEnum) {
+					trace.definedElement2String.put(type.elements.get(index),cstTerm.functor)
+				}
+
 				val cst = support.toConstant(cstTerm)
 				trace.uniqueInstances.add(cst)
-
-				val index = i-globalCounter
+
 				val enumScope = createVLSFofFormula => [
-					it.name = support.toIDMultiple("enumScope", type.lookup(trace.type2Predicate).constant.toString,
+					it.name = support.toIDMultiple(if(isNotEnum) "definedType" else "enumScope", type.lookup(trace.type2Predicate).constant.toString,
 						type.elements.get(index).name.split(" ").get(0))
 					it.fofRole = "axiom"
 					it.fofFormula = createVLSUniversalQuantifier => [

Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java

@@ -29,6 +29,8 @@ public class Logic2VampireLanguageMapperTrace {
 
   public Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace;
 
+  public Map<DefinedElement, String> definedElement2String = new HashMap<DefinedElement, String>();
+
   public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>();
 
   public final Map<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>();

Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java

@@ -19,9 +19,11 @@
 import com.google.common.base.Objects;
 import com.google.common.collect.Iterables;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference;
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference;
 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy;
 import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;
@@ -34,6 +36,7 @@
 import org.eclipse.xtext.xbase.lib.CollectionLiterals;
 import org.eclipse.xtext.xbase.lib.Conversions;
 import org.eclipse.xtext.xbase.lib.Extension;
+import org.eclipse.xtext.xbase.lib.InputOutput;
 import org.eclipse.xtext.xbase.lib.ObjectExtensions;
 import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
 
@@ -58,6 +61,7 @@ public void transformContainment(final VampireSolverConfiguration config, final
     final ContainmentHierarchy hierarchy = hierarchies.get(0);
     final EList<Type> containmentListCopy = hierarchy.getTypesOrderedInHierarchy();
     final EList<Relation> relationsList = hierarchy.getContainmentRelations();
+    final ArrayList<Object> toRemove = CollectionLiterals.<Object>newArrayList();
     for (final Relation l : relationsList) {
       {
         TypeReference _get = l.getParameters().get(1);
@@ -71,14 +75,40 @@ public void transformContainment(final VampireSolverConfiguration config, final
         }
       }
     }
-    for (final Type c : containmentListCopy) {
-      boolean _isIsAbstract = c.isIsAbstract();
-      if (_isIsAbstract) {
-        containmentListCopy.remove(c);
+    Type topTermVar = containmentListCopy.get(0);
+    for (final Relation l_1 : relationsList) {
+      {
+        TypeReference _get = l_1.getParameters().get(0);
+        Type _referred = ((ComplexTypeReference) _get).getReferred();
+        Type pointingFrom = ((Type) _referred);
+        boolean _contains = containmentListCopy.contains(pointingFrom);
+        if (_contains) {
+          topTermVar = pointingFrom;
+        }
+      }
+    }
+    final String topName = CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate).getConstant().toString();
+    final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate));
+    boolean topLvlIsInInitModel = false;
+    String topLvlString = "";
+    EList<Type> _subtypes = topTermVar.getSubtypes();
+    for (final Type c : _subtypes) {
+      boolean _equals = c.getClass().getSimpleName().equals("TypeDefinitionImpl");
+      if (_equals) {
+        EList<DefinedElement> _elements = ((TypeDefinition) c).getElements();
+        for (final DefinedElement d : _elements) {
+          boolean _containsKey = trace.definedElement2String.containsKey(d);
+          if (_containsKey) {
+            topLvlIsInInitModel = true;
+            topLvlString = CollectionsUtil.<DefinedElement, String>lookup(d, trace.definedElement2String);
+          }
+        }
       }
     }
-    final String topName = CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate).getConstant().toString();
-    final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate));
+    final boolean topInIM = topLvlIsInInitModel;
+    final String topStr = topLvlString;
+    InputOutput.<Boolean>print(Boolean.valueOf(topInIM));
+    InputOutput.<String>print(topStr);
     VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
     final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {
       it.setName(this.support.toIDMultiple("containment_topLevel", topName));
@@ -96,7 +126,13 @@ public void transformContainment(final VampireSolverConfiguration config, final
             it_3.setLeft(this.support.duplicate(this.variable));
             VLSConstant _createVLSConstant = this.factory.createVLSConstant();
             final Procedure1<VLSConstant> _function_4 = (VLSConstant it_4) -> {
-              it_4.setName("o1");
+              String _xifexpression = null;
+              if (topInIM) {
+                _xifexpression = topStr;
+              } else {
+                _xifexpression = "o1";
+              }
+              it_4.setName(_xifexpression);
             };
             VLSConstant _doubleArrow = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_4);
             it_3.setRight(_doubleArrow);
@@ -130,16 +166,16 @@ public void transformContainment(final VampireSolverConfiguration config, final
     final VLSVariable varC = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_3);
     final ArrayList<VLSVariable> varList = CollectionLiterals.<VLSVariable>newArrayList(varB, varA);
     final Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap<VLSFunction, List<VLSFunction>>();
-    for (final Relation l_1 : relationsList) {
+    for (final Relation l_2 : relationsList) {
       {
-        final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate), varList);
-        TypeReference _get = l_1.getParameters().get(1);
+        final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_2), trace.rel2Predicate), varList);
+        TypeReference _get = l_2.getParameters().get(1);
         Type _referred = ((ComplexTypeReference) _get).getReferred();
         final Type toType = ((Type) _referred);
         final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate);
         this.addToMap(type2cont, toFunc, rel);
-        EList<Type> _subtypes = toType.getSubtypes();
-        for (final Type c_1 : _subtypes) {
+        EList<Type> _subtypes_1 = toType.getSubtypes();
+        for (final Type c_1 : _subtypes_1) {
           this.addToMap(type2cont, toFunc, rel);
         }
         VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
@@ -244,9 +280,9 @@ public void transformContainment(final VampireSolverConfiguration config, final
         variables.add(_doubleArrow);
         for (int j = 0; (j < i); j++) {
           {
-            for (final Relation l_2 : relationsList) {
+            for (final Relation l_3 : relationsList) {
               {
-                final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_2), trace.rel2Predicate), CollectionLiterals.<VLSVariable>newArrayList(variables.get(j), variables.get(((j + 1) % i))));
+                final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_3), trace.rel2Predicate), CollectionLiterals.<VLSVariable>newArrayList(variables.get(j), variables.get(((j + 1) % i))));
                 disjunctionList.add(rel);
               }
             }

Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java

@@ -62,7 +62,13 @@ protected boolean transformTypes(final Collection<Type> types, final Collection<
         {
           VLSFunction _createVLSFunction = this.factory.createVLSFunction();
           final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {
-            it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0]));
+            int _length = type.getName().split(" ").length;
+            boolean _equals = (_length == 3);
+            if (_equals) {
+              it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0], type.getName().split(" ")[2]));
+            } else {
+              it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0]));
+            }
             EList<VLSTerm> _terms = it.getTerms();
             VLSVariable _duplicate = this.support.duplicate(variable);
             _terms.add(_duplicate);
@@ -74,6 +80,7 @@ protected boolean transformTypes(final Collection<Type> types, final Collection<
       Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class);
       for (final TypeDefinition type_1 : _filter) {
         {
+          final boolean isNotEnum = ((((Object[])Conversions.unwrapArray(type_1.getSupertypes(), Object.class)).length == 1) && type_1.getSupertypes().get(0).isIsAbstract());
           final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList();
           EList<DefinedElement> _elements = type_1.getElements();
           for (final DefinedElement e : _elements) {
@@ -156,17 +163,26 @@ protected boolean transformTypes(final Collection<Type> types, final Collection<
           for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) {
             {
               final int num = (i + 1);
+              final int index = (i - globalCounter);
               VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm();
               final Procedure1<VLSFunctionAsTerm> _function_2 = (VLSFunctionAsTerm it) -> {
                 it.setFunctor(("eo" + Integer.valueOf(num)));
               };
               final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2);
+              if (isNotEnum) {
+                trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor());
+              }
               final VLSConstant cst = this.support.toConstant(cstTerm);
               trace.uniqueInstances.add(cst);
-              final int index = (i - globalCounter);
               VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
               final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> {
-                it.setName(this.support.toIDMultiple("enumScope", CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString(), 
+                String _xifexpression = null;
+                if (isNotEnum) {
+                  _xifexpression = "definedType";
+                } else {
+                  _xifexpression = "enumScope";
+                }
+                it.setName(this.support.toIDMultiple(_xifexpression, CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString(), 
                   type_1.getElements().get(index).getName().split(" ")[0]));
                 it.setFofRole("axiom");
                 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();