From ec121db5c1a8a41c38fbee3922493d2e0a5e740e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 Jun 2013 12:02:35 -0700 Subject: [PATCH 1/3] addressing race condition on interrupts Signed-off-by: Nikolaj Bjorner --- src/shell/smtlib_frontend.cpp | 29 +++++++++++++++++++++-------- 1 file changed, 21 insertions(+), 8 deletions(-) diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp index a005462e2..b5d8635da 100644 --- a/src/shell/smtlib_frontend.cpp +++ b/src/shell/smtlib_frontend.cpp @@ -54,13 +54,19 @@ static void display_statistics() { } static void on_timeout() { - display_statistics(); - exit(0); + #pragma omp critical (g_display_stats) + { + display_statistics(); + exit(0); + } } static void on_ctrl_c(int) { signal (SIGINT, SIG_DFL); - display_statistics(); + #pragma omp critical (g_display_stats) + { + display_statistics(); + } raise(SIGINT); } @@ -83,9 +89,12 @@ unsigned read_smtlib_file(char const * benchmark_file) { } } - display_statistics(); - register_on_timeout_proc(0); - g_solver = 0; + #pragma omp critical (g_display_stats) + { + display_statistics(); + register_on_timeout_proc(0); + g_solver = 0; + } return solver.get_error_code(); } @@ -118,8 +127,12 @@ unsigned read_smtlib2_commands(char const * file_name) { result = parse_smt2_commands(ctx, std::cin, true); } - display_statistics(); - g_cmd_context = 0; + + #pragma omp critical (g_display_stats) + { + display_statistics(); + g_cmd_context = 0; + } return result ? 0 : 1; } From d569027e369ce834297873e990db098717155f88 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 Jun 2013 20:54:01 -0700 Subject: [PATCH 2/3] fix reference count bugs in overflow/underflow APIs for bit-vectors Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 4 + src/api/api_bv.cpp | 133 +++++++++++++++++++++---- src/muz_qe/qe.cpp | 2 +- src/smt/params/theory_arith_params.cpp | 1 + src/smt/theory_arith_core.h | 2 +- 5 files changed, 120 insertions(+), 22 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index c4b5c97d7..6855f6209 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1070,6 +1070,10 @@ extern "C" { case OP_BV2INT: return Z3_OP_BV2INT; case OP_CARRY: return Z3_OP_CARRY; case OP_XOR3: return Z3_OP_XOR3; + case OP_BSMUL_NO_OVFL: + case OP_BUMUL_NO_OVFL: + case OP_BSMUL_NO_UDFL: + return Z3_OP_UNINTERPRETED; default: UNREACHABLE(); return Z3_OP_UNINTERPRETED; diff --git a/src/api/api_bv.cpp b/src/api/api_bv.cpp index 8126c8e2a..07d4fda18 100644 --- a/src/api/api_bv.cpp +++ b/src/api/api_bv.cpp @@ -121,10 +121,20 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ unsigned sz = Z3_get_bv_sort_size(c, s); rational max_bound = power(rational(2), sz); Z3_ast bound = Z3_mk_numeral(c, max_bound.to_string().c_str(), int_s); - Z3_ast pred = Z3_mk_bvslt(c, n, Z3_mk_int(c, 0, s)); + Z3_inc_ref(c, bound); + Z3_ast zero = Z3_mk_int(c, 0, s); + Z3_inc_ref(c, zero); + Z3_ast pred = Z3_mk_bvslt(c, n, zero); + Z3_inc_ref(c, pred); // if n <_sigend 0 then r - s^sz else r Z3_ast args[2] = { r, bound }; - Z3_ast res = Z3_mk_ite(c, pred, Z3_mk_sub(c, 2, args), r); + Z3_ast sub = Z3_mk_sub(c, 2, args); + Z3_inc_ref(c, sub); + Z3_ast res = Z3_mk_ite(c, pred, sub, r); + Z3_dec_ref(c, bound); + Z3_dec_ref(c, pred); + Z3_dec_ref(c, sub); + Z3_dec_ref(c, zero); RETURN_Z3(res); } else { @@ -156,7 +166,14 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - return Z3_mk_bvshl(c, Z3_mk_int64(c, 1, s), Z3_mk_int64(c, sz - 1, s)); + Z3_ast x = Z3_mk_int64(c, 1, s); + Z3_inc_ref(c, x); + Z3_ast y = Z3_mk_int64(c, sz - 1, s); + Z3_inc_ref(c, y); + Z3_ast result = Z3_mk_bvshl(c, x, y); + Z3_dec_ref(c, x); + Z3_dec_ref(c, y); + return result; Z3_CATCH_RETURN(0); } @@ -177,17 +194,40 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ RESET_ERROR_CODE(); if (is_signed) { Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1)); + Z3_inc_ref(c, zero); Z3_ast r = Z3_mk_bvadd(c, t1, t2); - Z3_ast args[2] = { Z3_mk_bvslt(c, zero, t1), Z3_mk_bvslt(c, zero, t2) }; + Z3_inc_ref(c, r); + Z3_ast l1 = Z3_mk_bvslt(c, zero, t1); + Z3_inc_ref(c, l1); + Z3_ast l2 = Z3_mk_bvslt(c, zero, t2); + Z3_inc_ref(c, l2); + Z3_ast args[2] = { l1, l2 }; Z3_ast args_pos = Z3_mk_and(c, 2, args); - return Z3_mk_implies(c, args_pos, Z3_mk_bvslt(c, zero, r)); + Z3_inc_ref(c, args_pos); + Z3_ast result = Z3_mk_implies(c, args_pos, Z3_mk_bvslt(c, zero, r)); + Z3_dec_ref(c, r); + Z3_dec_ref(c, l1); + Z3_dec_ref(c, l2); + Z3_dec_ref(c, args_pos); + Z3_dec_ref(c, zero); + return result; } else { unsigned sz = Z3_get_bv_sort_size(c, Z3_get_sort(c, t1)); t1 = Z3_mk_zero_ext(c, 1, t1); + Z3_inc_ref(c, t1); t2 = Z3_mk_zero_ext(c, 1, t2); + Z3_inc_ref(c, t2); Z3_ast r = Z3_mk_bvadd(c, t1, t2); - return Z3_mk_eq(c, Z3_mk_extract(c, sz, sz, r), Z3_mk_int(c, 0, Z3_mk_bv_sort(c, 1))); + Z3_inc_ref(c, r); + Z3_ast ex = Z3_mk_extract(c, sz, sz, r); + Z3_inc_ref(c, ex); + Z3_ast result = Z3_mk_eq(c, ex, Z3_mk_int(c, 0, Z3_mk_bv_sort(c, 1))); + Z3_dec_ref(c, t1); + Z3_dec_ref(c, t2); + Z3_dec_ref(c, ex); + Z3_dec_ref(c, r); + return result; } Z3_CATCH_RETURN(0); } @@ -197,10 +237,26 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ Z3_TRY; RESET_ERROR_CODE(); Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1)); + Z3_inc_ref(c, zero); Z3_ast r = Z3_mk_bvadd(c, t1, t2); - Z3_ast args[2] = { Z3_mk_bvslt(c, t1, zero), Z3_mk_bvslt(c, t2, zero) }; + Z3_inc_ref(c, r); + Z3_ast l1 = Z3_mk_bvslt(c, t1, zero); + Z3_inc_ref(c, l1); + Z3_ast l2 = Z3_mk_bvslt(c, t2, zero); + Z3_inc_ref(c, l2); + Z3_ast args[2] = { l1, l2 }; Z3_ast args_neg = Z3_mk_and(c, 2, args); - return Z3_mk_implies(c, args_neg, Z3_mk_bvslt(c, r, zero)); + Z3_inc_ref(c, args_neg); + Z3_ast lt = Z3_mk_bvslt(c, r, zero); + Z3_inc_ref(c, lt); + Z3_ast result = Z3_mk_implies(c, args_neg, lt); + Z3_dec_ref(c, lt); + Z3_dec_ref(c, l1); + Z3_dec_ref(c, l2); + Z3_dec_ref(c, r); + Z3_dec_ref(c, args_neg); + Z3_dec_ref(c, zero); + return result; Z3_CATCH_RETURN(0); } @@ -208,12 +264,28 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ Z3_ast Z3_API Z3_mk_bvsub_no_overflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2) { Z3_TRY; RESET_ERROR_CODE(); - Z3_sort s = Z3_get_sort(c, t2); Z3_ast minus_t2 = Z3_mk_bvneg(c, t2); + Z3_inc_ref(c, minus_t2); + Z3_sort s = Z3_get_sort(c, t2); Z3_ast min = Z3_mk_bvsmin(c, s); - return Z3_mk_ite(c, Z3_mk_eq(c, t2, min), - Z3_mk_bvslt(c, t1, Z3_mk_int(c, 0, s)), - Z3_mk_bvadd_no_overflow(c, t1, minus_t2, true)); + Z3_inc_ref(c, min); + Z3_ast x = Z3_mk_eq(c, t2, min); + Z3_inc_ref(c, x); + Z3_ast zero = Z3_mk_int(c, 0, s); + Z3_inc_ref(c, zero); + Z3_ast y = Z3_mk_bvslt(c, t1, zero); + Z3_inc_ref(c, y); + Z3_ast z = Z3_mk_bvadd_no_overflow(c, t1, minus_t2, true); + Z3_inc_ref(c, z); + Z3_ast result = Z3_mk_ite(c, x, y, z); + mk_c(c)->save_ast_trail(to_app(result)); + Z3_dec_ref(c, minus_t2); + Z3_dec_ref(c, min); + Z3_dec_ref(c, x); + Z3_dec_ref(c, y); + Z3_dec_ref(c, z); + Z3_dec_ref(c, zero); + return result; Z3_CATCH_RETURN(0); } @@ -222,10 +294,19 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ RESET_ERROR_CODE(); if (is_signed) { Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1)); - if (Z3_get_error_code(c) != Z3_OK) return 0; + Z3_inc_ref(c, zero); Z3_ast minus_t2 = Z3_mk_bvneg(c, t2); - if (Z3_get_error_code(c) != Z3_OK) return 0; - return Z3_mk_implies(c, Z3_mk_bvslt(c, zero, t2), Z3_mk_bvadd_no_underflow(c, t1, minus_t2)); + Z3_inc_ref(c, minus_t2); + Z3_ast x = Z3_mk_bvslt(c, zero, t2); + Z3_inc_ref(c, x); + Z3_ast y = Z3_mk_bvadd_no_underflow(c, t1, minus_t2); + Z3_inc_ref(c, y); + Z3_ast result = Z3_mk_implies(c, x, y); + Z3_dec_ref(c, zero); + Z3_dec_ref(c, minus_t2); + Z3_dec_ref(c, x); + Z3_dec_ref(c, y); + return result; } else { return Z3_mk_bvule(c, t2, t1); @@ -267,12 +348,24 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ Z3_TRY; RESET_ERROR_CODE(); Z3_sort s = Z3_get_sort(c, t1); - if (Z3_get_error_code(c) != Z3_OK) return 0; Z3_ast min = Z3_mk_bvmsb(c, s); - if (Z3_get_error_code(c) != Z3_OK) return 0; - Z3_ast args[2] = { Z3_mk_eq(c, t1, min), - Z3_mk_eq(c, t2, Z3_mk_int(c, -1, s)) }; - return Z3_mk_not(c, Z3_mk_and(c, 2, args)); + Z3_inc_ref(c, min); + Z3_ast x = Z3_mk_eq(c, t1, min); + Z3_inc_ref(c, x); + Z3_ast y = Z3_mk_int(c, -1, s); + Z3_inc_ref(c, y); + Z3_ast z = Z3_mk_eq(c, t2, y); + Z3_inc_ref(c, z); + Z3_ast args[2] = { x, z }; + Z3_ast u = Z3_mk_and(c, 2, args); + Z3_inc_ref(c, u); + Z3_ast result = Z3_mk_not(c, u); + Z3_dec_ref(c, min); + Z3_dec_ref(c, x); + Z3_dec_ref(c, y); + Z3_dec_ref(c, z); + Z3_dec_ref(c, u); + return result; Z3_CATCH_RETURN(0); } diff --git a/src/muz_qe/qe.cpp b/src/muz_qe/qe.cpp index 894a935b5..5603b8102 100644 --- a/src/muz_qe/qe.cpp +++ b/src/muz_qe/qe.cpp @@ -2084,7 +2084,7 @@ namespace qe { flet fl1(m_fparams.m_model, true); flet fl2(m_fparams.m_simplify_bit2int, true); - flet fl3(m_fparams.m_arith_enum_const_mod, true); + //flet fl3(m_fparams.m_arith_enum_const_mod, true); flet fl4(m_fparams.m_bv_enable_int2bv2int, true); flet fl5(m_fparams.m_array_canonize_simplify, true); flet fl6(m_fparams.m_relevancy_lvl, 0); diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index 7281a5daa..dcffa83dc 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -33,6 +33,7 @@ void theory_arith_params::updt_params(params_ref const & _p) { m_arith_int_eq_branching = p.arith_int_eq_branch(); m_arith_ignore_int = p.arith_ignore_int(); m_arith_bound_prop = static_cast(p.arith_propagation_mode()); + m_arith_enum_const_mod = true; } diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index fafe73a79..195d78e25 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -408,7 +408,7 @@ namespace smt { mk_axiom(eqz, upper); rational k; if (m_params.m_arith_enum_const_mod && m_util.is_numeral(divisor, k) && - k.is_pos() && k < rational(512)) { + k.is_pos() && k < rational(8)) { rational j(0); #if 1 literal_buffer lits; From 56bfc06c4f7e33d4249551e269e443b19f71ef89 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 Jun 2013 20:55:15 -0700 Subject: [PATCH 3/3] fix reference count bugs in overflow/underflow APIs for bit-vectors Signed-off-by: Nikolaj Bjorner --- src/muz_qe/qe.cpp | 2 +- src/smt/params/theory_arith_params.cpp | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/src/muz_qe/qe.cpp b/src/muz_qe/qe.cpp index 5603b8102..894a935b5 100644 --- a/src/muz_qe/qe.cpp +++ b/src/muz_qe/qe.cpp @@ -2084,7 +2084,7 @@ namespace qe { flet fl1(m_fparams.m_model, true); flet fl2(m_fparams.m_simplify_bit2int, true); - //flet fl3(m_fparams.m_arith_enum_const_mod, true); + flet fl3(m_fparams.m_arith_enum_const_mod, true); flet fl4(m_fparams.m_bv_enable_int2bv2int, true); flet fl5(m_fparams.m_array_canonize_simplify, true); flet fl6(m_fparams.m_relevancy_lvl, 0); diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index dcffa83dc..7281a5daa 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -33,7 +33,6 @@ void theory_arith_params::updt_params(params_ref const & _p) { m_arith_int_eq_branching = p.arith_int_eq_branch(); m_arith_ignore_int = p.arith_ignore_int(); m_arith_bound_prop = static_cast(p.arith_propagation_mode()); - m_arith_enum_const_mod = true; }