22 files changed, 145 insertions, 29 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/plugin.xml b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/plugin.xml
index 2381b84f..beaf5498 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/plugin.xml
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/plugin.xml
@@ -1 +1,17 @@
-<?xml version="1.0" encoding="UTF-8"?><?eclipse version="3.4"?><plugin/>

+<?xml version="1.0" encoding="UTF-8"?><?eclipse version="3.4"?><plugin>

+  <extension id="ca.mcgill.ecse.dslreasoner.vampire.queries.VampireQueries" point="org.eclipse.viatra.query.runtime.queryspecification">

+    <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:ca.mcgill.ecse.dslreasoner.vampire.queries.VampireQueries" id="ca.mcgill.ecse.dslreasoner.vampire.queries.VampireQueries">

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSComment"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSFofFormula"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSAnnotation"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSOr"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSAnd"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSEquivalent"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSFunction"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSExistentialQuantifier"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSUniversalQuantifier"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSUnaryNegation"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSInequality"/>

+    </group>

+  </extension>

+</plugin>

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/src/ca/mcgill/ecse/dslreasoner/vampire/queries/vampireQueries.vql b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/src/ca/mcgill/ecse/dslreasoner/vampire/queries/vampireQueries.vql
index 2bc22f9e..ef61e4d1 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/src/ca/mcgill/ecse/dslreasoner/vampire/queries/vampireQueries.vql
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/src/ca/mcgill/ecse/dslreasoner/vampire/queries/vampireQueries.vql
@@ -48,9 +48,9 @@ pattern VLSInequality(term: VLSInequality){
         VLSInequality(term);

 }

 

-pattern VLSFunctionFof(term: VLSFunctionFof){

-        VLSFunctionFof(term);

-}

+//pattern VLSFunctionFof(term: VLSFunctionFof){

+//      VLSFunctionFof(term);

+//}

 

 //pattern VLSFofTerm(term: VLSFofTerm){

 //      VLSFofTerm(term);

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 => [
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
index b5e03979..7394b24e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
index 0714f36d..d328dcf2 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java
index 1f6b3d42..ac55ebd7 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java
@@ -4,4 +4,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration;
 

 @SuppressWarnings("all")

 public class VampireSolverConfiguration extends LogicSolverConfiguration {

+  public int contCycleLevel = 0;

+  

+  public boolean uniquenessDuplicates = false;

 }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
index 2cc60591..968a2df8 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
index 01b0a351..48756fcc 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
index cf049bd5..44b06208 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
index 7bc04e7b..4cab8309 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
index a97c7186..ccddb430 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
index a473c586..a069a62f 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
index 4e7796fe..46cd58fb 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
index 84d6c63a..1b5e4d0b 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
index 36a727b2..f04bd7dc 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
@@ -123,7 +123,7 @@ public class Logic2VampireLanguageMapper {
       this.relationMapper.transformRelation(it, trace);

     };

     problem.getRelations().forEach(_function_3);

-    this.containmentMapper.transformContainment(problem.getContainmentHierarchies(), trace);

+    this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace);

     trace.constantDefinitions = this.collectConstantDefinitions(problem);

     final Consumer<ConstantDefinition> _function_4 = (ConstantDefinition it) -> {

       this.constantMapper.transformConstantDefinitionSpecification(it, trace);

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
index 7bc70e9d..4cdc7e6a 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
@@ -1,5 +1,6 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

 

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;

@@ -16,6 +17,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;

 import com.google.common.base.Objects;

+import com.google.common.collect.Iterables;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration;

@@ -52,7 +54,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
     this.base = base;

   }

   

