Add sqrt and abs tokens for floating points

Author: agilot

src/main/scala/inox/ast/Deconstructors.scala

@@ -327,6 +327,16 @@ trait TreeDeconstructor {
       (NoIdentifiers, NoVariables, Seq(rm, t1, t2), NoTypes, NoFlags,
         (_, _, es, _, _) => t.FPDiv(es(0), es(1), es(2)))
     },
+    classOf[s.FPAbs] -> { expr =>
+      val s.FPAbs(e) = expr: @unchecked
+      (NoIdentifiers, NoVariables, Seq(e), NoTypes, NoFlags,
+        (_, _, es, _, _) => t.FPAbs(es(0)))
+    },
+    classOf[s.Sqrt] -> { expr =>
+      val s.Sqrt(rm, e) = expr: @unchecked
+      (NoIdentifiers, NoVariables, Seq(rm, e), NoTypes, NoFlags,
+        (_, _, es, _, _) => t.Sqrt(es(0), es(1)))
+    },
     classOf[s.FPCast] -> { expr =>
       val s.FPCast(eb, sb, rm, e) = expr: @unchecked
       (NoIdentifiers, NoVariables, Seq(rm, e), NoTypes, NoFlags,

src/main/scala/inox/ast/Expressions.scala

@@ -668,6 +668,15 @@ trait Expressions { self: Trees =>
       if getRoundingMode(rm).isTyped then getFPType(lhs, rhs) else Untyped
   }
 
+  sealed case class FPAbs(e: Expr) extends Expr with CachingTyped {
+    override protected def computeType(using Symbols): Type = getFPType(e)
+  }
+
+  sealed case class Sqrt(rm: Expr, e: Expr) extends Expr with CachingTyped {
+    override protected def computeType(using Symbols): Type =
+      if getRoundingMode(rm).isTyped then getFPType(e) else Untyped
+  }
+
   sealed case class FPCast(newExponent: Int, newSignificand: Int, rm: Expr, expr: Expr) extends Expr with CachingTyped {
     override protected def computeType(using Symbols): Type =
       if getRoundingMode(rm).isTyped &&

src/main/scala/inox/ast/Printers.scala

@@ -287,6 +287,8 @@ trait Printer {
     case FPSub(_, e1, e2) => p"$e1 - $e2"
     case FPMul(_, e1, e2) => p"$e1 * $e2"
     case FPDiv(_, e1, e2) => p"$e1 / $e2"
+    case FPAbs(e)         => p"abs($e)"
+    case Sqrt(_, e)       => p"sqrt($e)"
     case FPIsZero(e)      => p"$e == 0"
     case FPIsNaN(e)       => p"$e.isNaN"
     case FPIsInfinite(e)  => p"$e.isInfinite"

src/main/scala/inox/solvers/smtlib/SMTLIBParser.scala

@@ -218,10 +218,12 @@ trait SMTLIBParser {
     case FloatingPoint.Mul(rm, t1, t2) => fromSMTUnifyType(t1, t2, otpe)((e1, e2) => FPMul(fromSMT(rm, RoundingMode), e1, e2))
     case FloatingPoint.Div(rm, t1, t2) => fromSMTUnifyType(t1, t2, otpe)((e1, e2) => FPDiv(fromSMT(rm, RoundingMode), e1, e2))
     case FloatingPoint.Neg(t) => UMinus(fromSMT(t, otpe))
-    case FloatingPoint.GreaterThan(t1, t2) => fromSMTUnifyType(t1, t2, Some(BooleanType()))(GreaterThan.apply)
-    case FloatingPoint.LessThan(t1, t2) => fromSMTUnifyType(t1, t2, Some(BooleanType()))(LessThan.apply)
-    case FloatingPoint.GreaterEquals(t1, t2) => fromSMTUnifyType(t1, t2, Some(BooleanType()))(GreaterEquals.apply)
-    case FloatingPoint.LessEquals(t1, t2) => fromSMTUnifyType(t1, t2, Some(BooleanType()))(LessEquals.apply)
+    case FloatingPoint.Abs(t) => FPAbs(fromSMT(t, otpe))
+    case FloatingPoint.Sqrt(rm, t)               => Sqrt(fromSMT(rm, RoundingMode), fromSMT(t, otpe))
+    case FloatingPoint.GreaterThan(t1, t2)       => fromSMTUnifyType(t1, t2, Some(BooleanType()))(GreaterThan.apply)
+    case FloatingPoint.LessThan(t1, t2)          => fromSMTUnifyType(t1, t2, Some(BooleanType()))(LessThan.apply)
+    case FloatingPoint.GreaterEquals(t1, t2)     => fromSMTUnifyType(t1, t2, Some(BooleanType()))(GreaterEquals.apply)
+    case FloatingPoint.LessEquals(t1, t2)        => fromSMTUnifyType(t1, t2, Some(BooleanType()))(LessEquals.apply)
     case FloatingPoint.ToFP(newExp, newSig, seq) =>
       val (rm, arg) = seq match {
         case Seq(t1, t2) => (fromSMT(t1, Some(RoundingMode)), fromSMT(t2, None))

src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala

@@ -512,6 +512,8 @@ trait SMTLIBTarget extends SMTLIBParser with Interruptible with ADTManagers {
       case FPSub(rm, a, b) => FloatingPoint.Sub(toSMT(rm), toSMT(a), toSMT(b))
       case FPMul(rm, a, b) => FloatingPoint.Mul(toSMT(rm), toSMT(a), toSMT(b))
       case FPDiv(rm, a, b) => FloatingPoint.Div(toSMT(rm), toSMT(a), toSMT(b))
+      case FPAbs(e)        => FloatingPoint.Abs(toSMT(e))
+      case Sqrt(rm, e)     => FloatingPoint.Sqrt(toSMT(rm), toSMT(e))
       case FPCast(ne, ns, rm, e) => FloatingPoint.ToFP(ne, ns, toSMT(rm), toSMT(e))
       case FPIsInfinite(e) => FloatingPoint.IsInfinite(toSMT(e))
       case FPIsZero(e)     => FloatingPoint.IsZero(toSMT(e))

src/main/scala/inox/utils/Serialization.scala

@@ -476,7 +476,7 @@ class InoxSerializer(val trees: ast.Trees, serializeProducts: Boolean = false) e
     * The `Serializer[_]` identifiers in this mapping range from 10 to 105
     * (ignoring special identifiers that are smaller than 10).
     *
-    * NEXT ID: 109
+    * NEXT ID: 127
     */
   protected def classSerializers: Map[Class[?], Serializer[?]] = Map(
     // Inox Expressions
@@ -559,6 +559,8 @@ class InoxSerializer(val trees: ast.Trees, serializeProducts: Boolean = false) e
     classSerializer[FPMul]             (112),
     classSerializer[FPDiv]             (113),
     classSerializer[FPCast]            (114),
+    classSerializer[FPAbs]             (125),
+    classSerializer[Sqrt]              (126),
 
     classSerializer[RoundTowardZero.type]        (115),
     classSerializer[RoundTowardPositive.type]    (116),

src/test/scala/inox/solvers/SemanticsSuite.scala

@@ -426,6 +426,7 @@ class SemanticsSuite extends AnyFunSuite {
 
     for (i <- floatValues) {
       check(s, UMinus(Float32Literal(i)), Float32Literal(-i))
+      check(s, FPAbs(Float32Literal(i)), Float32Literal(Math.abs(i)))
     }
 
     for (i <- doubleValues; j <- doubleValues) {
@@ -437,6 +438,8 @@ class SemanticsSuite extends AnyFunSuite {
 
     for (i <- doubleValues) {
       check(s, UMinus(Float64Literal(i)), Float64Literal(-i))
+      check(s, Sqrt(RoundNearestTiesToEven, Float64Literal(i)), Float64Literal(Math.sqrt(i)))
+      check(s, FPAbs(Float64Literal(i)), Float64Literal(Math.abs(i)))
     }
 
   }