Polyhedron abstraction with Z3 for cardinality propagation

22 files changed, 833 insertions, 72 deletions

diff --git a/Solvers/SMT-Solver/com.microsoft.z3/.classpath b/Solvers/SMT-Solver/com.microsoft.z3/.classpath
new file mode 100644
index 00000000..ffdc022a
--- /dev/null
+++ b/Solvers/SMT-Solver/com.microsoft.z3/.classpath
@@ -0,0 +1,15 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<classpath>
+        <classpathentry exported="true" kind="lib" path="com.microsoft.z3.jar">
+                <attributes>
+                        <attribute name="org.eclipse.jdt.launching.CLASSPATH_ATTR_LIBRARY_PATH_ENTRY" value="com.microsoft.z3/lib"/>
+                </attributes>
+        </classpathentry>
+        <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER">
+                <attributes>
+                        <attribute name="module" value="true"/>
+                </attributes>
+        </classpathentry>
+        <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
+        <classpathentry kind="output" path="bin"/>
+</classpath>
diff --git a/Solvers/SMT-Solver/com.microsoft.z3/.gitignore b/Solvers/SMT-Solver/com.microsoft.z3/.gitignore
new file mode 100644
index 00000000..ae3c1726
--- /dev/null
+++ b/Solvers/SMT-Solver/com.microsoft.z3/.gitignore
@@ -0,0 +1 @@
+/bin/
diff --git a/Solvers/SMT-Solver/com.microsoft.z3/.project b/Solvers/SMT-Solver/com.microsoft.z3/.project
new file mode 100644
index 00000000..ec5bbc58
--- /dev/null
+++ b/Solvers/SMT-Solver/com.microsoft.z3/.project
@@ -0,0 +1,28 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+        <name>com.microsoft.z3</name>
+        <comment></comment>
+        <projects>
+        </projects>
+        <buildSpec>
+                <buildCommand>
+                        <name>org.eclipse.jdt.core.javabuilder</name>
+                        <arguments>
+                        </arguments>
+                </buildCommand>
+                <buildCommand>
+                        <name>org.eclipse.pde.ManifestBuilder</name>
+                        <arguments>
+                        </arguments>
+                </buildCommand>
+                <buildCommand>
+                        <name>org.eclipse.pde.SchemaBuilder</name>
+                        <arguments>
+                        </arguments>
+                </buildCommand>
+        </buildSpec>
+        <natures>
+                <nature>org.eclipse.pde.PluginNature</nature>
+                <nature>org.eclipse.jdt.core.javanature</nature>
+        </natures>
+</projectDescription>
diff --git a/Solvers/SMT-Solver/com.microsoft.z3/META-INF/MANIFEST.MF b/Solvers/SMT-Solver/com.microsoft.z3/META-INF/MANIFEST.MF
new file mode 100644
index 00000000..01faa2ad
--- /dev/null
+++ b/Solvers/SMT-Solver/com.microsoft.z3/META-INF/MANIFEST.MF
@@ -0,0 +1,22 @@
+Manifest-Version: 1.0
+Bundle-ManifestVersion: 2
+Bundle-Name: Z3
+Bundle-SymbolicName: com.microsoft.z3
+Bundle-Version: 4.8.5.qualifier
+Bundle-Vendor: Microsoft
+Automatic-Module-Name: com.microsoft.z3
+Bundle-ClassPath: com.microsoft.z3.jar
+Bundle-NativeCode: lib/libz3.so;
+ lib/libz3java.so;
+ osname=Linux;
+ processor=x86_64;
+ lib/libz3.dylib;
+ lib/libz3java.dylib;
+ osname=MacOSX;
+ processor=x86_64,
+ lib/libz3.dll;
+ lib/libz3java.dll;
+ osname=win32;
+ processor=x86_64
+Export-Package: com.microsoft.z3,
+ com.microsoft.z3.enumerations
diff --git a/Solvers/SMT-Solver/com.microsoft.z3/build.properties b/Solvers/SMT-Solver/com.microsoft.z3/build.properties
new file mode 100644
index 00000000..87f4e73f
--- /dev/null
+++ b/Solvers/SMT-Solver/com.microsoft.z3/build.properties
@@ -0,0 +1,3 @@
+bin.includes = META-INF/,\
+               lib/,\
+               com.microsoft.z3.jar
diff --git a/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.dll b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.dll
new file mode 100644
index 00000000..0b518988
--- /dev/null
+++ b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.dll
diff --git a/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.dylib b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.dylib
new file mode 100755
index 00000000..7884a0e7
--- /dev/null
+++ b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.dylib
diff --git a/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so
new file mode 100755
index 00000000..5beffe36
--- /dev/null
+++ b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so
diff --git a/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.dll b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.dll
new file mode 100644
index 00000000..5e8dbc9b
--- /dev/null
+++ b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.dll
diff --git a/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.dylib b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.dylib
new file mode 100755
index 00000000..2d9116ac
--- /dev/null
+++ b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.dylib
diff --git a/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so
new file mode 100755
index 00000000..e2d2618d
--- /dev/null
+++ b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF
index b2ee3981..37495e50 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF
@@ -4,6 +4,7 @@ Bundle-Name: Logic2viatra
 Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;singleton:=true
 Bundle-Version: 1.0.0.qualifier
 Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra,
+ hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality,
  hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval,
  hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.aggregators,
  hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns,
@@ -22,7 +23,8 @@ Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0",
  com.google.inject;bundle-version="3.0.0",
  org.eclipse.xtext;bundle-version="2.10.0",
  org.eclipse.viatra.transformation.runtime.emf;bundle-version="1.5.0",
- org.eclipse.xtext.xbase;bundle-version="2.10.0"
+ org.eclipse.xtext.xbase;bundle-version="2.10.0",
+ com.microsoft.z3;bundle-version="4.8.5"
 Bundle-RequiredExecutionEnvironment: JavaSE-1.8
 Import-Package: org.apache.log4j
 Automatic-Module-Name: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
index b6918294..0040dbcd 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
@@ -4,6 +4,11 @@ import com.google.common.collect.ImmutableMap
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel

 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem

 import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider

@@ -63,7 +68,7 @@ class ModelGenerationMethodProvider {
                 ReasonerWorkspace workspace,

                 boolean nameNewElements,

                 TypeInferenceMethod typeInferenceMethod,

-                ScopePropagator scopePropagator,

+                ScopePropagatorStrategy scopePropagatorStrategy,

                 DocumentationLevel debugLevel

         ) {

                 val statistics = new ModelGenerationStatistics

@@ -74,6 +79,8 @@ class ModelGenerationMethodProvider {
 

                 val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries,

                         workspace, typeInferenceMethod, writeFiles)

+                val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, queries)

+                scopePropagator.propagateAllScopeConstraints

                 val // LinkedHashMap<Pair<Relation, ? extends Type>, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>>

                 objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator,

                         nameNewElements, statistics)

@@ -104,4 +111,19 @@ class ModelGenerationMethodProvider {
                         queries.allQueries

                 )

         }

+

+        private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy,

+                PartialInterpretation emptySolution, GeneratedPatterns queries) {

+                switch (scopePropagatorStrategy) {

+                        case BasicTypeHierarchy:

+                                new ScopePropagator(emptySolution)

+                        case PolyhedralTypeHierarchy: {

+                                val types = queries.refineObjectQueries.keySet.map[newType].toSet

+                                val solver = new Z3PolyhedronSolver

+                                new PolyhedronScopePropagator(emptySolution, types, solver)

+                        }

+                        default:

+                                throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy)

+                }