-  public void transformContainment(final List<ContainmentHierarchy> hierarchies, final Logic2VampireLanguageMapperTrace trace) {

+  public void transformContainment(final VampireSolverConfiguration config, final List<ContainmentHierarchy> hierarchies, final Logic2VampireLanguageMapperTrace trace) {

     final ContainmentHierarchy hierarchy = hierarchies.get(0);

     final EList<Type> containmentListCopy = hierarchy.getTypesOrderedInHierarchy();

     final EList<Relation> relationsList = hierarchy.getContainmentRelations();

@@ -135,7 +137,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
         }

         VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

         final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> {

-          it.setName(this.support.toIDMultiple("noDupCont", rel.getConstant().toString()));

+          it.setName(this.support.toIDMultiple("containment_noDup", rel.getConstant().toString()));

           it.setFofRole("axiom");

           VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();

           final Procedure1<VLSExistentialQuantifier> _function_5 = (VLSExistentialQuantifier it_1) -> {

@@ -219,6 +221,57 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
         _formulas_1.add(relFormula);

       }

     }

+    final ArrayList<VLSVariable> variables = CollectionLiterals.<VLSVariable>newArrayList();

+    final ArrayList<VLSFunction> disjunctionList = CollectionLiterals.<VLSFunction>newArrayList();

+    final ArrayList<VLSTerm> conjunctionList = CollectionLiterals.<VLSTerm>newArrayList();

+    for (int i = 1; (i <= config.contCycleLevel); i++) {

+      {

+        final int ind = i;

+        VLSVariable _createVLSVariable_3 = this.factory.createVLSVariable();

+        final Procedure1<VLSVariable> _function_4 = (VLSVariable it) -> {

+          String _string = Integer.toString(ind);

+          String _plus = ("V" + _string);

+          it.setName(_plus);

+        };

+        VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_3, _function_4);

+        variables.add(_doubleArrow);

+        for (int j = 0; (j < i); j++) {

+          {

+            for (final Relation l_2 : relationsList) {

+              {

+                final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_2), trace.rel2Predicate), CollectionLiterals.<VLSVariable>newArrayList(variables.get(j), variables.get(((j + 1) % i))));

+                disjunctionList.add(rel);

+              }

+            }

+            conjunctionList.add(this.support.unfoldOr(disjunctionList));

+            disjunctionList.clear();

+          }

+        }

+        VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

+        final Procedure1<VLSFofFormula> _function_5 = (VLSFofFormula it) -> {

+          it.setName(this.support.toIDMultiple("containment_noCycle", Integer.toString(ind)));

+          it.setFofRole("axiom");

+          VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();

+          final Procedure1<VLSUnaryNegation> _function_6 = (VLSUnaryNegation it_1) -> {

+            VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();

+            final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_2) -> {

+              EList<VLSVariable> _variables = it_2.getVariables();

+              List<VLSVariable> _duplicate = this.support.duplicate(variables);

+              Iterables.<VLSVariable>addAll(_variables, _duplicate);

+              it_2.setOperand(this.support.unfoldAnd(conjunctionList));

+            };

+            VLSExistentialQuantifier _doubleArrow_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_7);

+            it_1.setOperand(_doubleArrow_1);

+          };

+          VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_6);

+          it.setFofFormula(_doubleArrow_1);

+        };

+        final VLSFofFormula contCycleForm = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_5);

+        EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas();

+        _formulas_1.add(contCycleForm);

+        conjunctionList.clear();

+      }

+    }

   }

   

   protected VLSTerm makeUnique(final List<VLSFunction> list) {

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
index 83543c92..f5d35b28 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
@@ -1,5 +1,6 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

 

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;

@@ -13,7 +14,6 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;

 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 hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;

 import java.util.ArrayList;

@@ -47,7 +47,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
     this.base = base;

   }

   

-  public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {

+  public void _transformScope(final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {

     final int ABSOLUTE_MIN = 0;

     final int ABSOLUTE_MAX = Integer.MAX_VALUE;

     final int GLOBAL_MIN = config.typeScopes.minNewElements;

@@ -105,7 +105,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
         }

       }

     }

-    final boolean DUPLICATES = false;

+    final boolean DUPLICATES = config.uniquenessDuplicates;

     final int numInst = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length;

     int ind = 1;

     if ((numInst != 0)) {

@@ -246,7 +246,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
     _formulas.add(cstDec);

   }

   

-  public void transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {

+  public void transformScope(final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {

     _transformScope(config, trace);

     return;

   }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
index 513618a9..89633ca1 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
@@ -129,6 +129,14 @@ public class Logic2VampireLanguageMapper_Support {
     return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);

   }

   

+  protected List<VLSVariable> duplicate(final List<VLSVariable> vars) {

+    ArrayList<VLSVariable> newList = CollectionLiterals.<VLSVariable>newArrayList();

+    for (final VLSVariable v : vars) {

+      newList.add(this.duplicate(v));

+    }

+    return newList;

+  }

+  

   protected VLSConstant toConstant(final VLSFunctionAsTerm term) {

     VLSConstant _createVLSConstant = this.factory.createVLSConstant();

     final Procedure1<VLSConstant> _function = (VLSConstant it) -> {