From 0bd06930aef34b2bd0bbdf01331d51bef4a8de01 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 4 Oct 2016 18:04:00 +0100 Subject: [PATCH 1/7] whitespace --- src/ast/fpa/fpa2bv_converter.cpp | 24 ++++++++++++------------ src/ast/fpa/fpa2bv_rewriter.cpp | 6 +++--- 2 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index d3257ac55..90007b330 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -264,7 +264,7 @@ void fpa2bv_converter::mk_function(func_decl * f, unsigned num, expr * const * a rng = f->get_range(); fapp = m.mk_app(f, num, args); if (m_util.is_float(rng)) { - sort_ref bv_rng(m); + sort_ref bv_rng(m); expr_ref new_eq(m); unsigned ebits = m_util.get_ebits(rng); unsigned sbits = m_util.get_sbits(rng); @@ -290,7 +290,7 @@ void fpa2bv_converter::mk_function(func_decl * f, unsigned num, expr * const * a m_extra_assertions.push_back(new_eq); result = flt_app; } - else + else result = fapp; TRACE("fpa2bv", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl; ); @@ -1057,7 +1057,7 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r // (x is 0) -> x c5 = x_is_zero; v5 = pzero; - + // exp(x) < exp(y) -> x unsigned ebits = m_util.get_ebits(s); unsigned sbits = m_util.get_sbits(s); @@ -1117,15 +1117,15 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r dbg_decouple("fpa2bv_rem_exp_diff", exp_diff); // CMW: This creates _huge_ bit-vectors, which is potentially sub-optimal, - // but calculating this via rem = x - y * nearest(x/y) creates huge + // but calculating this via rem = x - y * nearest(x/y) creates huge // circuits, too. Lazy instantiation seems the way to go in the long run - // (using the lazy bit-blaster helps on simple instances). + // (using the lazy bit-blaster helps on simple instances). expr_ref a_sig_ext(m), b_sig_ext(m), lshift(m), rshift(m), shifted(m), huge_rem(m); a_sig_ext = m_bv_util.mk_concat(m_bv_util.mk_zero_extend(max_exp_diff_ui, a_sig), m_bv_util.mk_numeral(0, 3)); b_sig_ext = m_bv_util.mk_concat(m_bv_util.mk_zero_extend(max_exp_diff_ui, b_sig), m_bv_util.mk_numeral(0, 3)); lshift = m_bv_util.mk_zero_extend(max_exp_diff_ui + sbits - (ebits+2) + 3, exp_diff); rshift = m_bv_util.mk_zero_extend(max_exp_diff_ui + sbits - (ebits+2) + 3, neg_exp_diff); - shifted = m.mk_ite(exp_diff_is_neg, m_bv_util.mk_bv_ashr(a_sig_ext, rshift), + shifted = m.mk_ite(exp_diff_is_neg, m_bv_util.mk_bv_ashr(a_sig_ext, rshift), m_bv_util.mk_bv_shl(a_sig_ext, lshift)); huge_rem = m_bv_util.mk_bv_urem(shifted, b_sig_ext); dbg_decouple("fpa2bv_rem_huge_rem", huge_rem); @@ -1142,7 +1142,7 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r expr_ref r_ge_y_half(m), r_gt_ny_half(m), r_le_y_half(m), r_lt_ny_half(m); expr_ref r_ge_zero(m), r_le_zero(m); expr_ref rounded_sub_y(m), rounded_add_y(m); - mpf zero, two; + mpf zero, two; m_mpf_manager.set(two, ebits, sbits, 2); m_mpf_manager.set(zero, ebits, sbits, 0); mk_numeral(s, two, two_e); @@ -1151,7 +1151,7 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r mk_neg(s, y_half, ny_half); mk_is_zero(y_half, y_half_is_zero); y_half_is_nz = m.mk_not(y_half_is_zero); - + mk_float_ge(s, rndd, y_half, r_ge_y_half); mk_float_gt(s, rndd, ny_half, r_gt_ny_half); mk_float_le(s, rndd, y_half, r_le_y_half); @@ -1161,8 +1161,8 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r mk_add(s, rne_bv, rndd, y, rounded_add_y); expr_ref sub_cnd(m), add_cnd(m); - sub_cnd = m.mk_and(y_half_is_nz, - m.mk_or(m.mk_and(y_is_pos, r_ge_y_half), + sub_cnd = m.mk_and(y_half_is_nz, + m.mk_or(m.mk_and(y_is_pos, r_ge_y_half), m.mk_and(y_is_neg, r_le_y_half))); add_cnd = m.mk_and(y_half_is_nz, m.mk_or(m.mk_and(y_is_pos, r_lt_ny_half), @@ -1170,7 +1170,7 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r mk_ite(add_cnd, rounded_add_y, rndd, v7); mk_ite(sub_cnd, rounded_sub_y, v7, v7); - + // And finally, we tie them together. mk_ite(c6, v6, v7, result); mk_ite(c5, v5, result, result); @@ -3698,7 +3698,7 @@ void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) { // CMW: This works only for quantifier-free formulas. if (m_util.is_fp(e)) { expr_ref new_bv(m); - expr *e_sgn, *e_sig, *e_exp; + expr *e_sgn, *e_sig, *e_exp; split_fp(e, e_sgn, e_exp, e_sig); unsigned ebits = m_bv_util.get_bv_size(e_exp); unsigned sbits = m_bv_util.get_bv_size(e_sig) + 1; diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index 0845393f4..65862bf90 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -103,7 +103,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co } return BR_FAILED; } - + if (m_conv.is_float_family(f)) { switch (f->get_decl_kind()) { case OP_FPA_RM_NEAREST_TIES_TO_AWAY: @@ -157,7 +157,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co case OP_FPA_INTERNAL_BVWRAP: case OP_FPA_INTERNAL_BV2RM: - + case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: @@ -169,7 +169,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co NOT_IMPLEMENTED_YET(); } } - else + else { SASSERT(!m_conv.is_float_family(f)); if (m_conv.fu().contains_floats(f)) { From acdaeca826179a8395c051b888cd5ef9befb407b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 4 Oct 2016 18:04:56 +0100 Subject: [PATCH 2/7] Bugfix for ITEs over FP rounding modes. Fixes #751. --- src/ast/fpa/fpa2bv_converter.cpp | 31 ++++++++++++++++++++----------- src/ast/fpa/fpa2bv_rewriter.cpp | 4 ++-- 2 files changed, 22 insertions(+), 13 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 90007b330..6bba4663d 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -90,19 +90,28 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) { } void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) { - SASSERT(m_util.is_fp(t) && m_util.is_fp(f)); + if (m_util.is_fp(t) && m_util.is_fp(f)) { + expr *t_sgn, *t_sig, *t_exp; + expr *f_sgn, *f_sig, *f_exp; + split_fp(t, t_sgn, t_exp, t_sig); + split_fp(f, f_sgn, f_exp, f_sig); - expr *t_sgn, *t_sig, *t_exp; - expr *f_sgn, *f_sig, *f_exp; - split_fp(t, t_sgn, t_exp, t_sig); - split_fp(f, f_sgn, f_exp, f_sig); + expr_ref sgn(m), s(m), e(m); + m_simp.mk_ite(c, t_sgn, f_sgn, sgn); + m_simp.mk_ite(c, t_sig, f_sig, s); + m_simp.mk_ite(c, t_exp, f_exp, e); - expr_ref sgn(m), s(m), e(m); - m_simp.mk_ite(c, t_sgn, f_sgn, sgn); - m_simp.mk_ite(c, t_sig, f_sig, s); - m_simp.mk_ite(c, t_exp, f_exp, e); - - result = m_util.mk_fp(sgn, e, s); + result = m_util.mk_fp(sgn, e, s); + } + else if (m_util.is_rm(t) && m_util.is_rm(f)) + { + SASSERT(m_util.is_bv2rm(t) && m_util.is_bv2rm(f)); + TRACE("fpa2bv", tout << "ite rm: t=" << mk_ismt2_pp(t, m) << " f=" << mk_ismt2_pp(f, m) << std::endl; ); + m_simp.mk_ite(c, to_app(t)->get_arg(0), to_app(f)->get_arg(0), result); + result = m_util.mk_bv2rm(result); + } + else + UNREACHABLE(); } void fpa2bv_converter::mk_distinct(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index 65862bf90..5f89e12db 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -86,10 +86,10 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co return BR_DONE; } return BR_FAILED; - } + } else if (m().is_ite(f)) { SASSERT(num == 3); - if (m_conv.is_float(args[1])) { + if (m_conv.is_float(args[1]) || m_conv.is_rm(args[1])) { m_conv.mk_ite(args[0], args[1], args[2], result); return BR_DONE; } From f4fd72174140d7e0246987d83520e5fec357354c Mon Sep 17 00:00:00 2001 From: Dionna Amalie Glaze Date: Tue, 4 Oct 2016 13:02:31 -0500 Subject: [PATCH 3/7] Z3_query_constructor documentation clarification Hit a segfault when I assumed the API would allocate these _out parameters for me. --- src/api/z3_api.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 666485a7f..cd889b3be 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1997,9 +1997,9 @@ extern "C" { \param c logical context. \param constr constructor container. The container must have been passed in to a #Z3_mk_datatype call. \param num_fields number of accessor fields in the constructor. - \param constructor constructor function declaration. - \param tester constructor test function declaration. - \param accessors array of accessor function declarations. + \param constructor constructor function declaration, allocated by user. + \param tester constructor test function declaration, allocated by user. + \param accessors array of accessor function declarations allocated by user. The array must contain num_fields elements. def_API('Z3_query_constructor', VOID, (_in(CONTEXT), _in(CONSTRUCTOR), _in(UINT), _out(FUNC_DECL), _out(FUNC_DECL), _out_array(2, FUNC_DECL))) */ From d495b086395ac8693151e0561938c3fddfbb1d76 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 5 Oct 2016 15:34:02 +0100 Subject: [PATCH 4/7] Build/test fix for python3 --- src/api/python/z3/z3num.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/api/python/z3/z3num.py b/src/api/python/z3/z3num.py index c8f15e7b8..2943b0796 100644 --- a/src/api/python/z3/z3num.py +++ b/src/api/python/z3/z3num.py @@ -10,6 +10,8 @@ from .z3core import * from .z3printer import * from fractions import Fraction +from .z3 import _get_ctx + def _to_numeral(num, ctx=None): if isinstance(num, Numeral): return num From 4956f6ef5bceeee429d83d8179ec3a7b45f01f4b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 5 Oct 2016 16:11:07 +0100 Subject: [PATCH 5/7] Test fix for python3 --- src/api/python/z3/z3num.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3/z3num.py b/src/api/python/z3/z3num.py index 2943b0796..b1af58dc3 100644 --- a/src/api/python/z3/z3num.py +++ b/src/api/python/z3/z3num.py @@ -88,7 +88,7 @@ class Numeral: def __init__(self, num, ctx=None): if isinstance(num, Ast): self.ast = num - self.ctx = z3._get_ctx(ctx) + self.ctx = _get_ctx(ctx) elif isinstance(num, RatNumRef) or isinstance(num, AlgebraicNumRef): self.ast = num.ast self.ctx = num.ctx From 9548b88e711d2abedd5db7c8af3e30c8ac2f200d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 6 Oct 2016 16:24:49 +0100 Subject: [PATCH 6/7] Added dummy code contracts for .NET Core/CoreCLR builds. --- src/api/dotnet/core/DummyContracts.cs | 59 +++++++++++++++++++++++++++ src/api/dotnet/core/project.json | 21 ++++++++++ 2 files changed, 80 insertions(+) create mode 100644 src/api/dotnet/core/DummyContracts.cs create mode 100644 src/api/dotnet/core/project.json diff --git a/src/api/dotnet/core/DummyContracts.cs b/src/api/dotnet/core/DummyContracts.cs new file mode 100644 index 000000000..e0002e5be --- /dev/null +++ b/src/api/dotnet/core/DummyContracts.cs @@ -0,0 +1,59 @@ +/*++ +Copyright () 2016 Microsoft Corporation + +Module Name: + + Contracts.cs + +Abstract: + + Z3 Managed API: Dummy Code Contracts class for .NET + frameworks that don't support them (e.g., CoreCLR). + +Author: + + Christoph Wintersteiger (cwinter) 2016-10-06 + +Notes: + +--*/ + +namespace System.Diagnostics.Contracts +{ + public class ContractClass : Attribute + { + public ContractClass(Type t) { } + } + + public class ContractClassFor : Attribute + { + public ContractClassFor(Type t) { } + } + + public class ContractInvariantMethod : Attribute + { + public ContractInvariantMethod() { } + } + + public class ContractVerification : Attribute + { + public ContractVerification(bool b) { } + } + + public class Pure : Attribute { } + + public static class Contract + { + public static void Ensures(bool b) { } + public static void Requires(bool b) { } + public static void Assume(bool b, string msg) { } + public static void Assert(bool b) { } + public static bool ForAll(bool b) { return true; } + public static bool ForAll(Object c, Func p) { return true; } + public static bool ForAll(int from, int to, Predicate p) { return true; } + public static void Invariant(bool b) { } + public static T[] Result() { return new T[1]; } + public static void EndContractBlock() { } + public static T ValueAtReturn(out T v) { T[] t = new T[1]; v = t[0]; return v; } + } +} \ No newline at end of file diff --git a/src/api/dotnet/core/project.json b/src/api/dotnet/core/project.json new file mode 100644 index 000000000..afe281a50 --- /dev/null +++ b/src/api/dotnet/core/project.json @@ -0,0 +1,21 @@ +{ + "version": "1.0.0-*", + "buildOptions": { + "debugType": "portable", + "emitEntryPoint": false, + "outputName": "Microsoft.Z3", + "compile": [ "../*.cs", "*.cs" ] + }, + "dependencies": { }, + "frameworks": { + "netcoreapp1.0": { + "dependencies": { + "Microsoft.NETCore.App": { + "type": "platform", + "version": "1.0.1" + } + }, + "imports": "dnxcore50" + } + } +} From 5dec919217354afe7b09edafecce618a0c9e2e42 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 6 Oct 2016 16:36:19 +0100 Subject: [PATCH 7/7] Remove unnecessary "unsafe" qualifier on internal .NET API class. --- scripts/update_api.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 4ca11938c..04378b371 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -363,7 +363,7 @@ def mk_dotnet(dotnet): dotnet.write(' {\n\n') dotnet.write(' [UnmanagedFunctionPointer(CallingConvention.Cdecl)]\n') dotnet.write(' public delegate void Z3_error_handler(Z3_context c, Z3_error_code e);\n\n') - dotnet.write(' public unsafe class LIB\n') + dotnet.write(' public class LIB\n') dotnet.write(' {\n') dotnet.write(' const string Z3_DLL_NAME = \"libz3.dll\";\n' ' \n')