VAMPIRE: implement Vampire Model Interpreter, 2/3 done

19 files changed, 179 insertions, 41 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
index e94584ae..7ab15fba 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
@@ -35,6 +35,7 @@ class Logic2VampireLanguageMapperTrace {
         public var topLevelType = null
         
         public val Map<Type, VLSFunction> type2Predicate = new HashMap;
+        public val Map<VLSFunction, Type> predicate2Type = new HashMap;
         public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap
         public val Map<Type, VLSTerm> type2PossibleNot = new HashMap
         public val Map<Type, VLSTerm> type2And = new HashMap
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 1b30393f..d2a01e0e 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
@@ -42,6 +42,7 @@ class Logic2VampireLanguageMapper_TypeMapper {
                                 it.terms += support.duplicate(variable)
                         ]
                         trace.type2Predicate.put(type, typePred)
+                        trace.predicate2Type.put(typePred, type)
                 }
 
                 // 2. Map each ENUM/InitialModelElement type definition to fof formula
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 c2cffa6b..0c93e3fe 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
@@ -1,49 +1,182 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
 
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSAndImpl
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSOrImpl
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSUnaryNegationImpl
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDeclarationImpl
+import java.util.HashMap
+import java.util.List
+import java.util.Map
+
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
 
 class VampireModelInterpretation implements LogicModelInterpretation {
         protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
-        
+
         protected val Logic2VampireLanguageMapperTrace forwardTrace;
-        
-        
+
+        private val Map<String, DefinedElement> name2DefinedElement = new HashMap
+        private val Map<TypeDeclaration, List<DefinedElement>> type2DefinedElement = new HashMap
+
+        var num = -1
+
         public new(VampireModel model, Logic2VampireLanguageMapperTrace trace) {
                 this.forwardTrace = trace
+
+                // 1. look at "finite_domain" formula (there should only be one)
+                // IN REALITY THE DEFINED ELEMENTS ARE DEFINED AS <nameOfDefinedEement>:$i
+                // SPECIFICALLY, THESE ARE "TYPE" FORMULAS
+                val finDomFormula = model.tfformulas.filter[name == "finite_domain"].get(0) as VLSTffFormula
+                val univQuant = finDomFormula.fofFormula as VLSUniversalQuantifier
+                var orFormulaTerm = univQuant.operand
+
+                var end = false
+                while (!end) {
+                        if (orFormulaTerm.class == VLSOrImpl) {
+                                val orFormula = orFormulaTerm as VLSOr
+                                val orRight = orFormula.right as VLSEquality
+                                add2ConstDefMap(orRight)
+                                orFormulaTerm = orFormula.left
+                        } else {
+                                val firstTerm = orFormulaTerm as VLSEquality
+                                add2ConstDefMap(firstTerm)
+                                end = true
+                        }
+
+                }
+
+                // 2. associate each type to defined elements
+//              println(trace.type2Predicate.keySet)
+//              println(trace.type2Predicate.keySet.length)
+//              println(trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl])
+//              println(trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl].length)
+//              println()
+//              println(trace.type2Predicate)
+                // Fill keys of map
+                val allTypeDecls = trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl]
+                val allTypeFunctions = trace.predicate2Type
+
+                for (type : allTypeDecls) {
+                        type2DefinedElement.put(type as TypeDeclaration, newArrayList)
+                }
+
+                // USE THE DECLARE_<TYPE_NAME> FORMULAS TO SEE WHAT THE TYPES ARE
+                val typeFormulas = model.tfformulas.filter[name.length > 12 && name.substring(0, 12) == "predicate_t_"]
+                // ^this way, we ignore the "object" type
+                //TODO potentially need to handle the enums in this case as well
+                for (formula : typeFormulas) {
+                        // get associated type
+                        val associatedTypeName = (formula as VLSTffFormula).name.substring(10)
+                        val associatedFunction = allTypeFunctions.keySet.filter[constant == associatedTypeName].
+                                get(0) as VLSFunction
+                        val associatedTypeAll = associatedFunction.lookup(allTypeFunctions)
+//                      val associatedTypeDeclFormula = model.tfformulas.filter[name == ("declare_t_" + associatedTypeName)].get(0) as VLSTffFormula
+//                      val associatedTypeDefn = associatedTypeDeclFormula.fofFormula as VLSOtherDeclaration
+//                      val associatedTypeFct = associatedTypeDefn.name as VLSConstant
+                        if (associatedTypeAll.class == TypeDeclarationImpl) {
+                                val associatedType = associatedTypeAll as TypeDeclaration
+
+                                // get definedElements
+                                var andFormulaTerm = formula.fofFormula
+                                end = false
+                                val List<DefinedElement> instances = newArrayList
+                                while (!end) {
+                                        if (andFormulaTerm.class == VLSAndImpl) {
+                                                val andFormula = andFormulaTerm as VLSAnd
+                                                val andRight = andFormula.right
+                                                addIfNotNeg(andRight, instances)
+                                                andFormulaTerm = andFormula.left
+                                        } else {
+                                                addIfNotNeg(andFormulaTerm as VLSTerm, instances)
+                                                end = true
+                                        }
+
+                                }
+                                for (elem : instances) {
+                                        associatedType.lookup(type2DefinedElement).add(elem)
+                                }
+                        }
+                }
+
+                printMap()
+
         }
