1 files changed, 584 insertions, 0 deletions

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/Interval.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/Interval.xtend
new file mode 100644
index 00000000..691c8783
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/interval/Interval.xtend
@@ -0,0 +1,584 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval
+
+import java.math.BigDecimal
+import java.math.MathContext
+import java.math.RoundingMode
+import org.eclipse.xtend.lib.annotations.Data
+
+abstract class Interval implements Comparable<Interval> {
+        static val PRECISION = 32
+        package static val ROUND_DOWN = new MathContext(PRECISION, RoundingMode.FLOOR)
+        package static val ROUND_UP = new MathContext(PRECISION, RoundingMode.CEILING)
+
+        private new() {
+        }
+
+        abstract def boolean mustEqual(Interval other)
+
+        abstract def boolean mayEqual(Interval other)
+
+        def mustNotEqual(Interval other) {
+                !mayEqual(other)
+        }
+
+        def mayNotEqual(Interval other) {
+                !mustEqual(other)
+        }
+
+        abstract def boolean mustBeLessThan(Interval other)
+
+        abstract def boolean mayBeLessThan(Interval other)
+
+        def mustBeLessThanOrEqual(Interval other) {
+                !mayBeGreaterThan(other)
+        }
+
+        def mayBeLessThanOrEqual(Interval other) {
+                !mustBeGreaterThan(other)
+        }
+
+        def mustBeGreaterThan(Interval other) {
+                other.mustBeLessThan(this)
+        }
+
+        def mayBeGreaterThan(Interval other) {
+                other.mayBeLessThan(this)
+        }
+
+        def mustBeGreaterThanOrEqual(Interval other) {
+                other.mustBeLessThanOrEqual(this)
+        }
+
+        def mayBeGreaterThanOrEqual(Interval other) {
+                other.mayBeLessThanOrEqual(this)
+        }
+
+        abstract def Interval min(Interval other)
+
+        abstract def Interval max(Interval other)
+
+        abstract def Interval join(Interval other)
+
+        def +() {
+                this
+        }
+
+        abstract def Interval -()
+
+        abstract def Interval +(Interval other)
+
+        abstract def Interval -(Interval other)
+
+        abstract def Interval *(int count)
+
+        abstract def Interval *(Interval other)
+
+        abstract def Interval /(Interval other)
+
+        abstract def Interval **(Interval other)
+
+        public static val EMPTY = new Interval {
+                override mustEqual(Interval other) {
+                        true
+                }
+
+                override mayEqual(Interval other) {
+                        false
+                }
+
+                override mustBeLessThan(Interval other) {
+                        true
+                }
+
+                override mayBeLessThan(Interval other) {
+                        false
+                }
+
+                override min(Interval other) {
+                        EMPTY
+                }
+
+                override max(Interval other) {
+                        EMPTY
+                }
+
+                override join(Interval other) {
+                        other
+                }
+
+                override -() {
+                        EMPTY
+                }
+
+                override +(Interval other) {
+                        EMPTY
+                }
+
+                override -(Interval other) {
+                        EMPTY
+                }
+
+                override *(int count) {
+                        EMPTY
+                }
+
+                override *(Interval other) {
+                        EMPTY
+                }
+
+                override /(Interval other) {
+                        EMPTY
+                }
+
+                override **(Interval other) {
+                        EMPTY
+                }
+
+                override toString() {
+                        "∅"
+                }
+
+                override compareTo(Interval o) {
+                        if (o == EMPTY) {
+                                0
+                        } else {
+                                -1
+                        }
+                }
+
+        }
+
+        public static val Interval ZERO = new NonEmpty(BigDecimal.ZERO, BigDecimal.ZERO)
+
+        public static val Interval UNBOUNDED = new NonEmpty(null, null)
+
+        static def Interval of(BigDecimal lower, BigDecimal upper) {
+                new NonEmpty(lower, upper)
+        }
+
+        static def between(double lower, double upper) {
+                of(new BigDecimal(lower, ROUND_DOWN), new BigDecimal(upper, ROUND_UP))
+        }
+
+        static def upTo(double upper) {
+                of(null, new BigDecimal(upper, ROUND_UP))
+        }
+
+        static def above(double lower) {
+                of(new BigDecimal(lower, ROUND_DOWN), null)
+        }
+
+        @Data
+        private static class NonEmpty extends Interval {
+                val BigDecimal lower
+                val BigDecimal upper
+
+                /**
+                 * Construct a new non-empty interval.
+                 * 
+                 * @param lower The lower bound of the interval. Use <code>null</code> for negative infinity.
+                 * @param upper The upper bound of the interval. Use <code>null</code> for positive infinity.
+                 */
+                new(BigDecimal lower, BigDecimal upper) {
+                        if (lower !== null && upper !== null && lower > upper) {
+                                throw new IllegalArgumentException("Lower bound of interval must not be larger than upper bound")
+                        }
+                        this.lower = lower
+                        this.upper = upper
+                }
+
+                override mustEqual(Interval other) {
+                        switch (other) {
+                                case EMPTY: true
+                                NonEmpty: lower == upper && lower == other.lower && lower == other.upper
+                                default: throw new IllegalArgumentException("Unknown interval: " + other)
+                        }
+                }
+
+                override mayEqual(Interval other) {
+                        if (other instanceof NonEmpty) {
+                                (lower === null || other.upper === null || lower <= other.upper) &&
+                                        (other.lower === null || upper === null || other.lower <= upper)
+                        } else {
+                                false
+                        }
+                }
+
+                override mustBeLessThan(Interval other) {
+                        switch (other) {
+                                case EMPTY: true
+                                NonEmpty: upper !== null && other.lower !== null && upper < other.lower
+                                default: throw new IllegalArgumentException("Unknown interval: " + other)
+                        }
+                }
+
+                override mayBeLessThan(Interval other) {
+                        if (other instanceof NonEmpty) {
+                                lower === null || other.upper === null || lower < other.upper
+                        } else {
+                                false
+                        }
+                }
+
+                override min(Interval other) {
+                        switch (other) {
+                                case EMPTY: this
+                                NonEmpty: min(other)
+                                default: throw new IllegalArgumentException("Unknown interval: " + other)
+                        }
+                }
+
+                def min(NonEmpty other) {
+                        new NonEmpty(
+                                lower.tryMin(other.lower),
+                                if(other.upper === null) upper else if(upper === null) other.upper else upper.min(other.upper)
+                        )
+                }
+
+                override max(Interval other) {
+                        switch (other) {
+                                case EMPTY: this
+                                NonEmpty: max(other)
+                                default: throw new IllegalArgumentException("Unknown interval: " + other)
+                        }
+                }
+
+                def max(NonEmpty other) {
+                        new NonEmpty(
+                                if(other.lower === null) lower else if(lower === null) other.lower else lower.max(other.lower),
+                                upper.tryMax(other.upper)
+                        )
+                }
+
+                override join(Interval other) {
+                        switch (other) {
+                                case EMPTY: this
+                                NonEmpty: new NonEmpty(lower.tryMin(other.lower), upper.tryMax(other.upper))
+                                default: throw new IllegalArgumentException("Unknown interval: " + other)
+                        }
+                }
+
+                override -() {
+                        new NonEmpty(upper?.negate(ROUND_DOWN), lower?.negate(ROUND_UP))
+                }
+
+                override +(Interval other) {
+                        switch (other) {
+                                case EMPTY: EMPTY
+                                NonEmpty: this + other
+                                default: throw new IllegalArgumentException("Unknown interval: " + other)
+                        }
+                }
+
+                def +(NonEmpty other) {
+                        new NonEmpty(
+                                lower.tryAdd(other.lower, ROUND_DOWN),
+                                upper.tryAdd(other.upper, ROUND_UP)
+                        )
+                }
+
+                private static def tryAdd(BigDecimal a, BigDecimal b, MathContext mc) {
+                        if (b === null) {
+                                null
+                        } else {
+                                a?.add(b, mc)
+                        }
+                }
+
+                override -(Interval other) {
+                        switch (other) {
+                                case EMPTY: EMPTY
+                                NonEmpty: this - other
+                                default: throw new IllegalArgumentException("Unknown interval: " + other)
+                        }
+                }
+
+                def -(NonEmpty other) {
+                        new NonEmpty(
+                                lower.trySubtract(other.upper, ROUND_DOWN),
+                                upper.trySubtract(other.lower, ROUND_UP)
+                        )
+                }
+
+                private static def trySubtract(BigDecimal a, BigDecimal b, MathContext mc) {
+                        if (b === null) {
+                                null
+                        } else {
+                                a?.subtract(b, mc)
+                        }
+                }
+
+                override *(int count) {
+                        val bigCount = new BigDecimal(count)
+                        new NonEmpty(
+                                lower.tryMultiply(bigCount, ROUND_DOWN),
+                                upper.tryMultiply(bigCount, ROUND_UP)
+                        )
+                }
+
+                override *(Interval other) {
+                        switch (other) {
+                                case EMPTY: EMPTY
+                                NonEmpty: this * other
+                                default: throw new IllegalArgumentException("Unknown interval: " + other)
+                        }
+                }
+
+                def *(NonEmpty other) {
+                        if (this == ZERO || other == ZERO) {
+                                ZERO
+                        } else if (nonpositive) {
+                                if (other.nonpositive) {
+                                        new NonEmpty(
+                                                upper.multiply(other.upper, ROUND_DOWN),
+                                                lower.tryMultiply(other.lower, ROUND_UP)
+                                        )
+                                } else if (other.nonnegative) {
+                                        new NonEmpty(
+                                                lower.tryMultiply(other.upper, ROUND_DOWN),
+                                                upper.multiply(other.lower, ROUND_UP)
+                                        )
+                                } else {
+                                        new NonEmpty(
+                                                lower.tryMultiply(other.upper, ROUND_DOWN),
+                                                lower.tryMultiply(other.lower, ROUND_UP)
+                                        )
+                                }
+                        } else if (nonnegative) {
+                                if (other.nonpositive) {
+                                        new NonEmpty(
+                                                upper.tryMultiply(other.lower, ROUND_DOWN),
+                                                lower.multiply(other.upper, ROUND_UP)
+                                        )
+                                } else if (other.nonnegative) {
+                                        new NonEmpty(
+                                                lower.multiply(other.lower, ROUND_DOWN),
+                                                upper.tryMultiply(other.upper, ROUND_UP)
+                                        )
+                                } else {
+                                        new NonEmpty(
+                                                upper.tryMultiply(other.lower, ROUND_DOWN),
+                                                upper.tryMultiply(other.upper, ROUND_UP)
+                                        )
+                                }
+                        } else {
+                                if (other.nonpositive) {
+                                        new NonEmpty(
+                                                upper.tryMultiply(other.lower, ROUND_DOWN),
+                                                lower.tryMultiply(other.lower, ROUND_UP)
+                                        )
+                                } else if (other.nonnegative) {
+                                        new NonEmpty(
+                                                lower.tryMultiply(other.upper, ROUND_DOWN),
+                                                upper.tryMultiply(other.upper, ROUND_UP)
+                                        )
+                                } else {
+                                        new NonEmpty(
+                                                lower.tryMultiply(other.upper, ROUND_DOWN).tryMin(upper.tryMultiply(other.lower, ROUND_DOWN)),
+                                                lower.tryMultiply(other.lower, ROUND_UP).tryMax(upper.tryMultiply(other.upper, ROUND_UP))
+                                        )
+                                }
+                        }
+                }
+
+                private def isNonpositive() {
+                        upper !== null && upper <= BigDecimal.ZERO
+                }
+
+                private def isNonnegative() {
+                        lower !== null && lower >= BigDecimal.ZERO
+                }
+
+                private static def tryMultiply(BigDecimal a, BigDecimal b, MathContext mc) {
+                        if (b === null) {
+                                null
+                        } else {
+                                a?.multiply(b, mc)
+                        }
+                }
+
+                private static def tryMin(BigDecimal a, BigDecimal b) {
+                        if (b === null) {
+                                null
+                        } else {
+                                a?.min(b)
+                        }
+                }
+
+                private static def tryMax(BigDecimal a, BigDecimal b) {
+                        if (b === null) {
+                                null
+                        } else {
+                                a?.max(b)
+                        }
+                }
+
+                override /(Interval other) {
+                        switch (other) {
+                                case EMPTY: EMPTY
+                                NonEmpty: this / other
+                                default: throw new IllegalArgumentException("Unknown interval: " + other)
+                        }
+                }
+
+                def /(NonEmpty other) {
+                        if (other == ZERO) {
+                                EMPTY
+                        } else if (this == ZERO) {
+                                ZERO
+                        } else if (other.strictlyNegative) {
+                                if (nonpositive) {
+                                        new NonEmpty(
+                                                upper.tryDivide(other.lower, ROUND_DOWN),
+                                                lower.tryDivide(other.upper, ROUND_UP)
+                                        )
+                                } else if (nonnegative) {
+                                        new NonEmpty(
+                                                upper.tryDivide(other.upper, ROUND_DOWN),
+                                                lower.tryDivide(other.lower, ROUND_UP)
+                                        )
+                                } else { // lower < 0 < upper
+                                        new NonEmpty(
+                                                upper.tryDivide(other.upper, ROUND_DOWN),
+                                                lower.tryDivide(other.upper, ROUND_UP)
+                                        )
+                                }
+                        } else if (other.strictlyPositive) {
+                                if (nonpositive) {
+                                        new NonEmpty(
+                                                lower.tryDivide(other.lower, ROUND_DOWN),
+                                                upper.tryDivide(other.upper, ROUND_UP)
+                                        )
+                                } else if (nonnegative) {
+                                        new NonEmpty(
+                                                lower.tryDivide(other.upper, ROUND_DOWN),
+                                                upper.tryDivide(other.lower, ROUND_UP)
+                                        )
+                                } else { // lower < 0 < upper
+                                        new NonEmpty(
+                                                lower.tryDivide(other.lower, ROUND_DOWN),
+                                                upper.tryDivide(other.lower, ROUND_UP)
+                                        )
+                                }
+                        } else { // other contains 0
+                                if (other.lower == BigDecimal.ZERO) { // 0 == other.lower < other.upper, because [0, 0] was exluded earlier
+                                        if (nonpositive) {
+                                                new NonEmpty(null, upper.tryDivide(other.upper, ROUND_UP))
+                                        } else if (nonnegative) {
+                                                new NonEmpty(lower.tryDivide(other.upper, ROUND_DOWN), null)
+                                        } else { // lower < 0 < upper
+                                                UNBOUNDED
+                                        }
+                                } else if (other.upper == BigDecimal.ZERO) { // other.lower < other.upper == 0
+                                        if (nonpositive) {
+                                                new NonEmpty(upper.tryDivide(other.lower, ROUND_DOWN), null)
+                                        } else if (nonnegative) {
+                                                new NonEmpty(null, lower.tryDivide(other.lower, ROUND_UP))
+                                        } else { // lower < 0 < upper
+                                                UNBOUNDED
+                                        }
+                                } else { // other.lower < 0 < other.upper
+                                        UNBOUNDED
+                                }
+                        }
+                }
+
+                private def isStrictlyNegative() {
+                        upper !== null && upper < BigDecimal.ZERO
+                }
+
+                private def isStrictlyPositive() {
+                        lower !== null && lower > BigDecimal.ZERO
+                }
+
+                private static def tryDivide(BigDecimal a, BigDecimal b, MathContext mc) {
+                        if (b === null) {
+                                BigDecimal.ZERO
+                        } else {
+                                a?.divide(b, mc)
+                        }
+                }
+
+                override **(Interval other) {
+                        switch (other) {
+                                case EMPTY: EMPTY
+                                NonEmpty: this ** other
+                                default: throw new IllegalArgumentException("Unknown interval: " + other)
+                        }
+                }
+
+                def **(NonEmpty other) {
+                        // XXX This should use proper rounding for log and exp instead of
+                        // converting to double.
+                        // XXX We should not ignore (integer) powers of negative numbers.
+                        val lowerLog = if (lower === null || lower <= BigDecimal.ZERO) {
+                                        null
+                                } else {
+                                        new BigDecimal(Math.log(lower.doubleValue), ROUND_DOWN)
+                                }
+                        val upperLog = if (upper === null) {
+                                        null
+                                } else if (upper == BigDecimal.ZERO) {
+                                        return ZERO
+                                } else if (upper < BigDecimal.ZERO) {
+                                        return EMPTY
+                                } else {
+                                        new BigDecimal(Math.log(upper.doubleValue), ROUND_UP)
+                                }
+                        val log = new NonEmpty(lowerLog, upperLog)
+                        val product = log * other
+                        if (product instanceof NonEmpty) {
+                                val lowerResult = if (product.lower === null) {
+                                                BigDecimal.ZERO
+                                        } else {
+                                                new BigDecimal(Math.exp(product.lower.doubleValue), ROUND_DOWN)
+                                        }
+                                val upperResult = if (product.upper === null) {
+                                                null
+                                        } else {
+                                                new BigDecimal(Math.exp(product.upper.doubleValue), ROUND_UP)
+                                        }
+                                new NonEmpty(lowerResult, upperResult)
+                        } else {
+                                throw new IllegalArgumentException("Unknown interval: " + product)
+                        }
+                }
+
+                override toString() {
+                        '''«IF lower === null»(-∞«ELSE»[«lower»«ENDIF», «IF upper === null»∞)«ELSE»«upper»]«ENDIF»'''
+                }
+
+                override compareTo(Interval o) {
+                        switch (o) {
+                                case EMPTY: 1
+                                NonEmpty: compareTo(o)
+                                default: throw new IllegalArgumentException("Unknown interval: " + o)
+                        }
+                }
+
+                def compareTo(NonEmpty o) {
+                        if (lower === null) {
+                                if (o.lower !== null) {
+                                        return -1
+                                }
+                        } else if (o.lower === null) { // lower !== null
+                                return 1
+                        } else { // both lower and o.lower are finite
+                                val lowerDifference = lower.compareTo(o.lower)
+                                if (lowerDifference != 0) {
+                                        return lowerDifference
+                                }
+                        }
+                        if (upper === null) {
+                                if (o.upper === null) {
+                                        return 0
+                                } else {
+                                        return 1
+                                }
+                        } else if (o.upper === null) { // upper !== null
+                                return -1
+                        }
+                        upper.compareTo(o.upper)
+                }
+        }
+}