12 files changed, 1359 insertions, 0 deletions

diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/CbcPolyhedronSolverTest.xtend b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/CbcPolyhedronSolverTest.xtend
new file mode 100644
index 00000000..b22e2a20
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/CbcPolyhedronSolverTest.xtend
@@ -0,0 +1,42 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality
+
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Dimension
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedron
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationResult
+import org.junit.Test
+
+import static org.junit.Assert.*
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearConstraint
+
+class CbcPolyhedronSolverTest extends IntegerPolyhedronSolverTest {
+
+        override protected createSolver() {
+                new CbcPolyhedronSolver(false, 10, true)
+        }
+}
+
+class RelaxedCbcPolyhedronSolverTest extends RelaxedPolyhedronSolverTest {
+
+        override protected createSolver() {
+                new CbcPolyhedronSolver(true, 10, true)
+        }
+}
+
+class CbcPolyhedronSolverTimeoutTest {
+
+        @Test
+        def void timeoutTest() {
+                val solver = new CbcPolyhedronSolver(false, 0, true)
+                val x = new Dimension("x", 0, 1)
+                val polyhedron = new Polyhedron(#[x], #[new LinearConstraint(#{x -> 1}, null, 0)], #[x])
+                val operator = solver.createSaturationOperator(polyhedron)
+                try {
+                        val result = operator.saturate
+
+                        assertEquals(PolyhedronSaturationResult.UNKNOWN, result)
+                } finally {
+                        operator.close()
+                }
+        }
+}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend
new file mode 100644
index 00000000..47534618
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend
@@ -0,0 +1,385 @@
+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.PolyhedronSolver
+import org.junit.After
+import org.junit.Before
+import org.junit.Test
+
+import static org.junit.Assert.*
+
+abstract class PolyhedronSolverTest {
+        var PolyhedronSolver solver
+        var PolyhedronSaturationOperator operator
+
+        protected def PolyhedronSolver createSolver()
+
+        @Before
+        def void setUp() {
+                solver = createSolver()
+        }
+
+        @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 singleDimensionUnboundedFromAboveTest() {
+                val x = new Dimension("x", -2, null)
+                createSaturationOperator(new Polyhedron(#[x], #[], #[x]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(-2, x.lowerBound)
+                assertEquals(null, x.upperBound)
+        }
+
+        @Test
+        def void singleDimensionUnboundedFromBelowTest() {
+                val x = new Dimension("x", null, 2)
+                createSaturationOperator(new Polyhedron(#[x], #[], #[x]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(null, x.lowerBound)
+                assertEquals(2, x.upperBound)
+        }
+
+        @Test
+        def void singleDimensionUnboundedTest() {
+                val x = new Dimension("x", null, null)
+                createSaturationOperator(new Polyhedron(#[x], #[], #[x]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(null, x.lowerBound)
+                assertEquals(null, x.upperBound)
+        }
+        
+        @Test
+        def void singleDimensionUnboundedObjectiveTest() {
+                val x = new Dimension("x", null, null)
+                val y = new Dimension("y", 0, 1)
+                val objective = new LinearConstraint(#{x -> 1, y -> 1}, null, null)
+                createSaturationOperator(new Polyhedron(#[x, y], #[], #[objective]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(null, objective.lowerBound)
+                assertEquals(null, objective.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 emptyConstraintTest() {
+                val x = new Dimension("x", 0, 1)
+                val constraint = new LinearConstraint(emptyMap, 0, 1)
+                createSaturationOperator(new Polyhedron(#[x], #[constraint], #[constraint]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(0, constraint.lowerBound)
+                assertEquals(0, constraint.upperBound)
+        }
+
+        @Test
+        def void emptyConstraintUnsatisfiableTest() {
+                val x = new Dimension("x", 0, 1)
+                val constraint = new LinearConstraint(emptyMap, 1, 0)
+                createSaturationOperator(new Polyhedron(#[x], #[constraint], #[constraint]))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.EMPTY, result)
+        }
+        
+        @Test
+        def void unboundedRelaxationWithIntegerSolutionTest() {
+                val x = new Dimension("x", 1, 3)
+                val y = new Dimension("y", null, null)
+                createSaturationOperator(new Polyhedron(
+                        #[x, y],
+                        #[new LinearConstraint(#{x -> 2}, 2, 6)],
+                        #[x, y]
+                ))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(1, x.lowerBound)
+                assertEquals(3, x.upperBound)
+                assertEquals(null, y.lowerBound)
+                assertEquals(null, y.upperBound)
+        }
+
+        protected def createSaturationOperator(Polyhedron polyhedron) {
+                destroyOperatorIfExists()
+                operator = solver.createSaturationOperator(polyhedron)
+        }
+
+        protected def destroyOperatorIfExists() {
+                if (operator !== null) {
+                        operator.close
+                }
+        }
+
+        protected def saturate() {
+                operator.saturate
+        }
+}
+
+abstract class IntegerPolyhedronSolverTest extends PolyhedronSolverTest {
+        @Test
+        def void singleDimensionConstraintNonIntegerTest() {
+                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 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)
+        }
+
+        @Test
+        def void unboundedRelaxationWithNoIntegerSolutionTest() {
+                val x = new Dimension("x", 0, 1)
+                val y = new Dimension("y", null, null)
+                createSaturationOperator(new Polyhedron(
+                        #[x, y],
+                        #[new LinearConstraint(#{x -> 2}, 1, 1)],
+                        #[x, y]
+                ))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.EMPTY, result)
+        }
+}
+
+abstract class RelaxedPolyhedronSolverTest extends PolyhedronSolverTest {
+        @Test
+        def void singleDimensionConstraintNonIntegerTest() {
+                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(2, x.upperBound)
+        }
+
+        @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.SATURATED, result)
+                assertEquals(0, x.lowerBound)
+                assertEquals(1, x.upperBound)
+                assertEquals(0, y.lowerBound)
+                assertEquals(1, y.upperBound)
+                assertEquals(0, z.lowerBound)
+                assertEquals(1, z.upperBound)
+        }
+
+        @Test
+        def void unboundedRelaxationWithNoIntegerSolutionUnconstrainedVariableTest() {
+                val x = new Dimension("x", 1, 2)
+                val y = new Dimension("y", null, null)
+                createSaturationOperator(new Polyhedron(
+                        #[x, y],
+                        #[new LinearConstraint(#{x -> 2}, 3, 3)],
+                        #[x, y]
+                ))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(1, x.lowerBound)
+                assertEquals(2, x.upperBound)
+                assertEquals(null, y.lowerBound)
+                assertEquals(null, y.upperBound)
+        }
+        
+        @Test
+        def void unboundedRelaxationWithNoIntegerSolutionConstrainedVariableTest() {
+                val x = new Dimension("x", 1, 2)
+                val y = new Dimension("y", null, null)
+                createSaturationOperator(new Polyhedron(
+                        #[x, y],
+                        #[new LinearConstraint(#{x -> 2}, 3, 3), new LinearConstraint(#{y -> 1}, null, 1)],
+                        #[x, y]
+                ))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(1, x.lowerBound)
+                assertEquals(2, x.upperBound)
+                assertEquals(null, y.lowerBound)
+                assertEquals(1, y.upperBound)
+        }
+        
+        @Test
+        def void unboundedRelaxationWithNoIntegerSolutionBoundedVariableTest() {
+                val x = new Dimension("x", 1, 2)
+                val y = new Dimension("y", null, 1)
+                createSaturationOperator(new Polyhedron(
+                        #[x, y],
+                        #[new LinearConstraint(#{x -> 2}, 3, 3)],
+                        #[x, y]
+                ))
+
+                val result = saturate()
+
+                assertEquals(PolyhedronSaturationResult.SATURATED, result)
+                assertEquals(1, x.lowerBound)
+                assertEquals(2, x.upperBound)
+                assertEquals(null, y.lowerBound)
+                assertEquals(1, y.upperBound)
+        }
+}
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..49b916d3
--- /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,17 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality
+
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver
+
+class Z3PolyhedronSolverTest extends IntegerPolyhedronSolverTest {
+        
+        override protected createSolver() {
+                new Z3PolyhedronSolver(false, 10)
+        }
+}
+
+class RelaxedZ3PolyhedronSolverTest extends RelaxedPolyhedronSolverTest {
+        
+        override protected createSolver() {
+                new Z3PolyhedronSolver(true, 10)
+        }
+}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/AdditionTest.xtend b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/AdditionTest.xtend
new file mode 100644
index 00000000..de5f40e1
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/AdditionTest.xtend
@@ -0,0 +1,49 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.interval
+
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.Interval
+import java.util.Collection
+import org.junit.Assert
+import org.junit.Test
+import org.junit.runner.RunWith
+import org.junit.runners.Parameterized
+import org.junit.runners.Parameterized.Parameter
+import org.junit.runners.Parameterized.Parameters
+
+import static hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.Interval.*
+
+@RunWith(Parameterized)
+class AdditionTest {
+        @Parameters(name = "{index}: {0} + {1} = {2}")
+        static def Collection<Object[]> data() {
+                #[
+                        #[EMPTY, EMPTY, EMPTY],
+                        #[EMPTY, between(-1, 1), EMPTY],
+                        #[between(-1, 1), EMPTY, EMPTY],
+                        #[UNBOUNDED, UNBOUNDED, UNBOUNDED],
+                        #[UNBOUNDED, upTo(2), UNBOUNDED],
+                        #[UNBOUNDED, above(-2), UNBOUNDED],
+                        #[UNBOUNDED, between(-1, 1), UNBOUNDED],
+                        #[upTo(2), UNBOUNDED, UNBOUNDED],
+                        #[upTo(2), upTo(1), upTo(3)],
+                        #[upTo(2), above(-1), UNBOUNDED],
+                        #[upTo(2), between(-1, 2), upTo(4)],
+                        #[above(-2), UNBOUNDED, UNBOUNDED],
+                        #[above(-2), upTo(1), UNBOUNDED],
+                        #[above(-2), above(-1), above(-3)],
+                        #[above(-2), between(-1, 2), above(-3)],
+                        #[between(-2, 3), UNBOUNDED, UNBOUNDED],
+                        #[between(-2, 3), upTo(1), upTo(4)],
+                        #[between(-2, 3), above(-1), above(-3)],
+                        #[between(-2, 3), between(-1, 2.5), between(-3, 5.5)]
+                ]
+        }
+        
+        @Parameter(0) public var Interval a
+        @Parameter(1) public var Interval b
+        @Parameter(2) public var Interval result
+        
+        @Test
+        def void additionTest() {
+                Assert.assertEquals(result, a + b)
+        }
+}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/DivisionTest.xtend b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/DivisionTest.xtend
new file mode 100644
index 00000000..3a8c0c5d
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/DivisionTest.xtend
@@ -0,0 +1,202 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.interval
+
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.Interval
+import java.util.Collection
+import org.junit.Assert
+import org.junit.Test
+import org.junit.runner.RunWith
+import org.junit.runners.Parameterized
+import org.junit.runners.Parameterized.Parameter
+import org.junit.runners.Parameterized.Parameters
+
+import static hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.Interval.*
+
+@RunWith(Parameterized)
+class DivisionTest {
+        @Parameters(name="{index}: {0} / {1} = {2}")
+        static def Collection<Object[]> data() {
+                #[
+                        #[EMPTY, EMPTY, EMPTY],
+                        #[EMPTY, between(-1, 1), EMPTY],
+                        #[between(-1, 1), EMPTY, EMPTY],
+                        #[UNBOUNDED, UNBOUNDED, UNBOUNDED],
+                        #[UNBOUNDED, upTo(-2), UNBOUNDED],
+                        #[UNBOUNDED, upTo(0), UNBOUNDED],
+                        #[UNBOUNDED, upTo(3), UNBOUNDED],
+                        #[UNBOUNDED, above(-2), UNBOUNDED],
+                        #[UNBOUNDED, above(0), UNBOUNDED],
+                        #[UNBOUNDED, above(3), UNBOUNDED],
+                        #[UNBOUNDED, between(-4, -3), UNBOUNDED],
+                        #[UNBOUNDED, between(-4, 0), UNBOUNDED],
+                        #[UNBOUNDED, between(-3, 4), UNBOUNDED],
+                        #[UNBOUNDED, between(0, 4), UNBOUNDED],
+                        #[UNBOUNDED, between(3, 4), UNBOUNDED],
+                        #[UNBOUNDED, ZERO, EMPTY],
+                        #[upTo(-12), UNBOUNDED, UNBOUNDED],
+                        #[upTo(-12), upTo(-2), above(0)],
+                        #[upTo(-12), upTo(0), above(0)],
+                        #[upTo(-12), upTo(3), UNBOUNDED],
+                        #[upTo(-12), above(-2), UNBOUNDED],
+                        #[upTo(-12), above(0), upTo(0)],
+                        #[upTo(-12), above(3), upTo(0)],
+                        #[upTo(-12), between(-4, -3), above(3)],
+                        #[upTo(-12), between(-4, 0), above(3)],
+                        #[upTo(-12), between(-3, 4), UNBOUNDED],
+                        #[upTo(-12), between(0, 4), upTo(-3)],
+                        #[upTo(-12), between(3, 4), upTo(-3)],
+                        #[upTo(-12), ZERO, EMPTY],
+                        #[upTo(0), UNBOUNDED, UNBOUNDED],
+                        #[upTo(0), upTo(-2), above(0)],
+                        #[upTo(0), upTo(0), above(0)],
+                        #[upTo(0), upTo(3), UNBOUNDED],
+                        #[upTo(0), above(-2), UNBOUNDED],
+                        #[upTo(0), above(0), upTo(0)],
+                        #[upTo(0), above(3), upTo(0)],
+                        #[upTo(0), between(-4, -3), above(0)],
+                        #[upTo(0), between(-4, 0), above(0)],
+                        #[upTo(0), between(-3, 4), UNBOUNDED],
+                        #[upTo(0), between(0, 4), upTo(0)],
+                        #[upTo(0), between(3, 4), upTo(0)],
+                        #[upTo(0), ZERO, EMPTY],
+                        #[upTo(12), UNBOUNDED, UNBOUNDED],
+                        #[upTo(12), upTo(-2), above(-6)],
+                        #[upTo(12), upTo(0), UNBOUNDED],
+                        #[upTo(12), upTo(3), UNBOUNDED],
+                        #[upTo(12), above(-2), UNBOUNDED],
+                        #[upTo(12), above(0), UNBOUNDED],
+                        #[upTo(12), above(3), upTo(4)],
+                        #[upTo(12), between(-4, -3), above(-4)],
+                        #[upTo(12), between(-4, 0), UNBOUNDED],
+                        #[upTo(12), between(-3, 4), UNBOUNDED],
+                        #[upTo(12), between(0, 4), UNBOUNDED],
+                        #[upTo(12), between(3, 4), upTo(4)],
+                        #[upTo(12), ZERO, EMPTY],
+                        #[above(-12), UNBOUNDED, UNBOUNDED],
+                        #[above(-12), upTo(-2), upTo(6)],
+                        #[above(-12), upTo(0), UNBOUNDED],
+                        #[above(-12), upTo(3), UNBOUNDED],
+                        #[above(-12), above(-2), UNBOUNDED],
+                        #[above(-12), above(0), UNBOUNDED],
+                        #[above(-12), above(3), above(-4)],
+                        #[above(-12), between(-4, -3), upTo(4)],
+                        #[above(-12), between(-4, 0), UNBOUNDED],
+                        #[above(-12), between(-3, 4), UNBOUNDED],
+                        #[above(-12), between(0, 4), UNBOUNDED],
+                        #[above(-12), between(3, 4), above(-4)],
+                        #[above(-12), ZERO, EMPTY],
+                        #[above(0), UNBOUNDED, UNBOUNDED],
+                        #[above(0), upTo(-2), upTo(0)],
+                        #[above(0), upTo(0), upTo(0)],
+                        #[above(0), upTo(3), UNBOUNDED],
+                        #[above(0), above(-2), UNBOUNDED],
+                        #[above(0), above(0), above(0)],
+                        #[above(0), above(3), above(0)],
+                        #[above(0), between(-4, -3), upTo(0)],
+                        #[above(0), between(-4, 0), upTo(0)],
+                        #[above(0), between(-3, 4), UNBOUNDED],
+                        #[above(0), between(0, 4), above(0)],
+                        #[above(0), between(3, 4), above(0)],
+                        #[above(0), ZERO, EMPTY],
+                        #[above(12), UNBOUNDED, UNBOUNDED],
+                        #[above(12), upTo(-2), upTo(0)],
+                        #[above(12), upTo(0), upTo(0)],
+                        #[above(12), upTo(3), UNBOUNDED],
+                        #[above(12), above(-2), UNBOUNDED],
+                        #[above(12), above(0), above(0)],
+                        #[above(12), above(3), above(0)],
+                        #[above(12), between(-4, -3), upTo(-3)],
+                        #[above(12), between(-4, 0), upTo(-3)],
+                        #[above(12), between(-3, 4), UNBOUNDED],
+                        #[above(12), between(0, 4), above(3)],
+                        #[above(12), between(3, 4), above(3)],
+                        #[above(12), ZERO, EMPTY],
+                        #[between(-36, -12), UNBOUNDED, UNBOUNDED],
+                        #[between(-36, -12), upTo(-2), between(0, 18)],
+                        #[between(-36, -12), upTo(0), above(0)],
+                        #[between(-36, -12), upTo(3), UNBOUNDED],
+                        #[between(-36, -12), above(-2), UNBOUNDED],
+                        #[between(-36, -12), above(0), upTo(0)],
+                        #[between(-36, -12), above(3), between(-12, 0)],
+                        #[between(-36, -12), between(-4, -3), between(3, 12)],
+                        #[between(-36, -12), between(-4, 0), above(3)],
+                        #[between(-36, -12), between(-3, 4), UNBOUNDED],
+                        #[between(-36, -12), between(0, 4), upTo(-3)],
+                        #[between(-36, -12), between(3, 4), between(-12, -3)],
+                        #[between(-36, -12), ZERO, EMPTY],
+                        #[between(-36, 0), UNBOUNDED, UNBOUNDED],
+                        #[between(-36, 0), upTo(-2), between(0, 18)],
+                        #[between(-36, 0), upTo(0), above(0)],
+                        #[between(-36, 0), upTo(3), UNBOUNDED],
+                        #[between(-36, 0), above(-2), UNBOUNDED],
+                        #[between(-36, 0), above(0), upTo(0)],
+                        #[between(-36, 0), above(3), between(-12, 0)],
+                        #[between(-36, 0), between(-4, -3), between(0, 12)],
+                        #[between(-36, 0), between(-4, 0), above(0)],
+                        #[between(-36, 0), between(-3, 4), UNBOUNDED],
+                        #[between(-36, 0), between(0, 4), upTo(0)],
+                        #[between(-36, 0), between(3, 4), between(-12, 0)],
+                        #[between(-36, 0), ZERO, EMPTY],
+                        #[between(-12, 36), UNBOUNDED, UNBOUNDED],
+                        #[between(-12, 36), upTo(-2), between(-18, 6)],
+                        #[between(-12, 36), upTo(0), UNBOUNDED],
+                        #[between(-12, 36), upTo(3), UNBOUNDED],
+                        #[between(-12, 36), above(-2), UNBOUNDED],
+                        #[between(-12, 36), above(0), UNBOUNDED],
+                        #[between(-12, 36), above(3), between(-4, 12)],
+                        #[between(-12, 36), between(-4, -3), between(-12, 4)],
+                        #[between(-12, 36), between(-4, 0), UNBOUNDED],
+                        #[between(-12, 36), between(-3, 4), UNBOUNDED],
+                        #[between(-12, 36), between(0, 4), UNBOUNDED],
+                        #[between(-12, 36), between(3, 4), between(-4, 12)],
+                        #[between(-12, 36), ZERO, EMPTY],
+                        #[between(0, 36), UNBOUNDED, UNBOUNDED],
+                        #[between(0, 36), upTo(-2), between(-18, 0)],
+                        #[between(0, 36), upTo(0), upTo(0)],
+                        #[between(0, 36), upTo(3), UNBOUNDED],
+                        #[between(0, 36), above(-2), UNBOUNDED],
+                        #[between(0, 36), above(0), above(0)],
+                        #[between(0, 36), above(3), between(0, 12)],
+                        #[between(0, 36), between(-4, -3), between(-12, 0)],
+                        #[between(0, 36), between(-4, 0), upTo(0)],
+                        #[between(0, 36), between(-3, 4), UNBOUNDED],
+                        #[between(0, 36), between(0, 4), above(0)],
+                        #[between(0, 36), between(3, 4), between(0, 12)],
+                        #[between(0, 36), ZERO, EMPTY],
+                        #[between(12, 36), UNBOUNDED, UNBOUNDED],
+                        #[between(12, 36), upTo(-2), between(-18, 0)],
+                        #[between(12, 36), upTo(0), upTo(0)],
+                        #[between(12, 36), upTo(3), UNBOUNDED],
+                        #[between(12, 36), above(-2), UNBOUNDED],
+                        #[between(12, 36), above(0), above(0)],
+                        #[between(12, 36), above(3), between(0, 12)],
+                        #[between(12, 36), between(-4, -3), between(-12, -3)],
+                        #[between(12, 36), between(-4, 0), upTo(-3)],
+                        #[between(12, 36), between(-3, 4), UNBOUNDED],
+                        #[between(12, 36), between(0, 4), above(3)],
+                        #[between(12, 36), between(3, 4), between(3, 12)],
+                        #[between(12, 36), ZERO, EMPTY],
+                        #[ZERO, UNBOUNDED, ZERO],
+                        #[ZERO, upTo(-2), ZERO],
+                        #[ZERO, upTo(0), ZERO],
+                        #[ZERO, upTo(3), ZERO],
+                        #[ZERO, above(-2), ZERO],
+                        #[ZERO, above(0), ZERO],
+                        #[ZERO, above(3), ZERO],
+                        #[ZERO, between(-4, -3), ZERO],
+                        #[ZERO, between(-4, 0), ZERO],
+                        #[ZERO, between(-3, 4), ZERO],
+                        #[ZERO, between(0, 4), ZERO],
+                        #[ZERO, between(3, 4), ZERO],
+                        #[ZERO, ZERO, EMPTY]
+                ]
+        }
+
+        @Parameter(0) public var Interval a
+        @Parameter(1) public var Interval b
+        @Parameter(2) public var Interval result
+
+        @Test
+        def void divisionTest() {
+                Assert.assertEquals(result, a / b)
+        }
+}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/MinAggregatorTest.xtend b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/MinAggregatorTest.xtend
new file mode 100644
index 00000000..7d46e16c
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/MinAggregatorTest.xtend
@@ -0,0 +1,67 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.interval
+
+import com.google.common.collect.HashMultiset
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.Interval
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.IntervalAggregationMode
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.IntervalAggregationOperator
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.IntervalRedBlackNode
+import java.math.BigDecimal
+import java.util.Random
+import org.junit.Assert
+import org.junit.Before
+import org.junit.Test
+
+import static hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.Interval.*
+
+class MinAggregatorTest {
+        val aggregator = new IntervalAggregationOperator(IntervalAggregationMode.MIN)
+        var IntervalRedBlackNode value = null
+
+        @Before
+        def void reset() {
+                value = aggregator.createNeutral
+        }
+
+        @Test
+        def void emptyTest() {
+                assertEquals(EMPTY)
+        }
+
+        @Test
+        def void largeTest() {
+                val starts = #[null, new BigDecimal(-3), new BigDecimal(-2), new BigDecimal(-1)]
+                val ends = #[new BigDecimal(1), new BigDecimal(2), new BigDecimal(3), null]
+                val current = HashMultiset.create
+                val random = new Random(1)
+                for (var int i = 0; i < 1000; i++) {
+                        val start = starts.get(random.nextInt(starts.size))
+                        val end = ends.get(random.nextInt(ends.size))
+                        val interval = Interval.of(start, end)
+                        val isInsert = !current.contains(interval) || random.nextInt(3) == 0
+                        if (isInsert) {
+                                current.add(interval)
+                        } else {
+                                current.remove(interval)
+                        }
+                        val expected = current.stream.reduce(aggregator.mode).orElse(EMPTY)
+                        update(interval, isInsert)
+                        assertEquals(expected)
+                }
+        }
+
+        private def update(Interval interval, boolean isInsert) {
+                value = aggregator.update(value, interval, isInsert)
+                val nodes = newArrayList
+                var node = value.min
+                while (node !== null) {
+                        nodes += node
+                        node = node.successor
+                }
+                value.assertSubtreeIsValid
+        }
+
+        private def assertEquals(Interval interval) {
+                val actual = aggregator.getAggregate(value)
+                Assert.assertEquals(interval, actual)
+        }
+}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/MultiplicationTest.xtend b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/MultiplicationTest.xtend
new file mode 100644
index 00000000..5f997094
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/MultiplicationTest.xtend
@@ -0,0 +1,205 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.interval
+
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.Interval
+import java.util.Collection
+import org.junit.Assert
+import org.junit.Test
+import org.junit.runner.RunWith
+import org.junit.runners.Parameterized
+import org.junit.runners.Parameterized.Parameter
+import org.junit.runners.Parameterized.Parameters
+
+import static hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.Interval.*
+
+@RunWith(Parameterized)
+class MultiplicationTest {
+        @Parameters(name="{index}: {0} * {1} = {2}")
+        static def Collection<Object[]> data() {
+                #[
+                        #[EMPTY, EMPTY, EMPTY],
+                        #[EMPTY, between(-1, 1), EMPTY],
+                        #[between(-1, 1), EMPTY, EMPTY],
+                        #[UNBOUNDED, UNBOUNDED, UNBOUNDED],
+                        #[UNBOUNDED, upTo(-2), UNBOUNDED],
+                        #[UNBOUNDED, upTo(0), UNBOUNDED],
+                        #[UNBOUNDED, upTo(3), UNBOUNDED],
+                        #[UNBOUNDED, above(-2), UNBOUNDED],
+                        #[UNBOUNDED, above(0), UNBOUNDED],
+                        #[UNBOUNDED, above(3), UNBOUNDED],
+                        #[UNBOUNDED, between(-4, -3), UNBOUNDED],
+                        #[UNBOUNDED, between(-4, 0), UNBOUNDED],
+                        #[UNBOUNDED, between(-3, 4), UNBOUNDED],
+                        #[UNBOUNDED, between(0, 4), UNBOUNDED],
+                        #[UNBOUNDED, between(3, 4), UNBOUNDED],
+                        #[UNBOUNDED, ZERO, ZERO],
+                        #[upTo(-5), UNBOUNDED, UNBOUNDED],
+                        #[upTo(-5), upTo(-2), above(10)],
+                        #[upTo(-5), upTo(0), above(0)],
+                        #[upTo(-5), upTo(3), UNBOUNDED],
+                        #[upTo(-5), above(-2), UNBOUNDED],
+                        #[upTo(-5), above(0), upTo(0)],
+                        #[upTo(-5), above(3), upTo(-15)],
+                        #[upTo(-5), between(-4, -3), above(15)],
+                        #[upTo(-5), between(-4, 0), above(0)],
+                        #[upTo(-5), between(-3, 4), UNBOUNDED],
+                        #[upTo(-5), between(0, 4), upTo(0)],
+                        #[upTo(-5), between(3, 4), upTo(-15)],
+                        #[upTo(-5), ZERO, ZERO],
+                        #[upTo(0), UNBOUNDED, UNBOUNDED],
+                        #[upTo(0), upTo(-2), above(0)],
+                        #[upTo(0), upTo(0), above(0)],
+                        #[upTo(0), upTo(3), UNBOUNDED],
+                        #[upTo(0), above(-2), UNBOUNDED],
+                        #[upTo(0), above(0), upTo(0)],
+                        #[upTo(0), above(3), upTo(0)],
+                        #[upTo(0), between(-4, -3), above(0)],
+                        #[upTo(0), between(-4, 0), above(0)],
+                        #[upTo(0), between(-3, 4), UNBOUNDED],
+                        #[upTo(0), between(0, 4), upTo(0)],
+                        #[upTo(0), between(3, 4), upTo(0)],
+                        #[upTo(0), ZERO, ZERO],
+                        #[upTo(5), UNBOUNDED, UNBOUNDED],
+                        #[upTo(5), upTo(-2), UNBOUNDED],
+                        #[upTo(5), upTo(0), UNBOUNDED],
+                        #[upTo(5), upTo(3), UNBOUNDED],
+                        #[upTo(5), above(-2), UNBOUNDED],
+                        #[upTo(5), above(0), UNBOUNDED],
+                        #[upTo(5), above(3), UNBOUNDED],
+                        #[upTo(5), between(-4, -3), above(-20)],
+                        #[upTo(5), between(-4, 0), above(-20)],
+                        #[upTo(5), between(-3, 4), UNBOUNDED],
+                        #[upTo(5), between(0, 4), upTo(20)],
+                        #[upTo(5), between(3, 4), upTo(20)],
+                        #[upTo(5), ZERO, ZERO],
+                        #[above(-5), UNBOUNDED, UNBOUNDED],
+                        #[above(-5), upTo(-2), UNBOUNDED],
+                        #[above(-5), upTo(0), UNBOUNDED],
+                        #[above(-5), upTo(3), UNBOUNDED],
+                        #[above(-5), above(-2), UNBOUNDED],
+                        #[above(-5), above(0), UNBOUNDED],
+                        #[above(-5), above(3), UNBOUNDED],
+                        #[above(-5), between(-4, -3), upTo(20)],
+                        #[above(-5), between(-4, 0), upTo(20)],
+                        #[above(-5), between(-3, 4), UNBOUNDED],
+                        #[above(-5), between(0, 4), above(-20)],
+                        #[above(-5), between(3, 4), above(-20)],
+                        #[above(-5), ZERO, ZERO],
+                        #[above(0), UNBOUNDED, UNBOUNDED],
+                        #[above(0), upTo(-2), upTo(0)],
+                        #[above(0), upTo(0), upTo(0)],
+                        #[above(0), upTo(3), UNBOUNDED],
+                        #[above(0), above(-2), UNBOUNDED],
+                        #[above(0), above(0), above(0)],
+                        #[above(0), above(3), above(0)],
+                        #[above(0), between(-4, -3), upTo(0)],
+                        #[above(0), between(-4, 0), upTo(0)],
+                        #[above(0), between(-3, 4), UNBOUNDED],
+                        #[above(0), between(0, 4), above(0)],
+                        #[above(0), between(3, 4), above(0)],
+                        #[above(0), ZERO, ZERO],
+                        #[above(5), UNBOUNDED, UNBOUNDED],
+                        #[above(5), upTo(-2), upTo(-10)],
+                        #[above(5), upTo(0), upTo(0)],
+                        #[above(5), upTo(3), UNBOUNDED],
+                        #[above(5), above(-2), UNBOUNDED],
+                        #[above(5), above(0), above(0)],
+                        #[above(5), above(3), above(15)],
+                        #[above(5), between(-4, -3), upTo(-15)],
+                        #[above(5), between(-4, 0), upTo(0)],
+                        #[above(5), between(-3, 4), UNBOUNDED],
+                        #[above(5), between(0, 4), above(0)],
+                        #[above(5), between(3, 4), above(15)],
+                        #[above(5), ZERO, ZERO],
+                        #[between(-6, -5), UNBOUNDED, UNBOUNDED],
+                        #[between(-6, -5), upTo(-2), above(10)],
+                        #[between(-6, -5), upTo(0), above(0)],
+                        #[between(-6, -5), upTo(3), above(-18)],
+                        #[between(-6, -5), above(-2), upTo(12)],
+                        #[between(-6, -5), above(0), upTo(0)],
+                        #[between(-6, -5), above(3), upTo(-15)],
+                        #[between(-6, -5), between(-4, -3), between(15, 24)],
+                        #[between(-6, -5), between(-4, 0), between(0, 24)],
+                        #[between(-6, -5), between(-3, 4), between(-24, 18)],
+                        #[between(-6, -5), between(0, 4), between(-24, 0)],
+                        #[between(-6, -5), between(3, 4), between(-24, -15)],
+                        #[between(-6, -5), ZERO, ZERO],
+                        #[between(-6, 0), UNBOUNDED, UNBOUNDED],
+                        #[between(-6, 0), upTo(-2), above(0)],
+                        #[between(-6, 0), upTo(0), above(0)],
+                        #[between(-6, 0), upTo(3), above(-18)],
+                        #[between(-6, 0), above(-2), upTo(12)],
+                        #[between(-6, 0), above(0), upTo(0)],
+                        #[between(-6, 0), above(3), upTo(0)],
+                        #[between(-6, 0), between(-4, -3), between(0, 24)],
+                        #[between(-6, 0), between(-4, 0), between(0, 24)],
+                        #[between(-6, 0), between(-3, 4), between(-24, 18)],
+                        #[between(-6, 0), between(0, 4), between(-24, 0)],
+                        #[between(-6, 0), between(3, 4), between(-24, 0)],
+                        #[between(-6, 0), ZERO, ZERO],
+                        #[between(-5, 6), UNBOUNDED, UNBOUNDED],
+                        #[between(-5, 6), upTo(-2), UNBOUNDED],
+                        #[between(-5, 6), upTo(0), UNBOUNDED],
+                        #[between(-5, 6), upTo(3), UNBOUNDED],
+                        #[between(-5, 6), above(-2), UNBOUNDED],
+                        #[between(-5, 6), above(0), UNBOUNDED],
+                        #[between(-5, 6), above(3), UNBOUNDED],
+                        #[between(-5, 6), between(-4, -3), between(-24, 20)],
+                        #[between(-5, 6), between(-4, 0), between(-24, 20)],
+                        #[between(-5, 6), between(-3, 4), between(-20, 24)],
+                        #[between(-5, 6), between(-3, 2), between(-18, 15)],
+                        #[between(-5, 1), between(-3, 4), between(-20, 15)],
+                        #[between(-5, 1), between(-3, 2), between(-10, 15)],
+                        #[between(-5, 6), between(0, 4), between(-20, 24)],
+                        #[between(-5, 6), between(3, 4), between(-20, 24)],
+                        #[between(-5, 6), ZERO, ZERO],
+                        #[between(0, 6), UNBOUNDED, UNBOUNDED],
+                        #[between(0, 6), upTo(-2), upTo(0)],
+                        #[between(0, 6), upTo(0), upTo(0)],
+                        #[between(0, 6), upTo(3), upTo(18)],
+                        #[between(0, 6), above(-2), above(-12)],
+                        #[between(0, 6), above(0), above(0)],
+                        #[between(0, 6), above(3), above(0)],
+                        #[between(0, 6), between(-4, -3), between(-24, 0)],
+                        #[between(0, 6), between(-4, 0), between(-24, 0)],
+                        #[between(0, 6), between(-3, 4), between(-18, 24)],
+                        #[between(0, 6), between(0, 4), between(0, 24)],
+                        #[between(0, 6), between(3, 4), between(0, 24)],
+                        #[between(0, 6), ZERO, ZERO],
+                        #[between(5, 6), UNBOUNDED, UNBOUNDED],
+                        #[between(5, 6), upTo(-2), upTo(-10)],
+                        #[between(5, 6), upTo(0), upTo(0)],
+                        #[between(5, 6), upTo(3), upTo(18)],
+                        #[between(5, 6), above(-2), above(-12)],
+                        #[between(5, 6), above(0), above(0)],
+                        #[between(5, 6), above(3), above(15)],
+                        #[between(5, 6), between(-4, -3), between(-24, -15)],
+                        #[between(5, 6), between(-4, 0), between(-24, 0)],
+                        #[between(5, 6), between(-3, 4), between(-18, 24)],
+                        #[between(5, 6), between(0, 4), between(0, 24)],
+                        #[between(5, 6), between(3, 4), between(15, 24)],
+                        #[between(5, 6), ZERO, ZERO],
+                        #[ZERO, UNBOUNDED, ZERO],
+                        #[ZERO, upTo(-2), ZERO],
+                        #[ZERO, upTo(0), ZERO],
+                        #[ZERO, upTo(3), ZERO],
+                        #[ZERO, above(-2), ZERO],
+                        #[ZERO, above(0), ZERO],
+                        #[ZERO, above(3), ZERO],
+                        #[ZERO, between(-4, -3), ZERO],
+                        #[ZERO, between(-4, 0), ZERO],
+                        #[ZERO, between(-3, 4), ZERO],
+                        #[ZERO, between(0, 4), ZERO],
+                        #[ZERO, between(3, 4), ZERO],
+                        #[ZERO, ZERO, ZERO]
+                ]
+        }
+
+        @Parameter(0) public var Interval a
+        @Parameter(1) public var Interval b
+        @Parameter(2) public var Interval result
+
+        @Test
+        def void multiplicatonTest() {
+                Assert.assertEquals(result, a * b)
+        }
+}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/NegationTest.xtend b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/NegationTest.xtend
new file mode 100644
index 00000000..477e925e
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/NegationTest.xtend
@@ -0,0 +1,34 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.interval
+
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.Interval
+import java.util.Collection
+import org.junit.Assert
+import org.junit.Test
+import org.junit.runner.RunWith
+import org.junit.runners.Parameterized
+import org.junit.runners.Parameterized.Parameter
+import org.junit.runners.Parameterized.Parameters
+
+import static hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.Interval.*
+
+@RunWith(Parameterized)
+class NegationTest {
+        @Parameters(name = "{index}: -{0} = {1}")
+        static def Collection<Object[]> data() {
+                #[
+                        #[EMPTY, EMPTY],
+                        #[UNBOUNDED, UNBOUNDED],
+                        #[upTo(1), above(-1)],
+                        #[above(1), upTo(-1)],
+                        #[between(2, 3), between(-3, -2)]
+                ]
+        }
+        
+        @Parameter(0) public var Interval a
+        @Parameter(1) public var Interval result
+        
+        @Test
+        def void negationTest() {
+                Assert.assertEquals(result, -a)
+        }
+}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/PowerTest.xtend b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/PowerTest.xtend
new file mode 100644
index 00000000..c842d90d
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/PowerTest.xtend
@@ -0,0 +1,43 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.interval
+
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.Interval
+import java.util.Collection
+import org.junit.Assert
+import org.junit.Test
+import org.junit.runner.RunWith
+import org.junit.runners.Parameterized
+import org.junit.runners.Parameterized.Parameter
+import org.junit.runners.Parameterized.Parameters
+
+import static hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.Interval.*
+
+@RunWith(Parameterized)
+class PowerTest {
+        @Parameters(name="{index}: {0} ** {1} = {2}")
+        static def Collection<Object[]> data() {
+                #[
+                        #[EMPTY, EMPTY, EMPTY],
+                        #[EMPTY, between(-1, 1), EMPTY],
+                        #[between(-1, 1), EMPTY, EMPTY],
+                        #[upTo(-1), between(-1, 2), EMPTY],
+                        #[upTo(0), between(-1, 2), between(0, 0)],
+                        #[upTo(2), between(-1, 2), above(0)],
+                        #[upTo(2), between(1, 2), between(0, 4)],
+                        #[above(1), between(1, 2), above(1)],
+                        #[between(2, 4), upTo(1), between(0, 4)],
+                        #[between(0.25, 0.5), upTo(1), above(0.25)],
+                        #[between(2, 3), above(1), above(2)],
+                        #[between(0.25, 0.5), above(1), between(0, 0.5)],
+                        #[between(1, 2), between(-1, 2), between(0.5, 4)]
+                ]
+        }
+
+        @Parameter(0) public var Interval a
+        @Parameter(1) public var Interval b
+        @Parameter(2) public var Interval result
+
+        @Test
+        def void powerTest() {
+                Assert.assertEquals(result, a ** b)
+        }
+}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/RelationTest.xtend b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/RelationTest.xtend
new file mode 100644
index 00000000..5527fbaa
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/RelationTest.xtend
@@ -0,0 +1,126 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.interval
+
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.Interval
+import java.util.Collection
+import org.junit.Assert
+import org.junit.Test
+import org.junit.runner.RunWith
+import org.junit.runners.Parameterized
+import org.junit.runners.Parameterized.Parameter
+import org.junit.runners.Parameterized.Parameters
+
+import static hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.Interval.*
+
+@RunWith(Parameterized)
+class RelationTest {
+        @Parameters(name = "{index}: {0} <> {1}")
+        static def Collection<Object[]> data() {
+                #[
+                        #[EMPTY, EMPTY, true, false, true, false, EMPTY],
+                        #[EMPTY, between(1, 2), true, false, true, false, between(1, 2)],
+                        #[between(1, 2), EMPTY, true, false, true, false, between(1, 2)],
+                        #[upTo(1), upTo(0), false, true, false, true, upTo(1)],
+                        #[upTo(1), upTo(1), false, true, false, true, upTo(1)],
+                        #[upTo(1), upTo(2), false, true, false, true, upTo(2)],
+                        #[upTo(1), above(0), false, true, false, true, UNBOUNDED],
+                        #[upTo(1), above(1), false, true, false, true, UNBOUNDED],
+                        #[upTo(1), above(2), false, false, true, true, UNBOUNDED],
+                        #[upTo(1), between(-1, -1), false, true, false, true, upTo(1)],
+                        #[upTo(1), between(-1, 0), false, true, false, true, upTo(1)],
+                        #[upTo(1), between(-1, 1), false, true, false, true, upTo(1)],
+                        #[upTo(1), between(-1, 2), false, true, false, true, upTo(2)],
+                        #[upTo(1), between(1, 1), false, true, false, true, upTo(1)],
+                        #[upTo(1), between(1, 2), false, true, false, true, upTo(2)],
+                        #[upTo(1), between(2, 2), false, false, true, true, upTo(2)],
+                        #[upTo(1), between(2, 3), false, false, true, true, upTo(3)],
+                        #[above(1), upTo(0), false, false, false, false, UNBOUNDED],
+                        #[above(1), upTo(1), false, true, false, false, UNBOUNDED],
+                        #[above(1), upTo(2), false, true, false, true, UNBOUNDED],
+                        #[above(1), above(0), false, true, false, true, above(0)],
+                        #[above(1), above(1), false, true, false, true, above(1)],
+                        #[above(1), above(2), false, true, false, true, above(1)],
+                        #[above(1), between(-1, -1), false, false, false, false, above(-1)],
+                        #[above(1), between(-1, 0), false, false, false, false, above(-1)],
+                        #[above(1), between(-1, 1), false, true, false, false, above(-1)],
+                        #[above(1), between(-1, 2), false, true, false, true, above(-1)],
+                        #[above(1), between(1, 1), false, true, false, false, above(1)],
+                        #[above(1), between(1, 2), false, true, false, true, above(1)],
+                        #[above(1), between(2, 2), false, true, false, true, above(1)],
+                        #[above(1), between(2, 3), false, true, false, true, above(1)],
+                        #[between(1, 1), upTo(0), false, false, false, false, upTo(1)],
+                        #[between(1, 1), upTo(1), false, true, false, false, upTo(1)],
+                        #[between(1, 1), upTo(2), false, true, false, true, upTo(2)],
+                        #[between(1, 1), above(0), false, true, false, true, above(0)],
+                        #[between(1, 1), above(1), false, true, false, true, above(1)],
+                        #[between(1, 1), above(2), false, false, true, true, above(1)],
+                        #[between(1, 1), between(-1, -1), false, false, false, false, between(-1, 1)],
+                        #[between(1, 1), between(-1, 0), false, false, false, false, between(-1, 1)],
+                        #[between(1, 1), between(-1, 1), false, true, false, false, between(-1, 1)],
+                        #[between(1, 1), between(-1, 2), false, true, false, true, between(-1, 2)],
+                        #[between(1, 1), between(1, 1), true, true, false, false, between(1, 1)],
+                        #[between(1, 1), between(1, 2), false, true, false, true, between(1, 2)],
+                        #[between(1, 1), between(2, 2), false, false, true, true, between(1, 2)],
+                        #[between(1, 1), between(2, 3), false, false, true, true, between(1, 3)],
+                        #[between(-1, 1), upTo(-2), false, false, false, false, upTo(1)],
+                        #[between(-1, 1), upTo(-1), false, true, false, false, upTo(1)],
+                        #[between(-1, 1), upTo(0), false, true, false, true, upTo(1)],
+                        #[between(-1, 1), upTo(1), false, true, false, true, upTo(1)],
+                        #[between(-1, 1), upTo(2), false, true, false, true, upTo(2)],
+                        #[between(-1, 1), above(-2), false, true, false, true, above(-2)],
+                        #[between(-1, 1), above(-1), false, true, false, true, above(-1)],
+                        #[between(-1, 1), above(0), false, true, false, true, above(-1)],
+                        #[between(-1, 1), above(1), false, true, false, true, above(-1)],
+                        #[between(-1, 1), above(2), false, false, true, true, above(-1)],
+                        #[between(-1, 1), between(-3, -2), false, false, false, false, between(-3, 1)],
+                        #[between(-1, 1), between(-2, -2), false, false, false, false, between(-2, 1)],
+                        #[between(-1, 1), between(-2, -1), false, true, false, false, between(-2, 1)],
+                        #[between(-1, 1), between(-2, 0), false, true, false, true, between(-2, 1)],
+                        #[between(-1, 1), between(-2, 1), false, true, false, true, between(-2, 1)],
+                        #[between(-1, 1), between(-2, 2), false, true, false, true, between(-2, 2)],
+                        #[between(-1, 1), between(-1, -1), false, true, false, false, between(-1, 1)],
+                        #[between(-1, 1), between(-1, 0), false, true, false, true, between(-1, 1)],
+                        #[between(-1, 1), between(-1, 1), false, true, false, true, between(-1, 1)],
+                        #[between(-1, 1), between(-1, 2), false, true, false, true, between(-1, 2)],
+                        #[between(-1, 1), between(0, 0), false, true, false, true, between(-1, 1)],
+                        #[between(-1, 1), between(0, 1), false, true, false, true, between(-1, 1)],
+                        #[between(-1, 1), between(0, 2), false, true, false, true, between(-1, 2)],
+                        #[between(-1, 1), between(1, 1), false, true, false, true, between(-1, 1)],
+                        #[between(-1, 1), between(1, 2), false, true, false, true, between(-1, 2)],
+                        #[between(-1, 1), between(2, 2), false, false, true, true, between(-1, 2)],
+                        #[between(-1, 1), between(2, 3), false, false, true, true, between(-1, 3)]
+                ]
+        }
+        
+        @Parameter(0) public var Interval a
+        @Parameter(1) public var Interval b
+        @Parameter(2) public var boolean mustEqual
+        @Parameter(3) public var boolean mayEqual
+        @Parameter(4) public var boolean mustBeLessThan
+        @Parameter(5) public var boolean mayBeLessThan
+        @Parameter(6) public var Interval join
+        
+        @Test
+        def void mustEqualTest() {
+                Assert.assertEquals(mustEqual, a.mustEqual(b))
+        }
+        
+        @Test
+        def void mayEqualTest() {
+                Assert.assertEquals(mayEqual, a.mayEqual(b))
+        }
+        
+        @Test
+        def void mustBeLessThanTest() {
+                Assert.assertEquals(mustBeLessThan, a.mustBeLessThan(b))
+        }
+        
+        @Test
+        def void mayBeLessThanTest() {
+                Assert.assertEquals(mayBeLessThan, a.mayBeLessThan(b))
+        }
+        
+        @Test
+        def void joinTest() {
+                Assert.assertEquals(join, a.join(b))
+        }
+}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/SubtractionTest.xtend b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/SubtractionTest.xtend
new file mode 100644
index 00000000..30709a9e
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/SubtractionTest.xtend
@@ -0,0 +1,49 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.interval
+
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.Interval
+import java.util.Collection
+import org.junit.Assert
+import org.junit.Test
+import org.junit.runner.RunWith
+import org.junit.runners.Parameterized
+import org.junit.runners.Parameterized.Parameter
+import org.junit.runners.Parameterized.Parameters
+
+import static hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.Interval.*
+
+@RunWith(Parameterized)
+class SubtractionTest {
+        @Parameters(name = "{index}: {0} - {1} = {2}")
+        static def Collection<Object[]> data() {
+                #[
+                        #[EMPTY, EMPTY, EMPTY],
+                        #[EMPTY, between(-1, 1), EMPTY],
+                        #[between(-1, 1), EMPTY, EMPTY],
+                        #[UNBOUNDED, UNBOUNDED, UNBOUNDED],
+                        #[UNBOUNDED, upTo(2), UNBOUNDED],
+                        #[UNBOUNDED, above(-2), UNBOUNDED],
+                        #[UNBOUNDED, between(-1, 1), UNBOUNDED],
+                        #[upTo(2), UNBOUNDED, UNBOUNDED],
+                        #[upTo(2), upTo(1), UNBOUNDED],
+                        #[upTo(2), above(-1), upTo(3)],
+                        #[upTo(2), between(-1, 2), upTo(3)],
+                        #[above(-2), UNBOUNDED, UNBOUNDED],
+                        #[above(-2), upTo(1), above(-3)],
+                        #[above(-2), above(-1), UNBOUNDED],
+                        #[above(-2), between(-1, 2), above(-4)],
+                        #[between(-2, 3), UNBOUNDED, UNBOUNDED],
+                        #[between(-2, 3), upTo(1), above(-3)],
+                        #[between(-2, 3), above(-1), upTo(4)],
+                        #[between(-2, 3), between(-1, 2.5), between(-4.5, 4)]
+                ]
+        }
+        
+        @Parameter(0) public var Interval a
+        @Parameter(1) public var Interval b
+        @Parameter(2) public var Interval result
+        
+        @Test
+        def void subtractionTest() {
+                Assert.assertEquals(result, a - b)
+        }
+}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/SumAggregatorTest.xtend b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/SumAggregatorTest.xtend
new file mode 100644
index 00000000..56172b6c
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/interval/SumAggregatorTest.xtend
@@ -0,0 +1,140 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.interval
+
+import com.google.common.collect.HashMultiset
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.Interval
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.IntervalAggregationMode
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.IntervalAggregationOperator
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.IntervalRedBlackNode
+import java.math.BigDecimal
+import java.util.Random
+import org.junit.Assert
+import org.junit.Before
+import org.junit.Test
+
+import static hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.Interval.*
+
+class SumAggregatorTest {
+        val aggregator = new IntervalAggregationOperator(IntervalAggregationMode.SUM)
+        var IntervalRedBlackNode value = null
+
+        @Before
+        def void reset() {
+                value = aggregator.createNeutral
+        }
+
+        @Test
+        def void emptyTest() {
+                assertEquals(ZERO)
+        }
+
+        @Test
+        def void addSingleTest() {
+                add(between(-1, 1))
+                assertEquals(between(-1, 1))
+        }
+
+        @Test
+        def void addRemoveTest() {
+                add(between(-1, 1))
+                remove(between(-1, 1))
+                assertEquals(ZERO)
+        }
+
+        @Test
+        def void addTwoTest() {
+                add(between(-1, 1))
+                add(above(2))
+                assertEquals(above(1))
+        }
+
+        @Test
+        def void addTwoRemoveFirstTest() {
+                add(between(-1, 1))
+                add(above(2))
+                remove(between(-1, 1))
+                assertEquals(above(2))
+        }
+
+        @Test
+        def void addTwoRemoveSecondTest() {
+                add(between(-1, 1))
+                add(above(2))
+                remove(above(2))
+                assertEquals(between(-1, 1))
+        }
+
+        @Test
+        def void addMultiplicityTest() {
+                add(between(-1, 1))
+                add(between(-1, 1))
+                add(between(-1, 1))
+                assertEquals(between(-3, 3))
+        }
+
+        @Test
+        def void removeAllMultiplicityTest() {
+                add(between(-1, 1))
+                add(between(-1, 1))
+                add(between(-1, 1))
+                remove(between(-1, 1))
+                remove(between(-1, 1))
+                remove(between(-1, 1))
+                assertEquals(ZERO)
+        }
+
+        @Test
+        def void removeSomeMultiplicityTest() {
+                add(between(-1, 1))
+                add(between(-1, 1))
+                add(between(-1, 1))
+                remove(between(-1, 1))
+                remove(between(-1, 1))
+                assertEquals(between(-1, 1))
+        }
+
+        @Test
+        def void largeTest() {
+                val starts = #[null, new BigDecimal(-3), new BigDecimal(-2), new BigDecimal(-1)]
+                val ends = #[new BigDecimal(1), new BigDecimal(2), new BigDecimal(3), null]
+                val current = HashMultiset.create
+                val random = new Random(1)
+                for (var int i = 0; i < 1000; i++) {
+                        val start = starts.get(random.nextInt(starts.size))
+                        val end = ends.get(random.nextInt(ends.size))
+                        val interval = Interval.of(start, end)
+                        val isInsert = !current.contains(interval) || random.nextInt(3) == 0
+                        if (isInsert) {
+                                current.add(interval)
+                        } else {
+                                current.remove(interval)
+                        }
+                        val expected = current.stream.reduce(aggregator.mode).orElse(ZERO)
+                        update(interval, isInsert)
+                        assertEquals(expected)
+                }
+        }
+
+        private def update(Interval interval, boolean isInsert) {
+                value = aggregator.update(value, interval, isInsert)
+                val nodes = newArrayList
+                var node = value.min
+                while (node !== null) {
+                        nodes += node
+                        node = node.successor
+                }
+                value.assertSubtreeIsValid
+        }
+
+        private def add(Interval interval) {
+                update(interval, true)
+        }
+
+        private def remove(Interval interval) {
+                update(interval, false)
+        }
+
+        private def assertEquals(Interval interval) {
+                val actual = aggregator.getAggregate(value)
+                Assert.assertEquals(interval, actual)
+        }
+}