VAMPIRE : initial model handling almost done. only typeScope remains #40

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

@@ -78,17 +78,17 @@ class Logic2VampireLanguageMapper {
 		if (!problem.types.isEmpty) {
 			typeMapper.transformTypes(problem.types, problem.elements, this, trace)
 		}
-
-		// SCOPE MAPPER
-		scopeMapper.transformScope(config, trace)
-
+
 		// RELATION MAPPER
 		trace.relationDefinitions = problem.collectRelationDefinitions
 		problem.relations.forEach[this.relationMapper.transformRelation(it, trace)]
 
 		// CONTAINMENT MAPPER
 		containmentMapper.transformContainment(config,problem.containmentHierarchies, trace)
 
+		// SCOPE MAPPER
+		scopeMapper.transformScope(problem.types, config, trace)
+
 		// CONSTANT MAPPER
 		// only transforms definitions
 		trace.constantDefinitions = problem.collectConstantDefinitions

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

@@ -31,6 +31,7 @@ class Logic2VampireLanguageMapperTrace {
 	public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace
 
 	public var Map<DefinedElement, String> definedElement2String = new HashMap
+	public var topLvlElementIsInInitialModel = null
 
 	public val Map<Type, VLSFunction> type2Predicate = new HashMap;
 	public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap

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

@@ -15,6 +15,7 @@ import java.util.Map
 
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl
 
 class Logic2VampireLanguageMapper_ContainmentMapper {
 	val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
@@ -36,7 +37,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
 		val containmentListCopy = hierarchy.typesOrderedInHierarchy
 		val relationsList = hierarchy.containmentRelations
 		val toRemove = newArrayList
-		
+
 		// STEP 1
 		// Find root element
 		for (l : relationsList) {
@@ -48,7 +49,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
 				containmentListCopy.remove(c)
 			}
 		}
-		
+
 //		OLD
 //		for (c : containmentListCopy) {
 //			if(c.isIsAbstract) {
@@ -58,42 +59,43 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
 		// 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))
-
 		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
+			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") ) {
+		var listToCheck = newArrayList(topTermVar)
+		listToCheck.addAll(topTermVar.subtypes)
+		for (c : listToCheck) {
+			if (c.class == typeof(TypeDefinitionImpl)) {
 
-				for (d : (c as TypeDefinition).elements) {
-				if (trace.definedElement2String.containsKey(d)) {
-					topLvlIsInInitModel = true
-					topLvlString = d.lookup(trace.definedElement2String)
+				if((c as TypeDefinition).elements.length >1) {
+					throw new IllegalArgumentException("You cannot have multiple top-level elements in your initial model")
+				}
+
+				for (d : (c as TypeDefinition).elements) {
+					if (trace.definedElement2String.containsKey(d)) {
+						topLvlIsInInitModel = true
+						topLvlString = d.lookup(trace.definedElement2String)
+					}
 				}
 			}
-
-			}
-
-
+
 		}
+
+		trace.topLvlElementIsInInitialModel = topLvlIsInInitModel
 		val topInIM = topLvlIsInInitModel
 		val topStr = topLvlString
-		print(topInIM)
-		print(topStr)
-
+
 		val contTop = createVLSFofFormula => [
 			it.name = support.toIDMultiple("containment_topLevel", topName)
 			it.fofRole = "axiom"
@@ -105,7 +107,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
 					it.right = createVLSEquality => [
 						it.left = support.duplicate(variable)
 						it.right = createVLSConstant => [
-							it.name = if (topInIM) topStr else "o1"
+							it.name = if(topInIM) topStr else "o1"
 						]
 					]
 				]
@@ -119,8 +121,8 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
 		]
 		trace.specification.formulas += contTop
 
-		// STEP 2
-		// for each edge, if the pointedTo element exists,the edge must exist also
+// STEP 2
+// for each edge, if the pointedTo element exists,the edge must exist also
 		val varA = createVLSVariable => [it.name = "A"]
 		val varB = createVLSVariable => [it.name = "B"]
 		val varC = createVLSVariable => [it.name = "C"]
@@ -207,23 +209,22 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
 		// STEP 4
 		// Ensure that there are no cycles in the hierarchy (maybe same as for step3?)
 		// Attempt 1: all possibilities, even the impossible one, based on MM constraints, are listed
-
-
 		val variables = newArrayList
 		val disjunctionList = newArrayList
 		val conjunctionList = newArrayList
 		for (var i = 1; i <= config.contCycleLevel; i++) {
 			val ind = i
-			variables.add(createVLSVariable => [it.name = ("V"+Integer.toString(ind))])
-			for ( var j = 0; j < i;j++){
+			variables.add(createVLSVariable => [it.name = ("V" + Integer.toString(ind))])
+			for (var j = 0; j < i; j++) {
 				for (l : relationsList) {
-					val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), newArrayList(variables.get(j), variables.get((j+1)%i)))
+					val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate),
+						newArrayList(variables.get(j), variables.get((j + 1) % i)))
 					disjunctionList.add(rel)
 				}
 				conjunctionList.add(support.unfoldOr(disjunctionList))
 				disjunctionList.clear
 			}
