1 files changed, 179 insertions, 0 deletions

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..4e046190
--- /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,179 @@
+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.Data
+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»
+        '''
+
+        def createSignature() {
+                val size = dimensions.size + constraints.size
+                val lowerBounds = newArrayOfSize(size)
+                val upperBounds = newArrayOfSize(size)
+                var int i = 0
+                for (dimension : dimensions) {
+                        lowerBounds.set(i, dimension.lowerBound)
+                        upperBounds.set(i, dimension.upperBound)
+                        i++
+                }
+                for (constraint : constraints) {
+                        lowerBounds.set(i, constraint.lowerBound)
+                        upperBounds.set(i, constraint.upperBound)
+                        i++
+                }
+                new PolyhedronSignature.Bounds(lowerBounds, upperBounds)
+        }
+
+        def applySignature(PolyhedronSignature.Bounds signature) {
+                val lowerBounds = signature.lowerBounds
+                val upperBounds = signature.upperBounds
+                var int i = 0
+                for (dimension : dimensions) {
+                        dimension.lowerBound = lowerBounds.get(i)
+                        dimension.upperBound = upperBounds.get(i)
+                        i++
+                }
+                for (constraint : constraints) {
+                        constraint.lowerBound = lowerBounds.get(i)
+                        constraint.upperBound = upperBounds.get(i)
+                        i++
+                }
+        }
+}
+
+abstract class PolyhedronSignature {
+        public static val EMPTY = new PolyhedronSignature {
+                override toString() {
+                        "PolyhedronSignature.EMPTY"
+                }
+        }
+
+        private new() {
+        }
+
+        @Data
+        static class Bounds extends PolyhedronSignature {
+                val Integer[] lowerBounds
+                val Integer[] upperBounds
+        }
+}
+
+@Accessors
+abstract class LinearBoundedExpression {
+        var Integer lowerBound
+        var Integer upperBound
+
+        def void tightenLowerBound(Integer tighterBound) {
+                if (lowerBound === null || (tighterBound !== null && lowerBound < tighterBound)) {
+                        lowerBound = tighterBound
+                }
+        }
+
+        def void tightenUpperBound(Integer tighterBound) {
+                if (upperBound === null || (tighterBound !== null && upperBound > tighterBound)) {
+                        upperBound = tighterBound
+                }
+        }
+
+        def void assertEqualsTo(int bound) {
+                tightenLowerBound(bound)
+                tightenUpperBound(bound)
+        }
+}
+
+@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»'''
+        }
+
+}