1 files changed, 91 insertions, 27 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 e5dfbf08..2da4cfd7 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
@@ -5,60 +5,124 @@ 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 static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
 class Logic2VampireLanguageMapper_ScopeMapper {
        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
        private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
        val Logic2VampireLanguageMapper base
+        private val VLSVariable variable = createVLSVariable => [it.name = "A"]
        public new(Logic2VampireLanguageMapper base) {
                this.base = base
        }
        def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) {
-                val VLSVariable variable = createVLSVariable => [it.name = "A"]
+//              HANDLE ERRORS RELATED TO MAX > MIN
+//              HANDLE ERROR RELATED TO SUM(MIN TYPES) > MAX OBJECTS
+//              NOT SPECIFIED MEANS =0 ?
                // 1. make a list of constants equaling the min number of specified objects
+                val GLOBAL_MIN = config.typeScopes.minNewElements
+                val GLOBAL_MAX = config.typeScopes.maxNewElements
                val localInstances = newArrayList
-                for (var i = 0; i < config.typeScopes.minNewElements; i++) {
+                // Handling Minimum_General
+                if (GLOBAL_MIN != 0) {
+                        getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, false) // fix last param
+                        makeFofFormula(localInstances, trace, true, "object")
+                }
+                // Handling Maximum_General
+                if (GLOBAL_MAX != 0) {
+                        getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true) // fix last param
+                        makeFofFormula(localInstances, trace, false, "object")
+                }
+                // Handling Minimum_Specific
+                var i = 0
+                var minNum = -1
+                for (t : config.typeScopes.minNewElementsByType.keySet) {
+                        minNum = t.lookup(config.typeScopes.minNewElementsByType)
+                        if (minNum != 0) {
+                                getInstanceConstants(i+minNum, i, localInstances, trace, false)
+                                i += minNum
+                                makeFofFormula(localInstances, trace, true, t.toString)//fix last param
+                        }
+                }
+                //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)
+                        if (maxNum != 0) {
+                                var forLimit = Math.min(GLOBAL_MAX, i+maxNum-minNum)
+                                getInstanceConstants(GLOBAL_MAX, i, localInstances, trace, false)
+                                makeFofFormula(localInstances, trace, false, t.toString)//fix last param
+                        }
+                }
+                // 3. Specify uniqueness of elements
+                if (trace.uniqueInstances.length != 0) {
+                        val uniqueness = createVLSFofFormula => [
+                                it.name = "typeUniqueness"
+                                it.fofRole = "axiom"
+                                it.fofFormula = support.establishUniqueness(trace.uniqueInstances)
+                        ]
+                        trace.specification.formulas += uniqueness
+                }
+        }
+        def protected void getInstanceConstants(int numElems, int init, ArrayList list,
+                Logic2VampireLanguageMapperTrace trace, boolean addToTrace) {
+                list.clear
+                for (var i = init; i < numElems; i++) {
                        val num = i + 1
                        val cst = createVLSConstant => [
                                it.name = "o" + num
                        ]
-                        trace.uniqueInstances.add(cst)
+                        if (addToTrace) {
-                        localInstances.add(cst)
+                                trace.uniqueInstances.add(cst)
+                        }
+                        list.add(cst)
                }
+        }
-                // TODO: specify for the max
+        def protected void makeFofFormula(ArrayList list, Logic2VampireLanguageMapperTrace trace, boolean minimum, String name) {
-                if (config.typeScopes.minNewElements != 0) {
+                val cstDec = createVLSFofFormula => [
-                        // 2. Create initial fof formula to specify the number of elems
+                        it.name = support.toIDMultiple("typeScope", if(minimum) "min" else "max", name)
-                        val cstDec = createVLSFofFormula => [
+                        it.fofRole = "axiom"
-                                it.name = "typeScope"
+                        it.fofFormula = createVLSUniversalQuantifier => [
-                                it.fofRole = "axiom"
+                                it.variables += support.duplicate(variable)
-                                it.fofFormula = createVLSUniversalQuantifier => [
+                                // check below
-                                        it.variables += support.duplicate(variable)
+                                it.operand = createVLSImplies => [
-                                        // check below
+                                        if (minimum) {
-                                        it.operand = createVLSImplies => [
+                                                it.left = support.unfoldOr(list.map [ i |
-                                                it.left = support.unfoldOr(localInstances.map [ i |
                                                        createVLSEquality => [
                                                                it.left = createVLSVariable => [it.name = variable.name]
                                                                it.right = i
                                                        ]
                                                ])
                                                it.right = support.topLevelTypeFunc
-                                        ]
+                                        } else {
+                                                it.right = support.unfoldOr(list.map [ i |
+                                                        createVLSEquality => [
+                                                                it.left = createVLSVariable => [it.name = variable.name]
+                                                                it.right = i
+                                                        ]
+                                                ])
+                                                it.left = support.topLevelTypeFunc
+                                        }
                                ]
                        ]
-                        trace.specification.formulas += cstDec
+                ]
+                trace.specification.formulas += cstDec
-                        // TODO: specify for scope per type
-                        // 3. Specify uniqueness of elements
-                        val uniqueness = createVLSFofFormula => [
-                                it.name = "typeUniqueness"
-                                it.fofRole = "axiom"
-                                it.fofFormula = support.establishUniqueness(trace.uniqueInstances)
-                        ]
-                        trace.specification.formulas += uniqueness
-                }
        }
 }

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 e5dfbf08..2da4cfd7 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
@@ -5,60 +5,124 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
5	import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory	5	import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
6	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration	6	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
7	import java.util.List	7	import java.util.List
		8	import java.util.ArrayList
		9
		10	import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
8		11
9	class Logic2VampireLanguageMapper_ScopeMapper {	12	class Logic2VampireLanguageMapper_ScopeMapper {
10	private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE	13	private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
11	private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support	14	private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
12	val Logic2VampireLanguageMapper base	15	val Logic2VampireLanguageMapper base
		16	private val VLSVariable variable = createVLSVariable => [it.name = "A"]
13		17
14	public new(Logic2VampireLanguageMapper base) {	18	public new(Logic2VampireLanguageMapper base) {
15	this.base = base	19	this.base = base
16	}	20	}
17		21
18	def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) {	22	def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) {
19	val VLSVariable variable = createVLSVariable => [it.name = "A"]
20		23
		24	// HANDLE ERRORS RELATED TO MAX > MIN
		25	// HANDLE ERROR RELATED TO SUM(MIN TYPES) > MAX OBJECTS
		26	// NOT SPECIFIED MEANS =0 ?
21	// 1. make a list of constants equaling the min number of specified objects	27	// 1. make a list of constants equaling the min number of specified objects
		28	val GLOBAL_MIN = config.typeScopes.minNewElements
		29	val GLOBAL_MAX = config.typeScopes.maxNewElements
		30
22	val localInstances = newArrayList	31	val localInstances = newArrayList
23	for (var i = 0; i < config.typeScopes.minNewElements; i++) {	32
		33	// Handling Minimum_General
		34	if (GLOBAL_MIN != 0) {
		35	getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, false) // fix last param
		36	makeFofFormula(localInstances, trace, true, "object")
		37	}
		38
		39	// Handling Maximum_General
		40	if (GLOBAL_MAX != 0) {
		41	getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true) // fix last param
		42	makeFofFormula(localInstances, trace, false, "object")
		43	}
		44
		45	// Handling Minimum_Specific
		46	var i = 0
		47	var minNum = -1
		48	for (t : config.typeScopes.minNewElementsByType.keySet) {
		49	minNum = t.lookup(config.typeScopes.minNewElementsByType)
		50	if (minNum != 0) {
		51	getInstanceConstants(i+minNum, i, localInstances, trace, false)
		52	i += minNum
		53	makeFofFormula(localInstances, trace, true, t.toString)//fix last param
		54	}
		55	}
		56
		57	//TODO: calc sum of mins, compare to current value of i
		58
		59	// Handling Maximum_Specific
		60	for (t : config.typeScopes.maxNewElementsByType.keySet) {
		61	var maxNum = t.lookup(config.typeScopes.maxNewElementsByType)
		62	minNum = t.lookup(config.typeScopes.minNewElementsByType)
		63	if (maxNum != 0) {
		64	var forLimit = Math.min(GLOBAL_MAX, i+maxNum-minNum)
		65	getInstanceConstants(GLOBAL_MAX, i, localInstances, trace, false)
		66	makeFofFormula(localInstances, trace, false, t.toString)//fix last param
		67	}
		68	}
		69
		70	// 3. Specify uniqueness of elements
		71	if (trace.uniqueInstances.length != 0) {
		72	val uniqueness = createVLSFofFormula => [
		73	it.name = "typeUniqueness"
		74	it.fofRole = "axiom"
		75	it.fofFormula = support.establishUniqueness(trace.uniqueInstances)
		76	]
		77	trace.specification.formulas += uniqueness
		78	}
		79
		80	}
		81
		82	def protected void getInstanceConstants(int numElems, int init, ArrayList list,
		83	Logic2VampireLanguageMapperTrace trace, boolean addToTrace) {
		84	list.clear
		85	for (var i = init; i < numElems; i++) {
24	val num = i + 1	86	val num = i + 1
25	val cst = createVLSConstant => [	87	val cst = createVLSConstant => [
26	it.name = "o" + num	88	it.name = "o" + num
27	]	89	]
28	trace.uniqueInstances.add(cst)	90	if (addToTrace) {
29	localInstances.add(cst)	91	trace.uniqueInstances.add(cst)
		92	}
		93	list.add(cst)
30	}	94	}
		95	}
31		96
32	// TODO: specify for the max	97	def protected void makeFofFormula(ArrayList list, Logic2VampireLanguageMapperTrace trace, boolean minimum, String name) {
33	if (config.typeScopes.minNewElements != 0) {	98	val cstDec = createVLSFofFormula => [
34	// 2. Create initial fof formula to specify the number of elems	99	it.name = support.toIDMultiple("typeScope", if(minimum) "min" else "max", name)
35	val cstDec = createVLSFofFormula => [	100	it.fofRole = "axiom"
36	it.name = "typeScope"	101	it.fofFormula = createVLSUniversalQuantifier => [
37	it.fofRole = "axiom"	102	it.variables += support.duplicate(variable)
38	it.fofFormula = createVLSUniversalQuantifier => [	103	// check below
39	it.variables += support.duplicate(variable)	104	it.operand = createVLSImplies => [
40	// check below	105	if (minimum) {
41	it.operand = createVLSImplies => [	106	it.left = support.unfoldOr(list.map [ i \|
42	it.left = support.unfoldOr(localInstances.map [ i \|
43	createVLSEquality => [	107	createVLSEquality => [
44	it.left = createVLSVariable => [it.name = variable.name]	108	it.left = createVLSVariable => [it.name = variable.name]
45	it.right = i	109	it.right = i
46	]	110	]
47	])	111	])
48	it.right = support.topLevelTypeFunc	112	it.right = support.topLevelTypeFunc
49	]	113	} else {
		114	it.right = support.unfoldOr(list.map [ i \|
		115	createVLSEquality => [
		116	it.left = createVLSVariable => [it.name = variable.name]
		117	it.right = i
		118	]
		119	])
		120	it.left = support.topLevelTypeFunc
		121	}
50	]	122	]
51	]	123	]
52	trace.specification.formulas += cstDec	124	]
53		125	trace.specification.formulas += cstDec
54	// TODO: specify for scope per type
55	// 3. Specify uniqueness of elements
56	val uniqueness = createVLSFofFormula => [
57	it.name = "typeUniqueness"
58	it.fofRole = "axiom"
59	it.fofFormula = support.establishUniqueness(trace.uniqueInstances)
60	]
61	trace.specification.formulas += uniqueness
62	}
63	}	126	}
		127
64	}	128	}