VAMPIRE: Implement wf constraint handling

5 files changed, 194 insertions, 163 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 a2449fc0..14926280 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
@@ -1,5 +1,10 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
 
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion
@@ -21,18 +26,14 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDefinitionImpl
 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel
 import java.util.Collections
 import java.util.HashMap
 import java.util.List
@@ -40,7 +41,7 @@ import java.util.Map
 import org.eclipse.xtend.lib.annotations.Accessors
 
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl
 
 class Logic2VampireLanguageMapper {
         private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
@@ -81,7 +82,8 @@ class Logic2VampireLanguageMapper {
                 
                 // RELATION MAPPER
                 trace.relationDefinitions = problem.collectRelationDefinitions
-                problem.relations.forEach[this.relationMapper.transformRelation(it, trace)]
+//              println(problem.relations.filter[class == RelationDefinitionImpl])
+                problem.relations.forEach[this.relationMapper.transformRelation(it, trace, new Logic2VampireLanguageMapper)]
                 
                 // CONTAINMENT MAPPER
                 containmentMapper.transformContainment(config,problem.containmentHierarchies, trace)
@@ -140,7 +142,7 @@ class Logic2VampireLanguageMapper {
         // ////////////
         def protected transformAssertion(Assertion assertion, Logic2VampireLanguageMapperTrace trace) {
                 val res = createVLSFofFormula => [
-                        it.name = support.toID(assertion.name)
+                        it.name = support.toID("assertion_" + assertion.name)
                         // below is temporary solution
                         it.fofRole = "axiom"
                         it.fofFormula = assertion.value.transformTerm(trace, Collections.EMPTY_MAP)
@@ -378,8 +380,18 @@ class Logic2VampireLanguageMapper {
 //                                              it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate)
 //                                              it.params += parameterSubstitutions.map[p|p.transformTerm(trace, variables)]
 //                                      ]
+//              println(relation.name)
+//              if(relation.class == RelationDefinitionImpl) {
+//                      println("(" + (relation as RelationDefinition).getDefines + ")")
+//              }
                 return createVLSFunction => [
-                        it.constant = (relation as RelationDeclaration).lookup(trace.rel2Predicate).constant
+                        if (relation.class == RelationDeclarationImpl) {
+                                                        it.constant = (relation as RelationDeclaration).lookup(trace.rel2Predicate).constant
+                        }
+                        else {
+                                it.constant = (relation as RelationDefinition).lookup(trace.relDef2Predicate).constant
+                        }
+                        
                         it.terms += parameterSubstitutions.map[p|p.transformTerm(trace, variables)]
                 ]
         }
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 6b383b12..13778dee 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
@@ -47,6 +47,8 @@ class Logic2VampireLanguageMapperTrace {
         public var Map<RelationDeclaration, RelationDefinition> relationDefinitions
         public var Map<RelationDeclaration, VLSFunction> rel2Predicate = new HashMap
         public var Map<VLSFunction, RelationDeclaration> predicate2Relation = new HashMap
+        public var Map<RelationDefinition, VLSFunction> relDef2Predicate = new HashMap
+        public var Map<VLSFunction, RelationDefinition> predicate2RelDef = new HashMap
         
         
 //NOT NEEDED    //public var VLSFunction constantDec
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_AssertionMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_AssertionMapper.xtend
new file mode 100644
index 00000000..cf218270
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_AssertionMapper.xtend
@@ -0,0 +1,5 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+
+class Logic2VampireLanguageMapper_AssertionMapper {
+        
+}
\ No newline at end of file
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
index 18e97020..181c59ca 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
@@ -1,14 +1,12 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
 
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
+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.RelationDeclaration
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
 import java.util.ArrayList
 import java.util.HashMap
 import java.util.List
@@ -25,7 +23,7 @@ class Logic2VampireLanguageMapper_RelationMapper {
                 this.base = base
         }
 
-        def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace) {
+        def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace, Logic2VampireLanguageMapper mapper) {
 
                 // 1. store all variables in support wrt their name
                 // 1.1 if variable has type, creating list of type declarations
@@ -81,91 +79,79 @@ class Logic2VampireLanguageMapper_RelationMapper {
                 trace.specification.formulas += comply
         }
 
-        def dispatch public void transformRelation(RelationDefinition reldef, Logic2VampireLanguageMapperTrace trace) {
-
-//              // 1. store all variables in support wrt their name
-//              // 1.1 if variable has type, creating list of type declarations
-////            val VLSVariable variable = createVLSVariable => [it.name = "A"]
-//              val Map<Variable, VLSVariable> relationVar2VLS = new HashMap
-//              val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap
-//              val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap
-//              val typedefs = new ArrayList<VLSTerm>
-//
-//              for (variable : reldef.variables) {
-//                      val v = createVLSVariable => [
-//                              it.name = support.toIDMultiple("V", variable.name)
-//                      ]
-//                      relationVar2VLS.put(variable, v)
-//
-//                      val varTypeComply = createVLSFunction => [
-//                              it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
-//                              it.terms += support.duplicate(v)
-//                      ]
-//                      relationVar2TypeDecComply.put(variable, varTypeComply)
-//                      relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply))
-//              }
-//              val nameArray = reldef.name.split(" ")
-//              val comply = createVLSFofFormula => [
-//                      it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2),
-//                              nameArray.get(nameArray.length - 1))
-//                      it.fofRole = "axiom"
-//                      it.fofFormula = createVLSUniversalQuantifier => [
-//                              for (variable : reldef.variables) {
-//                                      it.variables += support.duplicate(variable.lookup(relationVar2VLS))
-//
-//                              }
-//                              it.operand = createVLSImplies => [
-//                                      it.left = createVLSFunction => [
-//                                              it.constant = support.toIDMultiple("rel", reldef.name)
-//                                              for (variable : reldef.variables) {
-//                                                      val v = createVLSVariable => [
-//                                                              it.name = variable.lookup(relationVar2VLS).name
-//                                                      ]
-//                                                      it.terms += v
-//                                              }
-//                                      ]
-//                                      it.right = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecComply.values))
-//                              ]
-//                      ]
-//              ]
-//
-//              val res = createVLSFofFormula => [
-//                      it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2),
-//                              nameArray.get(nameArray.length - 1))
-//                      it.fofRole = "axiom"
-//                      it.fofFormula = createVLSUniversalQuantifier => [
-//                              for (variable : reldef.variables) {
-//                                      val v = createVLSVariable => [
-//                                              it.name = variable.lookup(relationVar2VLS).name
-//                                      ]
-//                                      it.variables += v
-//
-//                              }
-//                              it.operand = createVLSImplies => [
-//                                      it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values))
-//                                      it.right = createVLSEquivalent => [
-//                                              it.left = createVLSFunction => [
-//                                                      it.constant = support.toIDMultiple("rel", reldef.name)
-//                                                      for (variable : reldef.variables) {
-//                                                              val v = createVLSVariable => [
-//                                                                      it.name = variable.lookup(relationVar2VLS).name
-//                                                              ]
-//                                                              it.terms += v
-//
-//                                                      }
-//                                              ]
-//                                              it.right = base.transformTerm(reldef.value, trace, relationVar2VLS)
-//                                      ]
-//
-//                              ]
-//
-//                      ]
-//
-//              ]
-//
-//              // trace.relationDefinition2Predicate.put(r,res)
-//              trace.specification.formulas += comply;
-//              trace.specification.formulas += res;
+        def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace, Logic2VampireLanguageMapper mapper) {
+                
+//              println("XXXXXXXXXXXXXXXXX")
+
+// 1. store all variables in support wrt their name
+                // 1.1 if variable has type, creating list of type declarations
+                val Map<Variable, VLSVariable> relVar2VLS = new HashMap
+                val List<VLSVariable> vars = newArrayList
+                val List<VLSFunction> relVar2TypeDecComply = new ArrayList
+                for (i : 0 ..< r.parameters.length) {
+
+                        val v = createVLSVariable => [
+                                it.name = support.toIDMultiple("V", i.toString)
+                        ]
+                        relVar2VLS.put(r.variables.get(i), v)
+                        vars.add(v)
+
+                        val relType = (r.parameters.get(i) as ComplexTypeReference).referred
+                        val varTypeComply = support.duplicate(relType.lookup(trace.type2Predicate), v)
+                        relVar2TypeDecComply.add(varTypeComply)
+
+                }
+
+                //deciding name of relation
+                val nameArray = r.name.split(" ")
+                var relNameVar = ""
+                if (nameArray.length == 3) {
+                        relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2))
+                }
+                else {
+                        relNameVar = r.name
+                }
+                val relName = relNameVar
+                
+                //define logic for pattern
+//              val map = new HashMap
+//              map.put(r.variables.get(0), createVLSVariable)
+                val definition = mapper.transformTerm(r.value, trace, relVar2VLS)
+                
+                
+                
+                
+                //get entire contents of and
+                val compliance = support.unfoldAnd(relVar2TypeDecComply)
+                val compDefn = createVLSAnd=> [
+                        it.left = compliance
+                        it.right = definition
+                ]
+                
+                val relDef = createVLSFofFormula=> [
+                        
+                        it.name = support.toID(relName)
+                        it.fofRole = "axiom"
+                        it.fofFormula = createVLSUniversalQuantifier => [
+                                for (v : vars) {
+                                        it.variables += support.duplicate(v)
+                                }
+                                it.operand = createVLSImplies => [
+                                        val rel = createVLSFunction => [
+                                                it.constant = support.toIDMultiple("r", relName)
+                                                for (v : vars) {
+                                                        it.terms += support.duplicate(v)
+                                                }
+                                        ]
+                                        trace.relDef2Predicate.put(r, rel)
+                                        trace.predicate2RelDef.put(rel, r)
+                                        it.left = support.duplicate(rel)
+                                        it.right = compDefn
+                                ]
+                        ]
+                ]
+
+                trace.specification.formulas += relDef
 
         }
 
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 5df47bbc..ef77b6ca 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
@@ -24,26 +24,28 @@ 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.RelationDeclarationImpl
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDeclarationImpl
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl
 import java.util.Arrays
 import java.util.HashMap
 import java.util.List
 import java.util.Map
-import java.util.Set
 
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
+import java.util.concurrent.TimeUnit
 
 class VampireModelInterpretation implements LogicModelInterpretation {
         protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
 
         protected val Logic2VampireLanguageMapperTrace forwardTrace;
 
-        //These three maps capture all the information found in the Vampire output
+        // These three maps capture all the information found in the Vampire output
         private val Map<String, DefinedElement> name2DefinedElement = new HashMap
         private val Map<TypeDeclaration, List<DefinedElement>> type2DefinedElement = new HashMap
-        private val Map<RelationDeclaration, List<String[]>> rel2Inst = new HashMap
-        //end
+        private val Map<RelationDeclaration, List<String[]>> relDec2Inst = new HashMap
+        private val Map<RelationDefinition, List<String[]>> relDef2Inst = new HashMap
 
+        // end
         public new(VampireModel model, Logic2VampireLanguageMapperTrace trace) {
                 this.forwardTrace = trace
 
@@ -77,6 +79,7 @@ class VampireModelInterpretation implements LogicModelInterpretation {
 //              println()
 //              println(trace.type2Predicate)
                 // Fill keys of map
+                println(trace.type2Predicate.keySet)
                 val allTypeDecls = trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl]
                 val allTypeFunctions = trace.predicate2Type
                 println(trace.type2Predicate.keySet.filter[class == TypeDefinitionImpl])
@@ -86,52 +89,64 @@ class VampireModelInterpretation implements LogicModelInterpretation {
                 }
 
                 // 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_"]
+                val typeFormulas = model.tfformulas.filter [
+                        name.length > 12 && (name.substring(0, 12) == "predicate_t_" || name.substring(0, 12) == "predicate_e_")
+                ]
                 // ^this way, we ignore the "object" type
-                //TODO potentially need to handle the enums in this case as well
+                // 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)
+                        print(associatedTypeName)
+                        val associatedFunctions = allTypeFunctions.keySet.filter[constant == associatedTypeName]
+                        if (associatedFunctions.length > 0) {
+                                val associatedFunction = associatedFunctions.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
+                                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
+                                                }
 
-                                // 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)
+                                        for (elem : instances) {
+                                                associatedType.lookup(type2DefinedElement).add(elem)
+                                        }
                                 }
                         }
+
                 }
-                
+
                 printMap()
-                
+
                 // 3. get relations
                 // Fill keys of map
-                val allRelDecls = trace.rel2Predicate.keySet.filter[class == RelationDeclarationImpl]
-                val allRelFunctions = trace.predicate2Relation
+                val allRelDecls = trace.rel2Predicate.keySet
+                val allRelDefns = trace.relDef2Predicate.keySet
+                val allRelDeclFunctions = trace.predicate2Relation
+                val allRelDefnFunctions = trace.predicate2RelDef
 
                 for (rel : allRelDecls) {
-                        rel2Inst.put(rel as RelationDeclaration, newArrayList)
+                        relDec2Inst.put(rel as RelationDeclaration, newArrayList)
+                }
+
+                for (rel : allRelDefns) {
+                        relDef2Inst.put(rel as RelationDefinition, newArrayList)
                 }
 
                 // USE THE DECLARE_<RELATION_NAME> FORMULAS TO SEE WHAT THE RELATIONS ARE
@@ -140,34 +155,40 @@ class VampireModelInterpretation implements LogicModelInterpretation {
                 for (formula : relFormulas) {
                         // get associated type
                         val associatedRelName = (formula as VLSTffFormula).name.substring(10)
-                        val associatedRelFunction = allRelFunctions.keySet.filter[constant == associatedRelName].
-                                get(0) as VLSFunction
-                        val associatedRel = associatedRelFunction.lookup(allRelFunctions) as RelationDeclaration
-
-                        // get definedElements
-                        var andFormulaTerm = formula.fofFormula
-                        end = false
-                        val List<String[]> instances = newArrayList
-                        while (!end) {
-                                if (andFormulaTerm.class == VLSAndImpl) {
-                                        val andFormula = andFormulaTerm as VLSAnd
-                                        val andRight = andFormula.right
-                                        addRelIfNotNeg(andRight, instances)
-                                        andFormulaTerm = andFormula.left
-                                } else {
-                                        addRelIfNotNeg(andFormulaTerm as VLSTerm, instances)
-                                        end = true
+
+                        // TRY FOR DECLARATION
+                        val associatedRelFunctionList = allRelDeclFunctions.keySet.filter[constant == associatedRelName]
+                        if (associatedRelFunctionList.isEmpty) {
+                                // THEN IT IS NOT A DECLARATION
+                        } else {
+                                val associatedRelFunction = associatedRelFunctionList.get(0) as VLSFunction // ASSUMING ONLY 1 SATISFIES QUERY
+                                val associatedRel = associatedRelFunction.lookup(allRelDeclFunctions) as RelationDeclaration
+
+                                // get definedElements
+                                var andFormulaTerm = formula.fofFormula
+                                end = false
+                                val List<String[]> instances = newArrayList
+                                while (!end) {
+                                        if (andFormulaTerm.class == VLSAndImpl) {
+                                                val andFormula = andFormulaTerm as VLSAnd
+                                                val andRight = andFormula.right
+                                                addRelIfNotNeg(andRight, instances)
+                                                andFormulaTerm = andFormula.left
+                                        } else {
+                                                addRelIfNotNeg(andFormulaTerm as VLSTerm, instances)
+                                                end = true
+                                        }
+
+                                }
+                                for (elem : instances) {
+                                        associatedRel.lookup(relDec2Inst).add(elem)
                                 }
 
                         }
-                        for (elem : instances) {
-                                associatedRel.lookup(rel2Inst).add(elem)
-                        }
 
                 }
 
 //              printMap2()
-
         }
 
         def printMap() {
@@ -182,12 +203,12 @@ class VampireModelInterpretation implements LogicModelInterpretation {
                 }
                 println()
         }
-        
+
         def printMap2() {
                 println("------------------")
-                for (key : rel2Inst.keySet) {
+                for (key : relDec2Inst.keySet) {
                         println(key.name + "==>")
-                        for (elem : key.lookup(rel2Inst)) {
+                        for (elem : key.lookup(relDec2Inst)) {
                                 print("[" + elem.get(0) + "-" + elem.get(1) + "], ")
                         }
                         println()
@@ -203,7 +224,7 @@ class VampireModelInterpretation implements LogicModelInterpretation {
                         list.add(defnElem)
                 }
         }
-        
+
         def private addRelIfNotNeg(VLSTerm term, List<String[]> list) {
                 if (term.class != VLSUnaryNegationImpl) {
                         val nodeName1 = ((term as VLSFunction).terms.get(0) as VLSFunctionAsTerm).functor
@@ -232,14 +253,19 @@ class VampireModelInterpretation implements LogicModelInterpretation {
         }
 
         override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) {
+                print("-- " + relation.name)
                 val node1 = (parameterSubstitution.get(0) as DefinedElement).name
                 val node2 = (parameterSubstitution.get(1) as DefinedElement).name
-                val realRelations = relation.lookup(rel2Inst)
-                for (real : realRelations){
-                        if(real.contains(node1) && real.contains(node2)){
+                val realRelations = relation.lookup(relDec2Inst)
+                for (real : realRelations) {
+                        if (real.contains(node1) && real.contains(node2)) {
+                                println("  true")
+                                TimeUnit.SECONDS.sleep(1)
                                 return true
                         }
                 }
+                println("  false")
+                TimeUnit.SECONDS.sleep(1)
                 return false
         }