-        
-        override getElements(Type type) {
-                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+
+        def printMap() {
+                for (key : type2DefinedElement.keySet) {
+                        println(key.name + "==>")
+                        for (elem : key.lookup(type2DefinedElement)) {
+                                print(elem.name + ", ")
+                        }
+                        println()
+
+                }
+                println()
         }
-        
+
+        def private addIfNotNeg(VLSTerm term, List<DefinedElement> list) {
+                if (term.class != VLSUnaryNegationImpl) {
+                        val nodeName = ((term as VLSFunction).terms.get(0) as VLSFunctionAsTerm).functor
+                        val defnElem = nodeName.lookup(name2DefinedElement)
+                        list.add(defnElem)
+                }
+        }
+
+        def private add2ConstDefMap(VLSEquality eq) {
+                val defElemConst = (eq.right as VLSConstant)
+                val definedElement = createDefinedElement => [name = defElemConst.name]
+                this.name2DefinedElement.put(defElemConst.name, definedElement)
+        }
+
+        override getElements(Type type) { getElementsDispatch(type) }
+
+        def private dispatch getElementsDispatch(TypeDeclaration declaration) {
+                return declaration.lookup(this.type2DefinedElement)
+        }
+
+        def private dispatch getElementsDispatch(TypeDefinition declaration) { return declaration.elements }
+
         override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) {
                 throw new UnsupportedOperationException("TODO: auto-generated method stub")
         }
-        
+
         override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) {
                 throw new UnsupportedOperationException("TODO: auto-generated method stub")
         }
-        
+
         override getInterpretation(ConstantDeclaration constant) {
                 throw new UnsupportedOperationException("TODO: auto-generated method stub")
         }
-        
+
         override getAllIntegersInStructure() {
-                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+                return null
         }
-        
+
         override getAllRealsInStructure() {
-                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+                return null
         }
-        
+
         override getAllStringsInStructure() {
-                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+                return null
         }
