From 0faf329054fc64410f5d832ca4473678bf946604 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 3 Jan 2015 17:26:58 +0000 Subject: [PATCH] FPA API: bugfixes and examples for .NET and Java Signed-off-by: Christoph M. Wintersteiger --- examples/dotnet/Program.cs | 101 +++++++++++++++++++++------------ examples/java/JavaExample.java | 84 ++++++++++++++++++++++++++- src/api/api_fpa.cpp | 18 +++--- src/api/dotnet/Context.cs | 2 +- src/api/java/Expr.java | 8 +++ 5 files changed, 165 insertions(+), 48 deletions(-) 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: ; }