From 87ae5888ee603ec7e365700ac3eefcb98dc05938 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 12 Nov 2015 14:48:29 +0000 Subject: [PATCH 1/9] whitespace --- src/ast/rewriter/bool_rewriter.cpp | 88 +++++++++++++++--------------- 1 file changed, 44 insertions(+), 44 deletions(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 5b0c38616..6dec03307 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -84,7 +84,7 @@ br_status bool_rewriter::mk_nflat_and_core(unsigned num_args, expr * const * arg ptr_buffer buffer; expr_fast_mark1 neg_lits; expr_fast_mark2 pos_lits; - + for (unsigned i = 0; i < num_args; i++) { expr * arg = args[i]; if (m().is_true(arg)) { @@ -120,9 +120,9 @@ br_status bool_rewriter::mk_nflat_and_core(unsigned num_args, expr * const * arg } buffer.push_back(arg); } - + unsigned sz = buffer.size(); - + switch(sz) { case 0: result = m().mk_true(); @@ -208,9 +208,9 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args } buffer.push_back(arg); } - + unsigned sz = buffer.size(); - + switch(sz) { case 0: result = m().mk_false(); @@ -222,7 +222,7 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args if (m_local_ctx && m_local_ctx_cost <= m_local_ctx_limit) { neg_lits.reset(); pos_lits.reset(); - if (local_ctx_simp(sz, buffer.c_ptr(), result)) + if (local_ctx_simp(sz, buffer.c_ptr(), result)) return BR_DONE; } if (s) { @@ -273,11 +273,11 @@ expr * bool_rewriter::mk_or_app(unsigned num_args, expr * const * args) { /** \brief Auxiliary method for local_ctx_simp. - + Replace args[i] by true if marked in neg_lits. Replace args[i] by false if marked in pos_lits. */ -bool bool_rewriter::simp_nested_not_or(unsigned num_args, expr * const * args, +bool bool_rewriter::simp_nested_not_or(unsigned num_args, expr * const * args, expr_fast_mark1 & neg_lits, expr_fast_mark2 & pos_lits, expr_ref & result) { ptr_buffer new_args; bool simp = false; @@ -307,13 +307,13 @@ bool bool_rewriter::simp_nested_not_or(unsigned num_args, expr * const * args, } if (simp) { switch(new_args.size()) { - case 0: - result = m().mk_true(); + case 0: + result = m().mk_true(); return true; - case 1: - mk_not(new_args[0], result); + case 1: + mk_not(new_args[0], result); return true; - default: + default: result = m().mk_not(m().mk_or(new_args.size(), new_args.c_ptr())); return true; } @@ -358,7 +358,7 @@ void bool_rewriter::mk_nested_ite(expr * c, expr * t, expr * e, expr_ref & resul result = t; return; } - + if (m().is_false(c)) { result = e; return; @@ -368,7 +368,7 @@ void bool_rewriter::mk_nested_ite(expr * c, expr * t, expr * e, expr_ref & resul result = t; return; } - + if (m().is_bool(t)) { if (m().is_true(t)) { if (m().is_false(e)) { @@ -384,13 +384,13 @@ void bool_rewriter::mk_nested_ite(expr * c, expr * t, expr * e, expr_ref & resul return; } expr_ref tmp(m()); - mk_not(e, tmp); + mk_not(e, tmp); result = m().mk_not(m().mk_or(c, tmp)); return; } if (m().is_true(e)) { expr_ref tmp(m()); - mk_not(c, tmp); + mk_not(c, tmp); result = m().mk_or(tmp, t); return; } @@ -406,7 +406,7 @@ void bool_rewriter::mk_nested_ite(expr * c, expr * t, expr * e, expr_ref & resul result = m().mk_or(c, e); return; } - if (m().is_complement_core(t, e)) { // t = not(e) + if (m().is_complement_core(t, e)) { // t = not(e) mk_eq(c, t, result); return; } @@ -443,8 +443,8 @@ bool bool_rewriter::simp_nested_eq_ite(expr * t, expr_fast_mark1 & neg_lits, exp expr * new_e = simp_arg(to_app(t)->get_arg(2), neg_lits, pos_lits, modified); if (!modified) return false; - // It is not safe to invoke mk_ite here, since it can recursively call - // local_ctx_simp by + // It is not safe to invoke mk_ite here, since it can recursively call + // local_ctx_simp by // - transforming the ITE into an OR // - and invoked mk_or, that will invoke local_ctx_simp // mk_ite(new_c, new_t, new_e, result); @@ -522,7 +522,7 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_ PUSH_NEW_ARG(arg); \ } \ } - + m_local_ctx_cost += 2*num_args; #if 0 static unsigned counter = 0; @@ -567,9 +567,9 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_ /** \brief Apply simplification if ite is an if-then-else tree where every leaf is a value. - - This is an efficient way to - + + This is an efficient way to + */ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) { SASSERT(m().is_ite(ite)); @@ -585,7 +585,7 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) tout << t << " " << e << " " << val << "\n";); result = m().mk_false(); return BR_DONE; - } + } if (t == val && e == val) { result = m().mk_true(); @@ -598,7 +598,7 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) } SASSERT(e == val); - + mk_not(ite->get_arg(0), result); return BR_DONE; } @@ -642,14 +642,14 @@ static bool is_ite_value_tree_neq_value(ast_manager & m, app * ite, app * val) { return true; } -#endif +#endif br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { if (lhs == rhs) { result = m().mk_true(); return BR_DONE; } - + if (m().are_distinct(lhs, rhs)) { result = m().mk_false(); return BR_DONE; @@ -662,7 +662,7 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { // return BR_DONE; // } r = try_ite_value(to_app(lhs), to_app(rhs), result); - CTRACE("try_ite_value", r != BR_FAILED, + CTRACE("try_ite_value", r != BR_FAILED, tout << mk_ismt2_pp(lhs, m()) << "\n" << mk_ismt2_pp(rhs, m()) << "\n--->\n" << mk_ismt2_pp(result, m()) << "\n";); } else if (m().is_ite(rhs) && m().is_value(lhs)) { @@ -671,7 +671,7 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { // return BR_DONE; // } r = try_ite_value(to_app(rhs), to_app(lhs), result); - CTRACE("try_ite_value", r != BR_FAILED, + CTRACE("try_ite_value", r != BR_FAILED, tout << mk_ismt2_pp(lhs, m()) << "\n" << mk_ismt2_pp(rhs, m()) << "\n--->\n" << mk_ismt2_pp(result, m()) << "\n";); } if (r != BR_FAILED) @@ -756,13 +756,13 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args result = m().mk_and(new_diseqs.size(), new_diseqs.c_ptr()); return BR_REWRITE3; } - + return BR_FAILED; } br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result) { bool s = false; - + // (ite (not c) a b) ==> (ite c b a) if (m().is_not(c)) { c = to_app(c)->get_arg(0); @@ -788,7 +788,7 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re result = t; return BR_DONE; } - + if (m().is_false(c)) { result = e; return BR_DONE; @@ -814,18 +814,18 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re return BR_DONE; } expr_ref tmp(m()); - mk_not(c, tmp); + mk_not(c, tmp); mk_and(tmp, e, result); return BR_DONE; } if (m().is_true(e)) { expr_ref tmp(m()); - mk_not(c, tmp); + mk_not(c, tmp); mk_or(tmp, t, result); return BR_DONE; } if (m().is_false(e)) { - mk_and(c, t, result); + mk_and(c, t, result); return BR_DONE; } if (c == e) { @@ -833,10 +833,10 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re return BR_DONE; } if (c == t) { - mk_or(c, e, result); + mk_or(c, e, result); return BR_DONE; } - if (m().is_complement_core(t, e)) { // t = not(e) + if (m().is_complement_core(t, e)) { // t = not(e) mk_eq(c, t, result); return BR_DONE; } @@ -863,10 +863,10 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re result = m().mk_ite(new_c, to_app(t)->get_arg(1), e); return BR_REWRITE1; } - + if (m().is_ite(e)) { // (ite c1 (ite c2 t1 t2) (ite c3 t1 t2)) ==> (ite (or (and c1 c2) (and (not c1) c3)) t1 t2) - if (to_app(t)->get_arg(1) == to_app(e)->get_arg(1) && + if (to_app(t)->get_arg(1) == to_app(e)->get_arg(1) && to_app(t)->get_arg(2) == to_app(e)->get_arg(2)) { expr_ref and1(m()); expr_ref and2(m()); @@ -879,9 +879,9 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re result = m().mk_ite(new_c, to_app(t)->get_arg(1), to_app(t)->get_arg(2)); return BR_REWRITE1; } - + // (ite c1 (ite c2 t1 t2) (ite c3 t2 t1)) ==> (ite (or (and c1 c2) (and (not c1) (not c3))) t1 t2) - if (to_app(t)->get_arg(1) == to_app(e)->get_arg(2) && + if (to_app(t)->get_arg(1) == to_app(e)->get_arg(2) && to_app(t)->get_arg(2) == to_app(e)->get_arg(1)) { expr_ref and1(m()); expr_ref and2(m()); @@ -922,10 +922,10 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re result = m().mk_ite(c, t, e); return BR_DONE; } - + return BR_FAILED; } - + br_status bool_rewriter::mk_not_core(expr * t, expr_ref & result) { if (m().is_not(t)) { result = to_app(t)->get_arg(0); From 5cf2caa7e9a35705bf78a38a5076b89f3b4790d5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 12 Nov 2015 14:48:55 +0000 Subject: [PATCH 2/9] Added check for QF_BV in QF_UFBV tactic. --- src/tactic/smtlogics/qfufbv_tactic.cpp | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index d10b7c1b4..816d69b1f 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -25,6 +25,7 @@ Notes: #include"max_bv_sharing_tactic.h" #include"bv_size_reduction_tactic.h" #include"reduce_args_tactic.h" +#include"qfbv_tactic.h" tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) { params_ref main_p; @@ -41,13 +42,11 @@ tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) { ); tactic * st = using_params(and_then(preamble_st, - mk_smt_tactic()), + cond(mk_is_qfbv_probe(), + mk_qfbv_tactic(m), + mk_smt_tactic())), main_p); - //cond(is_qfbv(), - // and_then(mk_bit_blaster(m), - // mk_sat_solver(m)), - // mk_smt_solver()) st->updt_params(p); return st; } From 5f8f0b128022790bc6e4402c4a5671404cd92891 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 12 Nov 2015 14:49:21 +0000 Subject: [PATCH 3/9] Added bool rewriter case. --- src/ast/rewriter/bool_rewriter.cpp | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 6dec03307..0b8a51fb4 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -708,6 +708,19 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { result = m().mk_eq(lhs, rhs); return BR_DONE; } + + expr *la, *lb, *ra, *rb; + // fold (iff (iff a b) (iff (not a) b)) to false + if (m().is_iff(lhs, la, lb) && m().is_iff(rhs, ra, rb)) { + expr *n; + if ((la == ra && ((m().is_not(rb, n) && n == lb) || + (m().is_not(lb, n) && n == rb))) || + (lb == rb && ((m().is_not(ra, n) && n == la) || + (m().is_not(la, n) && n == ra)))) { + result = m().mk_false(); + return BR_DONE; + } + } } return BR_FAILED; } From 643dbb874b4db701b6ddbc13e5b9ddec1d819e15 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 12 Nov 2015 15:27:33 +0000 Subject: [PATCH 4/9] Added tactic that translates BV arrays into BV UFs. --- src/ast/array_decl_plugin.h | 15 +- src/tactic/bv/bvarray2uf_rewriter.cpp | 377 ++++++++++++++++++++++++++ src/tactic/bv/bvarray2uf_rewriter.h | 87 ++++++ src/tactic/bv/bvarray2uf_tactic.cpp | 168 ++++++++++++ src/tactic/bv/bvarray2uf_tactic.h | 33 +++ 5 files changed, 675 insertions(+), 5 deletions(-) create mode 100644 src/tactic/bv/bvarray2uf_rewriter.cpp create mode 100644 src/tactic/bv/bvarray2uf_rewriter.h create mode 100644 src/tactic/bv/bvarray2uf_tactic.cpp create mode 100644 src/tactic/bv/bvarray2uf_tactic.h diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index 778b94c33..60adc3ae6 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -22,7 +22,7 @@ Revision History: #include"ast.h" -inline sort* get_array_range(sort const * s) { +inline sort* get_array_range(sort const * s) { return to_sort(s->get_parameter(s->get_num_parameters() - 1).get_ast()); } @@ -104,20 +104,20 @@ class array_decl_plugin : public decl_plugin { } // - // Contract for sort: - // parameters[0] - 1st dimension + // Contract for sort: + // parameters[0] - 1st dimension // ... // parameters[n-1] - nth dimension // parameters[n] - range // virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters); - + // // Contract for func_decl: // parameters[0] - array sort // Contract for others: // no parameters - virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); virtual void get_op_names(svector & op_names, symbol const & logic); @@ -184,6 +184,11 @@ public: sort * mk_array_sort(sort* dom, sort* range) { return mk_array_sort(1, &dom, range); } sort * mk_array_sort(unsigned arity, sort* const* domain, sort* range); + + app * mk_as_array(sort * s, func_decl * f) { + parameter param(f); + return m_manager.mk_app(m_fid, OP_AS_ARRAY, 1, ¶m, 0, 0, s); + } }; diff --git a/src/tactic/bv/bvarray2uf_rewriter.cpp b/src/tactic/bv/bvarray2uf_rewriter.cpp new file mode 100644 index 000000000..83038cfa9 --- /dev/null +++ b/src/tactic/bv/bvarray2uf_rewriter.cpp @@ -0,0 +1,377 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + bvarray2uf_rewriter.cpp + +Abstract: + + Rewriter that rewrites bit-vector arrays into bit-vector + (uninterpreted) functions. + +Author: + + Christoph (cwinter) 2015-11-04 + +Notes: + +--*/ + +#include"cooperate.h" +#include"bv_decl_plugin.h" +#include"array_decl_plugin.h" +#include"params.h" +#include"ast_pp.h" +#include"bvarray2uf_rewriter.h" + +// [1] C. M. Wintersteiger, Y. Hamadi, and L. de Moura: Efficiently Solving +// Quantified Bit-Vector Formulas, in Formal Methods in System Design, +// vol. 42, no. 1, pp. 3-23, Springer, 2013. + +bvarray2uf_rewriter_cfg::bvarray2uf_rewriter_cfg(ast_manager & m, params_ref const & p) : + m_manager(m), + m_out(m), + m_bindings(m), + m_bv_util(m), + m_array_util(m), + m_emc(0), + m_fmc(0), + extra_assertions(m) { + updt_params(p); + // We need to make sure that the mananger has the BV and array plugins loaded. + symbol s_bv("bv"); + if (!m_manager.has_plugin(s_bv)) + m_manager.register_plugin(s_bv, alloc(bv_decl_plugin)); + symbol s_array("array"); + if (!m_manager.has_plugin(s_array)) + m_manager.register_plugin(s_array, alloc(array_decl_plugin)); +} + +bvarray2uf_rewriter_cfg::~bvarray2uf_rewriter_cfg() { + for (obj_map::iterator it = m_arrays_fs.begin(); + it != m_arrays_fs.end(); + it++) + m_manager.dec_ref(it->m_value); +} + +void bvarray2uf_rewriter_cfg::reset() {} + +sort * bvarray2uf_rewriter_cfg::get_index_sort(expr * e) { + return get_index_sort(m_manager.get_sort(e)); +} + +sort * bvarray2uf_rewriter_cfg::get_index_sort(sort * s) { + SASSERT(s->get_num_parameters() >= 2); + unsigned total_width = 0; + for (unsigned i = 0; i < s->get_num_parameters() - 1; i++) { + parameter const & p = s->get_parameter(i); + SASSERT(p.is_ast() && is_sort(to_sort(p.get_ast()))); + SASSERT(m_bv_util.is_bv_sort(to_sort(p.get_ast()))); + total_width += m_bv_util.get_bv_size(to_sort(p.get_ast())); + } + return m_bv_util.mk_sort(total_width); +} + +sort * bvarray2uf_rewriter_cfg::get_value_sort(expr * e) { + return get_value_sort(m_manager.get_sort(e)); +} + +sort * bvarray2uf_rewriter_cfg::get_value_sort(sort * s) { + SASSERT(s->get_num_parameters() >= 2); + parameter const & p = s->get_parameter(s->get_num_parameters() - 1); + SASSERT(p.is_ast() && is_sort(to_sort(p.get_ast()))); + return to_sort(p.get_ast()); +} + +bool bvarray2uf_rewriter_cfg::is_bv_array(expr * e) { + return is_bv_array(m_manager.get_sort(e)); +} + +bool bvarray2uf_rewriter_cfg::is_bv_array(sort * s) { + if (!m_array_util.is_array(s)) + return false; + + SASSERT(s->get_num_parameters() >= 2); + for (unsigned i = 0; i < s->get_num_parameters(); i++) { + parameter const & p = s->get_parameter(i); + if (!p.is_ast() || !is_sort(to_sort(p.get_ast())) || + !m_bv_util.is_bv_sort(to_sort(p.get_ast()))) + return false; + } + + return true; +} + +func_decl_ref bvarray2uf_rewriter_cfg::mk_uf_for_array(expr * e) { + SASSERT(is_bv_array(e)); + + if (m_array_util.is_as_array(e)) + return func_decl_ref(static_cast(to_app(e)->get_decl()->get_parameter(0).get_ast()), m_manager); + else { + app * a = to_app(e); + func_decl * bv_f = 0; + if (!m_arrays_fs.find(e, bv_f)) { + sort * domain = get_index_sort(a); + sort * range = get_value_sort(a); + bv_f = m_manager.mk_fresh_func_decl("f_t", "", 1, &domain, range); + if (is_uninterp_const(e)) { + if (m_emc) + m_emc->insert(to_app(e)->get_decl(), + m_array_util.mk_as_array(m_manager.get_sort(e), bv_f)); + } + else if (m_fmc) + m_fmc->insert(bv_f); + m_arrays_fs.insert(e, bv_f); + m_manager.inc_ref(bv_f); + } + + return func_decl_ref(bv_f, m_manager); + } +} + +br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + br_status res = BR_FAILED; + + if (m_manager.is_eq(f) && is_bv_array(f->get_domain()[0])) { + SASSERT(num == 2); + // From [1]: Finally, we replace equations of the form t = s, + // where t and s are arrays, with \forall x . f_t(x) = f_s(x). + func_decl_ref f_t(mk_uf_for_array(args[0]), m_manager); + func_decl_ref f_s(mk_uf_for_array(args[1]), m_manager); + + sort * sorts[1] = { get_index_sort(m_manager.get_sort(args[0])) }; + symbol names[1] = { symbol("x") }; + var_ref x(m_manager.mk_var(0, sorts[0]), m_manager); + + expr_ref body(m_manager); + body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), m_manager.mk_app(f_s, x.get())); + + result = m_manager.mk_forall(1, sorts, names, body); + res = BR_DONE; + } + else if (m_manager.is_distinct(f) && is_bv_array(f->get_domain()[0])) { + result = m_manager.mk_distinct_expanded(num, args); + res = BR_REWRITE1; + } + else if (f->get_family_id() == null_family_id) { + TRACE("bvarray2uf_rw", tout << "UF APP: " << f->get_name() << std::endl; ); + + bool has_bv_arrays = false; + func_decl_ref f_t(m_manager); + for (unsigned i = 0; i < num; i++) { + if (is_bv_array(args[i])) { + SASSERT(m_array_util.is_as_array(args[i])); + has_bv_arrays = true; + } + } + + expr_ref t(m_manager); + t = m_manager.mk_app(f, num, args); + + if (is_bv_array(t)) { + // From [1]: For every array term t we create a fresh uninterpreted function f_t. + f_t = mk_uf_for_array(t); + result = m_array_util.mk_as_array(m_manager.get_sort(t), f_t); + res = BR_DONE; + } + else if (has_bv_arrays) { + result = t; + res = BR_DONE; + } + else + res = BR_FAILED; + } + else if (m_array_util.get_family_id() == f->get_family_id()) { + TRACE("bvarray2uf_rw", tout << "APP: " << f->get_name() << std::endl; ); + + if (m_array_util.is_select(f)) { + SASSERT(num == 2); + expr * t = args[0]; + expr * i = args[1]; + TRACE("bvarray2uf_rw", tout << + "select; array: " << mk_ismt2_pp(t, m()) << + " index: " << mk_ismt2_pp(i, m()) << std::endl;); + + if (!is_bv_array(t)) + res = BR_FAILED; + else { + // From [1]: Then, we replace terms of the form select(t, i) with f_t(i). + func_decl_ref f_t(mk_uf_for_array(t), m_manager); + result = m_manager.mk_app(f_t, i); + res = BR_DONE; + } + } + else { + if (!is_bv_array(f->get_range())) + res = BR_FAILED; + else { + if (m_array_util.is_const(f)) { + SASSERT(num == 1); + expr_ref t(m_manager.mk_app(f, num, args), m_manager); + expr * v = args[0]; + func_decl_ref f_t(mk_uf_for_array(t), m_manager); + + result = m_array_util.mk_as_array(f->get_range(), f_t); + res = BR_DONE; + + // Add \forall x . f_t(x) = v + sort * sorts[1] = { get_index_sort(f->get_range()) }; + symbol names[1] = { symbol("x") }; + var_ref x(m_manager.mk_var(0, sorts[0]), m_manager); + + expr_ref body(m_manager); + body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), v); + + expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager); + extra_assertions.push_back(frllx); + } + else if (m_array_util.is_as_array(f)) { + res = BR_FAILED; + } + else if (m_array_util.is_map(f)) { + SASSERT(f->get_num_parameters() == 1); + SASSERT(f->get_parameter(0).is_ast()); + expr_ref t(m_manager.mk_app(f, num, args), m_manager); + func_decl_ref f_t(mk_uf_for_array(t), m_manager); + func_decl_ref map_f(to_func_decl(f->get_parameter(0).get_ast()), m_manager); + + func_decl_ref_vector ss(m_manager); + for (unsigned i = 0; i < num; i++) { + SASSERT(m_array_util.is_array(args[i])); + func_decl_ref fd(mk_uf_for_array(args[i]), m_manager); + ss.push_back(fd); + } + + // Add \forall x . f_t(x) = map_f(a[x], b[x], ...) + sort * sorts[1] = { get_index_sort(f->get_range()) }; + symbol names[1] = { symbol("x") }; + var_ref x(m_manager.mk_var(0, sorts[0]), m_manager); + + expr_ref_vector new_args(m_manager); + for (unsigned i = 0; i < num; i++) + new_args.push_back(m_manager.mk_app(ss[i].get(), x.get())); + + expr_ref body(m_manager); + body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), + m_manager.mk_app(map_f, num, new_args.c_ptr())); + + expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager); + extra_assertions.push_back(frllx); + + result = m_array_util.mk_as_array(f->get_range(), f_t); + res = BR_DONE; + } + else if (m_array_util.is_store(f)) { + SASSERT(num == 3); + expr * s = args[0]; + expr * i = args[1]; + expr * v = args[2]; + TRACE("bvarray2uf_rw", tout << + "store; array: " << mk_ismt2_pp(s, m()) << + " index: " << mk_ismt2_pp(i, m()) << + " value: " << mk_ismt2_pp(v, m()) << std::endl;); + if (!is_bv_array(s)) + res = BR_FAILED; + else { + expr_ref t(m_manager.mk_app(f, num, args), m_manager); + // From [1]: For every term t of the form store(s, i, v), we add the universal + // formula \forall x . x = i \vee f_t(x) = f_s(x), and the ground atom f_t(i) = v. + func_decl_ref f_s(mk_uf_for_array(s), m_manager); + func_decl_ref f_t(mk_uf_for_array(t), m_manager); + + result = m_array_util.mk_as_array(f->get_range(), f_t); + res = BR_DONE; + + sort * sorts[1] = { get_index_sort(f->get_range()) }; + symbol names[1] = { symbol("x") }; + var_ref x(m_manager.mk_var(0, sorts[0]), m_manager); + + expr_ref body(m_manager); + body = m_manager.mk_or(m_manager.mk_eq(x, i), + m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), + m_manager.mk_app(f_s, x.get()))); + + expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager); + extra_assertions.push_back(frllx); + + expr_ref ground_atom(m_manager); + ground_atom = m_manager.mk_eq(m_manager.mk_app(f_t, i), v); + extra_assertions.push_back(ground_atom); + TRACE("bvarray2uf_rw", tout << "ground atom: " << mk_ismt2_pp(ground_atom, m()) << std::endl; ); + } + } + else { + NOT_IMPLEMENTED_YET(); + res = BR_FAILED; + } + } + } + } + + CTRACE("bvarray2uf_rw", res==BR_DONE, tout << "result: " << mk_ismt2_pp(result, m()) << std::endl; ); + return res; +} + +bool bvarray2uf_rewriter_cfg::pre_visit(expr * t) +{ + TRACE("bvarray2uf_rw_q", tout << "pre_visit: " << mk_ismt2_pp(t, m()) << std::endl;); + + if (is_quantifier(t)) { + quantifier * q = to_quantifier(t); + TRACE("bvarray2uf_rw_q", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m()) << std::endl;); + sort_ref_vector new_bindings(m_manager); + for (unsigned i = 0; i < q->get_num_decls(); i++) + new_bindings.push_back(q->get_decl_sort(i)); + SASSERT(new_bindings.size() == q->get_num_decls()); + m_bindings.append(new_bindings); + } + return true; +} + +bool bvarray2uf_rewriter_cfg::reduce_quantifier(quantifier * old_q, + expr * new_body, + expr * const * new_patterns, + expr * const * new_no_patterns, + expr_ref & result, + proof_ref & result_pr) { + unsigned curr_sz = m_bindings.size(); + SASSERT(old_q->get_num_decls() <= curr_sz); + unsigned num_decls = old_q->get_num_decls(); + unsigned old_sz = curr_sz - num_decls; + string_buffer<> name_buffer; + ptr_buffer new_decl_sorts; + sbuffer new_decl_names; + for (unsigned i = 0; i < num_decls; i++) { + symbol const & n = old_q->get_decl_name(i); + sort * s = old_q->get_decl_sort(i); + + NOT_IMPLEMENTED_YET(); + + } + result = m().mk_quantifier(old_q->is_forall(), new_decl_sorts.size(), new_decl_sorts.c_ptr(), new_decl_names.c_ptr(), + new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(), + old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns); + result_pr = 0; + m_bindings.shrink(old_sz); + TRACE("bvarray2uf_rw_q", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " << + mk_ismt2_pp(old_q->get_expr(), m()) << std::endl << + " new body: " << mk_ismt2_pp(new_body, m()) << std::endl; + tout << "result = " << mk_ismt2_pp(result, m()) << std::endl;); + return true; +} + +bool bvarray2uf_rewriter_cfg::bvarray2uf_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & result_pr) { + if (t->get_idx() >= m_bindings.size()) + return false; + + expr_ref new_exp(m()); + sort * s = t->get_sort(); + + NOT_IMPLEMENTED_YET(); + + result = new_exp; + result_pr = 0; + TRACE("bvarray2uf_rw_q", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;); + return true; +} diff --git a/src/tactic/bv/bvarray2uf_rewriter.h b/src/tactic/bv/bvarray2uf_rewriter.h new file mode 100644 index 000000000..e65340cc3 --- /dev/null +++ b/src/tactic/bv/bvarray2uf_rewriter.h @@ -0,0 +1,87 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + bvarray2uf_rewriter.h + +Abstract: + + Rewriter that rewrites bit-vector arrays into bit-vector + (uninterpreted) functions. + +Author: + + Christoph (cwinter) 2015-11-04 + +Notes: + +--*/ +#ifndef BVARRAY2UF_REWRITER_H_ +#define BVARRAY2UF_REWRITER_H_ + +#include"rewriter_def.h" +#include"extension_model_converter.h" +#include"filter_model_converter.h" + +class bvarray2uf_rewriter_cfg : public default_rewriter_cfg { + ast_manager & m_manager; + expr_ref_vector m_out; + sort_ref_vector m_bindings; + bv_util m_bv_util; + array_util m_array_util; + extension_model_converter * m_emc; + filter_model_converter * m_fmc; + + obj_map m_arrays_fs; + +public: + bvarray2uf_rewriter_cfg(ast_manager & m, params_ref const & p); + ~bvarray2uf_rewriter_cfg(); + + ast_manager & m() const { return m_manager; } + void updt_params(params_ref const & p) {} + + void reset(); + + bool pre_visit(expr * t); + + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr); + + bool reduce_quantifier(quantifier * old_q, + expr * new_body, + expr * const * new_patterns, + expr * const * new_no_patterns, + expr_ref & result, + proof_ref & result_pr); + + bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr); + + expr_ref_vector extra_assertions; + + void set_mcs(extension_model_converter * emc, filter_model_converter * fmc) { m_emc = emc; m_fmc = fmc; } + +protected: + sort * get_index_sort(expr * e); + sort * get_index_sort(sort * s); + sort * get_value_sort(expr * e); + sort * get_value_sort(sort * s); + bool is_bv_array(expr * e); + bool is_bv_array(sort * e); + func_decl_ref mk_uf_for_array(expr * e); +}; + +template class rewriter_tpl; + +struct bvarray2uf_rewriter : public rewriter_tpl { + bvarray2uf_rewriter_cfg m_cfg; + bvarray2uf_rewriter(ast_manager & m, params_ref const & p) : + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(m, p) { + } + + void set_mcs(extension_model_converter * emc, filter_model_converter * fmc) { m_cfg.set_mcs(emc, fmc); } +}; + +#endif + diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp new file mode 100644 index 000000000..6bf1324f1 --- /dev/null +++ b/src/tactic/bv/bvarray2uf_tactic.cpp @@ -0,0 +1,168 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + bvarray2uf_tactic.cpp + +Abstract: + + Tactic that rewrites bit-vector arrays into bit-vector + (uninterpreted) functions. + +Author: + + Christoph (cwinter) 2015-11-04 + +Notes: + +--*/ +#include"tactical.h" +#include"bv_decl_plugin.h" +#include"expr_replacer.h" +#include"extension_model_converter.h" +#include"filter_model_converter.h" +#include"ast_smt2_pp.h" + +#include"bvarray2uf_tactic.h" +#include"bvarray2uf_rewriter.h" + +class bvarray2uf_tactic : public tactic { + + struct imp { + ast_manager & m_manager; + bool m_produce_models; + bool m_produce_proofs; + bool m_produce_cores; + volatile bool m_cancel; + bvarray2uf_rewriter m_rw; + + ast_manager & m() { return m_manager; } + + imp(ast_manager & m, params_ref const & p) : + m_manager(m), + m_produce_models(false), + m_cancel(false), + m_produce_proofs(false), + m_produce_cores(false), + m_rw(m, p) { + updt_params(p); + } + + void set_cancel(bool f) { + m_cancel = f; + } + + void checkpoint() { + if (m_cancel) + throw tactic_exception(TACTIC_CANCELED_MSG); + } + + void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) + { + SASSERT(g->is_well_sorted()); + tactic_report report("bvarray2uf", *g); + mc = 0; pc = 0; core = 0; result.reset(); + fail_if_proof_generation("bvarray2uf", g); + fail_if_unsat_core_generation("bvarray2uf", g); + + TRACE("bvarray2uf", tout << "Before: " << std::endl; g->display(tout); ); + m_produce_models = g->models_enabled(); + + if (m_produce_models) { + extension_model_converter * emc = alloc(extension_model_converter, m_manager); + filter_model_converter * fmc = alloc(filter_model_converter, m_manager); + mc = concat(emc, fmc); + m_rw.set_mcs(emc, fmc); + + } + + + m_rw.reset(); + expr_ref new_curr(m_manager); + proof_ref new_pr(m_manager); + unsigned size = g->size(); + for (unsigned idx = 0; idx < size; idx++) { + if (g->inconsistent()) + break; + expr * curr = g->form(idx); + m_rw(curr, new_curr, new_pr); + //if (m_produce_proofs) { + // proof * pr = g->pr(idx); + // new_pr = m.mk_modus_ponens(pr, new_pr); + //} + g->update(idx, new_curr, new_pr, g->dep(idx)); + } + + for (unsigned i = 0; i < m_rw.m_cfg.extra_assertions.size(); i++) + g->assert_expr(m_rw.m_cfg.extra_assertions[i].get()); + + g->inc_depth(); + result.push_back(g.get()); + TRACE("bvarray2uf", tout << "After: " << std::endl; g->display(tout);); + SASSERT(g->is_well_sorted()); + } + + void updt_params(params_ref const & p) { + } + }; + + imp * m_imp; + params_ref m_params; + +public: + bvarray2uf_tactic(ast_manager & m, params_ref const & p) : + m_params(p) { + m_imp = alloc(imp, m, p); + } + + virtual tactic * translate(ast_manager & m) { + return alloc(bvarray2uf_tactic, m, m_params); + } + + virtual ~bvarray2uf_tactic() { + dealloc(m_imp); + } + + virtual void updt_params(params_ref const & p) { + m_params = p; + m_imp->updt_params(p); + } + + virtual void collect_param_descrs(param_descrs & r) { + insert_produce_models(r); + } + + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + (*m_imp)(in, result, mc, pc, core); + } + + virtual void cleanup() { + ast_manager & m = m_imp->m(); + imp * d = alloc(imp, m, m_params); + #pragma omp critical (tactic_cancel) + { + std::swap(d, m_imp); + } + dealloc(d); + } + + virtual void set_cancel(bool f) { + if (m_imp) + m_imp->set_cancel(f); + } + +}; + + +tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p) { + return clean(alloc(bvarray2uf_tactic, m, p)); +} diff --git a/src/tactic/bv/bvarray2uf_tactic.h b/src/tactic/bv/bvarray2uf_tactic.h new file mode 100644 index 000000000..608a831e0 --- /dev/null +++ b/src/tactic/bv/bvarray2uf_tactic.h @@ -0,0 +1,33 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + bvarray2ufbvarray2uf_tactic.h + +Abstract: + + Tactic that rewrites bit-vector arrays into bit-vector + (uninterpreted) functions. + +Author: + + Christoph (cwinter) 2015-11-04 + +Notes: + +--*/ +#ifndef BV_ARRAY2UF_TACTIC_H_ +#define BV_ARRAY2UF_TACTIC_H_ + +#include"params.h" +class ast_manager; +class tactic; + +tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("bvarray2uf", "Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.", "mk_bvarray2uf_tactic(m, p)") +*/ + + +#endif \ No newline at end of file From 806016c315ca8969bb34c340930337df6de34b1f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 13 Nov 2015 14:11:39 +0000 Subject: [PATCH 5/9] build fix --- src/tactic/bv/bvarray2uf_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/bv/bvarray2uf_rewriter.cpp b/src/tactic/bv/bvarray2uf_rewriter.cpp index 83038cfa9..6245ed2bc 100644 --- a/src/tactic/bv/bvarray2uf_rewriter.cpp +++ b/src/tactic/bv/bvarray2uf_rewriter.cpp @@ -361,7 +361,7 @@ bool bvarray2uf_rewriter_cfg::reduce_quantifier(quantifier * old_q, return true; } -bool bvarray2uf_rewriter_cfg::bvarray2uf_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & result_pr) { +bool bvarray2uf_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & result_pr) { if (t->get_idx() >= m_bindings.size()) return false; From 4cb96bfe76a1b63209f42d8186d48ea0929c0f0b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 13 Nov 2015 15:55:01 +0000 Subject: [PATCH 6/9] Fixed assertion failure in fpa2bv_converter. Partially addresses #307 --- src/ast/fpa/fpa2bv_converter.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 4ee6366f0..19b07035f 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2648,9 +2648,8 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const SASSERT(num == 2); SASSERT(m_util.is_float(f->get_range())); - SASSERT(m_bv_util.is_bv(args[0])); - SASSERT(m_bv_util.is_bv(args[1])); SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM)); + SASSERT(m_bv_util.is_bv(args[1])); expr_ref bv_rm(m), x(m); bv_rm = to_app(args[0])->get_arg(0); From 954400cfa27cedf508b18da146e17973e5dbbc6f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 13 Nov 2015 16:35:08 +0000 Subject: [PATCH 7/9] whitespace --- src/api/api_solver_old.cpp | 48 +++++++++++++++++++------------------- 1 file changed, 24 insertions(+), 24 deletions(-) diff --git a/src/api/api_solver_old.cpp b/src/api/api_solver_old.cpp index 7e994a0e2..7fa469718 100644 --- a/src/api/api_solver_old.cpp +++ b/src/api/api_solver_old.cpp @@ -34,7 +34,7 @@ extern "C" { mk_c(c)->push(); Z3_CATCH; } - + void Z3_API Z3_pop(Z3_context c, unsigned num_scopes) { Z3_TRY; LOG_Z3_pop(c, num_scopes); @@ -62,7 +62,7 @@ extern "C" { Z3_TRY; LOG_Z3_assert_cnstr(c, a); RESET_ERROR_CODE(); - CHECK_FORMULA(a,); + CHECK_FORMULA(a,); mk_c(c)->assert_cnstr(to_expr(a)); Z3_CATCH; } @@ -81,11 +81,11 @@ extern "C" { result = mk_c(c)->check(_m); if (m) { if (_m) { - Z3_model_ref * m_ref = alloc(Z3_model_ref); + Z3_model_ref * m_ref = alloc(Z3_model_ref); m_ref->m_model = _m; // Must bump reference counter for backward compatibility reasons. // Don't need to invoke save_object, since the counter was bumped - m_ref->inc_ref(); + m_ref->inc_ref(); *m = of_model(m_ref); } else { @@ -100,21 +100,21 @@ extern "C" { RETURN_Z3_check_and_get_model static_cast(result); Z3_CATCH_RETURN(Z3_L_UNDEF); } - + Z3_lbool Z3_API Z3_check(Z3_context c) { Z3_TRY; - // This is just syntax sugar... - RESET_ERROR_CODE(); + // This is just syntax sugar... + RESET_ERROR_CODE(); CHECK_SEARCHING(c); Z3_lbool r = Z3_check_and_get_model(c, 0); return r; Z3_CATCH_RETURN(Z3_L_UNDEF); } - - Z3_lbool Z3_API Z3_check_assumptions(Z3_context c, - unsigned num_assumptions, Z3_ast const assumptions[], - Z3_model * m, Z3_ast* proof, + + Z3_lbool Z3_API Z3_check_assumptions(Z3_context c, + unsigned num_assumptions, Z3_ast const assumptions[], + Z3_model * m, Z3_ast* proof, unsigned* core_size, Z3_ast core[]) { Z3_TRY; LOG_Z3_check_assumptions(c, num_assumptions, assumptions, m, proof, core_size, core); @@ -130,11 +130,11 @@ extern "C" { model_ref _m; mk_c(c)->get_smt_kernel().get_model(_m); if (_m) { - Z3_model_ref * m_ref = alloc(Z3_model_ref); + Z3_model_ref * m_ref = alloc(Z3_model_ref); m_ref->m_model = _m; // Must bump reference counter for backward compatibility reasons. // Don't need to invoke save_object, since the counter was bumped - m_ref->inc_ref(); + m_ref->inc_ref(); *m = of_model(m_ref); } else { @@ -159,7 +159,7 @@ extern "C" { else if (proof) { *proof = 0; // breaks abstraction. } - RETURN_Z3_check_assumptions static_cast(result); + RETURN_Z3_check_assumptions static_cast(result); Z3_CATCH_RETURN(Z3_L_UNDEF); } @@ -185,7 +185,7 @@ extern "C" { symbol const& get_label() const { return m_label; } expr* get_literal() { return m_literal.get(); } }; - + typedef vector labels; Z3_literals Z3_API Z3_get_relevant_labels(Z3_context c) { @@ -196,7 +196,7 @@ extern "C" { ast_manager& m = mk_c(c)->m(); expr_ref_vector lits(m); mk_c(c)->get_smt_kernel().get_relevant_labels(0, labl_syms); - mk_c(c)->get_smt_kernel().get_relevant_labeled_literals(mk_c(c)->fparams().m_at_labels_cex, lits); + mk_c(c)->get_smt_kernel().get_relevant_labeled_literals(mk_c(c)->fparams().m_at_labels_cex, lits); labels* lbls = alloc(labels); SASSERT(labl_syms.size() == lits.size()); for (unsigned i = 0; i < lits.size(); ++i) { @@ -212,12 +212,12 @@ extern "C" { RESET_ERROR_CODE(); ast_manager& m = mk_c(c)->m(); expr_ref_vector lits(m); - mk_c(c)->get_smt_kernel().get_relevant_literals(lits); + mk_c(c)->get_smt_kernel().get_relevant_literals(lits); labels* lbls = alloc(labels); for (unsigned i = 0; i < lits.size(); ++i) { lbls->push_back(labeled_literal(m,lits[i].get())); } - RETURN_Z3(reinterpret_cast(lbls)); + RETURN_Z3(reinterpret_cast(lbls)); Z3_CATCH_RETURN(0); } @@ -227,12 +227,12 @@ extern "C" { RESET_ERROR_CODE(); ast_manager& m = mk_c(c)->m(); expr_ref_vector lits(m); - mk_c(c)->get_smt_kernel().get_guessed_literals(lits); + mk_c(c)->get_smt_kernel().get_guessed_literals(lits); labels* lbls = alloc(labels); for (unsigned i = 0; i < lits.size(); ++i) { lbls->push_back(labeled_literal(m,lits[i].get())); } - RETURN_Z3(reinterpret_cast(lbls)); + RETURN_Z3(reinterpret_cast(lbls)); Z3_CATCH_RETURN(0); } @@ -248,7 +248,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_num_literals(c, lbls); RESET_ERROR_CODE(); - return reinterpret_cast(lbls)->size(); + return reinterpret_cast(lbls)->size(); Z3_CATCH_RETURN(0); } @@ -256,7 +256,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_label_symbol(c, lbls, idx); RESET_ERROR_CODE(); - return of_symbol((*reinterpret_cast(lbls))[idx].get_label()); + return of_symbol((*reinterpret_cast(lbls))[idx].get_label()); Z3_CATCH_RETURN(0); } @@ -274,7 +274,7 @@ extern "C" { Z3_TRY; LOG_Z3_disable_literal(c, lbls, idx); RESET_ERROR_CODE(); - (*reinterpret_cast(lbls))[idx].disable(); + (*reinterpret_cast(lbls))[idx].disable(); Z3_CATCH; } @@ -348,4 +348,4 @@ void Z3_display_statistics(Z3_context c, std::ostream& s) { void Z3_display_istatistics(Z3_context c, std::ostream& s) { mk_c(c)->get_smt_kernel().display_istatistics(s); } - + From 15c48eeaf9352a73515e0b6badf042879a6f19dc Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 13 Nov 2015 16:42:46 +0000 Subject: [PATCH 8/9] Fix for timeout/rlimit in deprecated solver API. Partially fixes #307. --- src/api/api_solver_old.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/api/api_solver_old.cpp b/src/api/api_solver_old.cpp index 7fa469718..fbd57ad97 100644 --- a/src/api/api_solver_old.cpp +++ b/src/api/api_solver_old.cpp @@ -23,6 +23,8 @@ Revision History: #include"api_context.h" #include"api_model.h" #include"cancel_eh.h" +#include"scoped_timer.h" +#include"rlimit.h" extern "C" { @@ -75,8 +77,13 @@ extern "C" { cancel_eh eh(mk_c(c)->get_smt_kernel()); api::context::set_interruptable si(*(mk_c(c)), eh); flet _model(mk_c(c)->fparams().m_model, true); + unsigned timeout = mk_c(c)->params().m_timeout; + unsigned rlimit = mk_c(c)->params().m_rlimit; lbool result; try { + scoped_timer timer(timeout, &eh); + scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); + model_ref _m; result = mk_c(c)->check(_m); if (m) { From 27dcd8c5b6bd6fdb9c2b1acd724346618bac2113 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 13 Nov 2015 17:15:04 +0000 Subject: [PATCH 9/9] Fix for python decoding of command line output strings Fixes #302 --- scripts/mk_util.py | 2 +- scripts/update_api.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 0baed2968..225a38c04 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -90,7 +90,7 @@ FPMATH="Default" FPMATH_FLAGS="-mfpmath=sse -msse -msse2" def check_output(cmd): - return (subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]).decode("utf-8").rstrip('\r\n') + return (subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]).decode(sys.stdout.encoding).rstrip('\r\n') def git_hash(): try: diff --git a/scripts/update_api.py b/scripts/update_api.py index 0b6ddfb32..1ad85d228 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -96,7 +96,7 @@ if sys.version < '3': return s else: def _to_pystr(s): - return s.decode('utf-8') + return s.decode(sys.stdout.encoding) def init(PATH): global _lib