From b1bbb821c0e5a3f721de211826dab19c7d9dca4f Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Fri, 5 Apr 2019 03:32:48 -0400 Subject: Implement containment circularity avoidance #20 --- .../reasoner/VampireAnalyzerConfiguration.xtend | 3 +- .../builder/Logic2VampireLanguageMapper.xtend | 2 +- ...c2VampireLanguageMapper_ContainmentMapper.xtend | 46 ++++++++++++++++++---- .../Logic2VampireLanguageMapper_ScopeMapper.xtend | 13 +++--- .../Logic2VampireLanguageMapper_Support.xtend | 8 ++++ 5 files changed, 54 insertions(+), 18 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill') diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend index 618980a3..98967181 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend @@ -4,7 +4,8 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration class VampireSolverConfiguration extends LogicSolverConfiguration { - //public var int symmetry = 0 // by default + public var int contCycleLevel = 0 + public var boolean uniquenessDuplicates = false //choose needed backend solver // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J } 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 b7ad8f3d..2be6c093 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 @@ -87,7 +87,7 @@ class Logic2VampireLanguageMapper { problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] // CONTAINMENT MAPPER - containmentMapper.transformContainment(problem.containmentHierarchies, trace) + containmentMapper.transformContainment(config,problem.containmentHierarchies, trace) // CONSTANT MAPPER // only transforms definitions 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 48ee8789..395b4305 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 @@ -1,6 +1,6 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable @@ -25,9 +25,9 @@ class Logic2VampireLanguageMapper_ContainmentMapper { this.base = base } - def public void transformContainment(List hierarchies, + def public void transformContainment(VampireSolverConfiguration config, List hierarchies, Logic2VampireLanguageMapperTrace trace) { - //TODO throw error is there exists a circular containment that does not involve hierarchy + // 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) @@ -94,7 +94,6 @@ class Logic2VampireLanguageMapper_ContainmentMapper { // for (c : support.listSubtypes(toType)) { // addToMap(type2cont, toFunc, rel) // } - // val listForAnd = newArrayList //// listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB)) // listForAnd.add(support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList)) @@ -111,7 +110,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { // STEP 3 // Ensure that an objct only has 1 parent val relFormula = createVLSFofFormula => [ - it.name = support.toIDMultiple("noDupCont", rel.constant.toString) + it.name = support.toIDMultiple("containment_noDup", rel.constant.toString) it.fofRole = "axiom" it.fofFormula = createVLSExistentialQuantifier => [ it.variables += support.duplicate(varA) @@ -133,7 +132,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { } -// STEP CONT'D +// STEP 2 CONT'D for (e : type2cont.entrySet) { val relFormula = createVLSFofFormula => [ it.name = support.toIDMultiple("containment", e.key.constant.toString) @@ -159,8 +158,39 @@ class Logic2VampireLanguageMapper_ContainmentMapper { } - // STEP 4 - // Ensure that there are no cycles in the hierarchy (maybe same as for step3?) + // STEP 4 + // Ensure that there are no cycles in the hierarchy (maybe same as for step3?) + // Attempt 1: all possibilities, even the impossible one, based on MM constraints, are listed + + + val variables = newArrayList + val disjunctionList = newArrayList + val conjunctionList = newArrayList + for (var i = 1; i <= config.contCycleLevel; i++) { + val ind = i + variables.add(createVLSVariable => [it.name = ("V"+Integer.toString(ind))]) + for ( var j = 0; j < i;j++){ + for (l : relationsList) { + val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), newArrayList(variables.get(j), variables.get((j+1)%i))) + disjunctionList.add(rel) + } + conjunctionList.add(support.unfoldOr(disjunctionList)) + disjunctionList.clear + } + + val contCycleForm = createVLSFofFormula => [ + it.name = support.toIDMultiple("containment_noCycle", Integer.toString(ind)) + it.fofRole = "axiom" + it.fofFormula = createVLSUnaryNegation => [ + it.operand = createVLSExistentialQuantifier => [ + it.variables += support.duplicate(variables) + it.operand = support.unfoldAnd(conjunctionList) + ] + ] + ] + trace.specification.formulas += contCycleForm + conjunctionList.clear + } } protected def VLSTerm makeUnique(List list) { 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 0d0be576..0a8812e4 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 @@ -1,17 +1,15 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction +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 hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type import java.util.ArrayList +import java.util.HashMap import java.util.Map import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* -import java.util.HashMap -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm -import java.util.List class Logic2VampireLanguageMapper_ScopeMapper { private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE @@ -23,7 +21,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { this.base = base } - def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { + def dispatch public void transformScope(VampireSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { val ABSOLUTE_MIN = 0 val ABSOLUTE_MAX = Integer.MAX_VALUE @@ -40,7 +38,6 @@ class Logic2VampireLanguageMapper_ScopeMapper { // Handling Minimum_General if (GLOBAL_MIN != ABSOLUTE_MIN) { - // * getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, !consistant) if (consistant) { for (i : trace.uniqueInstances) { @@ -94,7 +91,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { // 3. Specify uniqueness of elements // TEMP - val DUPLICATES = false + val DUPLICATES = config.uniquenessDuplicates val numInst = trace.uniqueInstances.length var ind = 1 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 dd88a53a..195b89bb 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 @@ -77,6 +77,14 @@ class Logic2VampireLanguageMapper_Support { it.terms += duplicate(v) ] } + + def protected List duplicate(List vars) { + var newList = newArrayList + for (v : vars) { + newList.add(duplicate(v)) + } + return newList + } def protected VLSConstant toConstant(VLSFunctionAsTerm term) { return createVLSConstant => [ -- cgit v1.2.3-54-g00ecf