From f4a37cba3665a9cb38982b978d81fd4d269dedf7 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Wed, 6 Mar 2019 14:18:35 -0500 Subject: Restructure Vampire Reasoner project --- ...reLanguageMapper_TypeMapper_FilteredTypes.xtend | 153 --------------------- 1 file changed, 153 deletions(-) delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend') 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 types, Collection 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 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(typeTrace.type2PossibleNot.values))) -// typeTrace.type2PossibleNot.clear - trace.type2And.put(t1, support.unfoldAnd(new ArrayList(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(typeTrace.type2And.values)) - it.right = support.unfoldOr(new ArrayList(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") - } - -} -- cgit v1.2.3-70-g09d2