-			
+
 			val contCycleForm = createVLSFofFormula => [
 				it.name = support.toIDMultiple("containment_noCycle", Integer.toString(ind))
 				it.fofRole = "axiom"

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

@@ -5,8 +5,10 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
 import java.util.ArrayList
 import java.util.HashMap
+import java.util.List
 import java.util.Map
 
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
@@ -21,7 +23,7 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 		this.base = base
 	}
 
-	def dispatch public void transformScope(VampireSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) {
+	def dispatch public void transformScope(List<Type> types, VampireSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) {
 		val ABSOLUTE_MIN = 0
 		val ABSOLUTE_MAX = Integer.MAX_VALUE
 
@@ -31,8 +33,22 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 		// 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
+		//Number of defined non-abstract elements that are not enum elements
+		//Equals the number of elements in te initial model
+		var elemsInIM = trace.definedElement2String.size
+//		var elemsInIM = 0
+//		
+//		for(t : types.filter(TypeDefinition).filter[!isIsAbstract]) {
+//			val len = t.name.length
+//			val isNotEnum = !t.name.substring(len-4, len).equals("enum")
+//			if (isNotEnum) {
+//				elemsInIM += 1
+//			}
+//		}
+
+		//TODO handle errors related to GLOBAL_MIN/MAX < 0
+		val GLOBAL_MIN = config.typeScopes.minNewElements-elemsInIM
+		val GLOBAL_MAX = config.typeScopes.maxNewElements-elemsInIM
 
 		val localInstances = newArrayList
 
@@ -63,31 +79,61 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 
 		// Handling Minimum_Specific
 		var i = 1
+		if (trace.topLvlElementIsInInitialModel as Boolean){
+			i = 0
+		}
 		var minNum = -1
 		var Map<Type, Integer> startPoints = new HashMap
-		for (t : config.typeScopes.minNewElementsByType.keySet) {
-			minNum = t.lookup(config.typeScopes.minNewElementsByType)
+//		var inIM = false
+		for (tConfig : config.typeScopes.minNewElementsByType.keySet) {
+//			var numIniIntModel = 0
+//			for (elem : trace.definedElement2String.keySet) {
+//				println(elem.definedInType)
+//				for (tDefined : elem.definedInType) {
+//					inIM = support.dfsSubtypeCheck(tConfig, tDefined) || tConfig.equals(tDefined)
+//				}
+//				if (inIM) {
+//					numIniIntModel += 1
+//				}
+//				inIM = false
+//			}		
+
+			minNum = tConfig.lookup(config.typeScopes.minNewElementsByType)//-numIniIntModel
 			if (minNum != 0) {
 				getInstanceConstants(i + minNum, i, localInstances, trace, true, false)
-				startPoints.put(t, i)
+				startPoints.put(tConfig, i)
 				i += minNum
-				makeFofFormula(localInstances, trace, true, t)
+				makeFofFormula(localInstances, trace, true, tConfig)
 			}
 		}
 
 		// TODO: calc sum of mins, compare to current value of i
 		// Handling Maximum_Specific
-		for (t : config.typeScopes.maxNewElementsByType.keySet) {
-			var maxNum = t.lookup(config.typeScopes.maxNewElementsByType)
-			minNum = t.lookup(config.typeScopes.minNewElementsByType)
-			var startpoint = t.lookup(startPoints)
+		for (tConfig : config.typeScopes.maxNewElementsByType.keySet) {
+
+//			var numIniIntModel = 0
+//			for (elem : trace.definedElement2String.keySet) {
+//				println(elem.definedInType)
+//				for (tDefined : elem.definedInType) {
+//					inIM = support.dfsSubtypeCheck(tConfig, tDefined) || tConfig.equals(tDefined)
+//				}
+//				if (inIM) {
+//					numIniIntModel += 1
+//				}
+//				inIM = false
+//			}	
+
+			var maxNum = tConfig.lookup(config.typeScopes.maxNewElementsByType)//-numIniIntModel
+			minNum = tConfig.lookup(config.typeScopes.minNewElementsByType)//-numIniIntModel
+			var startpoint = tConfig.lookup(startPoints)
 			if (minNum != 0) {
 				getInstanceConstants(startpoint + minNum, startpoint, localInstances, trace, true, false)
 			}
+			//I do not understand the line below
 			if (maxNum != minNum) {
 				var instEndInd = Math.min(GLOBAL_MAX, i + maxNum - minNum)
 				getInstanceConstants(instEndInd, i, localInstances, trace, false, false)
-				makeFofFormula(localInstances, trace, false, t)
+				makeFofFormula(localInstances, trace, false, tConfig)
 			}
 		}
 

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

@@ -44,13 +44,31 @@ class Logic2VampireLanguageMapper_TypeMapper {
 			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)) {
+		// 2. Map each ENUM/InitialModelElement type definition to fof formula
+		//    In the case where , for example, a supertype that is abstract has a subtype of which an instance is in the initial model,
+		//    The logic problem will contain a TypeDefinition for the subtype as well as for the supertype
+		//    This defined elemtn for the supertype will be abstract, and we do not wish to associate a constant to it, or associate it with a type
+		//    Within our vampireproblem.tptp
+		for (type : types.filter(TypeDefinition).filter[!isIsAbstract]) {
+
+			//Detect if it is a defined element (from initial model)
+			//Otherwise it is an Enum
+
+			//val isNotEnum = type.supertypes.length == 1 && type.supertypes.get(0).isIsAbstract
+			//^does not work in cases where a defined type already has a supertype from within the MM
+
+//			var isNotEnumVar = !type.supertypes.isEmpty 
+//			if(isNotEnumVar) {
+//				for (sup : type.supertypes){
+//					type.name.contains(sup.name)
+//				}
+//			}
+//			
+//			val isNotEnum = isNotEnumVar
 
-			//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
+			//Another possibility is..
+			val len = type.name.length
+			val isNotEnum = !type.name.substring(len-4, len).equals("enum")
 
 			// Create a VLSFunction for each Enum Element
 			val List<VLSFunction> orElems = newArrayList

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

@@ -117,13 +117,13 @@ public TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformPro
     if (_not) {
       this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace);
     }
-    this.scopeMapper.transformScope(config, trace);
     trace.relationDefinitions = this.collectRelationDefinitions(problem);
     final Consumer<Relation> _function_3 = (Relation it) -> {
       this.relationMapper.transformRelation(it, trace);
     };
     problem.getRelations().forEach(_function_3);
     this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace);
+    this.scopeMapper.transformScope(problem.getTypes(), config, trace);
     trace.constantDefinitions = this.collectConstantDefinitions(problem);
     final Consumer<ConstantDefinition> _function_4 = (ConstantDefinition it) -> {
       this.constantMapper.transformConstantDefinitionSpecification(it, trace);

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

@@ -31,6 +31,8 @@ public class Logic2VampireLanguageMapperTrace {
 
   public Map<DefinedElement, String> definedElement2String = new HashMap<DefinedElement, String>();
 
+  public Object topLvlElementIsInInitialModel = null;
+
   public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>();
 
   public final Map<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>();