1 files changed, 34 insertions, 19 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 54fcdc86..5e8819a6 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
@@ -36,31 +36,30 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                val localInstances = newArrayList
+                val consistant = GLOBAL_MAX > GLOBAL_MIN
                // Handling Minimum_General
                if (GLOBAL_MIN != ABSOLUTE_MIN) {
-                        getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false)
+                        // *
-                        for (i : trace.uniqueInstances) {
+                        getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, !consistant)
-                                localInstances.add(support.duplicate(i))
+                        if (consistant) {
+                                for (i : trace.uniqueInstances) {
+                                        localInstances.add(support.duplicate(i))
+                                }
+                                makeFofFormula(localInstances, trace, true, null)
+                        } else {
+                                makeFofFormula(trace.uniqueInstances as ArrayList, trace, true, null)
                        }
-                        makeFofFormula(localInstances, trace, true, null)
-//                      //For testing Min>Max scope
-//                      getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, true)
-//                      makeFofFormula(trace.uniqueInstances as ArrayList, trace, true, null)
-//                      //end for testing
                }
                // Handling Maximum_General
                if (GLOBAL_MAX != ABSOLUTE_MAX) {
-                        getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true)
+                        getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant)
-                        makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null)
+                        if (consistant) {
+                                makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null)
-//                      //For testing Min>Max scope
+                        } else {
-//                      getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, false)
+                                makeFofFormula(localInstances, trace, false, null)
-//                      makeFofFormula(localInstances, trace, false, null)
+                        }
-//                      //end for testing
                }
                // Handling Minimum_Specific
@@ -94,14 +93,30 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                }
 // 3. Specify uniqueness of elements
-                if (trace.uniqueInstances.length != 0) {
+                val numInst = trace.uniqueInstances.length
+                var ind = 1
+                if (numInst != 0) {
+                        /*
+                         * // SHORTER
+                         * for (e : trace.uniqueInstances.subList(0, numInst-1)) {
+                         /*/
+                        // LONGER
                        for (e : trace.uniqueInstances) {
+                                // */
+                                val x = ind
                                val uniqueness = createVLSFofFormula => [
                                        it.name = support.toIDMultiple("t_uniqueness", e.name)
                                        it.fofRole = "axiom"
+                                        /*
+                                         * // SHORTER
+                                         * it.fofFormula = support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e)
+                                         /*/
+                                        // LONGER
                                        it.fofFormula = support.establishUniqueness(trace.uniqueInstances, e)
+                                // */
                                ]
                                trace.specification.formulas += uniqueness
+                                ind++
                        }
                }
        }

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 54fcdc86..5e8819a6 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
@@ -36,31 +36,30 @@ class Logic2VampireLanguageMapper_ScopeMapper {
36		36
37	val localInstances = newArrayList	37	val localInstances = newArrayList
38		38
		39	val consistant = GLOBAL_MAX > GLOBAL_MIN
		40
39	// Handling Minimum_General	41	// Handling Minimum_General
40	if (GLOBAL_MIN != ABSOLUTE_MIN) {	42	if (GLOBAL_MIN != ABSOLUTE_MIN) {
41	getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false)	43	// *
42	for (i : trace.uniqueInstances) {	44	getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, !consistant)
43	localInstances.add(support.duplicate(i))	45	if (consistant) {
		46	for (i : trace.uniqueInstances) {
		47	localInstances.add(support.duplicate(i))
		48	}
		49	makeFofFormula(localInstances, trace, true, null)
		50	} else {
		51	makeFofFormula(trace.uniqueInstances as ArrayList, trace, true, null)
44	}	52	}
45
46	makeFofFormula(localInstances, trace, true, null)
47
48	// //For testing Min>Max scope
49	// getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, true)
50	// makeFofFormula(trace.uniqueInstances as ArrayList, trace, true, null)
51	// //end for testing
52
53	}	53	}
54		54
55	// Handling Maximum_General	55	// Handling Maximum_General
56	if (GLOBAL_MAX != ABSOLUTE_MAX) {	56	if (GLOBAL_MAX != ABSOLUTE_MAX) {
57	getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true)	57	getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant)
58	makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null)	58	if (consistant) {
59		59	makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null)
60	// //For testing Min>Max scope	60	} else {
61	// getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, false)	61	makeFofFormula(localInstances, trace, false, null)
62	// makeFofFormula(localInstances, trace, false, null)	62	}
63	// //end for testing
64	}	63	}
65		64
66	// Handling Minimum_Specific	65	// Handling Minimum_Specific
@@ -94,14 +93,30 @@ class Logic2VampireLanguageMapper_ScopeMapper {
94	}	93	}
95		94
96	// 3. Specify uniqueness of elements	95	// 3. Specify uniqueness of elements
97	if (trace.uniqueInstances.length != 0) {	96	val numInst = trace.uniqueInstances.length
		97	var ind = 1
		98	if (numInst != 0) {
		99	/*
		100	* // SHORTER
		101	* for (e : trace.uniqueInstances.subList(0, numInst-1)) {
		102	/*/
		103	// LONGER
98	for (e : trace.uniqueInstances) {	104	for (e : trace.uniqueInstances) {
		105	// */
		106	val x = ind
99	val uniqueness = createVLSFofFormula => [	107	val uniqueness = createVLSFofFormula => [
100	it.name = support.toIDMultiple("t_uniqueness", e.name)	108	it.name = support.toIDMultiple("t_uniqueness", e.name)
101	it.fofRole = "axiom"	109	it.fofRole = "axiom"
		110	/*
		111	* // SHORTER
		112	* it.fofFormula = support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e)
		113	/*/
		114	// LONGER
102	it.fofFormula = support.establishUniqueness(trace.uniqueInstances, e)	115	it.fofFormula = support.establishUniqueness(trace.uniqueInstances, e)
		116	// */
103	]	117	]
104	trace.specification.formulas += uniqueness	118	trace.specification.formulas += uniqueness
		119	ind++
105	}	120	}
106	}	121	}
107	}	122	}