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

---
 ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 9570 -> 9829 bytes
 .../Logic2VampireLanguageMapper_ScopeMapper.java   |  47 +++++++++++++++------
 2 files changed, 34 insertions(+), 13 deletions(-)

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

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
index 1108945f..f6006175 100644
Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
index 24b46e3e..cd3b1d13 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
@@ -18,6 +18,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
 import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;
 import java.util.ArrayList;
 import java.util.HashMap;
+import java.util.List;
 import java.util.Map;
 import java.util.Set;
 import org.eclipse.emf.common.util.EList;
@@ -104,22 +105,42 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
         }
       }
     }
+    final boolean DUPLICATES = true;
     final int numInst = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length;
     int ind = 1;
     if ((numInst != 0)) {
-      for (final VLSConstant e : trace.uniqueInstances) {
-        {
-          final int x = ind;
-          VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
-          final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {
-            it.setName(this.support.toIDMultiple("t_uniqueness", e.getName()));
-            it.setFofRole("axiom");
-            it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances, e));
-          };
-          final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);
-          EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
-          _formulas.add(uniqueness);
-          ind++;
+      if (DUPLICATES) {
+        for (final VLSConstant e : trace.uniqueInstances) {
+          {
+            final int x = ind;
+            VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
+            final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {
+              it.setName(this.support.toIDMultiple("t_uniqueness", e.getName()));
+              it.setFofRole("axiom");
+              it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances, e));
+            };
+            final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);
+            EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
+            _formulas.add(uniqueness);
+            ind++;
+          }
+        }
+      } else {
+        List<VLSConstant> _subList = trace.uniqueInstances.subList(0, (numInst - 1));
+        for (final VLSConstant e_1 : _subList) {
+          {
+            final int x = ind;
+            VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
+            final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {
+              it.setName(this.support.toIDMultiple("t_uniqueness", e_1.getName()));
+              it.setFofRole("axiom");
+              it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e_1));
+            };
+            final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);
+            EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
+            _formulas.add(uniqueness);
+            ind++;
+          }
         }
       }
     }
-- 
cgit v1.2.3-54-g00ecf