Facilitate #31, close #36

6 files changed, 58 insertions, 28 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) {

-                                localInstances.add(support.duplicate(i))

+                        // *

+                        getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, !consistant)

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

-                        makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null)

-

-//                      //For testing Min>Max scope

-//                      getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, false)

-//                      makeFofFormula(localInstances, trace, false, null)

-//                      //end for testing

+                        getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant)

+                        if (consistant) {

+                                makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null)

+                        } else {

+                                makeFofFormula(localInstances, trace, false, null)

+                        }

                 }

 

                 // 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_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
index b00dad42..dd88a53a 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
@@ -109,6 +109,8 @@ class Logic2VampireLanguageMapper_Support {
 
 // TODO Make more general
         def establishUniqueness(List<VLSConstant> terms, VLSConstant t2) {
+                
+//              OLD
 //              val List<VLSInequality> eqs = newArrayList
 //              for (t1 : terms.subList(1, terms.length)) {
 //                      for (t2 : terms.subList(0, terms.indexOf(t1))) {
@@ -122,6 +124,8 @@ class Logic2VampireLanguageMapper_Support {
 //                      }
 //              }
 //              return unfoldAnd(eqs)
+//              END OLD
+
                 val List<VLSInequality> eqs = newArrayList
                 for (t1 : terms) {
                         if (t1 != t2) {
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
index 6c46d2e3..2cc60591 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
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 e5600049..1108945f 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_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
index f9813a92..a473c586 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.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 d40b0dd2..24b46e3e 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
@@ -52,16 +52,25 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
     final int GLOBAL_MIN = config.typeScopes.minNewElements;

     final int GLOBAL_MAX = config.typeScopes.maxNewElements;

     final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList();

+    final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN);

     if ((GLOBAL_MIN != ABSOLUTE_MIN)) {

-      this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false);

-      for (final VLSConstant i : trace.uniqueInstances) {

-        localInstances.add(this.support.duplicate(i));

+      this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, (!consistant));

+      if (consistant) {

+        for (final VLSConstant i : trace.uniqueInstances) {

+          localInstances.add(this.support.duplicate(i));

+        }

+        this.makeFofFormula(localInstances, trace, true, null);

+      } else {

+        this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, true, null);

       }

-      this.makeFofFormula(localInstances, trace, true, null);

     }

     if ((GLOBAL_MAX != ABSOLUTE_MAX)) {

-      this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true);

-      this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null);

+      this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant);

+      if (consistant) {

+        this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null);

+      } else {

+        this.makeFofFormula(localInstances, trace, false, null);

+      }

     }

     int i_1 = 1;

     int minNum = (-1);

@@ -95,11 +104,12 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
         }

       }

     }

-    int _length = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length;

-    boolean _notEquals = (_length != 0);

-    if (_notEquals) {

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

@@ -109,6 +119,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
           final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);

           EList<VLSFofFormula> _formulas = trace.specification.getFormulas();

           _formulas.add(uniqueness);

+          ind++;

         }

       }

     }