From 0145f83dc3503e6590496ddc039e7e462c53cba4 Mon Sep 17 00:00:00 2001
From: ArenBabikian <aren.babikian@mail.mcgill.ca>
Date: Thu, 4 Apr 2019 20:08:30 -0400
Subject: Add small detail to #36

---
 .../Logic2VampireLanguageMapper_ScopeMapper.xtend  | 48 ++++++++++++----------
 1 file changed, 27 insertions(+), 21 deletions(-)

(limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill')

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 5e8819a6..741389bb 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
@@ -93,30 +93,36 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 		}
 
 // 3. Specify uniqueness of elements
+		// TEMP
+		val DUPLICATES = true
+
 		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++
+			if (DUPLICATES) {
+				// W/ DUPLICATES
+				for (e : trace.uniqueInstances) {
+					val x = ind
+					val uniqueness = createVLSFofFormula => [
+						it.name = support.toIDMultiple("t_uniqueness", e.name)
+						it.fofRole = "axiom"
+						it.fofFormula = support.establishUniqueness(trace.uniqueInstances, e)
+					]
+					trace.specification.formulas += uniqueness
+					ind++
+				}
+			} else {
+				// W/O DUPLICATES
+				for (e : trace.uniqueInstances.subList(0, numInst - 1)) {
+					val x = ind
+					val uniqueness = createVLSFofFormula => [
+						it.name = support.toIDMultiple("t_uniqueness", e.name)
+						it.fofRole = "axiom"
+						it.fofFormula = support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e)
+					]
+					trace.specification.formulas += uniqueness
+					ind++
+				}
 			}
 		}
 	}
-- 
cgit v1.2.3-54-g00ecf