diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java index a79d7b109f..cbdee2d98b 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java @@ -71,7 +71,9 @@ public static ExprSimplifier create(final SimplifierLevel level) { @SuppressWarnings("unchecked") public Expr simplify(final Expr expr, final Valuation valuation) { return (Expr) TABLE.dispatch(expr, valuation); - } private final DispatchTable2> TABLE = DispatchTable2.>builder() + } + + private final DispatchTable2> TABLE = DispatchTable2.>builder() // Boolean @@ -1958,8 +1960,8 @@ private Expr simplifyFpEq(final FpEqExpr expr, final Valuation val) { final Expr leftOp = simplify(expr.getLeftOp(), val); final Expr rightOp = simplify(expr.getRightOp(), val); - if (leftOp instanceof FpLitExpr && rightOp instanceof FpLitExpr) { - return Bool(leftOp.equals(rightOp)); + if (leftOp instanceof FpLitExpr lLit && rightOp instanceof FpLitExpr rLit) { + return lLit.eq(rLit); } return expr.with(leftOp, rightOp); @@ -2024,8 +2026,8 @@ private Expr simplifyFpNeq(final FpNeqExpr expr, final Valuation val) final Expr leftOp = simplify(expr.getLeftOp(), val); final Expr rightOp = simplify(expr.getRightOp(), val); - if (leftOp instanceof FpLitExpr && rightOp instanceof FpLitExpr) { - return Bool(!leftOp.equals(rightOp)); + if (leftOp instanceof FpLitExpr lLit && rightOp instanceof FpLitExpr rLit) { + return lLit.neq(rLit); } else if (leftOp instanceof RefExpr && rightOp instanceof RefExpr) { if (level != LITERAL_ONLY && leftOp.equals(rightOp)) { return False();