mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 10:19:23 +00:00
Code Activity

FPA API: bugfixes and examples for .NET and Java

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-01-03 17:26:58 +00:00
parent fa26e2423e
commit 0faf329054
5 changed files with 165 additions and 48 deletions
Download patch file Download diff file Expand all files Collapse all files

101
examples/dotnet/Program.cs
View file

@ -2028,53 +2028,81 @@ namespace test_mapi
// Console.WriteLine("{0}", ctx.MkEq(s1, t1)); // 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); FPSort s = ctx.MkFPSort(11, 53);
Console.WriteLine("Sort: {0}", s); Console.WriteLine("Sort: {0}", s);
FPNum x = (FPNum)ctx.MkNumeral("-1e1", s); FPNum x = (FPNum)ctx.MkNumeral("-1e1", s); /* -1 * 10^1 = -10 */
Console.WriteLine("Numeral: {0}", x.ToString()); FPNum y = (FPNum)ctx.MkNumeral("-10", s); /* -10 */
FPNum z = (FPNum)ctx.MkNumeral("-1.25p3", s); /* -1.25 * 2^3 = -1.25 * 8 = -10 */
FPNum y = (FPNum)ctx.MkNumeral("-10", s); Console.WriteLine("x={0}; y={1}; z={2}", x.ToString(), y.ToString(), z.ToString());
Console.WriteLine("Numeral: {0}", y.ToString());
FPNum z = (FPNum)ctx.MkNumeral("-1.25p3", s);
Console.WriteLine("Numeral: {0}", z.ToString());
BoolExpr a = ctx.MkAnd(ctx.MkFPEq(x, y), ctx.MkFPEq(y, z)); BoolExpr a = ctx.MkAnd(ctx.MkFPEq(x, y), ctx.MkFPEq(y, z));
Check(ctx, ctx.MkNot(a), Status.UNSATISFIABLE); Check(ctx, ctx.MkNot(a), Status.UNSATISFIABLE);
x = ctx.MkFPNaN(s); /* nothing is equal to NaN according to floating-point
FPExpr c = (FPExpr)ctx.MkConst("y", s); * 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 /* solver that runs the default tactic for QF_FP. */
// general solver does not support FPA yet. Solver slvr = ctx.MkSolver("QF_FP");
slvr.Add(ctx.MkFPEq(nan, k));
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)));
if (slvr.Check() != Status.UNSATISFIABLE) if (slvr.Check() != Status.UNSATISFIABLE)
throw new TestFailedException(); 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) static void Main(string[] args)
@ -2118,7 +2146,8 @@ namespace test_mapi
FindSmallModelExample(ctx); FindSmallModelExample(ctx);
SimplifierExample(ctx); SimplifierExample(ctx);
FiniteDomainExample(ctx); FiniteDomainExample(ctx);
FloatingPointExample(ctx); FloatingPointExample1(ctx);
FloatingPointExample2(ctx);
} }
// These examples need proof generation turned on. // These examples need proof generation turned on.

84
examples/java/JavaExample.java
View file

@ -1095,7 +1095,7 @@ class JavaExample
// / Shows how to use Solver(logic) // / Shows how to use Solver(logic)
// / <param name="ctx"></param> // / @param ctx
void logicExample(Context ctx) throws Z3Exception, TestFailedException void logicExample(Context ctx) throws Z3Exception, TestFailedException
{ {
System.out.println("LogicTest"); System.out.println("LogicTest");
@ -2157,6 +2157,86 @@ class JavaExample
// System.out.println(ctx.mkEq(s1, t1)); // 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) public static void main(String[] args)
{ {
JavaExample p = new JavaExample(); JavaExample p = new JavaExample();
@ -2200,6 +2280,8 @@ class JavaExample
p.findSmallModelExample(ctx); p.findSmallModelExample(ctx);
p.simplifierExample(ctx); p.simplifierExample(ctx);
p.finiteDomainExample(ctx); p.finiteDomainExample(ctx);
p.floatingPointExample1(ctx);
p.floatingPointExample2(ctx);
} }
{ // These examples need proof generation turned on. { // These examples need proof generation turned on.

18
src/api/api_fpa.cpp
View file

@ -649,23 +649,21 @@ extern "C" {
Z3_CATCH_RETURN(0); 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; Z3_TRY;
LOG_Z3_mk_fpa_get_ebits(c, s); LOG_Z3_fpa_get_ebits(c, s);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); CHECK_NON_NULL(s, 0);
unsigned r = ctx->float_util().get_ebits(to_sort(s)); return mk_c(c)->float_util().get_ebits(to_sort(s));
RETURN_Z3(r);
Z3_CATCH_RETURN(0); 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; Z3_TRY;
LOG_Z3_mk_fpa_get_sbits(c, s); LOG_Z3_fpa_get_ebits(c, s);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); CHECK_NON_NULL(s, 0);
unsigned r = ctx->float_util().get_sbits(to_sort(s)); return mk_c(c)->float_util().get_sbits(to_sort(s));
RETURN_Z3(r);
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }

2
src/api/dotnet/Context.cs
View file

@ -3895,7 +3895,7 @@ namespace Microsoft.Z3
/// the closest integer, again represented as a floating-point number. /// the closest integer, again represented as a floating-point number.
/// </summary> /// </summary>
/// <param name="rm">term of RoundingMode sort</param> /// <param name="rm">term of RoundingMode sort</param>
/// <param name="t2">floating-point term</param> /// <param name="t">floating-point term</param>
public FPExpr MkFPRoundToIntegral(FPRMExpr rm, FPExpr t) public FPExpr MkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
{ {
Contract.Ensures(Contract.Result<FPNum>() != null); Contract.Ensures(Contract.Result<FPNum>() != null);

8
src/api/java/Expr.java
View file

@ -1791,6 +1791,10 @@ public class Expr extends AST
return new RatNum(ctx, obj); return new RatNum(ctx, obj);
case Z3_BV_SORT: case Z3_BV_SORT:
return new BitVecNum(ctx, obj); 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: ; default: ;
} }
} }
@ -1809,6 +1813,10 @@ public class Expr extends AST
return new ArrayExpr(ctx, obj); return new ArrayExpr(ctx, obj);
case Z3_DATATYPE_SORT: case Z3_DATATYPE_SORT:
return new DatatypeExpr(ctx, obj); 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: ; default: ;
} }