add new API methods for FP_SQRT, FP_MAX and FP_MIN.

All FP-supporting solvers have this operation, thus we can provide it.
For users, it might be more convenient to use these methods
than to check for special values NaN, -Inf and Inf.

Author: kfriedberger

src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java

@@ -142,6 +142,14 @@ FloatingPointFormula castFrom(
 
   FloatingPointFormula abs(FloatingPointFormula number);
 
+  FloatingPointFormula max(FloatingPointFormula number1, FloatingPointFormula number2);
+
+  FloatingPointFormula min(FloatingPointFormula number1, FloatingPointFormula number2);
+
+  FloatingPointFormula sqrt(FloatingPointFormula number);
+
+  FloatingPointFormula sqrt(FloatingPointFormula number, FloatingPointRoundingMode roundingMode);
+
   FloatingPointFormula add(FloatingPointFormula number1, FloatingPointFormula number2);
 
   FloatingPointFormula add(

src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java

@@ -200,6 +200,15 @@ public enum FunctionDeclarationKind {
   /** Absolute value of a floating point. */
   FP_ABS,
 
+  /** Maximum of two floating points. */
+  FP_MAX,
+
+  /** Minimum of two floating points. */
+  FP_MIN,
+
+  /** Square root of a floating point. */
+  FP_SQRT,
+
   /** Subtraction over floating points. */
   FP_SUB,
 

src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java

@@ -258,6 +258,33 @@ public FloatingPointFormula abs(FloatingPointFormula pNumber) {
 
   protected abstract TFormulaInfo abs(TFormulaInfo pParam1);
 
+  @Override
+  public FloatingPointFormula max(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2) {
+    return wrap(max(extractInfo(pNumber1), extractInfo(pNumber2)));
+  }
+
+  protected abstract TFormulaInfo max(TFormulaInfo pParam1, TFormulaInfo pParam2);
+
+  @Override
+  public FloatingPointFormula min(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2) {
+    return wrap(min(extractInfo(pNumber1), extractInfo(pNumber2)));
+  }
+
+  protected abstract TFormulaInfo min(TFormulaInfo pParam1, TFormulaInfo pParam2);
+
+  @Override
+  public FloatingPointFormula sqrt(FloatingPointFormula pNumber) {
+    return wrap(sqrt(extractInfo(pNumber), getDefaultRoundingMode()));
+  }
+
+  @Override
+  public FloatingPointFormula sqrt(
+      FloatingPointFormula number, FloatingPointRoundingMode pFloatingPointRoundingMode) {
+    return wrap(sqrt(extractInfo(number), getRoundingMode(pFloatingPointRoundingMode)));
+  }
+
+  protected abstract TFormulaInfo sqrt(TFormulaInfo pNumber, TFormulaInfo pRoundingMode);
+
   @Override
   public FloatingPointFormula add(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2) {
     TFormulaInfo param1 = extractInfo(pNumber1);

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java

@@ -251,6 +251,21 @@ protected Expr abs(Expr pParam1) {
     return exprManager.mkExpr(Kind.FLOATINGPOINT_ABS, pParam1);
   }
 
+  @Override
+  protected Expr max(Expr pParam1, Expr pParam2) {
+    return exprManager.mkExpr(Kind.FLOATINGPOINT_MAX, pParam1, pParam2);
+  }
+
+  @Override
+  protected Expr min(Expr pParam1, Expr pParam2) {
+    return exprManager.mkExpr(Kind.FLOATINGPOINT_MIN, pParam1, pParam2);
+  }
+
+  @Override
+  protected Expr sqrt(Expr pParam1, Expr pRoundingMode) {
+    return exprManager.mkExpr(Kind.FLOATINGPOINT_SQRT, pRoundingMode, pParam1);
+  }
+
   @Override
   protected Expr add(Expr pParam1, Expr pParam2, Expr pRoundingMode) {
     return exprManager.mkExpr(Kind.FLOATINGPOINT_PLUS, pRoundingMode, pParam1, pParam2);

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java

@@ -371,6 +371,9 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Expr f) {
           .put(Kind.FLOATINGPOINT_ISZ, FunctionDeclarationKind.FP_IS_ZERO)
           .put(Kind.FLOATINGPOINT_EQ, FunctionDeclarationKind.FP_EQ)
           .put(Kind.FLOATINGPOINT_ABS, FunctionDeclarationKind.FP_ABS)
+          .put(Kind.FLOATINGPOINT_MAX, FunctionDeclarationKind.FP_MAX)
+          .put(Kind.FLOATINGPOINT_MIN, FunctionDeclarationKind.FP_MIN)
+          .put(Kind.FLOATINGPOINT_SQRT, FunctionDeclarationKind.FP_SQRT)
           .put(Kind.FLOATINGPOINT_PLUS, FunctionDeclarationKind.FP_ADD)
           .put(Kind.FLOATINGPOINT_SUB, FunctionDeclarationKind.FP_SUB)
           .put(Kind.FLOATINGPOINT_MULT, FunctionDeclarationKind.FP_MUL)

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java

@@ -34,6 +34,8 @@
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_iszero;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_leq;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_lt;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_max;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_min;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_minus;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_minus_inf;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_nan;
@@ -46,6 +48,7 @@
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_roundingmode_nearest_even;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_roundingmode_plus_inf;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_roundingmode_zero;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_sqrt;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_times;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_to_bv;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_uf;
@@ -220,6 +223,21 @@ protected Long abs(Long pNumber) {
     return msat_make_fp_abs(mathsatEnv, pNumber);
   }
 
+  @Override
+  protected Long max(Long pNumber1, Long pNumber2) {
+    return msat_make_fp_max(mathsatEnv, pNumber1, pNumber2);
+  }
+
+  @Override
+  protected Long min(Long pNumber1, Long pNumber2) {
+    return msat_make_fp_min(mathsatEnv, pNumber1, pNumber2);
+  }
+
+  @Override
+  protected Long sqrt(Long pNumber, Long pRoundingMode) {
+    return msat_make_fp_sqrt(mathsatEnv, pRoundingMode, pNumber);
+  }
+
   @Override
   protected Long add(Long pNumber1, Long pNumber2, Long pRoundingMode) {
     return msat_make_fp_plus(mathsatEnv, pRoundingMode, pNumber1, pNumber2);

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java

@@ -64,9 +64,12 @@
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_FP_ISZERO;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_FP_LE;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_FP_LT;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_FP_MAX;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_FP_MIN;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_FP_MUL;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_FP_NEG;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_FP_ROUND_TO_INT;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_FP_SQRT;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_FP_SUB;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_FP_TO_BV;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_IFF;
@@ -435,6 +438,12 @@ private FunctionDeclarationKind getDeclarationKind(long pF) {
         return FunctionDeclarationKind.FP_NEG;
       case MSAT_TAG_FP_ABS:
         return FunctionDeclarationKind.FP_ABS;
+      case MSAT_TAG_FP_MAX:
+        return FunctionDeclarationKind.FP_MAX;
+      case MSAT_TAG_FP_MIN:
+        return FunctionDeclarationKind.FP_MIN;
+      case MSAT_TAG_FP_SQRT:
+        return FunctionDeclarationKind.FP_SQRT;
       case MSAT_TAG_FP_ADD:
         return FunctionDeclarationKind.FP_ADD;
       case MSAT_TAG_FP_SUB:

src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java

@@ -191,6 +191,21 @@ protected Long abs(Long pNumber) {
     return Native.mkFpaAbs(z3context, pNumber);
   }
 
+  @Override
+  protected Long max(Long pNumber1, Long pNumber2) {
+    return Native.mkFpaMax(z3context, pNumber1, pNumber2);
+  }
+
+  @Override
+  protected Long min(Long pNumber1, Long pNumber2) {
+    return Native.mkFpaMin(z3context, pNumber1, pNumber2);
+  }
+
+  @Override
+  protected Long sqrt(Long pNumber, Long pRoundingMode) {
+    return Native.mkFpaSqrt(z3context, pRoundingMode, pNumber);
+  }
+
   @Override
   protected Long add(Long pNumber1, Long pNumber2, Long pRoundingMode) {
     return Native.mkFpaAdd(z3context, pRoundingMode, pNumber1, pNumber2);

src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java

@@ -565,6 +565,12 @@ private FunctionDeclarationKind getDeclarationKind(long f) {
         return FunctionDeclarationKind.FP_NEG;
       case Z3_OP_FPA_ABS:
         return FunctionDeclarationKind.FP_ABS;
+      case Z3_OP_FPA_MAX:
+        return FunctionDeclarationKind.FP_MAX;
+      case Z3_OP_FPA_MIN:
+        return FunctionDeclarationKind.FP_MIN;
+      case Z3_OP_FPA_SQRT:
+        return FunctionDeclarationKind.FP_SQRT;
       case Z3_OP_FPA_SUB:
         return FunctionDeclarationKind.FP_SUB;
       case Z3_OP_FPA_ADD:

src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java

@@ -185,6 +185,16 @@ public void infinityOrdering() throws SolverException, InterruptedException {
     BooleanFormula order3 = fpmgr.greaterThan(posInf, negInf);
 
     assertThatFormula(bmgr.and(order1, order2, order3)).isTautological();
+
+    assertThatFormula(fpmgr.equalWithFPSemantics(fpmgr.max(posInf, zero), posInf)).isTautological();
+    assertThatFormula(fpmgr.equalWithFPSemantics(fpmgr.max(posInf, negInf), posInf))
+        .isTautological();
+    assertThatFormula(fpmgr.equalWithFPSemantics(fpmgr.max(negInf, zero), zero)).isTautological();
+
+    assertThatFormula(fpmgr.equalWithFPSemantics(fpmgr.min(posInf, zero), zero)).isTautological();
+    assertThatFormula(fpmgr.equalWithFPSemantics(fpmgr.min(posInf, negInf), negInf))
+        .isTautological();
+    assertThatFormula(fpmgr.equalWithFPSemantics(fpmgr.min(negInf, zero), negInf)).isTautological();
   }
 
   @Test
@@ -198,6 +208,24 @@ public void infinityVariableOrdering() throws SolverException, InterruptedExcept
     assertThatFormula(bmgr.or(varIsNan, bmgr.and(order1, order2))).isTautological();
   }
 
+  @Test
+  public void sqrt() throws SolverException, InterruptedException {
+    for (double d : new double[] {0.25, 1, 2, 4, 9, 15, 1234, 1000000}) {
+      assertThatFormula(
+              fpmgr.equalWithFPSemantics(
+                  fpmgr.sqrt(fpmgr.makeNumber(d * d, doublePrecType)),
+                  fpmgr.makeNumber(d, doublePrecType)))
+          .isTautological();
+      assertThatFormula(
+              fpmgr.equalWithFPSemantics(
+                  fpmgr.sqrt(fpmgr.makeNumber(d, doublePrecType)),
+                  fpmgr.makeNumber(Math.sqrt(d), doublePrecType)))
+          .isTautological();
+      assertThatFormula(fpmgr.isNaN(fpmgr.sqrt(fpmgr.makeNumber(-d, doublePrecType))))
+          .isTautological();
+    }
+  }
+
   @Test
   public void specialValueFunctions() throws SolverException, InterruptedException {
     assertThatFormula(fpmgr.isInfinity(posInf)).isTautological();

src/org/sosy_lab/java_smt/test/SolverVisitorTest.java

@@ -191,6 +191,7 @@ public void floatMoreVisit() {
     requireBitvectors();
     FloatingPointType fp = FormulaType.getSinglePrecisionFloatingPointType();
     FloatingPointFormula x = fpmgr.makeVariable("x", fp);
+    FloatingPointFormula y = fpmgr.makeVariable("x", fp);
     BitvectorFormula z = bvmgr.makeVariable(32, "z");
 
     checkKind(
@@ -206,6 +207,9 @@ public void floatMoreVisit() {
     checkKind(fpmgr.isSubnormal(x), FunctionDeclarationKind.FP_IS_SUBNORMAL);
     checkKind(fpmgr.isZero(x), FunctionDeclarationKind.FP_IS_ZERO);
     checkKind(fpmgr.abs(x), FunctionDeclarationKind.FP_ABS);
+    checkKind(fpmgr.max(x, y), FunctionDeclarationKind.FP_MAX);
+    checkKind(fpmgr.min(x, y), FunctionDeclarationKind.FP_MIN);
+    checkKind(fpmgr.sqrt(x), FunctionDeclarationKind.FP_SQRT);
     if (Solvers.CVC4 != solverToUse()) { // CVC4 does not support this operation
       checkKind(fpmgr.toIeeeBitvector(x), FunctionDeclarationKind.FP_AS_IEEEBV);
     }