Make polyhedron solvers more robust

4 files changed, 81 insertions, 29 deletions

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/AbstractPolyhedronSaturationOperator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/AbstractPolyhedronSaturationOperator.xtend
new file mode 100644
index 00000000..94f97e94
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/AbstractPolyhedronSaturationOperator.xtend
@@ -0,0 +1,53 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
+
+import com.google.common.collect.ImmutableList
+import org.eclipse.xtend.lib.annotations.Accessors
+
+abstract class AbstractPolyhedronSaturationOperator implements PolyhedronSaturationOperator {
+        @Accessors val Polyhedron polyhedron
+
+        new(Polyhedron polyhedron) {
+                if (polyhedron.dimensions.empty) {
+                        throw new IllegalArgumentException("Polyhedron must have at least one dimension.")
+                }
+                this.polyhedron = polyhedron
+        }
+
+        override saturate() {
+                if (polyhedron.expressionsToSaturate.empty) {
+                        return PolyhedronSaturationResult.SATURATED
+                }
+                for (constraint : polyhedron.constraints) {
+                        if (constraint.zero) {
+                                if (constraint.lowerBound !== null && constraint.lowerBound > 0) {
+                                        return PolyhedronSaturationResult.EMPTY
+                                }
+                                if (constraint.upperBound !== null && constraint.upperBound < 0) {
+                                        return PolyhedronSaturationResult.EMPTY
+                                }
+                        } else {
+                                if (constraint.lowerBound !== null && constraint.upperBound !== null &&
+                                        constraint.upperBound < constraint.lowerBound) {
+                                        return PolyhedronSaturationResult.EMPTY
+                                }
+                        }
+                }
+                doSaturate()
+        }
+
+        protected def PolyhedronSaturationResult doSaturate()
+
+        protected def getNonTrivialConstraints() {
+                ImmutableList.copyOf(polyhedron.constraints.filter [ constraint |
+                        (constraint.lowerBound !== null || constraint.upperBound !== null) && !constraint.zero
+                ])
+        }
+
+        private static def isZero(LinearConstraint constraint) {
+                constraint.coefficients.values.forall[it == 0]
+        }
+
+        override close() throws Exception {
+                // Nothing to close by default.
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend
index 1f6d4e8f..7753e68e 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend
@@ -3,8 +3,8 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
 import com.google.common.collect.ImmutableMap
 import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcResult
 import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcSolver
+import java.util.List
 import java.util.Map
-import org.eclipse.xtend.lib.annotations.Accessors
 import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
 
 @FinalFieldsConstructor
@@ -21,8 +21,7 @@ class CbcPolyhedronSolver implements PolyhedronSolver {
         }
 }
 
-class CbcSaturationOperator implements PolyhedronSaturationOperator {
-        @Accessors val Polyhedron polyhedron
+class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator {
         val double timeoutSeconds
         val boolean silent
         val double[] columnLowerBounds
@@ -31,7 +30,7 @@ class CbcSaturationOperator implements PolyhedronSaturationOperator {
         val Map<Dimension, Integer> dimensionsToIndicesMap
 
         new(Polyhedron polyhedron, double timeoutSeconds, boolean silent) {
-                this.polyhedron = polyhedron
+                super(polyhedron)
                 this.timeoutSeconds = timeoutSeconds
                 this.silent = silent
                 val numDimensions = polyhedron.dimensions.size
@@ -41,25 +40,26 @@ class CbcSaturationOperator implements PolyhedronSaturationOperator {
                 dimensionsToIndicesMap = ImmutableMap.copyOf(polyhedron.dimensions.indexed.toMap([value], [key]))
         }
 
-        override saturate() {
+        override doSaturate() {
                 val numDimensions = polyhedron.dimensions.size
                 for (var int j = 0; j < numDimensions; j++) {
                         val dimension = polyhedron.dimensions.get(j)
                         columnLowerBounds.set(j, dimension.lowerBound.toDouble(Double.NEGATIVE_INFINITY))
                         columnUpperBounds.set(j, dimension.upperBound.toDouble(Double.POSITIVE_INFINITY))
                 }
-                val numConstraints = polyhedron.constraints.size
+                val constraints = nonTrivialConstraints
+                val numConstraints = constraints.size
                 val rowStarts = newIntArrayOfSize(numConstraints + 1)
                 val rowLowerBounds = newDoubleArrayOfSize(numConstraints)
                 val rowUpperBounds = newDoubleArrayOfSize(numConstraints)
-                val numEntries = polyhedron.constraints.map[coefficients.size].reduce[a, b|a + b] ?: 0
+                val numEntries = constraints.map[coefficients.size].reduce[a, b|a + b] ?: 0
                 rowStarts.set(numConstraints, numEntries)
                 val columnIndices = newIntArrayOfSize(numEntries)
                 val entries = newDoubleArrayOfSize(numEntries)
                 var int index = 0
                 for (var int i = 0; i < numConstraints; i++) {
                         rowStarts.set(i, index)
-                        val constraint = polyhedron.constraints.get(i)
+                        val constraint = constraints.get(i)
                         rowLowerBounds.set(i, constraint.lowerBound.toDouble(Double.NEGATIVE_INFINITY))
                         rowUpperBounds.set(i, constraint.upperBound.toDouble(Double.POSITIVE_INFINITY))
                         if (!dimensionsToIndicesMap.keySet.containsAll(constraint.coefficients.keySet)) {
@@ -102,11 +102,12 @@ class CbcSaturationOperator implements PolyhedronSaturationOperator {
                                 CbcResult.SolutionBounded: {
                                         val value = Math.floor(minimizationResult.value)
                                         expressionToSaturate.lowerBound = value as int
-                                        setBound(expressionToSaturate, value, columnLowerBounds, rowLowerBounds)
+                                        setBound(expressionToSaturate, constraints, value, columnLowerBounds, rowLowerBounds)
                                 }
                                 case CbcResult.SOLUTION_UNBOUNDED: {
                                         expressionToSaturate.lowerBound = null
-                                        setBound(expressionToSaturate, Double.NEGATIVE_INFINITY, columnLowerBounds, rowLowerBounds)
+                                        setBound(expressionToSaturate, constraints, Double.NEGATIVE_INFINITY, columnLowerBounds,
+                                                rowLowerBounds)
                                 }
                                 case CbcResult.UNSAT:
                                         return PolyhedronSaturationResult.EMPTY
@@ -126,11 +127,12 @@ class CbcSaturationOperator implements PolyhedronSaturationOperator {
                                 CbcResult.SolutionBounded: {
                                         val value = Math.ceil(-maximizationResult.value)
                                         expressionToSaturate.upperBound = value as int
-                                        setBound(expressionToSaturate, value, columnUpperBounds, rowUpperBounds)
+                                        setBound(expressionToSaturate, constraints, value, columnUpperBounds, rowUpperBounds)
                                 }
                                 case CbcResult.SOLUTION_UNBOUNDED: {
                                         expressionToSaturate.upperBound = null
-                                        setBound(expressionToSaturate, Double.POSITIVE_INFINITY, columnUpperBounds, rowUpperBounds)
+                                        setBound(expressionToSaturate, constraints, Double.POSITIVE_INFINITY, columnUpperBounds,
+                                                rowUpperBounds)
                                 }
                                 case CbcResult.UNSAT:
                                         throw new RuntimeException("Minimization was SAT, but maximization is UNSAT")
@@ -160,23 +162,19 @@ class CbcSaturationOperator implements PolyhedronSaturationOperator {
                 index
         }
 
-        private def void setBound(LinearBoundedExpression expression, double bound, double[] columnBounds,
-                double[] rowBounds) {
+        private def void setBound(LinearBoundedExpression expression, List<LinearConstraint> constraints, double bound,
+                double[] columnBounds, double[] rowBounds) {
                 switch (expression) {
                         Dimension: {
                                 val j = getIndex(expression)
                                 columnBounds.set(j, bound)
                         }
                         LinearConstraint: {
-                                val i = polyhedron.constraints.indexOf(expression)
+                                val i = constraints.indexOf(expression)
                                 if (i >= 0) {
                                         rowBounds.set(i, bound)
                                 }
                         }
                 }
         }
-
-        override close() throws Exception {
-                // Nothing to close
-        }
 }
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
index ce357272..3fd50071 100644
--- 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
@@ -61,7 +61,7 @@ class PolyhedronScopePropagator extends ScopePropagator {
         override void propagateAllScopeConstraints() {
                 resetBounds()
                 populatePolyhedronFromScope()
-                println(polyhedron)
+//              println(polyhedron)
                 val result = operator.saturate()
                 if (result == PolyhedronSaturationResult.EMPTY) {
                         throw new IllegalStateException("Scope bounds cannot be satisfied")
@@ -71,7 +71,7 @@ class PolyhedronScopePropagator extends ScopePropagator {
                                 super.propagateAllScopeConstraints()
                         }
                 }
-                println(polyhedron)
+//              println(polyhedron)
         }
 
         def resetBounds() {
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
index f1a84f2d..c8759a46 100644
--- 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
@@ -8,7 +8,6 @@ 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 {
@@ -27,21 +26,20 @@ class Z3PolyhedronSolver implements PolyhedronSolver {
         }
 }
 
-class Z3SaturationOperator implements PolyhedronSaturationOperator {
+class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator {
         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) {
+                super(polyhedron)
                 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) {
@@ -52,8 +50,8 @@ class Z3SaturationOperator implements PolyhedronSaturationOperator {
                 ]
         }
 
-        override saturate() {
-                val status = doSaturate()
+        override doSaturate() {
+                val status = executeSolver()
                 convertStatusToSaturationResult(status)
         }
 
@@ -70,7 +68,7 @@ class Z3SaturationOperator implements PolyhedronSaturationOperator {
                 }
         }
 
-        private def doSaturate() {
+        private def executeSolver() {
                 for (expressionToSaturate : polyhedron.expressionsToSaturate) {
                         val expr = expressionToSaturate.toExpr
                         val lowerResult = saturateLowerBound(expr, expressionToSaturate)
@@ -147,7 +145,7 @@ class Z3SaturationOperator implements PolyhedronSaturationOperator {
                 for (pair : variables.entrySet) {
                         assertBounds(pair.value, pair.key)
                 }
-                for (constraint : polyhedron.constraints) {
+                for (constraint : nonTrivialConstraints) {
                         val expr = createLinearCombination(constraint.coefficients)
                         assertBounds(expr, constraint)
                 }
@@ -181,6 +179,9 @@ class Z3SaturationOperator implements PolyhedronSaturationOperator {
 
         private def createLinearCombination(Map<Dimension, Integer> coefficients) {
                 val size = coefficients.size
+                if (size == 0) {
+                        return mkInt(0)
+                }
                 val array = newArrayOfSize(size)
                 var int i = 0
                 for (pair : coefficients.entrySet) {