8 files changed, 34 insertions, 21 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
index 14926280..b617912d 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
@@ -265,7 +265,11 @@ class Logic2VampireLanguageMapper {
         def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred,
                 List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
                 Map<Variable, VLSVariable> variables) {
-                typeMapper.transformReference(referred, trace)
+                        val name = referred.lookup(trace.definedElement2String)
+                        return createVLSConstant => [
+                                it.name = name
+                        ]
+//              typeMapper.transformReference(referred, trace)
         }
 
         def dispatch protected VLSTerm transformSymbolicReference(ConstantDeclaration constant,
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
index d2a01e0e..38c99a89 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
@@ -138,9 +138,9 @@ class Logic2VampireLanguageMapper_TypeMapper {
                                 val cstTerm = createVLSFunctionAsTerm => [
                                         it.functor = "eo" + num
                                 ]
-                                if (isNotEnum) {
+//                              if (isNotEnum) {
                                         trace.definedElement2String.put(type.elements.get(index),cstTerm.functor)
-                                }
+//                              }
                                 
                                 val cst = support.toConstant(cstTerm)
                                 trace.uniqueInstances.add(cst)
@@ -249,8 +249,13 @@ class Logic2VampireLanguageMapper_TypeMapper {
         }
 
         def protected transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) {
-                createVLSDoubleQuote => [
-                        it.value = "\"a" + referred.name + "\""
+                
+//              createVLSDoubleQuote => [
+//                      it.value = "\"a" + referred.name + "\""
+//              ]
+                
+                createVLSConstant => [
+                        it.name = referred.name
                 ]
         }
 
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend
index ef77b6ca..9eb47f41 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend
@@ -246,7 +246,12 @@ class VampireModelInterpretation implements LogicModelInterpretation {
                 return declaration.lookup(this.type2DefinedElement)
         }
 
-        def private dispatch getElementsDispatch(TypeDefinition declaration) { return declaration.elements }
+        def private dispatch getElementsDispatch(TypeDefinition declaration) {
+                println("~~" + declaration)
+                println(declaration.elements)
+                println()
+                return declaration.elements
+        }
 
         override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) {
                 throw new UnsupportedOperationException("TODO: auto-generated method stub")
@@ -260,12 +265,12 @@ class VampireModelInterpretation implements LogicModelInterpretation {
                 for (real : realRelations) {
                         if (real.contains(node1) && real.contains(node2)) {
                                 println("  true")
-                                TimeUnit.SECONDS.sleep(1)
+                                TimeUnit.MILLISECONDS.sleep(10)
                                 return true
                         }
                 }
                 println("  false")
-                TimeUnit.SECONDS.sleep(1)
+                TimeUnit.MILLISECONDS.sleep(10)
                 return false
         }
 
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 b1e3b95d..8ce1beed 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 803b5fed..f7259e75 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_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
index 7e8b1703..116b2d15 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
index f8a65187..c8961c6e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
@@ -283,7 +283,12 @@ public class Logic2VampireLanguageMapper {
   }

   

   protected VLSTerm _transformSymbolicReference(final DefinedElement referred, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

-    return this.typeMapper.transformReference(referred, trace);

+    final String name = CollectionsUtil.<DefinedElement, String>lookup(referred, trace.definedElement2String);

+    VLSConstant _createVLSConstant = this.factory.createVLSConstant();

+    final Procedure1<VLSConstant> _function = (VLSConstant it) -> {

+      it.setName(name);

+    };

+    return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function);

   }

   

   protected VLSTerm _transformSymbolicReference(final ConstantDeclaration constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
index c8888eb0..72fea6d3 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
@@ -5,7 +5,6 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant;

-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;

@@ -177,9 +176,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
                 it.setFunctor(("eo" + Integer.valueOf(num)));

               };

               final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_3);

-              if (isNotEnum) {

-                trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor());

-              }

+              trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor());

               final VLSConstant cst = this.support.toConstant(cstTerm);

               trace.uniqueInstances.add(cst);

               VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

@@ -328,15 +325,12 @@ public class Logic2VampireLanguageMapper_TypeMapper {
     throw new UnsupportedOperationException("TODO: auto-generated method stub");

   }

   

-  protected VLSDoubleQuote transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) {

-    VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote();

-    final Procedure1<VLSDoubleQuote> _function = (VLSDoubleQuote it) -> {

-      String _name = referred.getName();

-      String _plus = ("\"a" + _name);

-      String _plus_1 = (_plus + "\"");

-      it.setValue(_plus_1);

+  protected VLSConstant transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) {

+    VLSConstant _createVLSConstant = this.factory.createVLSConstant();

+    final Procedure1<VLSConstant> _function = (VLSConstant it) -> {

+      it.setName(referred.getName());

     };

-    return ObjectExtensions.<VLSDoubleQuote>operator_doubleArrow(_createVLSDoubleQuote, _function);

+    return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function);

   }

   

   protected void getTypeInterpreter() {