1 files changed, 58 insertions, 46 deletions

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 e12180fa..4c4247ce 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
@@ -1,12 +1,12 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
 
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd
 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.VampireLanguageFactory
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
 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.logicproblem.LogicproblemPackage
 import java.util.ArrayList
@@ -14,7 +14,6 @@ import java.util.Collection
 import java.util.List
 
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
-import java.util.Collections
 
 class Logic2VampireLanguageMapper_TypeMapper {
         private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
@@ -28,10 +27,8 @@ class Logic2VampireLanguageMapper_TypeMapper {
 
         def protected transformTypes(Collection<Type> types, Collection<DefinedElement> elements,
                 Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) {
-
-//              val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes
-//              trace.typeMapperTrace = typeTrace
                 val VLSVariable variable = createVLSVariable => [it.name = "A"]
+                var globalCounter = 0
 
                 // 1. Each type (class) is a predicate with a single variable as input
                 for (type : types) {
@@ -39,94 +36,109 @@ class Logic2VampireLanguageMapper_TypeMapper {
                                 it.constant = support.toIDMultiple("t", type.name.split(" ").get(0))
                                 it.terms += support.duplicate(variable)
                         ]
-//                      typeTrace.type2Predicate.put(type, typePred)
                         trace.type2Predicate.put(type, typePred)
                 }
 
                 // 2. Map each ENUM type definition to fof formula
                 for (type : types.filter(TypeDefinition)) {
+
+                        // Create a VLSFunction for each Enum Element
                         val List<VLSFunction> orElems = newArrayList
                         for (e : type.elements) {
                                 val enumElemPred = createVLSFunction => [
                                         val splitName = e.name.split(" ")
-                                        if( splitName.length > 2) {
+                                        if (splitName.length > 2) {
                                                 it.constant = support.toIDMultiple("e", splitName.get(0), splitName.get(2))
-                                        }
-                                        else {
+                                        } else {
                                                 it.constant = support.toIDMultiple("e", splitName.get(0))
                                         }
                                         it.terms += support.duplicate(variable)
                                 ]
-//                              typeTrace.element2Predicate.put(e, enumElemPred)
                                 trace.element2Predicate.put(e, enumElemPred)
-                                orElems.add(enumElemPred)
                         }
 
+                        // Similar to InheritanceHierarchy for the Enum
+                        val List<VLSTerm> possibleNots = newArrayList
+                        val List<VLSTerm> typeDefs = newArrayList
+
+                        for (t1 : type.elements) {
+                                for (t2 : type.elements) {
+                                        if (t1 == t2) {
+                                                val fct = support.duplicate(t2.lookup(trace.element2Predicate), variable)
+                                                possibleNots.add(fct)
+                                        } else {
+                                                val op = support.duplicate(t2.lookup(trace.element2Predicate), variable)
+                                                val negFct = createVLSUnaryNegation => [
+                                                        it.operand = op
+                                                ]
+                                                possibleNots.add(negFct)
+                                        }
+                                }
+                                typeDefs.add(support.unfoldAnd(possibleNots))
+                                possibleNots.clear
+                        }
+
+                        // Implement Enum Inheritence Hierarchy
                         val res = createVLSFofFormula => [
                                 it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0))
-                                // below is temporary solution
                                 it.fofRole = "axiom"
                                 it.fofFormula = createVLSUniversalQuantifier => [
                                         it.variables += support.duplicate(variable)
                                         it.operand = createVLSEquivalent => [
                                                 it.left = type.lookup(trace.type2Predicate)
-                                                it.right = support.unfoldOr(orElems)
+                                                it.right = createVLSAnd => [
+                                                        it.left = support.topLevelTypeFunc(variable)
+                                                        it.right = support.unfoldOr(typeDefs)
+                                                ]
+//                                              it.right = support.unfoldOr((typeDefs))
+
                                         ]
                                 ]
-
                         ]
                         trace.specification.formulas += res
 
-                        // Create objects for the enum elements
-                        val List<VLSTerm> enumScopeElems = newArrayList
-                        for (var i = 0; i < type.elements.length; i++) {
+                        for (var i = globalCounter; i < globalCounter+type.elements.length; i++) {
+                                // Create objects for the enum elements
                                 val num = i + 1
                                 val cstTerm = createVLSFunctionAsTerm => [
                                         it.functor = "eo" + num
                                 ]
                                 val cst = support.toConstant(cstTerm)
                                 trace.uniqueInstances.add(cst)
-                                val fct = support.duplicate(type.elements.get(i).lookup(trace.element2Predicate), cstTerm)
-                                enumScopeElems.add(fct)
-                                
-                                //For paradox Only
-                                for (var j = 0; j < type.elements.length; j++) {
-                                        if(j != i) {
-                                                val op = support.duplicate(type.elements.get(j).lookup(trace.element2Predicate), cstTerm)
-                                                val negFct = createVLSUnaryNegation => [
-                                                        it.operand = op
+
+                                val index = i
+                                val enumScope = createVLSFofFormula => [
+                                        it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0),
+                                                type.elements.get(index).name.split(" ").get(0))
+                                        it.fofRole = "axiom"
+                                        it.fofFormula = createVLSUniversalQuantifier => [
+                                                it.variables += support.duplicate(variable)
+                                                it.operand = createVLSEquivalent => [
+                                                        it.left = createVLSEquality => [
+                                                                it.left = support.duplicate(variable)
+                                                                it.right = support.duplicate(support.toConstant(cstTerm))
+                                                        ]
+                                                        it.right = support.duplicate(type.elements.get(index).lookup(trace.element2Predicate),
+                                                                variable)
                                                 ]
-                                                enumScopeElems.add(negFct)
-                                        }
-                                }
-                                //End Paradox
-//                              enumScopeElems.add(support.topLevelTypeFunc(cstTerm))
+                                        ]
+                                ]
+
+                                trace.specification.formulas += enumScope
+
                         }
-                        
-                        
-                        
-                        val enumScope = createVLSFofFormula => [
-                                it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0))
-                                // below is temporary solution
-                                it.fofRole = "axiom"                    
-                                it.fofFormula = support.unfoldAnd(enumScopeElems)
-                        ]
-                        
-                        trace.specification.formulas += enumScope
+                        globalCounter+=type.elements.size
                 }
 
                 // HIERARCHY HANDLER
                 // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates
                 // and store in a map
-//              println(types.filter[!isIsAbstract])
-                for (t1 : types.filter[!isIsAbstract].filter(TypeDeclaration)) {
+                for (t1 : types.filter[!isIsAbstract]) {
                         for (t2 : types) {
                                 // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes
                                 if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) {
-//                                      typeTrace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(typeTrace.type2Predicate)))
                                         trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate)))
                                 } else {
-//                                      typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
                                         trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
                                                 it.operand = support.duplicate(t2.lookup(trace.type2Predicate))
                                         ])