1 files changed, 51 insertions, 50 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
index ec841546..df3cfd82 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
@@ -23,18 +23,22 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                this.base = base
        }
-        def dispatch public void transformScope(List<Type> types, 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
 //              TODO HANDLE ERRORS RELATED TO MAX > MIN
 //              TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS
-//              TODO HANDLE 
+//              TODO HANDLE case where init model does not satisfy for example ine and only one criterion of toplvl elem
-                // 1. make a list of constants equaling the min number of specified objects
+//              We are currently ignoring all typescope spec related to the topLevel type
-                //These numbers do not include enums or initial model elements
+//              TODO Case where typeScope spec continas numbers for a type and its subtype
+//              We shouldnt waste constants for each one
                
-                //Number of defined non-abstract elements that are not enum elements
+                // 1. make a list of constants equaling the min number of specified objects
-                //Equals the number of elements in te initial model
+                // These numbers do not include enums or initial model elements
+                // 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
 //              
@@ -45,10 +49,9 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 //                              elemsInIM += 1
 //                      }
 //              }
-                
+                // TODO handle errors related to GLOBAL_MIN/MAX < 0
-                //TODO handle errors related to GLOBAL_MIN/MAX < 0
+                val GLOBAL_MIN = config.typeScopes.minNewElements - elemsInIM
-                val GLOBAL_MIN = config.typeScopes.minNewElements-elemsInIM
+                val GLOBAL_MAX = config.typeScopes.maxNewElements - elemsInIM
-                val GLOBAL_MAX = config.typeScopes.maxNewElements-elemsInIM
                val localInstances = newArrayList
@@ -79,62 +82,60 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                // Handling Minimum_Specific
                var i = 1
-                if (trace.topLvlElementIsInInitialModel as Boolean){
+                if (trace.topLvlElementIsInInitialModel as Boolean) {
                        i = 0
                }
                var minNum = -1
                var Map<Type, Integer> startPoints = new HashMap
-//              var inIM = false
+                for (t : config.typeScopes.minNewElementsByType.keySet.filter[!equals(trace.topLevelType)]) {
-                for (tConfig : config.typeScopes.minNewElementsByType.keySet) {
+                        var numIniIntModel = 0
-//                      var numIniIntModel = 0
+                        for (elem : trace.definedElement2String.keySet) {
-//                      for (elem : trace.definedElement2String.keySet) {
+                                for (tDefined : elem.definedInType) {
-//                              println(elem.definedInType)
+                                        if (support.dfsSubtypeCheck(t, tDefined)) {
-//                              for (tDefined : elem.definedInType) {
+                                                numIniIntModel += 1
-//                                      inIM = support.dfsSubtypeCheck(tConfig, tDefined) || tConfig.equals(tDefined)
+                                        }
-//                              }
+                                }
-//                              if (inIM) {
+                        }
-//                                      numIniIntModel += 1
+                        minNum = t.lookup(config.typeScopes.minNewElementsByType) - numIniIntModel
-//                              }
-//                              inIM = false
-//                      }               
-                        
-                        minNum = tConfig.lookup(config.typeScopes.minNewElementsByType)//-numIniIntModel
                        if (minNum != 0) {
                                getInstanceConstants(i + minNum, i, localInstances, trace, true, false)
-                                startPoints.put(tConfig, i)
+                                startPoints.put(t, i)
                                i += minNum
-                                makeFofFormula(localInstances, trace, true, tConfig)
+                                makeFofFormula(localInstances, trace, true, t)
                        }
                }
                // TODO: calc sum of mins, compare to current value of i
                // Handling Maximum_Specific
-                for (tConfig : config.typeScopes.maxNewElementsByType.keySet) {
+                for (t : config.typeScopes.maxNewElementsByType.keySet.filter[!equals(trace.topLevelType)]) {
-                        
-//                      var numIniIntModel = 0
+                        var numIniIntModel = 0
-//                      for (elem : trace.definedElement2String.keySet) {
+                        for (elem : trace.definedElement2String.keySet) {
-//                              println(elem.definedInType)
+                                if (elem.definedInType == t) {
-//                              for (tDefined : elem.definedInType) {
+                                        numIniIntModel += 1
-//                                      inIM = support.dfsSubtypeCheck(tConfig, tDefined) || tConfig.equals(tDefined)
+                                }
-//                              }
+                        }
-//                              if (inIM) {
-//                                      numIniIntModel += 1
+                        var maxNum = t.lookup(config.typeScopes.maxNewElementsByType) - numIniIntModel
-//                              }
+                        if (config.typeScopes.minNewElementsByType.keySet.contains(t)) {
-//                              inIM = false
+                                minNum = t.lookup(config.typeScopes.minNewElementsByType) - numIniIntModel
-//                      }       
+                        } else {
-                        
+                                minNum = 0
-                        var maxNum = tConfig.lookup(config.typeScopes.maxNewElementsByType)//-numIniIntModel
+                        }
-                        minNum = tConfig.lookup(config.typeScopes.minNewElementsByType)//-numIniIntModel
-                        var startpoint = tConfig.lookup(startPoints)
                        if (minNum != 0) {
+                                var startpoint = t.lookup(startPoints)
                                getInstanceConstants(startpoint + minNum, startpoint, localInstances, trace, true, false)
                        }
-                        //I do not understand the line below
+                        else {
-                        if (maxNum != minNum) {
+                                localInstances.clear
-                                var instEndInd = Math.min(GLOBAL_MAX, i + maxNum - minNum)
-                                getInstanceConstants(instEndInd, i, localInstances, trace, false, false)
-                                makeFofFormula(localInstances, trace, false, tConfig)
                        }
+                        // 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)
+//                      }
                }
 // 3. Specify uniqueness of elements

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend index ec841546..df3cfd82 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
@@ -23,18 +23,22 @@ class Logic2VampireLanguageMapper_ScopeMapper {
23	this.base = base	23	this.base = base
24	}	24	}
25		25
26	def dispatch public void transformScope(List<Type> types, VampireSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) {	26	def dispatch public void transformScope(List<Type> types, VampireSolverConfiguration config,
		27	Logic2VampireLanguageMapperTrace trace) {
27	val ABSOLUTE_MIN = 0	28	val ABSOLUTE_MIN = 0
28	val ABSOLUTE_MAX = Integer.MAX_VALUE	29	val ABSOLUTE_MAX = Integer.MAX_VALUE
29		30
30	// TODO HANDLE ERRORS RELATED TO MAX > MIN	31	// TODO HANDLE ERRORS RELATED TO MAX > MIN
31	// TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS	32	// TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS
32	// TODO HANDLE	33	// TODO HANDLE case where init model does not satisfy for example ine and only one criterion of toplvl elem
33	// 1. make a list of constants equaling the min number of specified objects	34	// We are currently ignoring all typescope spec related to the topLevel type
34	//These numbers do not include enums or initial model elements	35	// TODO Case where typeScope spec continas numbers for a type and its subtype
		36	// We shouldnt waste constants for each one
35		37
36	//Number of defined non-abstract elements that are not enum elements	38	// 1. make a list of constants equaling the min number of specified objects
37	//Equals the number of elements in te initial model	39	// These numbers do not include enums or initial model elements
		40	// Number of defined non-abstract elements that are not enum elements
		41	// Equals the number of elements in te initial model
38	var elemsInIM = trace.definedElement2String.size	42	var elemsInIM = trace.definedElement2String.size
39	// var elemsInIM = 0	43	// var elemsInIM = 0
40	//	44	//
@@ -45,10 +49,9 @@ class Logic2VampireLanguageMapper_ScopeMapper {
45	// elemsInIM += 1	49	// elemsInIM += 1
46	// }	50	// }
47	// }	51	// }
48		52	// TODO handle errors related to GLOBAL_MIN/MAX < 0
49	//TODO handle errors related to GLOBAL_MIN/MAX < 0	53	val GLOBAL_MIN = config.typeScopes.minNewElements - elemsInIM
50	val GLOBAL_MIN = config.typeScopes.minNewElements-elemsInIM	54	val GLOBAL_MAX = config.typeScopes.maxNewElements - elemsInIM
51	val GLOBAL_MAX = config.typeScopes.maxNewElements-elemsInIM
52		55
53	val localInstances = newArrayList	56	val localInstances = newArrayList
54		57
@@ -79,62 +82,60 @@ class Logic2VampireLanguageMapper_ScopeMapper {
79		82
80	// Handling Minimum_Specific	83	// Handling Minimum_Specific
81	var i = 1	84	var i = 1
82	if (trace.topLvlElementIsInInitialModel as Boolean){	85	if (trace.topLvlElementIsInInitialModel as Boolean) {
83	i = 0	86	i = 0
84	}	87	}
85	var minNum = -1	88	var minNum = -1
86	var Map<Type, Integer> startPoints = new HashMap	89	var Map<Type, Integer> startPoints = new HashMap
87	// var inIM = false	90	for (t : config.typeScopes.minNewElementsByType.keySet.filter[!equals(trace.topLevelType)]) {
88	for (tConfig : config.typeScopes.minNewElementsByType.keySet) {	91	var numIniIntModel = 0
89	// var numIniIntModel = 0	92	for (elem : trace.definedElement2String.keySet) {
90	// for (elem : trace.definedElement2String.keySet) {	93	for (tDefined : elem.definedInType) {
91	// println(elem.definedInType)	94	if (support.dfsSubtypeCheck(t, tDefined)) {
92	// for (tDefined : elem.definedInType) {	95	numIniIntModel += 1
93	// inIM = support.dfsSubtypeCheck(tConfig, tDefined) \|\| tConfig.equals(tDefined)	96	}
94	// }	97	}
95	// if (inIM) {	98	}
96	// numIniIntModel += 1	99	minNum = t.lookup(config.typeScopes.minNewElementsByType) - numIniIntModel
97	// }
98	// inIM = false
99	// }
100
101	minNum = tConfig.lookup(config.typeScopes.minNewElementsByType)//-numIniIntModel
102	if (minNum != 0) {	100	if (minNum != 0) {
103	getInstanceConstants(i + minNum, i, localInstances, trace, true, false)	101	getInstanceConstants(i + minNum, i, localInstances, trace, true, false)
104	startPoints.put(tConfig, i)	102	startPoints.put(t, i)
105	i += minNum	103	i += minNum
106	makeFofFormula(localInstances, trace, true, tConfig)	104	makeFofFormula(localInstances, trace, true, t)
107	}	105	}
108	}	106	}
109		107
110	// TODO: calc sum of mins, compare to current value of i	108	// TODO: calc sum of mins, compare to current value of i
111	// Handling Maximum_Specific	109	// Handling Maximum_Specific
112	for (tConfig : config.typeScopes.maxNewElementsByType.keySet) {	110	for (t : config.typeScopes.maxNewElementsByType.keySet.filter[!equals(trace.topLevelType)]) {
113		111
114	// var numIniIntModel = 0	112	var numIniIntModel = 0
115	// for (elem : trace.definedElement2String.keySet) {	113	for (elem : trace.definedElement2String.keySet) {
116	// println(elem.definedInType)	114	if (elem.definedInType == t) {
117	// for (tDefined : elem.definedInType) {	115	numIniIntModel += 1
118	// inIM = support.dfsSubtypeCheck(tConfig, tDefined) \|\| tConfig.equals(tDefined)	116	}
119	// }	117	}
120	// if (inIM) {	118
121	// numIniIntModel += 1	119	var maxNum = t.lookup(config.typeScopes.maxNewElementsByType) - numIniIntModel
122	// }	120	if (config.typeScopes.minNewElementsByType.keySet.contains(t)) {
123	// inIM = false	121	minNum = t.lookup(config.typeScopes.minNewElementsByType) - numIniIntModel
124	// }	122	} else {
125		123	minNum = 0
126	var maxNum = tConfig.lookup(config.typeScopes.maxNewElementsByType)//-numIniIntModel	124	}
127	minNum = tConfig.lookup(config.typeScopes.minNewElementsByType)//-numIniIntModel	125
128	var startpoint = tConfig.lookup(startPoints)
129	if (minNum != 0) {	126	if (minNum != 0) {
		127	var startpoint = t.lookup(startPoints)
130	getInstanceConstants(startpoint + minNum, startpoint, localInstances, trace, true, false)	128	getInstanceConstants(startpoint + minNum, startpoint, localInstances, trace, true, false)
131	}	129	}
132	//I do not understand the line below	130	else {
133	if (maxNum != minNum) {	131	localInstances.clear
134	var instEndInd = Math.min(GLOBAL_MAX, i + maxNum - minNum)
135	getInstanceConstants(instEndInd, i, localInstances, trace, false, false)
136	makeFofFormula(localInstances, trace, false, tConfig)
137	}	132	}
		133	// I do not understand the line below
		134	// if (maxNum != minNum) {
		135	var instEndInd = Math.min(GLOBAL_MAX, i + maxNum - minNum)
		136	getInstanceConstants(instEndInd, i, localInstances, trace, false, false)
		137	makeFofFormula(localInstances, trace, false, t)
		138	// }
138	}	139	}
139		140
140	// 3. Specify uniqueness of elements	141	// 3. Specify uniqueness of elements