From 4d01994940121fc255bd242358b5135a27e8dce5 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Thu, 4 Apr 2019 14:43:17 -0400 Subject: Closes #34, adds code to test cases where minScope>maxScope. --- ...c2VampireLanguageMapper_ContainmentMapper.xtend | 5 ++- .../Logic2VampireLanguageMapper_ScopeMapper.xtend | 18 ++++++-- .../Logic2VampireLanguageMapper_Support.xtend | 48 +++++++++++++++++----- .../Logic2VampireLanguageMapper_TypeMapper.xtend | 8 ++-- 4 files changed, 60 insertions(+), 19 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse') diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend index 820d0db2..48ee8789 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend @@ -27,7 +27,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { def public void transformContainment(List hierarchies, Logic2VampireLanguageMapperTrace trace) { - + //TODO throw error is there exists a circular containment that does not involve hierarchy // TODO CONSIDER CASE WHERE MULTIPLE CONTAINMMENT HIERARCHIES EXIST // TEMP val hierarchy = hierarchies.get(0) @@ -91,6 +91,9 @@ class Logic2VampireLanguageMapper_ContainmentMapper { for (c : toType.subtypes) { addToMap(type2cont, toFunc, rel) } +// for (c : support.listSubtypes(toType)) { +// addToMap(type2cont, toFunc, rel) +// } // val listForAnd = newArrayList //// listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB)) diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend index bc87d3b7..54fcdc86 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend @@ -24,11 +24,12 @@ class Logic2VampireLanguageMapper_ScopeMapper { } def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { + val ABSOLUTE_MIN = 0 + val ABSOLUTE_MAX = Integer.MAX_VALUE // TODO HANDLE ERRORS RELATED TO MAX > MIN // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS // TODO HANDLE -// TODO NOT SPECIFIED MEANS =0 ? // 1. make a list of constants equaling the min number of specified objects val GLOBAL_MIN = config.typeScopes.minNewElements val GLOBAL_MAX = config.typeScopes.maxNewElements @@ -36,19 +37,30 @@ class Logic2VampireLanguageMapper_ScopeMapper { val localInstances = newArrayList // Handling Minimum_General - if (GLOBAL_MIN != 0) { + if (GLOBAL_MIN != ABSOLUTE_MIN) { getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) for (i : trace.uniqueInstances) { localInstances.add(support.duplicate(i)) } makeFofFormula(localInstances, trace, true, null) + +// //For testing Min>Max scope +// getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, true) +// makeFofFormula(trace.uniqueInstances as ArrayList, trace, true, null) +// //end for testing + } // Handling Maximum_General - if (GLOBAL_MAX != 0) { + if (GLOBAL_MAX != ABSOLUTE_MAX) { getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true) makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null) + +// //For testing Min>Max scope +// getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, false) +// makeFofFormula(localInstances, trace, false, null) +// //end for testing } // Handling Minimum_Specific diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend index d1ea2a15..b00dad42 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend @@ -23,7 +23,7 @@ import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* class Logic2VampireLanguageMapper_Support { private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE - // ID Handler +// ID Handler def protected String toIDMultiple(String... ids) { ids.map[it.split("\\s+").join("_")].join("_") } @@ -32,8 +32,8 @@ class Logic2VampireLanguageMapper_Support { ids.split("\\s+").join("_") } - // Term Handling - // TODO Make more general +// Term Handling +// TODO Make more general def protected VLSVariable duplicate(VLSVariable term) { return createVLSVariable => [it.name = term.name] } @@ -107,7 +107,7 @@ class Logic2VampireLanguageMapper_Support { ] } - // TODO Make more general +// TODO Make more general def establishUniqueness(List terms, VLSConstant t2) { // val List eqs = newArrayList // for (t1 : terms.subList(1, terms.length)) { @@ -135,9 +135,9 @@ class Logic2VampireLanguageMapper_Support { return unfoldAnd(eqs) } - // Support Functions - // booleans - // AND and OR +// Support Functions +// booleans +// AND and OR def protected VLSTerm unfoldAnd(List operands) { if (operands.size == 1) { return operands.head @@ -163,7 +163,7 @@ class Logic2VampireLanguageMapper_Support { throw new UnsupportedOperationException('''Logic operator with 0 operands!''') // TEMP } - // can delete below +// can delete below def protected VLSTerm unfoldDistinctTerms(Logic2VampireLanguageMapper m, EList operands, Logic2VampireLanguageMapperTrace trace, Map variables) { if (operands.size == 1) { @@ -183,8 +183,8 @@ class Logic2VampireLanguageMapper_Support { throw new UnsupportedOperationException('''Logic operator with 0 operands!''') } - // Symbolic - // def postprocessResultOfSymbolicReference(TypeReference type, VLSTerm term, Logic2VampireLanguageMapperTrace trace) { +// Symbolic +// def postprocessResultOfSymbolicReference(TypeReference type, VLSTerm term, Logic2VampireLanguageMapperTrace trace) { // if(type instanceof BoolTypeReference) { // return booleanToLogicValue(term ,trace) // } @@ -198,7 +198,7 @@ class Logic2VampireLanguageMapper_Support { * ids.map[it.split("\\s+").join("'")].join("'") * } */ - // QUANTIFIERS + VARIABLES +// QUANTIFIERS + VARIABLES def protected VLSTerm createQuantifiedExpression(Logic2VampireLanguageMapper mapper, QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map variables, boolean isUniversal) { @@ -245,6 +245,32 @@ class Logic2VampireLanguageMapper_Support { } } } + //TODO rewrite such that it uses "listSubTypes" + def protected boolean dfsSubtypeCheck(Type type, Type type2) { + // There is surely a better way to do this + if (type.subtypes.isEmpty) + return false + else { + if (type.subtypes.contains(type2)) + return true + else { + for (subtype : type.subtypes) { + if(dfsSubtypeCheck(subtype, type2)) return true + } + } + } + } + + def protected List listSubtypes(Type t) { + var List allSubtypes = newArrayList + if (!t.subtypes.isEmpty) { + for (subt : t.subtypes) { + allSubtypes.add(subt) + allSubtypes = listSubtypes(subt) + } + } + return allSubtypes + } def protected withAddition(Map map1, Map map2) { new HashMap(map1) => [putAll(map2)] 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 1719bbcc..3bc945df 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 @@ -150,10 +150,10 @@ class Logic2VampireLanguageMapper_TypeMapper { } - // 4. case where an object is not an object + // 3.5: case where an object is not an object val List type2Not = newArrayList - - for(t : types) { + + for (t : types) { type2Not.add(createVLSUnaryNegation => [ it.operand = support.duplicate(t.lookup(trace.type2Predicate)) ]) @@ -174,7 +174,7 @@ class Logic2VampireLanguageMapper_TypeMapper { ] trace.specification.formulas += notObj - + // End 3.5 // 4. create fof function that is an or with all the elements in map val hierarch = createVLSFofFormula => [ it.name = "inheritanceHierarchyHandler" -- cgit v1.2.3-54-g00ecf