From 8ca023d541b3a80fc1fcd8384dcb3ed9f71990fe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 17 Dec 2021 16:12:47 -0800 Subject: [PATCH] expose propagate created --- src/api/api_solver.cpp | 19 +++++++++++++++++++ src/api/z3_api.h | 15 +++++++++++++++ src/ast/ast.h | 2 +- src/ast/recfun_decl_plugin.h | 2 +- src/ast/rewriter/maximize_ac_sharing.h | 2 +- src/smt/params/preprocessor_params.cpp | 4 ++-- src/smt/params/preprocessor_params.h | 6 +++--- src/smt/smt_setup.cpp | 8 ++++---- src/solver/assertions/asserted_formulas.cpp | 14 +++++++------- src/solver/assertions/asserted_formulas.h | 6 +++--- src/util/zstring.cpp | 8 ++++---- src/util/zstring.h | 14 +++++++------- 12 files changed, 67 insertions(+), 33 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index ea009b1bc..bb5ab9752 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -964,4 +964,23 @@ extern "C" { Z3_CATCH; } + void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh) { + Z3_TRY; + RESET_ERROR_CODE(); + user_propagator::register_created_eh_t c = (void(*)(void*, user_propagator::callback*, expr*, unsigned))created_eh; + to_solver_ref(s)->user_propagate_register_created(c); + Z3_CATCH; + } + + Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_solver s, Z3_symbol name, unsigned n, Z3_sort* domain, Z3_sort range) { + Z3_TRY; + LOG_Z3_solver_propagate_declare(c, s, name, n, domain, range); + RESET_ERROR_CODE(); + func_decl* f = to_solver_ref(s)->user_propagate_declare(to_symbol(name), n, to_sorts(domain), to_sort(range)); + mk_c(c)->save_ast_trail(f); + RETURN_Z3(of_func_decl(f)); + Z3_CATCH_RETURN(nullptr); + } + + }; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 767eebc43..899a5e7d1 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1430,6 +1430,7 @@ typedef void* Z3_fresh_eh(void* ctx, Z3_context new_context); typedef void Z3_fixed_eh(void* ctx, Z3_solver_callback cb, unsigned id, Z3_ast value); typedef void Z3_eq_eh(void* ctx, Z3_solver_callback cb, unsigned x, unsigned y); typedef void Z3_final_eh(void* ctx, Z3_solver_callback cb); +typedef void Z3_created_eh(void* ctx, Z3_solver_callback cb, Z3_ast e, unsigned id); /** @@ -6676,6 +6677,20 @@ extern "C" { */ void Z3_API Z3_solver_propagate_diseq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh); + /** + * \brief register a callback when a new expression with a registered function is used by the solver + * The registered function appears at the top level and is created using \c Z3_solver_declare. + */ + void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh); + + /** + \brief Create a registered function. Expressions used by the solver \c s that uses the registered function + at top level cause the callback propagate_created to be invoked. + + def_API('Z3_solver_propagate_declare', FUNC_DECL, (_in(CONTEXT), _in(SOLVER), _in(SYMBOL), _in(UINT), _in_array(3, SORT), _in(SORT))) + */ + Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_solver s, Z3_symbol name, unsigned n, Z3_sort* domain, Z3_sort range); + /** \brief register an expression to propagate on with the solver. Only expressions of type Bool and type Bit-Vector can be registered for propagation. diff --git a/src/ast/ast.h b/src/ast/ast.h index b04e67003..13898c2a6 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -845,7 +845,7 @@ class quantifier : public expr { char m_patterns_decls[0]; static unsigned get_obj_size(unsigned num_decls, unsigned num_patterns, unsigned num_no_patterns) { - return sizeof(quantifier) + num_decls * (sizeof(sort *) + sizeof(symbol)) + (num_patterns + num_no_patterns) * sizeof(expr*); + return (unsigned)(sizeof(quantifier) + num_decls * (sizeof(sort *) + sizeof(symbol)) + (num_patterns + num_no_patterns) * sizeof(expr*)); } quantifier(quantifier_kind k, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body, sort* s, diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index 1146b7aaf..dd07e8baf 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -305,7 +305,7 @@ namespace recfun { m_pred(pred), m_cdef(&d), m_args(args) {} body_expansion(body_expansion const & from): m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(from.m_args) {} - body_expansion(body_expansion && from) : + body_expansion(body_expansion && from) noexcept : m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(std::move(from.m_args)) {} std::ostream& display(std::ostream& out) const; diff --git a/src/ast/rewriter/maximize_ac_sharing.h b/src/ast/rewriter/maximize_ac_sharing.h index 53e102b74..a2741aa89 100644 --- a/src/ast/rewriter/maximize_ac_sharing.h +++ b/src/ast/rewriter/maximize_ac_sharing.h @@ -46,7 +46,7 @@ class maximize_ac_sharing : public default_rewriter_cfg { entry(func_decl * d = nullptr, expr * arg1 = nullptr, expr * arg2 = nullptr):m_decl(d), m_arg1(arg1), m_arg2(arg2) { SASSERT((d == 0 && arg1 == 0 && arg2 == 0) || (d != 0 && arg1 != 0 && arg2 != 0)); - if (arg1->get_id() > arg2->get_id()) + if (arg1 && arg2 && arg1->get_id() > arg2->get_id()) std::swap(m_arg1, m_arg2); } diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp index a87d4959d..9fcb09843 100644 --- a/src/smt/params/preprocessor_params.cpp +++ b/src/smt/params/preprocessor_params.cpp @@ -40,8 +40,8 @@ void preprocessor_params::display(std::ostream & out) const { pattern_inference_params::display(out); bit_blaster_params::display(out); - DISPLAY_PARAM(m_lift_ite); - DISPLAY_PARAM(m_ng_lift_ite); + DISPLAY_PARAM((int)m_lift_ite); + DISPLAY_PARAM((int)m_ng_lift_ite); DISPLAY_PARAM(m_pull_cheap_ite); DISPLAY_PARAM(m_pull_nested_quantifiers); DISPLAY_PARAM(m_eliminate_term_ite); diff --git a/src/smt/params/preprocessor_params.h b/src/smt/params/preprocessor_params.h index a0d56182a..53568c366 100644 --- a/src/smt/params/preprocessor_params.h +++ b/src/smt/params/preprocessor_params.h @@ -21,7 +21,7 @@ Revision History: #include "params/pattern_inference_params.h" #include "params/bit_blaster_params.h" -enum lift_ite_kind { +enum class lift_ite_kind { LI_NONE, LI_CONSERVATIVE, LI_FULL @@ -50,8 +50,8 @@ struct preprocessor_params : public pattern_inference_params, public: preprocessor_params(params_ref const & p = params_ref()): - m_lift_ite(LI_NONE), - m_ng_lift_ite(LI_NONE), + m_lift_ite(lift_ite_kind::LI_NONE), + m_ng_lift_ite(lift_ite_kind::LI_NONE), m_pull_cheap_ite(false), m_pull_nested_quantifiers(false), m_eliminate_term_ite(false), diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index ba601272d..2d131c6ab 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -643,8 +643,8 @@ namespace smt { // It destroys the existing patterns. // m_params.m_macro_finder = true; - if (m_params.m_ng_lift_ite == LI_NONE) - m_params.m_ng_lift_ite = LI_CONSERVATIVE; + if (m_params.m_ng_lift_ite == lift_ite_kind::LI_NONE) + m_params.m_ng_lift_ite = lift_ite_kind::LI_CONSERVATIVE; TRACE("setup", tout << "max_eager_multipatterns: " << m_params.m_qi_max_eager_multipatterns << "\n";); m_context.register_plugin(alloc(smt::theory_i_arith, m_context)); setup_arrays(); @@ -668,8 +668,8 @@ namespace smt { m_params.m_qi_lazy_threshold = 20; // m_params.m_macro_finder = true; - if (m_params.m_ng_lift_ite == LI_NONE) - m_params.m_ng_lift_ite = LI_CONSERVATIVE; + if (m_params.m_ng_lift_ite == lift_ite_kind::LI_NONE) + m_params.m_ng_lift_ite = lift_ite_kind::LI_CONSERVATIVE; m_params.m_pi_max_multi_patterns = 10; //<< it was used for SMT-COMP m_params.m_array_lazy_ieq = true; m_params.m_array_lazy_ieq_delay = 4; diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp index b3be7e8ab..1b8bfe9dd 100644 --- a/src/solver/assertions/asserted_formulas.cpp +++ b/src/solver/assertions/asserted_formulas.cpp @@ -71,12 +71,12 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & sp, params_re void asserted_formulas::setup() { switch (m_smt_params.m_lift_ite) { - case LI_FULL: - m_smt_params.m_ng_lift_ite = LI_NONE; + case lift_ite_kind::LI_FULL: + m_smt_params.m_ng_lift_ite = lift_ite_kind::LI_NONE; break; - case LI_CONSERVATIVE: - if (m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE) - m_smt_params.m_ng_lift_ite = LI_NONE; + case lift_ite_kind::LI_CONSERVATIVE: + if (m_smt_params.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE) + m_smt_params.m_ng_lift_ite = lift_ite_kind::LI_NONE; break; default: break; @@ -281,8 +281,8 @@ void asserted_formulas::reduce() { if (!invoke(m_reduce_asserted_formulas)) return; if (!invoke(m_pull_nested_quantifiers)) return; if (!invoke(m_lift_ite)) return; - m_lift_ite.m_functor.set_conservative(m_smt_params.m_lift_ite == LI_CONSERVATIVE); - m_ng_lift_ite.m_functor.set_conservative(m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE); + m_lift_ite.m_functor.set_conservative(m_smt_params.m_lift_ite == lift_ite_kind::LI_CONSERVATIVE); + m_ng_lift_ite.m_functor.set_conservative(m_smt_params.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE); if (!invoke(m_ng_lift_ite)) return; if (!invoke(m_elim_term_ite)) return; if (!invoke(m_refine_inj_axiom)) return; diff --git a/src/solver/assertions/asserted_formulas.h b/src/solver/assertions/asserted_formulas.h index 95848133c..23a4f5a0a 100644 --- a/src/solver/assertions/asserted_formulas.h +++ b/src/solver/assertions/asserted_formulas.h @@ -154,7 +154,7 @@ class asserted_formulas { public: elim_term_ite_fn(asserted_formulas& af): simplify_fmls(af, "elim-term-ite"), m_elim(af.m, af.m_defined_names) {} void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_elim(j.get_fml(), n, p); } - bool should_apply() const override { return af.m_smt_params.m_eliminate_term_ite && af.m_smt_params.m_lift_ite != LI_FULL; } + bool should_apply() const override { return af.m_smt_params.m_eliminate_term_ite && af.m_smt_params.m_lift_ite != lift_ite_kind::LI_FULL; } void post_op() override { af.m_formulas.append(m_elim.new_defs()); af.reduce_and_solve(); m_elim.reset(); } void push() { m_elim.push(); } void pop(unsigned n) { m_elim.pop(n); } @@ -187,8 +187,8 @@ class asserted_formulas { MK_SIMPLIFIERF(cheap_quant_fourier_motzkin, elim_bounds_rw, "cheap-fourier-motzkin", af.m_smt_params.m_eliminate_bounds && af.has_quantifiers(), true); MK_SIMPLIFIERF(elim_bvs_from_quantifiers, bv_elim_rw, "eliminate-bit-vectors-from-quantifiers", af.m_smt_params.m_bb_quantifiers, true); MK_SIMPLIFIERF(apply_bit2int, bit2int, "propagate-bit-vector-over-integers", af.m_smt_params.m_simplify_bit2int, true); - MK_SIMPLIFIERF(lift_ite, push_app_ite_rw, "lift-ite", af.m_smt_params.m_lift_ite != LI_NONE, true); - MK_SIMPLIFIERF(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_smt_params.m_ng_lift_ite != LI_NONE, true); + MK_SIMPLIFIERF(lift_ite, push_app_ite_rw, "lift-ite", af.m_smt_params.m_lift_ite != lift_ite_kind::LI_NONE, true); + MK_SIMPLIFIERF(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_smt_params.m_ng_lift_ite != lift_ite_kind::LI_NONE, true); reduce_asserted_formulas_fn m_reduce_asserted_formulas; diff --git a/src/util/zstring.cpp b/src/util/zstring.cpp index 534999606..e73c4cd52 100644 --- a/src/util/zstring.cpp +++ b/src/util/zstring.cpp @@ -87,12 +87,12 @@ zstring::zstring(char const* s) { string_encoding zstring::get_encoding() { if (gparams::get_value("encoding") == "unicode") - return unicode; + return string_encoding::unicode; if (gparams::get_value("encoding") == "bmp") - return bmp; + return string_encoding::bmp; if (gparams::get_value("encoding") == "ascii") - return ascii; - return unicode; + return string_encoding::ascii; + return string_encoding::unicode; } bool zstring::well_formed() const { diff --git a/src/util/zstring.h b/src/util/zstring.h index c5606b267..cb462238a 100644 --- a/src/util/zstring.h +++ b/src/util/zstring.h @@ -21,7 +21,7 @@ Author: #include "util/buffer.h" #include "util/rational.h" -enum string_encoding { +enum class string_encoding { ascii, // exactly 8 bits unicode, bmp // basic multilingual plane; exactly 16 bits @@ -41,22 +41,22 @@ public: static unsigned ascii_num_bits() { return 8; } static unsigned max_char() { switch (get_encoding()) { - case unicode: + case string_encoding::unicode: return unicode_max_char(); - case bmp: + case string_encoding::bmp: return bmp_max_char(); - case ascii: + case string_encoding::ascii: return ascii_max_char(); } return unicode_max_char(); } static unsigned num_bits() { switch (get_encoding()) { - case unicode: + case string_encoding::unicode: return unicode_num_bits(); - case bmp: + case string_encoding::bmp: return bmp_num_bits(); - case ascii: + case string_encoding::ascii: return ascii_num_bits(); } return unicode_num_bits();