+        }

 }

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend
new file mode 100644
index 00000000..8f210ffb
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend
@@ -0,0 +1,153 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+
+import com.google.common.collect.ImmutableList
+import com.google.common.collect.ImmutableMap
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope
+import java.util.ArrayDeque
+import java.util.HashMap
+import java.util.HashSet
+import java.util.Map
+import java.util.Set
+
+class PolyhedronScopePropagator extends ScopePropagator {
+        val Map<Scope, LinearBoundedExpression> scopeBounds
+        val LinearConstraint topLevelBounds
+        val PolyhedronSaturationOperator operator
+
+        new(PartialInterpretation p, Set<? extends Type> possibleNewDynamicTypes, PolyhedronSolver solver) {
+                super(p)
+                val instanceCounts = possibleNewDynamicTypes.toInvertedMap[new Dimension(name, 0, null)]
+                val primitiveDimensions = new HashMap
+                val constraintsBuilder = ImmutableList.builder
+                val scopeBoundsBuilder = ImmutableMap.builder
+                // Dimensions for instantiable types were created according to the type analysis,
+                // but for any possible primitive types, we create them on demand,
+                // as there is no Type directly associated with a PartialPrimitiveInterpretation.
+                for (scope : p.scopes) {
+                        switch (targetTypeInterpretation : scope.targetTypeInterpretation) {
+                                PartialPrimitiveInterpretation: {
+                                        val dimension = primitiveDimensions.computeIfAbsent(targetTypeInterpretation) [ interpretation |
+                                                new Dimension(interpretation.eClass.name, 0, null)
+                                        ]
+                                        scopeBoundsBuilder.put(scope, dimension)
+                                }
+                                PartialComplexTypeInterpretation: {
+                                        val complexType = targetTypeInterpretation.interpretationOf
+                                        val dimensions = findSubtypeDimensions(complexType, instanceCounts)
+                                        switch (dimensions.size) {
+                                                case 0:
+                                                        if (scope.minNewElements > 0) {
+                                                                throw new IllegalArgumentException("Found scope for " + complexType.name +
+                                                                        ", but the type cannot be instantiated")
+                                                        }
+                                                case 1:
+                                                        scopeBoundsBuilder.put(scope, dimensions.head)
+                                                default: {
+                                                        val constraint = new LinearConstraint(dimensions.toInvertedMap[1], null, null)
+                                                        constraintsBuilder.add(constraint)
+                                                        scopeBoundsBuilder.put(scope, constraint)
+                                                }
+                                        }
+                                }
+                                default:
+                                        throw new IllegalArgumentException("Unknown PartialTypeInterpretation: " + targetTypeInterpretation)
+                        }
+                }
+                val allDimensions = ImmutableList.builder.addAll(instanceCounts.values).addAll(primitiveDimensions.values).build
+                scopeBounds = scopeBoundsBuilder.build
+                topLevelBounds = new LinearConstraint(allDimensions.toInvertedMap[1], null, null)
+                constraintsBuilder.add(topLevelBounds)
+                val expressionsToSaturate = ImmutableList.builder.addAll(scopeBounds.values).add(topLevelBounds).build
+                val polyhedron = new Polyhedron(allDimensions, constraintsBuilder.build, expressionsToSaturate)
+                operator = solver.createSaturationOperator(polyhedron)
+        }
+
+        private def findSubtypeDimensions(Type type, Map<Type, Dimension> instanceCounts) {
+                val subtypes = new HashSet
+                val dimensions = new HashSet
+                val stack = new ArrayDeque
+                stack.addLast(type)
+                while (!stack.empty) {
+                        val subtype = stack.removeLast
+                        if (subtypes.add(subtype)) {
+                                val dimension = instanceCounts.get(subtype)
+                                if (dimension !== null) {
+                                        dimensions.add(dimension)
+                                }
+                                stack.addAll(subtype.subtypes)
+                        }
+                }
+                dimensions
+        }
+
+        override void propagateAllScopeConstraints() {
+                populatePolyhedronFromScope()
+                val result = operator.saturate()
+                if (result == PolyhedronSaturationResult.EMPTY) {
+                        throw new IllegalStateException("Scope bounds cannot be satisfied")
+                } else {
+                        populateScopesFromPolyhedron()
+                        if (result != PolyhedronSaturationResult.SATURATED) {
+                                super.propagateAllScopeConstraints()
+                        }
+                }
+        }
+
+        private def populatePolyhedronFromScope() {
+                topLevelBounds.lowerBound = partialInterpretation.minNewElements
+                if (partialInterpretation.maxNewElements >= 0) {
+                        topLevelBounds.upperBound = partialInterpretation.maxNewElements
+                }
+                for (pair : scopeBounds.entrySet) {
+                        val scope = pair.key
+                        val bounds = pair.value
+                        bounds.lowerBound = scope.minNewElements
+                        if (scope.maxNewElements >= 0) {
+                                bounds.upperBound = scope.maxNewElements
+                        }
+                }
+        }
+
+        private def populateScopesFromPolyhedron() {
+                checkFiniteBounds(topLevelBounds)
+                if (partialInterpretation.minNewElements > topLevelBounds.lowerBound) {
+                        throw new IllegalArgumentException('''Lower bound of «topLevelBounds» smaller than top-level scope: «partialInterpretation.minNewElements»''')
+                } else if (partialInterpretation.minNewElements != topLevelBounds.lowerBound) {
+                        partialInterpretation.minNewElements = topLevelBounds.lowerBound
+                }
+                if (partialInterpretation.maxNewElements >= 0 &&
+                        partialInterpretation.maxNewElements < topLevelBounds.upperBound) {
+                        throw new IllegalArgumentException('''Upper bound of «topLevelBounds» larger than top-level scope: «partialInterpretation.maxNewElements»''')
+                } else if (partialInterpretation.maxNewElements != topLevelBounds.upperBound) {
+                        partialInterpretation.maxNewElements = topLevelBounds.upperBound
+                }
+                for (pair : scopeBounds.entrySet) {
+                        val scope = pair.key
+                        val bounds = pair.value
+                        checkFiniteBounds(bounds)
+                        if (scope.minNewElements > bounds.lowerBound) {
+                                throw new IllegalArgumentException('''Lower bound of «bounds» smaller than «scope.targetTypeInterpretation» scope: «scope.minNewElements»''')
+                        } else if (scope.minNewElements != bounds.lowerBound) {
+                                scope.minNewElements = bounds.lowerBound
+                        }
+                        if (scope.maxNewElements >= 0 && scope.maxNewElements < bounds.upperBound) {
+                                throw new IllegalArgumentException('''Upper bound of «bounds» larger than «scope.targetTypeInterpretation» scope: «scope.maxNewElements»''')
+                        } else if (scope.maxNewElements != bounds.upperBound) {
+                                scope.maxNewElements = bounds.upperBound
+                        }
+                }
+        }
+
+        private def checkFiniteBounds(LinearBoundedExpression bounds) {
+                if (bounds.lowerBound === null) {
+                        throw new IllegalArgumentException("Infinite lower bound: " + bounds)
+                }
+                if (bounds.upperBound === null) {
+                        throw new IllegalArgumentException("Infinite upper bound: " + bounds)
+                }
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend
new file mode 100644
index 00000000..08bf25b9
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend
@@ -0,0 +1,115 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+
+import java.util.List
+import java.util.Map
+import org.eclipse.xtend.lib.annotations.Accessors
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+
+interface PolyhedronSolver {
+        def PolyhedronSaturationOperator createSaturationOperator(Polyhedron polyhedron)
+}
+
+enum PolyhedronSaturationResult {
+        SATURATED,
+        EMPTY,
+        UNKNOWN
+}
+
+interface PolyhedronSaturationOperator extends AutoCloseable {
+        def Polyhedron getPolyhedron()
+
+        def PolyhedronSaturationResult saturate()
+}
+
+@FinalFieldsConstructor
+@Accessors
+class Polyhedron {
+        /**
+         * The list of dimensions (variables) for this polyhedron.
+         * 
+         * This list must not be modified after the polyhedron was created.
+         * However, lower and upper bounds of the dimensions may be changed.
+         * 
+         * Names of dimensions in this list are assumed to be unique.
+         */
+        val List<Dimension> dimensions
+
+        /**
+         * The list of constraints defining this polyhedron.
+         * 
+         * The list and its elements may be freely modified.
+         */
+        val List<LinearConstraint> constraints
+
+        /**
+         * The list of constraints that should be saturated (tightened)
+         * when a {@link PolyhedronSaturationOperator} is invoked.
+         * 
+         * This list may be freely modified.
+         * 
+         * Place all dimensions and constraints here to saturate all the bounds.
+         */
+        val List<LinearBoundedExpression> expressionsToSaturate
+
+        override toString() '''
+                Dimensions:
+                        «FOR dimension : dimensions»
+                                «dimension»
+                        «ENDFOR»
+                Constraints:
+                        «FOR constraint : constraints»
+                                «constraint»
+                        «ENDFOR»
+«««          Saturate:
+«««                  «FOR expression : expressionsToSaturate»
+«««                          «IF expression instanceof Dimension»dimension«ELSEIF expression instanceof LinearConstraint»constraint«ELSE»unknown«ENDIF» «expression»
+«««                  «ENDFOR»
+        '''
+
+}
+
+@Accessors
+abstract class LinearBoundedExpression {
+        var Integer lowerBound
+        var Integer upperBound
+}
+
+@Accessors
+class Dimension extends LinearBoundedExpression {
+        val String name
+
+        @FinalFieldsConstructor
+        new() {
+        }
+
+        new(String name, Integer lowerBound, Integer upperBound) {
+                this(name)
+                this.lowerBound = lowerBound
+                this.upperBound = upperBound
+        }
+
+        override toString() {
+                '''«IF lowerBound !== null»«lowerBound» <= «ENDIF»«name»«IF upperBound !== null» <= «upperBound»«ENDIF»'''
+        }
+
+}
+
+@Accessors
+class LinearConstraint extends LinearBoundedExpression {
+        val Map<Dimension, Integer> coefficients
+
+        @FinalFieldsConstructor
+        new() {
+        }
+
+        new(Map<Dimension, Integer> coefficients, Integer lowerBound, Integer upperBound) {
+                this(coefficients)
+                this.lowerBound = lowerBound
+                this.upperBound = upperBound
+        }
+
+        override toString() {
+                '''«IF lowerBound !== null»«lowerBound» <= «ENDIF»«FOR pair : coefficients.entrySet SEPARATOR " + "»«IF pair.value != 1»«pair.value» * «ENDIF»«pair.key.name»«ENDFOR»«IF upperBound !== null» <= «upperBound»«ENDIF»'''
+        }
+
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
index 38633c07..c8fb3409 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend
@@ -1,40 +1,46 @@
-package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra

+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality

 

+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope

 import java.util.HashMap

+import java.util.HashSet

 import java.util.Map

 import java.util.Set

-import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation

-import java.util.HashSet

+import org.eclipse.xtend.lib.annotations.Accessors

+

+enum ScopePropagatorStrategy {

+        BasicTypeHierarchy,

+        PolyhedralTypeHierarchy

+}

 

 class ScopePropagator {

-        PartialInterpretation partialInterpretation

-        Map<PartialTypeInterpratation,Scope> type2Scope

-        

+        @Accessors(PROTECTED_GETTER) PartialInterpretation partialInterpretation

+        Map<PartialTypeInterpratation, Scope> type2Scope

+

         val Map<Scope, Set<Scope>> superScopes

         val Map<Scope, Set<Scope>> subScopes

-        

-        public new(PartialInterpretation p) {

+

+        new(PartialInterpretation p) {

                 partialInterpretation = p

                 type2Scope = new HashMap

-                for(scope : p.scopes) {

-                        type2Scope.put(scope.targetTypeInterpretation,scope)

+                for (scope : p.scopes) {

+                        type2Scope.put(scope.targetTypeInterpretation, scope)

                 }

-                

+

                 superScopes = new HashMap

                 subScopes = new HashMap

-                for(scope : p.scopes) {

-                        superScopes.put(scope,new HashSet)

-                        subScopes.put(scope,new HashSet)

+                for (scope : p.scopes) {

+                        superScopes.put(scope, new HashSet)

+                        subScopes.put(scope, new HashSet)

                 }

-                

-                for(scope : p.scopes) {

+

+                for (scope : p.scopes) {

                         val target = scope.targetTypeInterpretation

-                        if(target instanceof PartialComplexTypeInterpretation) {

+                        if (target instanceof PartialComplexTypeInterpretation) {

                                 val supertypeInterpretations = target.supertypeInterpretation

-                                for(supertypeInterpretation : supertypeInterpretations) {

+                                for (supertypeInterpretation : supertypeInterpretations) {

                                         val supertypeScope = type2Scope.get(supertypeInterpretation)

                                         superScopes.get(scope).add(supertypeScope)

                                         subScopes.get(supertypeScope).add(scope)

@@ -42,70 +48,57 @@ class ScopePropagator {
                         }

                 }

         }

-        

-        def public propagateAllScopeConstraints() {

+

+        def propagateAllScopeConstraints() {

                 var boolean hadChanged

-                do{

+                do {

                         hadChanged = false

-                        for(superScopeEntry : superScopes.entrySet) {

+                        for (superScopeEntry : superScopes.entrySet) {

                                 val sub = superScopeEntry.key

-                                hadChanged = propagateLowerLimitUp(sub,partialInterpretation) || hadChanged

-                                hadChanged = propagateUpperLimitDown(sub,partialInterpretation) || hadChanged

-                                for(sup: superScopeEntry.value) {

-                                        hadChanged = propagateLowerLimitUp(sub,sup) || hadChanged

-                                        hadChanged = propagateUpperLimitDown(sub,sup) || hadChanged

+                                hadChanged = propagateLowerLimitUp(sub, partialInterpretation) || hadChanged

+                                hadChanged = propagateUpperLimitDown(sub, partialInterpretation) || hadChanged

+                                for (sup : superScopeEntry.value) {

+                                        hadChanged = propagateLowerLimitUp(sub, sup) || hadChanged

+                                        hadChanged = propagateUpperLimitDown(sub, sup) || hadChanged

                                 }

                         }

-                } while(hadChanged)

-//              println('''All constraints are propagated.''')

+                } while (hadChanged)

         }

-        

-        def public propagateAdditionToType(PartialTypeInterpratation t) {

+

+        def propagateAdditionToType(PartialTypeInterpratation t) {

 //              println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''')

                 val targetScope = type2Scope.get(t)

                 targetScope.removeOne

                 val sups = superScopes.get(targetScope)

                 sups.forEach[removeOne]

-                if(this.partialInterpretation.minNewElements > 0) {

-                        this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements-1

+                if (this.partialInterpretation.minNewElements > 0) {

+                        this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements - 1

                 }

-                if(this.partialInterpretation.maxNewElements > 0) {

-                        this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements-1

-                } else if(this.partialInterpretation.maxNewElements === 0) {

+                if (this.partialInterpretation.maxNewElements > 0) {

+                        this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements - 1

+                } else if (this.partialInterpretation.maxNewElements === 0) {

                         throw new IllegalArgumentException('''Inconsistent object creation: lower node limit is 0!''')

                 }

-                

-//              subScopes.get(targetScope).forEach[propagateUpperLimitDown(it,targetScope)]

-//              for(sup: sups) {

-//                      subScopes.get(sup).forEach[propagateUpperLimitDown(it,sup)]

-//              }

-//              for(scope : type2Scope.values) {

-//                      propagateUpperLimitDown(scope,partialInterpretation)

-//              }

-

                 propagateAllScopeConstraints

-                

+

 //              println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''')

 //              println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''')

 //              this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')]

 //              println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''')

         }

-        

+

         private def propagateLowerLimitUp(Scope subScope, Scope superScope) {

-                if(subScope.minNewElements>superScope.minNewElements) {

-//                      println('''

-//                      «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»

-//                      superScope.minNewElements «superScope.minNewElements» = subScope.minNewElements «subScope.minNewElements»

-//                      ''')

+                if (subScope.minNewElements > superScope.minNewElements) {

                         superScope.minNewElements = subScope.minNewElements

                         return true

                 } else {

                         return false

                 }

         }

-        

+

         private def propagateUpperLimitDown(Scope subScope, Scope superScope) {

-                if(superScope.maxNewElements>=0 && (superScope.maxNewElements<subScope.maxNewElements || subScope.maxNewElements<0)) {

+                if (superScope.maxNewElements >= 0 &&

+                        (superScope.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) {

 //                      println('''

 //                      «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»

 //                      subScope.maxNewElements «subScope.maxNewElements» = superScope.maxNewElements «superScope.maxNewElements»

@@ -116,9 +109,9 @@ class ScopePropagator {
                         return false

                 }

         }

-        

+

         private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) {

-                if(subScope.minNewElements>p.minNewElements) {

+                if (subScope.minNewElements > p.minNewElements) {

 //                      println('''

 //                      «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes

 //                      p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements»

@@ -129,9 +122,9 @@ class ScopePropagator {
                         return false

                 }

         }

-        

+

         private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) {

-                if(p.maxNewElements>=0 && (p.maxNewElements<subScope.maxNewElements || subScope.maxNewElements<0)) {

+                if (p.maxNewElements >= 0 && (p.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) {

 //                      println('''

 //                      «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes

 //                      subScope.maxNewElements «subScope.maxNewElements» = p.maxNewElements «p.maxNewElements»

@@ -142,15 +135,15 @@ class ScopePropagator {
                         return false

                 }

         }

+

         private def removeOne(Scope scope) {

-                if(scope.maxNewElements===0) {

+                if (scope.maxNewElements === 0) {

                         throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''')

-                } else if(scope.maxNewElements>0) {

-                        scope.maxNewElements= scope.maxNewElements-1

+                } else if (scope.maxNewElements > 0) {

+                        scope.maxNewElements = scope.maxNewElements - 1

                 }

-                if(scope.minNewElements>0) {

-                        scope.minNewElements= scope.minNewElements-1

+                if (scope.minNewElements > 0) {

+                        scope.minNewElements = scope.minNewElements - 1

                 }

         }

 }

-                        
\ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend
new file mode 100644
index 00000000..f1a84f2d
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend
@@ -0,0 +1,206 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+
+import com.microsoft.z3.ArithExpr
+import com.microsoft.z3.Context
+import com.microsoft.z3.Expr
+import com.microsoft.z3.IntNum
+import com.microsoft.z3.Optimize
+import com.microsoft.z3.Status
+import com.microsoft.z3.Symbol
+import java.util.Map
+import org.eclipse.xtend.lib.annotations.Accessors
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+
+class Z3PolyhedronSolver implements PolyhedronSolver {
+        val boolean lpRelaxation
+
+        @FinalFieldsConstructor
+        new() {
+        }
+
+        new() {
+                this(true)
+        }
+
+        override createSaturationOperator(Polyhedron polyhedron) {
+                new Z3SaturationOperator(polyhedron, lpRelaxation)
+        }
+}
+
+class Z3SaturationOperator implements PolyhedronSaturationOperator {
+        static val INFINITY_SYMBOL_NAME = "oo"
+        static val MULT_SYMBOL_NAME = "*"
+
+        extension val Context context
+        val Symbol infinitySymbol
+        val Symbol multSymbol
+        @Accessors val Polyhedron polyhedron
+        val Map<Dimension, ArithExpr> variables
+
+        new(Polyhedron polyhedron, boolean lpRelaxation) {
+                context = new Context
+                infinitySymbol = context.mkSymbol(INFINITY_SYMBOL_NAME)
+                multSymbol = context.mkSymbol(MULT_SYMBOL_NAME)
+                this.polyhedron = polyhedron
+                variables = polyhedron.dimensions.toInvertedMap [ dimension |
+                        val name = dimension.name
+                        if (lpRelaxation) {
+                                mkRealConst(name)
+                        } else {
+                                mkIntConst(name)
+                        }
+                ]
+        }
+
+        override saturate() {
+                val status = doSaturate()
+                convertStatusToSaturationResult(status)
+        }
+
+        private def convertStatusToSaturationResult(Status status) {
+                switch (status) {
+                        case SATISFIABLE:
+                                PolyhedronSaturationResult.SATURATED
+                        case UNSATISFIABLE:
+                                PolyhedronSaturationResult.EMPTY
+                        case UNKNOWN:
+                                PolyhedronSaturationResult.UNKNOWN
+                        default:
+                                throw new IllegalArgumentException("Unknown Status: " + status)
+                }
+        }
+
+        private def doSaturate() {
+                for (expressionToSaturate : polyhedron.expressionsToSaturate) {
+                        val expr = expressionToSaturate.toExpr
+                        val lowerResult = saturateLowerBound(expr, expressionToSaturate)
+                        if (lowerResult != Status.SATISFIABLE) {
+                                return lowerResult
+                        }
+                        val upperResult = saturateUpperBound(expr, expressionToSaturate)
+                        if (upperResult != Status.SATISFIABLE) {
+                                return upperResult
+                        }
+                }
+                Status.SATISFIABLE
+        }
+
+        private def saturateLowerBound(ArithExpr expr, LinearBoundedExpression expressionToSaturate) {
+                val optimize = prepareOptimize
+                val handle = optimize.MkMinimize(expr)
+                val status = optimize.Check()
+                if (status == Status.SATISFIABLE) {
+                        val value = switch (resultExpr : handle.lower) {
+                                IntNum:
+                                        resultExpr.getInt()
+                                default:
+                                        if (isNegativeInfinity(resultExpr)) {
+                                                null
+                                        } else {
+                                                throw new IllegalArgumentException("Integer result expected, got: " + resultExpr)
+                                        }
+                        }
+                        expressionToSaturate.lowerBound = value
+                }
+                status
+        }
+
+        private def saturateUpperBound(ArithExpr expr, LinearBoundedExpression expressionToSaturate) {
+                val optimize = prepareOptimize
+                val handle = optimize.MkMaximize(expr)
+                val status = optimize.Check()
+                if (status == Status.SATISFIABLE) {
+                        val value = switch (resultExpr : handle.upper) {
+                                IntNum:
+                                        resultExpr.getInt()
+                                default:
+                                        if (isPositiveInfinity(resultExpr)) {
+                                                null
+                                        } else {
+                                                throw new IllegalArgumentException("Integer result expected, got: " + resultExpr)
+                                        }
+                        }
+                        expressionToSaturate.upperBound = value
+                }
+                status
+        }
+
+        private def isPositiveInfinity(Expr expr) {
+                expr.app && expr.getFuncDecl.name == infinitySymbol
+        }
+
+        private def isNegativeInfinity(Expr expr) {
+                // Negative infinity is represented as (* (- 1) oo)
+                if (!expr.app || expr.getFuncDecl.name != multSymbol || expr.numArgs != 2) {
+                        return false
+                }
+                isPositiveInfinity(expr.args.get(1))
+        }
+
+        private def prepareOptimize() {
+                val optimize = mkOptimize()
+                assertConstraints(optimize)
+                optimize
+        }
+
+        private def assertConstraints(Optimize it) {
+                for (pair : variables.entrySet) {
+                        assertBounds(pair.value, pair.key)
+                }
+                for (constraint : polyhedron.constraints) {
+                        val expr = createLinearCombination(constraint.coefficients)
+                        assertBounds(expr, constraint)
+                }
+        }
+
+        private def assertBounds(Optimize it, ArithExpr expression, LinearBoundedExpression bounds) {
+                val lowerBound = bounds.lowerBound
+                val upperBound = bounds.upperBound
+                if (lowerBound == upperBound) {
+                        if (lowerBound === null) {
+                                return
+                        }
+                        Assert(mkEq(expression, mkInt(lowerBound)))
+                } else {
+                        if (lowerBound !== null) {
+                                Assert(mkGe(expression, mkInt(lowerBound)))
+                        }
+                        if (upperBound !== null) {
+                                Assert(mkLe(expression, mkInt(upperBound)))
+                        }
+                }
+        }
+
+        private def toExpr(LinearBoundedExpression linearBoundedExpression) {
+                switch (linearBoundedExpression) {
+                        Dimension: variables.get(linearBoundedExpression)
+                        LinearConstraint: createLinearCombination(linearBoundedExpression.coefficients)
+                        default: throw new IllegalArgumentException("Unknown linear bounded expression:" + linearBoundedExpression)
+                }
+        }
+
+        private def createLinearCombination(Map<Dimension, Integer> coefficients) {
+                val size = coefficients.size
+                val array = newArrayOfSize(size)
+                var int i = 0
+                for (pair : coefficients.entrySet) {
+                        val variable = variables.get(pair.key)
+                        if (variable === null) {
+                                throw new IllegalArgumentException("Unknown dimension: " + pair.key.name)
+                        }
+                        val coefficient = pair.value
+                        val term = if (coefficient == 1) {
+                                        variable
+                                } else {
+                                        mkMul(mkInt(coefficient), variable)
+                                }
+                        array.set(i, term)
+                        i++
+                }
+                mkAdd(array)
+        }
+
+        override close() throws Exception {
+                context.close()
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend
index 20d24b77..5fefa551 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend
@@ -6,7 +6,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics

-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ScopePropagator

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ObjectCreationPrecondition

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
index 701eb054..101f0a3e 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
@@ -12,7 +12,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory

 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethodProvider

-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ScopePropagator

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage

@@ -71,16 +71,13 @@ class ViatraReasoner extends LogicReasoner {
                 }

                 emptySolution.problemConainer = problem

 

-                val ScopePropagator scopePropagator = new ScopePropagator(emptySolution)

-                scopePropagator.propagateAllScopeConstraints

-

                 val method = modelGenerationMethodProvider.createModelGenerationMethod(

                         problem,

                         emptySolution,

                         workspace,

                         viatraConfig.nameNewElements,

                         viatraConfig.typeInferenceMethod,

-                        scopePropagator,

+                        viatraConfig.scopePropagatorStrategy,

                         viatraConfig.documentationLevel

                 )

 

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
index 99decdd9..7a3a2d67 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
@@ -6,6 +6,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser

 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind

 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold

@@ -49,6 +50,8 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration {
          * Configuration for cutting search space.

          */

         public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint

+        

+        public var ScopePropagatorStrategy scopePropagatorStrategy = ScopePropagatorStrategy.PolyhedralTypeHierarchy

 

         public var List<CostObjectiveConfiguration> costObjectives = newArrayList

 }

diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/META-INF/MANIFEST.MF b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/META-INF/MANIFEST.MF
index 76c113c1..43e40319 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/META-INF/MANIFEST.MF
+++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/META-INF/MANIFEST.MF
@@ -11,3 +11,5 @@ Require-Bundle: com.google.guava,
  org.eclipse.xtend.lib,
  org.eclipse.xtend.lib.macro,
  hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery
+Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality,
+ hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.interval
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/Z3PolyhedronSolverTest.xtend b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/Z3PolyhedronSolverTest.xtend
new file mode 100644
index 00000000..2d159752
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/Z3PolyhedronSolverTest.xtend
@@ -0,0 +1,199 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality
+
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Dimension
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearConstraint
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedron
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationOperator
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationResult
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver
+import org.junit.After
+import org.junit.Before
+import org.junit.Test
+
+import static org.junit.Assert.*
+
+class Z3PolyhedronSolverTest {
+        var Z3PolyhedronSolver solver
+        var PolyhedronSaturationOperator operator
+
+        @Before
+        def void setUp() {
+                solver = new Z3PolyhedronSolver(false)
+        }
+
+        @After
+        def void tearDown() {
+                destroyOperatorIfExists()
+        }
+
+        @Test
+        def void singleDimensionTest() {
+                val x = new Dimension("x", 0, 1)
+                createSaturationOperator(new Polyhedron(#[x], #[], #[x]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(0, x.lowerBound)
+                assertEquals(1, x.upperBound)
+        }
+
+        @Test
+        def void singleDimensionNegativeValueTest() {
+                val x = new Dimension("x", -2, -1)
+                createSaturationOperator(new Polyhedron(#[x], #[], #[x]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(-2, x.lowerBound)
+                assertEquals(-1, x.upperBound)
+        }
+
+        @Test
+        def void singleDimensionConstraintTest() {
+                val x = new Dimension("x", null, null)
+                val constraint = new LinearConstraint(#{x -> 2}, 0, 2)
+                createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(0, x.lowerBound)
+                assertEquals(1, x.upperBound)
+        }
+
+        @Test
+        def void singleDimensionConstraintUnitCoefficientTest() {
+                val x = new Dimension("x", null, null)
+                val constraint = new LinearConstraint(#{x -> 1}, 1, 3)
+                createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(1, x.lowerBound)
+                assertEquals(3, x.upperBound)
+        }
+
+        @Test
+        def void singleDimensionConstraintIntegerTest() {
+                val x = new Dimension("x", null, null)
+                val constraint = new LinearConstraint(#{x -> 2}, 0, 3)
+                createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(0, x.lowerBound)
+                assertEquals(1, x.upperBound)
+        }
+
+        @Test
+        def void singleDimensionUnboundedFromAboveTest() {
+                val x = new Dimension("x", 0, null)
+                createSaturationOperator(new Polyhedron(#[x], #[], #[x]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(0, x.lowerBound)
+                assertEquals(null, x.upperBound)
+        }
+
+        @Test
+        def void singleDimensionUnboundedFromBelowTest() {
+                val x = new Dimension("x", null, 0)
+                createSaturationOperator(new Polyhedron(#[x], #[], #[x]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(null, x.lowerBound)
+                assertEquals(0, x.upperBound)
+        }
+
+        @Test
+        def void singleDimensionUnsatisfiableTest() {
+                val x = new Dimension("x", 0, 1)
+                val constraint = new LinearConstraint(#{x -> 2}, -2, -1)
+                createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.EMPTY, result)
+        }
+
+        @Test
+        def void equalityConstraintTest() {
+                val x = new Dimension("x", null, null)
+                val y = new Dimension("y", 1, 2)
+                val constraint = new LinearConstraint(#{x -> 2, y -> 2}, 6, 6)
+                createSaturationOperator(new Polyhedron(#[x, y], #[constraint], #[x]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(1, x.lowerBound)
+                assertEquals(2, x.upperBound)
+        }
+
+        @Test
+        def void saturateConstraintTest() {
+                val x = new Dimension("x", 0, 2)
+                val y = new Dimension("y", 1, 2)
+                val constraint = new LinearConstraint(#{x -> 2, y -> 1}, 0, 8)
+                createSaturationOperator(new Polyhedron(#[x, y], #[constraint], #[constraint]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(1, constraint.lowerBound)
+                assertEquals(6, constraint.upperBound)
+        }
+
+        @Test(expected=IllegalArgumentException)
+        def void unknownVariableTest() {
+                val x = new Dimension("x", 0, 1)
+                val y = new Dimension("y", 0, 1)
+                val constraint = new LinearConstraint(#{y -> 2}, 0, 2)
+                createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))
+
+                saturate()
+        }
+
+        @Test
+        def void unsatisfiableMultipleInheritanceTest() {
+                val x = new Dimension("x", 0, 1)
+                val y = new Dimension("y", 0, 1)
+                val z = new Dimension("z", 0, 1)
+                createSaturationOperator(new Polyhedron(
+                        #[x, y, z],
+                        #[
+                                new LinearConstraint(#{x -> 1, y -> 1}, 1, 1),
+                                new LinearConstraint(#{x -> 1, z -> 1}, 1, 1),
+                                new LinearConstraint(#{y -> 1, z -> 1}, 1, 1)
+                        ],
+                        #[x, y, z]
+                ))
+                
+                val result = saturate()
+                
+                assertEquals(PolyhedronSaturationResult.EMPTY, result)
+        }
+
+        private def createSaturationOperator(Polyhedron polyhedron) {
+                destroyOperatorIfExists()
+                operator = solver.createSaturationOperator(polyhedron)
+        }
+
+        private def destroyOperatorIfExists() {
+                if (operator !== null) {
+                        operator.close
+                }
+        }
+
+        private def saturate() {
+                operator.saturate
+        }
+}