diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs
index 3d2910c8f..b03cfd28c 100644
--- a/examples/dotnet/Program.cs
+++ b/examples/dotnet/Program.cs
@@ -2028,53 +2028,81 @@ namespace test_mapi
// Console.WriteLine("{0}", ctx.MkEq(s1, t1));
}
- public static void FloatingPointExample(Context ctx)
+ public static void FloatingPointExample1(Context ctx)
{
- Console.WriteLine("FloatingPointExample");
+ Console.WriteLine("FloatingPointExample1");
FPSort s = ctx.MkFPSort(11, 53);
Console.WriteLine("Sort: {0}", s);
- FPNum x = (FPNum)ctx.MkNumeral("-1e1", s);
- Console.WriteLine("Numeral: {0}", x.ToString());
-
- FPNum y = (FPNum)ctx.MkNumeral("-10", s);
- Console.WriteLine("Numeral: {0}", y.ToString());
-
- FPNum z = (FPNum)ctx.MkNumeral("-1.25p3", s);
- Console.WriteLine("Numeral: {0}", z.ToString());
+ FPNum x = (FPNum)ctx.MkNumeral("-1e1", s); /* -1 * 10^1 = -10 */
+ FPNum y = (FPNum)ctx.MkNumeral("-10", s); /* -10 */
+ FPNum z = (FPNum)ctx.MkNumeral("-1.25p3", s); /* -1.25 * 2^3 = -1.25 * 8 = -10 */
+ Console.WriteLine("x={0}; y={1}; z={2}", x.ToString(), y.ToString(), z.ToString());
BoolExpr a = ctx.MkAnd(ctx.MkFPEq(x, y), ctx.MkFPEq(y, z));
-
Check(ctx, ctx.MkNot(a), Status.UNSATISFIABLE);
- x = ctx.MkFPNaN(s);
- FPExpr c = (FPExpr)ctx.MkConst("y", s);
+ /* nothing is equal to NaN according to floating-point
+ * equality, so NaN == k should be unsatisfiable. */
+ FPExpr k = (FPExpr)ctx.MkConst("x", s);
+ FPExpr nan = ctx.MkFPNaN(s);
- // Note: We need to use a special solver for QF_FPA here; the
- // general solver does not support FPA yet.
-
- Solver slvr = ctx.MkSolver("QF_FPA");
- slvr.Add(ctx.MkFPEq(x, c));
- if (slvr.Check() != Status.UNSATISFIABLE) // nothing is equal to NaN according to floating-point equality.
- throw new TestFailedException();
-
- slvr = ctx.MkSolver("QF_FPA");
- slvr.Add(ctx.MkEq(x, c)); // NaN is equal to NaN according to normal equality.
- if (slvr.Check() != Status.SATISFIABLE)
- throw new TestFailedException();
-
-
- x = (FPNum)ctx.MkNumeral("-1e1", s);
- y = (FPNum)ctx.MkNumeral("-10", s);
- FPExpr q = (FPExpr)ctx.MkConst("q", s);
- FPNum mh = (FPNum)ctx.MkNumeral("100", s);
- slvr = ctx.MkSolver("QF_FPA");
- // Let's prove -1e1 * -10 == +100
- slvr.Add(ctx.MkEq(ctx.MkFPMul(ctx.MkFPRMNearestTiesToAway(), x, y), q));
- slvr.Add(ctx.MkNot(ctx.MkFPEq(q, mh)));
+ /* solver that runs the default tactic for QF_FP. */
+ Solver slvr = ctx.MkSolver("QF_FP");
+ slvr.Add(ctx.MkFPEq(nan, k));
if (slvr.Check() != Status.UNSATISFIABLE)
throw new TestFailedException();
+ Console.WriteLine("OK, unsat:" + Environment.NewLine + slvr);
+
+ /* NaN is equal to NaN according to normal equality. */
+ slvr = ctx.MkSolver("QF_FP");
+ slvr.Add(ctx.MkEq(nan, nan));
+ if (slvr.Check() != Status.SATISFIABLE)
+ throw new TestFailedException();
+ Console.WriteLine("OK, sat:" + Environment.NewLine + slvr);
+
+ /* Let's prove -1e1 * -1.25e3 == +100 */
+ x = (FPNum)ctx.MkNumeral("-1e1", s);
+ y = (FPNum)ctx.MkNumeral("-1.25p3", s);
+ FPExpr x_plus_y = (FPExpr)ctx.MkConst("x_plus_y", s);
+ FPNum r = (FPNum)ctx.MkNumeral("100", s);
+ slvr = ctx.MkSolver("QF_FP");
+
+ slvr.Add(ctx.MkEq(x_plus_y, ctx.MkFPMul(ctx.MkFPRoundNearestTiesToAway(), x, y)));
+ slvr.Add(ctx.MkNot(ctx.MkFPEq(x_plus_y, r)));
+ if (slvr.Check() != Status.UNSATISFIABLE)
+ throw new TestFailedException();
+ Console.WriteLine("OK, unsat:" + Environment.NewLine + slvr);
+ }
+
+ public static void FloatingPointExample2(Context ctx)
+ {
+ Console.WriteLine("FloatingPointExample2");
+ FPSort double_sort = ctx.MkFPSort(11, 53);
+ FPRMSort rm_sort = ctx.MkFPRoundingModeSort();
+
+ FPRMExpr rm = (FPRMExpr)ctx.MkConst(ctx.MkSymbol("rm"), rm_sort);
+ BitVecExpr x = (BitVecExpr)ctx.MkConst(ctx.MkSymbol("x"), ctx.MkBitVecSort(64));
+ FPExpr y = (FPExpr)ctx.MkConst(ctx.MkSymbol("y"), double_sort);
+ RealExpr real_val = ctx.MkReal(42);
+ BitVecExpr bv_val = ctx.MkBV(42, 64);
+ FPExpr fp_val = ctx.MkFP(42, double_sort);
+
+ BoolExpr c1 = ctx.MkEq(x, ctx.MkFPToIEEEBV(fp_val));
+ BoolExpr c2 = ctx.MkEq(x, ctx.MkBV(42, 64));
+ BoolExpr c3 = ctx.MkEq(fp_val, ctx.MkFPToFP(rm, real_val, double_sort));
+ BoolExpr c4 = ctx.MkAnd(c1, c2);
+ Console.WriteLine("c3 = " + c3);
+
+ /* Generic solver */
+ Solver s = ctx.MkSolver();
+ s.Assert(c3);
+
+ if (s.Check() != Status.SATISFIABLE)
+ throw new TestFailedException();
+
+ Console.WriteLine("OK, model: ", s.Model.ToString());
}
static void Main(string[] args)
@@ -2118,7 +2146,8 @@ namespace test_mapi
FindSmallModelExample(ctx);
SimplifierExample(ctx);
FiniteDomainExample(ctx);
- FloatingPointExample(ctx);
+ FloatingPointExample1(ctx);
+ FloatingPointExample2(ctx);
}
// These examples need proof generation turned on.
diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java
index 48395d8c2..878ec4693 100644
--- a/examples/java/JavaExample.java
+++ b/examples/java/JavaExample.java
@@ -1095,7 +1095,7 @@ class JavaExample
// / Shows how to use Solver(logic)
- // /
+ // / @param ctx
void logicExample(Context ctx) throws Z3Exception, TestFailedException
{
System.out.println("LogicTest");
@@ -2157,6 +2157,86 @@ class JavaExample
// System.out.println(ctx.mkEq(s1, t1));
}
+ public void floatingPointExample1(Context ctx) throws Z3Exception, TestFailedException
+ {
+ System.out.println("FloatingPointExample1");
+ Log.append("FloatingPointExample1");
+
+ FPSort s = ctx.mkFPSort(11, 53);
+ System.out.println("Sort: " + s);
+
+ FPNum x = (FPNum)ctx.mkNumeral("-1e1", s); /* -1 * 10^1 = -10 */
+ FPNum y = (FPNum)ctx.mkNumeral("-10", s); /* -10 */
+ FPNum z = (FPNum)ctx.mkNumeral("-1.25p3", s); /* -1.25 * 2^3 = -1.25 * 8 = -10 */
+ System.out.println("x=" + x.toString() +
+ "; y=" + y.toString() +
+ "; z=" + z.toString());
+
+ BoolExpr a = ctx.mkAnd(ctx.mkFPEq(x, y), ctx.mkFPEq(y, z));
+ check(ctx, ctx.mkNot(a), Status.UNSATISFIABLE);
+
+ /* nothing is equal to NaN according to floating-point
+ * equality, so NaN == k should be unsatisfiable. */
+ FPExpr k = (FPExpr)ctx.mkConst("x", s);
+ FPExpr nan = ctx.mkFPNaN(s);
+
+ /* solver that runs the default tactic for QF_FP. */
+ Solver slvr = ctx.mkSolver("QF_FP");
+ slvr.add(ctx.mkFPEq(nan, k));
+ if (slvr.check() != Status.UNSATISFIABLE)
+ throw new TestFailedException();
+ System.out.println("OK, unsat:" + System.getProperty("line.separator") + slvr);
+
+ /* NaN is equal to NaN according to normal equality. */
+ slvr = ctx.mkSolver("QF_FP");
+ slvr.add(ctx.mkEq(nan, nan));
+ if (slvr.check() != Status.SATISFIABLE)
+ throw new TestFailedException();
+ System.out.println("OK, sat:" + System.getProperty("line.separator") + slvr);
+
+ /* Let's prove -1e1 * -1.25e3 == +100 */
+ x = (FPNum)ctx.mkNumeral("-1e1", s);
+ y = (FPNum)ctx.mkNumeral("-1.25p3", s);
+ FPExpr x_plus_y = (FPExpr)ctx.mkConst("x_plus_y", s);
+ FPNum r = (FPNum)ctx.mkNumeral("100", s);
+ slvr = ctx.mkSolver("QF_FP");
+
+ slvr.add(ctx.mkEq(x_plus_y, ctx.mkFPMul(ctx.mkFPRoundNearestTiesToAway(), x, y)));
+ slvr.add(ctx.mkNot(ctx.mkFPEq(x_plus_y, r)));
+ if (slvr.check() != Status.UNSATISFIABLE)
+ throw new TestFailedException();
+ System.out.println("OK, unsat:" + System.getProperty("line.separator") + slvr);
+ }
+
+ public void floatingPointExample2(Context ctx) throws Z3Exception, TestFailedException
+ {
+ System.out.println("FloatingPointExample2");
+ Log.append("FloatingPointExample2");
+
+ FPSort double_sort = ctx.mkFPSort(11, 53);
+ FPRMSort rm_sort = ctx.mkFPRoundingModeSort();
+
+ FPRMExpr rm = (FPRMExpr)ctx.mkConst(ctx.mkSymbol("rm"), rm_sort);
+ BitVecExpr x = (BitVecExpr)ctx.mkConst(ctx.mkSymbol("x"), ctx.mkBitVecSort(64));
+ RealExpr real_val = ctx.mkReal(42);
+ FPExpr fp_val = ctx.mkFP(42, double_sort);
+
+ BoolExpr c1 = ctx.mkEq(x, ctx.mkFPToIEEEBV(fp_val));
+ BoolExpr c2 = ctx.mkEq(x, ctx.mkBV(42, 64));
+ BoolExpr c3 = ctx.mkEq(fp_val, ctx.mkFPToFP(rm, real_val, double_sort));
+ BoolExpr c4 = ctx.mkAnd(c1, c2);
+ System.out.println("c3 = " + c3);
+
+ /* Generic solver */
+ Solver s = ctx.mkSolver();
+ s.add(c3);
+
+ if (s.check() != Status.SATISFIABLE)
+ throw new TestFailedException();
+
+ System.out.println("OK, model: " + s.getModel().toString());
+ }
+
public static void main(String[] args)
{
JavaExample p = new JavaExample();
@@ -2200,6 +2280,8 @@ class JavaExample
p.findSmallModelExample(ctx);
p.simplifierExample(ctx);
p.finiteDomainExample(ctx);
+ p.floatingPointExample1(ctx);
+ p.floatingPointExample2(ctx);
}
{ // These examples need proof generation turned on.
diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp
index d2d4e7155..87568af09 100644
--- a/src/api/api_fpa.cpp
+++ b/src/api/api_fpa.cpp
@@ -649,23 +649,21 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
- unsigned int Z3_API Z3_mk_fpa_get_ebits(Z3_context c, Z3_sort s) {
+ unsigned Z3_API Z3_fpa_get_ebits(Z3_context c, Z3_sort s) {
Z3_TRY;
- LOG_Z3_mk_fpa_get_ebits(c, s);
+ LOG_Z3_fpa_get_ebits(c, s);
RESET_ERROR_CODE();
- api::context * ctx = mk_c(c);
- unsigned r = ctx->float_util().get_ebits(to_sort(s));
- RETURN_Z3(r);
+ CHECK_NON_NULL(s, 0);
+ return mk_c(c)->float_util().get_ebits(to_sort(s));
Z3_CATCH_RETURN(0);
}
- unsigned Z3_API Z3_mk_fpa_get_sbits(Z3_context c, Z3_sort s) {
+ unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s) {
Z3_TRY;
- LOG_Z3_mk_fpa_get_sbits(c, s);
+ LOG_Z3_fpa_get_ebits(c, s);
RESET_ERROR_CODE();
- api::context * ctx = mk_c(c);
- unsigned r = ctx->float_util().get_sbits(to_sort(s));
- RETURN_Z3(r);
+ CHECK_NON_NULL(s, 0);
+ return mk_c(c)->float_util().get_sbits(to_sort(s));
Z3_CATCH_RETURN(0);
}
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index f3e6220cf..609db802d 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -3895,7 +3895,7 @@ namespace Microsoft.Z3
/// the closest integer, again represented as a floating-point number.
///
/// term of RoundingMode sort
- /// floating-point term
+ /// floating-point term
public FPExpr MkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
{
Contract.Ensures(Contract.Result() != null);
diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java
index 6a7241e98..233076516 100644
--- a/src/api/java/Expr.java
+++ b/src/api/java/Expr.java
@@ -1791,6 +1791,10 @@ public class Expr extends AST
return new RatNum(ctx, obj);
case Z3_BV_SORT:
return new BitVecNum(ctx, obj);
+ case Z3_FLOATING_POINT_SORT:
+ return new FPNum(ctx, obj);
+ case Z3_FLOATING_POINT_ROUNDING_MODE_SORT:
+ return new FPRMNum(ctx, obj);
default: ;
}
}
@@ -1809,6 +1813,10 @@ public class Expr extends AST
return new ArrayExpr(ctx, obj);
case Z3_DATATYPE_SORT:
return new DatatypeExpr(ctx, obj);
+ case Z3_FLOATING_POINT_SORT:
+ return new FPExpr(ctx, obj);
+ case Z3_FLOATING_POINT_ROUNDING_MODE_SORT:
+ return new FPRMExpr(ctx, obj);
default: ;
}