Implement containment circularity avoidance #20

12 files changed, 68 insertions, 7 deletions

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) -> {