1 files changed, 64 insertions, 8 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
index 9c6cb82e..4e046190 100644
--- 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
@@ -3,6 +3,7 @@ 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 {
@@ -52,16 +53,66 @@ class Polyhedron {
         val List<LinearBoundedExpression> expressionsToSaturate
 
         override toString() '''
-        Dimensions:
-                «FOR dimension : dimensions»
-                        «dimension»
-                «ENDFOR»
-        Constraints:
-                «FOR constraint : constraints»
-                        «constraint»
-                «ENDFOR»
+                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
@@ -80,6 +131,11 @@ abstract class LinearBoundedExpression {
                         upperBound = tighterBound
                 }
         }
+
+        def void assertEqualsTo(int bound) {
+                tightenLowerBound(bound)
+                tightenUpperBound(bound)
+        }
 }
 
 @Accessors