Implement containment circularity avoidance #20

5 files changed, 54 insertions, 18 deletions

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<ContainmentHierarchy> hierarchies,

+        def public void transformContainment(VampireSolverConfiguration config, List<ContainmentHierarchy> 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<VLSFunction> 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<VLSVariable> duplicate(List<VLSVariable> vars) {
+                        var newList = newArrayList
+                        for (v : vars) {
+                                newList.add(duplicate(v))
+                        }
+                        return newList
+        }
 
         def protected VLSConstant toConstant(VLSFunctionAsTerm term) {
                 return createVLSConstant => [