From 285b991abeb47609faec9b9578b5acdb4f9e4476 Mon Sep 17 00:00:00 2001
From: Balazs Robert Rippl <balrip.play@gmail.com>
Date: Fri, 5 Jul 2024 15:23:08 +0200
Subject: [PATCH] Fix simplifying of fp NaN literal (non)equalities

NaN floating point values should not be equal to any other value. This
behavior is correctly implemented in the FpLitExpr #eq and #neq methods.
To utilize that, manual comparison in simplification is now swapped to
call these methods, resulting in correct behaviour: (= (NaN) (NaN)) for
example now simplifies to false.
---
 .../hu/bme/mit/theta/core/utils/ExprSimplifier.java  | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

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 <T extends Type> Expr<T> simplify(final Expr<T> expr, final Valuation valuation) {
         return (Expr<T>) TABLE.dispatch(expr, valuation);
-    }    private final DispatchTable2<Valuation, Expr<?>> TABLE = DispatchTable2.<Valuation, Expr<?>>builder()
+    }
+
+    private final DispatchTable2<Valuation, Expr<?>> TABLE = DispatchTable2.<Valuation, Expr<?>>builder()
 
             // Boolean
 
@@ -1958,8 +1960,8 @@ private Expr<BoolType> simplifyFpEq(final FpEqExpr expr, final Valuation val) {
         final Expr<FpType> leftOp = simplify(expr.getLeftOp(), val);
         final Expr<FpType> 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<BoolType> simplifyFpNeq(final FpNeqExpr expr, final Valuation val)
         final Expr<FpType> leftOp = simplify(expr.getLeftOp(), val);
         final Expr<FpType> 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();