Add small detail to #36

3 files changed, 61 insertions, 34 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 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++

+                                }

                         }

                 }

         }

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
--- 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
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++;

+          }

         }

       }

     }