-        
-}
\ No newline at end of file
+
+}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
index 298a6c08..0fafa9e9 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
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 863b572e..7174bfba 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/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
index 410f2550..af66dabc 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
index b1b39a4f..b9301875 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
index 3710e753..88c3e932 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
index 9dc7abaf..e3437e53 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.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 7029d196..1a884261 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 03aead59..7e2aba1c 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_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 62960704..187a0447 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/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
index 56a10b3c..ee115b16 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
index c2ae099e..4537240e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
@@ -37,6 +37,8 @@ public class Logic2VampireLanguageMapperTrace {
   

   public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>();

   

+  public final Map<VLSFunction, Type> predicate2Type = new HashMap<VLSFunction, Type>();

+  

   public final Map<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>();

   

   public final Map<Type, VLSTerm> type2PossibleNot = new HashMap<Type, VLSTerm>();

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
index 7daf1b2f..2100b92f 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
@@ -12,10 +12,10 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;

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

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

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm;

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

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

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

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

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

 import com.google.common.base.Objects;

 import com.google.common.collect.Iterables;

@@ -123,7 +123,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
       it.setFofRole("axiom");

       VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

       final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> {

-        EList<VLSVariableDeclaration> _variables = it_1.getVariables();

+        EList<VLSTffTerm> _variables = it_1.getVariables();

         VLSVariable _duplicate = this.support.duplicate(this.variable);

         _variables.add(_duplicate);

         VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

@@ -193,10 +193,10 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
           it.setFofRole("axiom");

           VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();

           final Procedure1<VLSExistentialQuantifier> _function_5 = (VLSExistentialQuantifier it_1) -> {

-            EList<VLSVariableDeclaration> _variables = it_1.getVariables();

+            EList<VLSTffTerm> _variables = it_1.getVariables();

             VLSVariable _duplicate = this.support.duplicate(varA);

             _variables.add(_duplicate);

-            EList<VLSVariableDeclaration> _variables_1 = it_1.getVariables();

+            EList<VLSTffTerm> _variables_1 = it_1.getVariables();

             VLSVariable _duplicate_1 = this.support.duplicate(varB);

             _variables_1.add(_duplicate_1);

             VLSImplies _createVLSImplies = this.factory.createVLSImplies();

@@ -206,10 +206,10 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
               final Procedure1<VLSUnaryNegation> _function_7 = (VLSUnaryNegation it_3) -> {

                 VLSExistentialQuantifier _createVLSExistentialQuantifier_1 = this.factory.createVLSExistentialQuantifier();

                 final Procedure1<VLSExistentialQuantifier> _function_8 = (VLSExistentialQuantifier it_4) -> {

-                  EList<VLSVariableDeclaration> _variables_2 = it_4.getVariables();

+                  EList<VLSTffTerm> _variables_2 = it_4.getVariables();

                   VLSVariable _duplicate_2 = this.support.duplicate(varC);

                   _variables_2.add(_duplicate_2);

-                  EList<VLSVariableDeclaration> _variables_3 = it_4.getVariables();

+                  EList<VLSTffTerm> _variables_3 = it_4.getVariables();

                   VLSVariable _duplicate_3 = this.support.duplicate(varB);

                   _variables_3.add(_duplicate_3);

                   it_4.setOperand(this.support.duplicate(rel, CollectionLiterals.<VLSVariable>newArrayList(varC, varB)));

@@ -240,7 +240,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
           it.setFofRole("axiom");

           VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

           final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> {

-            EList<VLSVariableDeclaration> _variables = it_1.getVariables();

+            EList<VLSTffTerm> _variables = it_1.getVariables();

             VLSVariable _duplicate = this.support.duplicate(varA);

             _variables.add(_duplicate);

             VLSImplies _createVLSImplies = this.factory.createVLSImplies();

@@ -248,7 +248,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
               it_2.setLeft(this.support.duplicate(e.getKey(), varA));

               VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();

               final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_3) -> {

-                EList<VLSVariableDeclaration> _variables_1 = it_3.getVariables();

+                EList<VLSTffTerm> _variables_1 = it_3.getVariables();

                 VLSVariable _duplicate_1 = this.support.duplicate(varB);

                 _variables_1.add(_duplicate_1);

                 int _length_1 = ((Object[])Conversions.unwrapArray(e.getValue(), Object.class)).length;

@@ -308,9 +308,9 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
           final Procedure1<VLSUnaryNegation> _function_6 = (VLSUnaryNegation it_1) -> {

             VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();

             final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_2) -> {

-              EList<VLSVariableDeclaration> _variables = it_2.getVariables();

+              EList<VLSTffTerm> _variables = it_2.getVariables();

               List<VLSVariable> _duplicate = this.support.duplicate(variables);

-              Iterables.<VLSVariableDeclaration>addAll(_variables, _duplicate);

+              Iterables.<VLSTffTerm>addAll(_variables, _duplicate);

               it_2.setOperand(this.support.unfoldAnd(conjunctionList));

             };

             VLSExistentialQuantifier _doubleArrow_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_7);

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
index 657c3292..8d36952b 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
@@ -7,9 +7,9 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;

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

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

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm;

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

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

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

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

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation;

@@ -77,7 +77,7 @@ public class Logic2VampireLanguageMapper_RelationMapper {
       VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

       final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> {

         for (final VLSVariable v : relVar2VLS) {

-          EList<VLSVariableDeclaration> _variables = it_1.getVariables();

+          EList<VLSTffTerm> _variables = it_1.getVariables();

           VLSVariable _duplicate = this.support.duplicate(v);

           _variables.add(_duplicate);

         }

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 6d4767a7..6da75271 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
@@ -11,9 +11,9 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;

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

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

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm;

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

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

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

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

 import com.google.common.base.Objects;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement;

@@ -245,7 +245,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
       it.setFofRole("axiom");

       VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

       final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> {

-        EList<VLSVariableDeclaration> _variables = it_1.getVariables();

+        EList<VLSTffTerm> _variables = it_1.getVariables();

         VLSVariable _duplicate = this.support.duplicate(this.variable);

         _variables.add(_duplicate);

         VLSImplies _createVLSImplies = this.factory.createVLSImplies();

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
index 6cd53fae..dae0df6e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
@@ -11,9 +11,9 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality;

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

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

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm;

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

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

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

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

 import com.google.common.base.Objects;

 import com.google.common.collect.Iterables;

@@ -324,9 +324,9 @@ public class Logic2VampireLanguageMapper_Support {
       if (isUniversal) {

         VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

         final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it) -> {

-          EList<VLSVariableDeclaration> _variables = it.getVariables();

+          EList<VLSTffTerm> _variables = it.getVariables();

           Collection<VLSVariable> _values = variableMap.values();

-          Iterables.<VLSVariableDeclaration>addAll(_variables, _values);

+          Iterables.<VLSTffTerm>addAll(_variables, _values);

           VLSImplies _createVLSImplies = this.factory.createVLSImplies();

           final Procedure1<VLSImplies> _function_2 = (VLSImplies it_1) -> {

             it_1.setLeft(this.unfoldAnd(typedefs));

@@ -342,9 +342,9 @@ public class Logic2VampireLanguageMapper_Support {
           typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap)));

           VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();

           final Procedure1<VLSExistentialQuantifier> _function_2 = (VLSExistentialQuantifier it) -> {

-            EList<VLSVariableDeclaration> _variables = it.getVariables();

+            EList<VLSTffTerm> _variables = it.getVariables();

             Collection<VLSVariable> _values = variableMap.values();

-            Iterables.<VLSVariableDeclaration>addAll(_variables, _values);

+            Iterables.<VLSTffTerm>addAll(_variables, _values);

             it.setOperand(this.unfoldAnd(typedefs));

           };

           _xblockexpression_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_2);

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 7921f204..c8888eb0 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
@@ -12,10 +12,10 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;

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

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

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm;

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

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

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

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

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

 import com.google.common.base.Objects;

 import com.google.common.collect.Iterables;

@@ -76,6 +76,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
           };

           final VLSFunction typePred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);

           trace.type2Predicate.put(type, typePred);

+          trace.predicate2Type.put(typePred, type);

         }

       }

       final Function1<TypeDefinition, Boolean> _function_1 = (TypeDefinition it) -> {

@@ -144,7 +145,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
             it.setFofRole("axiom");

             VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

             final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> {

-              EList<VLSVariableDeclaration> _variables = it_1.getVariables();

+              EList<VLSTffTerm> _variables = it_1.getVariables();

               VLSVariable _duplicate = this.support.duplicate(variable);

               _variables.add(_duplicate);

               VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

@@ -194,7 +195,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
                 it.setFofRole("axiom");

                 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

                 final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> {

-                  EList<VLSVariableDeclaration> _variables = it_1.getVariables();

+                  EList<VLSTffTerm> _variables = it_1.getVariables();

                   VLSVariable _duplicate = this.support.duplicate(variable);

                   _variables.add(_duplicate);

                   VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

@@ -264,7 +265,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
         it.setFofRole("axiom");

         VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

         final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> {

-          EList<VLSVariableDeclaration> _variables = it_1.getVariables();

+          EList<VLSTffTerm> _variables = it_1.getVariables();

           VLSVariable _duplicate = this.support.duplicate(variable);

           _variables.add(_duplicate);

           VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

@@ -292,7 +293,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
         it.setFofRole("axiom");

         VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

         final Procedure1<VLSUniversalQuantifier> _function_6 = (VLSUniversalQuantifier it_1) -> {

-          EList<VLSVariableDeclaration> _variables = it_1.getVariables();

+          EList<VLSTffTerm> _variables = it_1.getVariables();

           VLSVariable _duplicate = this.support.duplicate(variable);

           _variables.add(_duplicate);

           VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();