1 files changed, 0 insertions, 153 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
deleted file mode 100644
index ea72940e..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
+++ /dev/null
@@ -1,153 +0,0 @@
-package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
-
-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.TypeDefinition
-import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
-import java.util.ArrayList
-import java.util.Collection
-
-import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
-import java.util.List
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
-
-class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper {
-        private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
-        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
-
-        new() {
-                LogicproblemPackage.eINSTANCE.class
-        }
-
-        override 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"]
-
-                // 1. Each type (class) is a predicate with a single variable as input
-                for (type : types) {
-                        val typePred = createVLSFunction => [
-                                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)) {
-                        val List<VLSFunction> orElems = newArrayList
-                        for (e : type.elements) {
-                                val enumElemPred = createVLSFunction => [
-                                        it.constant = support.toIDMultiple("e", e.name.split(" ").get(0), e.name.split(" ").get(2))
-                                        it.terms += support.duplicate(variable)
-                                ]
-//                              typeTrace.element2Predicate.put(e, enumElemPred)
-                                trace.element2Predicate.put(e, enumElemPred)
-                                orElems.add(enumElemPred)
-                        }
-
-                        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 = createVLSFunction => [
-//                                                      it.constant = type.lookup(typeTrace.type2Predicate).constant
-//                                                      it.terms += createVLSVariable => [it.name = "A"]
-//                                              ]
-//                                              it.left = type.lookup(typeTrace.type2Predicate)
-                                                it.left = type.lookup(trace.type2Predicate)
-
-                                                it.right = support.unfoldOr(orElems)
-
-                                        // TEMPPPPPPP
-//                                              it.right = support.unfoldOr(type.elements.map [e |
-//                                                      
-//                                                      createVLSEquality => [
-//                                                              it.left = support.duplicate(variable)
-//                                                              it.right = createVLSDoubleQuote => [
-//                                                                      it.value = "\"a" + e.name + "\""
-//                                                              ]
-//                                                      ]
-//                                              ])
-                                        // END TEMPPPPP
-                                        ]
-                                ]
-
-                        ]
-                        trace.specification.formulas += res
-                }
-                
-                //HIERARCHY HANDLER
-                
-                
-                // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates
-                // and store in a map
-                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))
-                                        ])
-                                }
-                        }
-//                      typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values)))
-//                      typeTrace.type2PossibleNot.clear
-                        trace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(trace.type2PossibleNot.values)))
-                        trace.type2PossibleNot.clear
-                }
-
-                // 5. create fof function that is an or with all the elements in map
-                val hierarch = createVLSFofFormula => [
-                        it.name = "hierarchyHandler"
-                        it.fofRole = "axiom"
-                        it.fofFormula = createVLSUniversalQuantifier => [
-                                it.variables += support.duplicate(variable)
-                                it.operand = createVLSEquivalent => [
-                                        it.left = support.topLevelTypeFunc
-//                                      it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values))
-                                        it.right = support.unfoldOr(new ArrayList<VLSTerm>(trace.type2And.values))
-                                ]
-                        ]
-                ]
-
-                trace.specification.formulas += hierarch
-
-        }
-
-        override transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper,
-                Logic2VampireLanguageMapperTrace trace) {
-                throw new UnsupportedOperationException("TODO: auto-generated method stub")
-        }
-
-        override getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) {
-                throw new UnsupportedOperationException("TODO: auto-generated method stub")
-        }
-
-        override getUndefinedSupertypeScope(int undefinedScope, Logic2VampireLanguageMapperTrace trace) {
-                throw new UnsupportedOperationException("TODO: auto-generated method stub")
-        }
-
-        override transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) {
-                createVLSDoubleQuote => [
-                        it.value = "\"a" + referred.name + "\""
-                ]
-        }
-
-        override getTypeInterpreter() {
-                throw new UnsupportedOperationException("TODO: auto-generated method stub")
-        }
-
-}