diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java index df5afada31..00998e25b2 100644 --- a/src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java +++ b/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( diff --git a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java index ddcaebd0b4..be4ff3c8a0 100644 --- a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java +++ b/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, diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index 7194c12018..6b334916d6 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/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); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java index d4d805f06f..a7472d6bca 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/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); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java index 465149041e..f0c176a759 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java @@ -371,6 +371,9 @@ public R visit(FormulaVisitor 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) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java index 019be35d32..3323e0d547 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java +++ b/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); diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java index 3ddaabd7cc..b5feb37bd1 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java +++ b/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: diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java index 1b20b71084..e95154fa3f 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java +++ b/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); diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java index 3fb894cb60..d024c6d790 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/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: diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index e74a2d7ce5..962d56620c 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/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(); diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index ee813e07dc..efab95aeb0 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/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); }