From e1ffaa7faf1cdcde8e5a42769c5205121fc09e65 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 17 Dec 2021 11:34:54 -0800 Subject: [PATCH 01/12] na Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 12b5449eb..13d8ef4fb 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -3368,9 +3368,8 @@ expr_ref seq_rewriter::mk_regex_inter_normalize(expr* r1, expr* r2) { result = r2; else if (re().is_dot_plus(r2) && re().get_info(r1).min_length > 0) result = r1; - else { - result = merge_regex_sets(r1, r2, re().mk_empty(r1->get_sort()), test, compose); - } + else + result = merge_regex_sets(r1, r2, re().mk_empty(r1->get_sort()), test, compose); return result; } @@ -3380,7 +3379,6 @@ expr_ref seq_rewriter::merge_regex_sets(expr* r1, expr* r2, expr* unit, sort* seq_sort; expr_ref result(unit, m()); expr_ref_vector prefix(m()); - expr* a, * ar1, * b, * br1; VERIFY(m_util.is_re(r1, seq_sort)); SASSERT(m_util.is_re(r2)); SASSERT(r2->get_sort() == r1->get_sort()); @@ -3414,6 +3412,7 @@ expr_ref seq_rewriter::merge_regex_sets(expr* r1, expr* r2, expr* unit, if (are_complements(ar, br)) return expr_ref(unit, m()); + expr* a, * ar1, * b, * br1; if (test(br, b, br1) && !test(ar, a, ar1)) std::swap(ar, br); From 8ca023d541b3a80fc1fcd8384dcb3ed9f71990fe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 17 Dec 2021 16:12:47 -0800 Subject: [PATCH 02/12] 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(); From 4856581b68d63929d8913240c9ce25360c0fba8f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 17 Dec 2021 16:40:19 -0800 Subject: [PATCH 03/12] na --- src/api/api_solver.cpp | 2 +- src/ast/recfun_decl_plugin.h | 2 +- src/cmd_context/pdecl.cpp | 24 ++++++++++++------------ src/cmd_context/pdecl.h | 16 ++++++++-------- src/smt/smt_context.h | 2 +- src/smt/smt_kernel.cpp | 4 ++-- src/smt/smt_kernel.h | 2 +- src/smt/smt_solver.cpp | 3 +-- src/smt/tactic/smt_tactic_core.cpp | 6 +++--- src/smt/theory_user_propagator.h | 6 +++--- src/tactic/tactical.cpp | 2 +- src/tactic/user_propagator_base.h | 4 ++-- 12 files changed, 36 insertions(+), 37 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index bb5ab9752..222fe7061 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -967,7 +967,7 @@ extern "C" { 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; + user_propagator::created_eh_t c = (void(*)(void*, user_propagator::callback*, expr*, unsigned))created_eh; to_solver_ref(s)->user_propagate_register_created(c); Z3_CATCH; } diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index dd07e8baf..70447ff67 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) noexcept : + 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/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index e34c7e38a..7a93382e9 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -416,9 +416,9 @@ void psort_builtin_decl::display(std::ostream & out) const { void ptype::display(std::ostream & out, pdatatype_decl const * const * dts) const { switch (kind()) { - case PTR_PSORT: get_psort()->display(out); break; - case PTR_REC_REF: out << dts[get_idx()]->get_name(); break; - case PTR_MISSING_REF: out << get_missing_ref(); break; + case ptype_kind::PTR_PSORT: get_psort()->display(out); break; + case ptype_kind::PTR_REC_REF: out << dts[get_idx()]->get_name(); break; + case ptype_kind::PTR_MISSING_REF: out << get_missing_ref(); break; } } @@ -426,19 +426,19 @@ paccessor_decl::paccessor_decl(unsigned id, unsigned num_params, pdecl_manager & pdecl(id, num_params), m_name(n), m_type(r) { - if (m_type.kind() == PTR_PSORT) { + if (m_type.kind() == ptype_kind::PTR_PSORT) { m.inc_ref(r.get_psort()); } } void paccessor_decl::finalize(pdecl_manager & m) { - if (m_type.kind() == PTR_PSORT) { + if (m_type.kind() == ptype_kind::PTR_PSORT) { m.lazy_dec_ref(m_type.get_psort()); } } bool paccessor_decl::has_missing_refs(symbol & missing) const { - if (m_type.kind() == PTR_MISSING_REF) { + if (m_type.kind() == ptype_kind::PTR_MISSING_REF) { missing = m_type.get_missing_ref(); return true; } @@ -446,14 +446,14 @@ bool paccessor_decl::has_missing_refs(symbol & missing) const { } bool paccessor_decl::fix_missing_refs(dictionary const & symbol2idx, symbol & missing) { - TRACE("fix_missing_refs", tout << "m_type.kind(): " << m_type.kind() << "\n"; - if (m_type.kind() == PTR_MISSING_REF) tout << m_type.get_missing_ref() << "\n";); - if (m_type.kind() != PTR_MISSING_REF) + TRACE("fix_missing_refs", tout << "m_type.kind(): " << (int)m_type.kind() << "\n"; + if (m_type.kind() == ptype_kind::PTR_MISSING_REF) tout << m_type.get_missing_ref() << "\n";); + if (m_type.kind() != ptype_kind::PTR_MISSING_REF) return true; int idx; if (symbol2idx.find(m_type.get_missing_ref(), idx)) { m_type = ptype(idx); - SASSERT(m_type.kind() == PTR_REC_REF); + SASSERT(m_type.kind() == ptype_kind::PTR_REC_REF); return true; } missing = m_type.get_missing_ref(); @@ -462,8 +462,8 @@ bool paccessor_decl::fix_missing_refs(dictionary const & symbol2idx, symbol accessor_decl * paccessor_decl::instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s) { switch (m_type.kind()) { - case PTR_REC_REF: return mk_accessor_decl(m.m(), m_name, type_ref(m_type.get_idx())); - case PTR_PSORT: return mk_accessor_decl(m.m(), m_name, type_ref(m_type.get_psort()->instantiate(m, n, s))); + case ptype_kind::PTR_REC_REF: return mk_accessor_decl(m.m(), m_name, type_ref(m_type.get_idx())); + case ptype_kind::PTR_PSORT: return mk_accessor_decl(m.m(), m_name, type_ref(m_type.get_psort()->instantiate(m, n, s))); default: // missing refs must have been eliminated. UNREACHABLE(); diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h index e5b630902..3a1db06c1 100644 --- a/src/cmd_context/pdecl.h +++ b/src/cmd_context/pdecl.h @@ -157,7 +157,7 @@ class pdatatype_decl; class pconstructor_decl; class paccessor_decl; -enum ptype_kind { +enum class ptype_kind { PTR_PSORT, // psort PTR_REC_REF, // recursive reference PTR_MISSING_REF // a symbol, it is useful for building parsers. @@ -171,14 +171,14 @@ class ptype { }; symbol m_missing_ref; public: - ptype():m_kind(PTR_PSORT), m_sort(nullptr) {} - ptype(int idx):m_kind(PTR_REC_REF), m_idx(idx) {} - ptype(psort * s):m_kind(PTR_PSORT), m_sort(s) {} - ptype(symbol const & s):m_kind(PTR_MISSING_REF), m_missing_ref(s) {} + ptype():m_kind(ptype_kind::PTR_PSORT), m_sort(nullptr) {} + ptype(int idx):m_kind(ptype_kind::PTR_REC_REF), m_idx(idx) {} + ptype(psort * s):m_kind(ptype_kind::PTR_PSORT), m_sort(s) {} + ptype(symbol const & s):m_kind(ptype_kind::PTR_MISSING_REF), m_sort(nullptr), m_missing_ref(s) {} ptype_kind kind() const { return m_kind; } - psort * get_psort() const { SASSERT(kind() == PTR_PSORT); return m_sort; } - int get_idx() const { SASSERT(kind() == PTR_REC_REF); return m_idx; } - symbol const & get_missing_ref() const { SASSERT(kind() == PTR_MISSING_REF); return m_missing_ref; } + psort * get_psort() const { SASSERT(kind() == ptype_kind::PTR_PSORT); return m_sort; } + int get_idx() const { SASSERT(kind() == ptype_kind::PTR_REC_REF); return m_idx; } + symbol const & get_missing_ref() const { SASSERT(kind() == ptype_kind::PTR_MISSING_REF); return m_missing_ref; } void display(std::ostream & out, pdatatype_decl const * const * dts) const; }; diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index ba8005484..85f59d26c 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1729,7 +1729,7 @@ namespace smt { return m_user_propagator->add_expr(e); } - void user_propagate_register_created(user_propagator::register_created_eh_t& r) { + void user_propagate_register_created(user_propagator::created_eh_t& r) { if (!m_user_propagator) throw default_exception("user propagator must be initialized"); m_user_propagator->register_created(r); diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index 13f7da7dc..b26823291 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -249,7 +249,7 @@ namespace smt { return m_kernel.user_propagate_register(e); } - void user_propagate_register_created(user_propagator::register_created_eh_t& r) { + void user_propagate_register_created(user_propagator::created_eh_t& r) { m_kernel.user_propagate_register_created(r); } @@ -484,7 +484,7 @@ namespace smt { return m_imp->user_propagate_register(e); } - void kernel::user_propagate_register_created(user_propagator::register_created_eh_t& r) { + void kernel::user_propagate_register_created(user_propagator::created_eh_t& r) { m_imp->user_propagate_register_created(r); } diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index e8fdbc648..0296c29a6 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -303,7 +303,7 @@ namespace smt { unsigned user_propagate_register(expr* e); - void user_propagate_register_created(user_propagator::register_created_eh_t& r); + void user_propagate_register_created(user_propagator::created_eh_t& r); func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index a755fe5ae..fe4aec944 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -200,7 +200,6 @@ namespace { return m_context.check(num_assumptions, assumptions); } - lbool check_sat_cc_core(expr_ref_vector const& cube, vector const& clauses) override { return m_context.check(cube, clauses); } @@ -241,7 +240,7 @@ namespace { return m_context.user_propagate_register(e); } - void user_propagate_register_created(user_propagator::register_created_eh_t& c) override { + void user_propagate_register_created(user_propagator::created_eh_t& c) override { m_context.user_propagate_register_created(c); } diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp index 93ce81976..d67e430e2 100644 --- a/src/smt/tactic/smt_tactic_core.cpp +++ b/src/smt/tactic/smt_tactic_core.cpp @@ -319,7 +319,7 @@ public: user_propagator::final_eh_t m_final_eh; user_propagator::eq_eh_t m_eq_eh; user_propagator::eq_eh_t m_diseq_eh; - user_propagator::register_created_eh_t m_created_eh; + user_propagator::created_eh_t m_created_eh; expr_ref_vector m_vars; unsigned_vector m_var2internal; @@ -333,7 +333,7 @@ public: user_propagator::final_eh_t i_final_eh; user_propagator::eq_eh_t i_eq_eh; user_propagator::eq_eh_t i_diseq_eh; - user_propagator::register_created_eh_t i_created_eh; + user_propagator::created_eh_t i_created_eh; struct callback : public user_propagator::callback { @@ -502,7 +502,7 @@ public: return m_ctx->user_propagate_declare(name, n, domain, range); } - void user_propagate_register_created(user_propagator::register_created_eh_t& created_eh) override { + void user_propagate_register_created(user_propagator::created_eh_t& created_eh) override { m_ctx->user_propagate_register_created(created_eh); } }; diff --git a/src/smt/theory_user_propagator.h b/src/smt/theory_user_propagator.h index a9b340d4a..0189b13cb 100644 --- a/src/smt/theory_user_propagator.h +++ b/src/smt/theory_user_propagator.h @@ -56,7 +56,7 @@ namespace smt { user_propagator::fixed_eh_t m_fixed_eh; user_propagator::eq_eh_t m_eq_eh; user_propagator::eq_eh_t m_diseq_eh; - user_propagator::register_created_eh_t m_created_eh; + user_propagator::created_eh_t m_created_eh; user_propagator::context_obj* m_api_context = nullptr; unsigned m_qhead = 0; @@ -96,7 +96,7 @@ namespace smt { void register_fixed(user_propagator::fixed_eh_t& fixed_eh) { m_fixed_eh = fixed_eh; } void register_eq(user_propagator::eq_eh_t& eq_eh) { m_eq_eh = eq_eh; } void register_diseq(user_propagator::eq_eh_t& diseq_eh) { m_diseq_eh = diseq_eh; } - void register_created(user_propagator::register_created_eh_t& created_eh) { m_created_eh = created_eh; } + void register_created(user_propagator::created_eh_t& created_eh) { m_created_eh = created_eh; } func_decl* declare(symbol const& name, unsigned n, sort* const* domain, sort* range); bool has_fixed() const { return (bool)m_fixed_eh; } @@ -123,7 +123,7 @@ namespace smt { void collect_statistics(::statistics & st) const override; model_value_proc * mk_value(enode * n, model_generator & mg) override { return nullptr; } void init_model(model_generator & m) override {} - bool include_func_interp(func_decl* f) override { return false; } + bool include_func_interp(func_decl* f) override { return true; } bool can_propagate() override; void propagate() override; void display(std::ostream& out) const override {} diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 171a8314d..07fc88b37 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -200,7 +200,7 @@ public: m_t2->user_propagate_clear(); } - void user_propagate_register_created(user_propagator::register_created_eh_t& created_eh) override { + void user_propagate_register_created(user_propagator::created_eh_t& created_eh) override { m_t2->user_propagate_register_created(created_eh); } diff --git a/src/tactic/user_propagator_base.h b/src/tactic/user_propagator_base.h index e5a2d282f..db9ca88fd 100644 --- a/src/tactic/user_propagator_base.h +++ b/src/tactic/user_propagator_base.h @@ -23,7 +23,7 @@ namespace user_propagator { typedef std::function fresh_eh_t; typedef std::function push_eh_t; typedef std::function pop_eh_t; - typedef std::function register_created_eh_t; + typedef std::function created_eh_t; class plugin : public decl_plugin { @@ -95,7 +95,7 @@ namespace user_propagator { throw default_exception("user-propagators are only supported on the SMT solver"); } - virtual void user_propagate_register_created(register_created_eh_t& r) { + virtual void user_propagate_register_created(created_eh_t& r) { throw default_exception("user-propagators are only supported on the SMT solver"); } From f0740bdf607520ae1d687e45534421e7a7a5ce1e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 18 Dec 2021 10:56:42 -0800 Subject: [PATCH 04/12] move user propagte declare to context level declaration of user propagate functions are declared at context level instead of at solver scope. --- src/api/api_solver.cpp | 13 +- src/api/z3_api.h | 14 +- src/sat/sat_solver/inc_sat_solver.cpp | 4 +- src/sat/smt/euf_solver.h | 2 +- src/smt/smt_context.h | 8 +- src/smt/smt_kernel.cpp | 302 ++++-------------------- src/smt/smt_kernel.h | 4 +- src/smt/smt_solver.cpp | 8 +- src/smt/tactic/smt_tactic_core.cpp | 8 +- src/smt/theory_user_propagator.cpp | 12 +- src/smt/theory_user_propagator.h | 1 - src/solver/tactic2solver.cpp | 4 +- src/tactic/core/elim_uncnstr_tactic.cpp | 2 +- src/tactic/core/reduce_args_tactic.cpp | 4 +- src/tactic/tactic.h | 2 +- src/tactic/tactical.cpp | 12 +- src/tactic/user_propagator_base.h | 16 +- 17 files changed, 92 insertions(+), 324 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 222fe7061..8e8360cd3 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -944,7 +944,7 @@ extern "C" { Z3_TRY; LOG_Z3_solver_propagate_register(c, s, e); RESET_ERROR_CODE(); - return to_solver_ref(s)->user_propagate_register(to_expr(e)); + return to_solver_ref(s)->user_propagate_register_expr(to_expr(e)); Z3_CATCH_RETURN(0); } @@ -972,11 +972,16 @@ extern "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_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_symbol name, unsigned n, Z3_sort* domain, Z3_sort range) { Z3_TRY; - LOG_Z3_solver_propagate_declare(c, s, name, n, domain, range); + LOG_Z3_solver_propagate_declare(c, 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)); + ast_manager& m = mk_c(c)->m(); + family_id fid = m.mk_family_id(user_propagator::plugin::name()); + if (!m.has_plugin(fid)) + m.register_plugin(fid, alloc(user_propagator::plugin)); + func_decl_info info(fid, user_propagator::plugin::kind_t::OP_USER_PROPAGATE); + func_decl* f = m.mk_func_decl(to_symbol(name), n, to_sorts(domain), to_sort(range), info); 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 899a5e7d1..0ac70ee98 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6679,17 +6679,21 @@ extern "C" { /** * \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. + * The registered function appears at the top level and is created using \ref Z3_propagate_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. + Create uninterpreted function declaration for the user propagator. + When expressions using the function are created by the solver invoke a callback + to \ref \Z3_solver_progate_created with arguments + 1. context and callback solve + 2. declared_expr: expression using function that was used as the top-level symbol + 3. declared_id: a unique identifier (unique within the current scope) to track the expression. - def_API('Z3_solver_propagate_declare', FUNC_DECL, (_in(CONTEXT), _in(SOLVER), _in(SYMBOL), _in(UINT), _in_array(3, SORT), _in(SORT))) + def_API('Z3_solver_propagate_declare', FUNC_DECL, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, 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); + Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_symbol name, unsigned n, Z3_sort* domain, Z3_sort range); /** \brief register an expression to propagate on with the solver. diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index ea81f0c4d..97a319382 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -683,8 +683,8 @@ public: ensure_euf()->user_propagate_register_diseq(diseq_eh); } - unsigned user_propagate_register(expr* e) override { - return ensure_euf()->user_propagate_register(e); + unsigned user_propagate_register_expr(expr* e) override { + return ensure_euf()->user_propagate_register_expr(e); } private: diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index d70206d11..384e15822 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -425,7 +425,7 @@ namespace euf { check_for_user_propagator(); m_user_propagator->register_diseq(diseq_eh); } - unsigned user_propagate_register(expr* e) { + unsigned user_propagate_register_expr(expr* e) { check_for_user_propagator(); return m_user_propagator->add_expr(e); } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 85f59d26c..4a764e975 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1723,7 +1723,7 @@ namespace smt { m_user_propagator->register_diseq(diseq_eh); } - unsigned user_propagate_register(expr* e) { + unsigned user_propagate_register_expr(expr* e) { if (!m_user_propagator) throw default_exception("user propagator must be initialized"); return m_user_propagator->add_expr(e); @@ -1735,12 +1735,6 @@ namespace smt { m_user_propagator->register_created(r); } - func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { - if (!m_user_propagator) - throw default_exception("user propagator must be initialized"); - return m_user_propagator->declare(name, n, domain, range); - } - bool watches_fixed(enode* n) const; void assign_fixed(enode* n, expr* val, unsigned sz, literal const* explain); diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index b26823291..fdfbbb97a 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -49,14 +49,6 @@ namespace smt { return m_kernel.get_manager(); } - bool set_logic(symbol logic) { - return m_kernel.set_logic(logic); - } - - void set_progress_callback(progress_callback * callback) { - return m_kernel.set_progress_callback(callback); - } - void display(std::ostream & out) const { // m_kernel.display(out); <<< for external users it is just junk // TODO: it will be replaced with assertion_stack.display @@ -67,195 +59,7 @@ namespace smt { out << "\n " << mk_ismt2_pp(f, m(), 2); } out << ")"; - } - - void assert_expr(expr * e) { - TRACE("smt_kernel", tout << "assert:\n" << mk_ismt2_pp(e, m()) << "\n";); - m_kernel.assert_expr(e); - } - - void assert_expr(expr * e, proof * pr) { - m_kernel.assert_expr(e, pr); - } - - unsigned size() const { - return m_kernel.get_num_asserted_formulas(); - } - - void get_formulas(ptr_vector& fmls) const { - m_kernel.get_asserted_formulas(fmls); - } - - expr* get_formula(unsigned i) const { - return m_kernel.get_asserted_formula(i); - } - - void push() { - TRACE("smt_kernel", tout << "push()\n";); - m_kernel.push(); - } - - void pop(unsigned num_scopes) { - TRACE("smt_kernel", tout << "pop()\n";); - m_kernel.pop(num_scopes); - } - - unsigned get_scope_level() const { - return m_kernel.get_scope_level(); - } - - lbool setup_and_check() { - return m_kernel.setup_and_check(); - } - - bool inconsistent() { - return m_kernel.inconsistent(); - } - - lbool check(unsigned num_assumptions, expr * const * assumptions) { - return m_kernel.check(num_assumptions, assumptions); - } - - lbool check(expr_ref_vector const& cube, vector const& clause) { - return m_kernel.check(cube, clause); - } - - lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed) { - return m_kernel.get_consequences(assumptions, vars, conseq, unfixed); - } - - lbool preferred_sat(expr_ref_vector const& asms, vector& cores) { - return m_kernel.preferred_sat(asms, cores); - } - - lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { - return m_kernel.find_mutexes(vars, mutexes); - } - - void get_model(model_ref & m) { - m_kernel.get_model(m); - } - - proof * get_proof() { - return m_kernel.get_proof(); - } - - unsigned get_unsat_core_size() const { - return m_kernel.get_unsat_core_size(); - } - - expr * get_unsat_core_expr(unsigned idx) const { - return m_kernel.get_unsat_core_expr(idx); - } - - void get_levels(ptr_vector const& vars, unsigned_vector& depth) { - m_kernel.get_levels(vars, depth); - } - - expr_ref_vector get_trail() { - return m_kernel.get_trail(); - } - - failure last_failure() const { - return m_kernel.get_last_search_failure(); - } - - std::string last_failure_as_string() const { - return m_kernel.last_failure_as_string(); - } - - void set_reason_unknown(char const* msg) { - m_kernel.set_reason_unknown(msg); - } - - void get_assignments(expr_ref_vector & result) { - m_kernel.get_assignments(result); - } - - void get_relevant_labels(expr * cnstr, buffer & result) { - m_kernel.get_relevant_labels(cnstr, result); - } - - void get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) { - m_kernel.get_relevant_labeled_literals(at_lbls, result); - } - - void get_relevant_literals(expr_ref_vector & result) { - m_kernel.get_relevant_literals(result); - } - - void get_guessed_literals(expr_ref_vector & result) { - m_kernel.get_guessed_literals(result); - } - - expr_ref next_cube() { - lookahead lh(m_kernel); - return lh.choose(); - } - - expr_ref_vector cubes(unsigned depth) { - lookahead lh(m_kernel); - return lh.choose_rec(depth); - } - - void collect_statistics(::statistics & st) const { - m_kernel.collect_statistics(st); - } - - void reset_statistics() { - } - - void display_statistics(std::ostream & out) const { - m_kernel.display_statistics(out); - } - - void display_istatistics(std::ostream & out) const { - m_kernel.display_istatistics(out); - } - - bool canceled() { - return m_kernel.get_cancel_flag(); - } - - void updt_params(params_ref const & p) { - m_kernel.updt_params(p); - } - - void user_propagate_init( - void* ctx, - user_propagator::push_eh_t& push_eh, - user_propagator::pop_eh_t& pop_eh, - user_propagator::fresh_eh_t& fresh_eh) { - m_kernel.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); - } - - void user_propagate_register_final(user_propagator::final_eh_t& final_eh) { - m_kernel.user_propagate_register_final(final_eh); - } - - void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) { - m_kernel.user_propagate_register_fixed(fixed_eh); - } - - void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) { - m_kernel.user_propagate_register_eq(eq_eh); - } - - void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) { - m_kernel.user_propagate_register_diseq(diseq_eh); - } - - unsigned user_propagate_register(expr* e) { - return m_kernel.user_propagate_register(e); - } - - void user_propagate_register_created(user_propagator::created_eh_t& r) { - m_kernel.user_propagate_register_created(r); - } - - func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { - return m_kernel.user_propagate_declare(name, n, domain, range); - } + } }; @@ -268,7 +72,7 @@ namespace smt { } ast_manager & kernel::m() const { - return m_imp->m(); + return m_imp->m_kernel.get_manager(); } void kernel::copy(kernel& src, kernel& dst) { @@ -276,45 +80,44 @@ namespace smt { } bool kernel::set_logic(symbol logic) { - return m_imp->set_logic(logic); + return m_imp->m_kernel.set_logic(logic); } void kernel::set_progress_callback(progress_callback * callback) { - m_imp->set_progress_callback(callback); + m_imp->m_kernel.set_progress_callback(callback); } void kernel::assert_expr(expr * e) { - m_imp->assert_expr(e); + m_imp->m_kernel.assert_expr(e); } void kernel::assert_expr(expr_ref_vector const& es) { - for (unsigned i = 0; i < es.size(); ++i) { - m_imp->assert_expr(es[i]); - } + for (unsigned i = 0; i < es.size(); ++i) + m_imp->m_kernel.assert_expr(es[i]); } void kernel::assert_expr(expr * e, proof * pr) { - m_imp->assert_expr(e, pr); + m_imp->m_kernel.assert_expr(e, pr); } unsigned kernel::size() const { - return m_imp->size(); + return m_imp->m_kernel.get_num_asserted_formulas(); } expr* kernel::get_formula(unsigned i) const { - return m_imp->get_formula(i); + return m_imp->m_kernel.get_asserted_formula(i); } void kernel::push() { - m_imp->push(); + m_imp->m_kernel.push(); } void kernel::pop(unsigned num_scopes) { - m_imp->pop(num_scopes); + m_imp->m_kernel.pop(num_scopes); } unsigned kernel::get_scope_level() const { - return m_imp->get_scope_level(); + return m_imp->m_kernel.get_scope_level(); } void kernel::reset() { @@ -326,89 +129,91 @@ namespace smt { } bool kernel::inconsistent() { - return m_imp->inconsistent(); + return m_imp->m_kernel.inconsistent(); } lbool kernel::setup_and_check() { - return m_imp->setup_and_check(); + return m_imp->m_kernel.setup_and_check(); } lbool kernel::check(unsigned num_assumptions, expr * const * assumptions) { - lbool r = m_imp->check(num_assumptions, assumptions); + lbool r = m_imp->m_kernel.check(num_assumptions, assumptions); TRACE("smt_kernel", tout << "check result: " << r << "\n";); return r; } lbool kernel::check(expr_ref_vector const& cube, vector const& clauses) { - return m_imp->check(cube, clauses); + return m_imp->m_kernel.check(cube, clauses); } lbool kernel::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed) { - return m_imp->get_consequences(assumptions, vars, conseq, unfixed); + return m_imp->m_kernel.get_consequences(assumptions, vars, conseq, unfixed); } lbool kernel::preferred_sat(expr_ref_vector const& asms, vector& cores) { - return m_imp->preferred_sat(asms, cores); + return m_imp->m_kernel.preferred_sat(asms, cores); } lbool kernel::find_mutexes(expr_ref_vector const& vars, vector& mutexes) { - return m_imp->find_mutexes(vars, mutexes); + return m_imp->m_kernel.find_mutexes(vars, mutexes); } void kernel::get_model(model_ref & m) { - m_imp->get_model(m); + m_imp->m_kernel.get_model(m); } proof * kernel::get_proof() { - return m_imp->get_proof(); + return m_imp->m_kernel.get_proof(); } unsigned kernel::get_unsat_core_size() const { - return m_imp->get_unsat_core_size(); + return m_imp->m_kernel.get_unsat_core_size(); } expr * kernel::get_unsat_core_expr(unsigned idx) const { - return m_imp->get_unsat_core_expr(idx); + return m_imp->m_kernel.get_unsat_core_expr(idx); } failure kernel::last_failure() const { - return m_imp->last_failure(); + return m_imp->m_kernel.get_last_search_failure(); } std::string kernel::last_failure_as_string() const { - return m_imp->last_failure_as_string(); + return m_imp->m_kernel.last_failure_as_string(); } void kernel::set_reason_unknown(char const* msg) { - m_imp->set_reason_unknown(msg); + m_imp->m_kernel.set_reason_unknown(msg); } void kernel::get_assignments(expr_ref_vector & result) { - m_imp->get_assignments(result); + m_imp->m_kernel.get_assignments(result); } void kernel::get_relevant_labels(expr * cnstr, buffer & result) { - m_imp->get_relevant_labels(cnstr, result); + m_imp->m_kernel.get_relevant_labels(cnstr, result); } void kernel::get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) { - m_imp->get_relevant_labeled_literals(at_lbls, result); + m_imp->m_kernel.get_relevant_labeled_literals(at_lbls, result); } void kernel::get_relevant_literals(expr_ref_vector & result) { - m_imp->get_relevant_literals(result); + m_imp->m_kernel.get_relevant_literals(result); } void kernel::get_guessed_literals(expr_ref_vector & result) { - m_imp->get_guessed_literals(result); + m_imp->m_kernel.get_guessed_literals(result); } expr_ref kernel::next_cube() { - return m_imp->next_cube(); + lookahead lh(m_imp->m_kernel); + return lh.choose(); } expr_ref_vector kernel::cubes(unsigned depth) { - return m_imp->cubes(depth); + lookahead lh(m_imp->m_kernel); + return lh.choose_rec(depth); } std::ostream& kernel::display(std::ostream & out) const { @@ -417,27 +222,26 @@ namespace smt { } void kernel::collect_statistics(::statistics & st) const { - m_imp->collect_statistics(st); + m_imp->m_kernel.collect_statistics(st); } void kernel::reset_statistics() { - m_imp->reset_statistics(); } void kernel::display_statistics(std::ostream & out) const { - m_imp->display_statistics(out); + m_imp->m_kernel.display_statistics(out); } void kernel::display_istatistics(std::ostream & out) const { - m_imp->display_istatistics(out); + m_imp->m_kernel.display_istatistics(out); } bool kernel::canceled() const { - return m_imp->canceled(); + return m_imp->m_kernel.get_cancel_flag(); } void kernel::updt_params(params_ref const & p) { - return m_imp->updt_params(p); + return m_imp->m_kernel.updt_params(p); } void kernel::collect_param_descrs(param_descrs & d) { @@ -449,11 +253,11 @@ namespace smt { } void kernel::get_levels(ptr_vector const& vars, unsigned_vector& depth) { - m_imp->get_levels(vars, depth); + m_imp->m_kernel.get_levels(vars, depth); } expr_ref_vector kernel::get_trail() { - return m_imp->get_trail(); + return m_imp->m_kernel.get_trail(); } void kernel::user_propagate_init( @@ -461,35 +265,31 @@ namespace smt { user_propagator::push_eh_t& push_eh, user_propagator::pop_eh_t& pop_eh, user_propagator::fresh_eh_t& fresh_eh) { - m_imp->user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); + m_imp->m_kernel.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); } void kernel::user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) { - m_imp->user_propagate_register_fixed(fixed_eh); + m_imp->m_kernel.user_propagate_register_fixed(fixed_eh); } void kernel::user_propagate_register_final(user_propagator::final_eh_t& final_eh) { - m_imp->user_propagate_register_final(final_eh); + m_imp->m_kernel.user_propagate_register_final(final_eh); } void kernel::user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) { - m_imp->user_propagate_register_eq(eq_eh); + m_imp->m_kernel.user_propagate_register_eq(eq_eh); } void kernel::user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) { - m_imp->user_propagate_register_diseq(diseq_eh); + m_imp->m_kernel.user_propagate_register_diseq(diseq_eh); } - unsigned kernel::user_propagate_register(expr* e) { - return m_imp->user_propagate_register(e); + unsigned kernel::user_propagate_register_expr(expr* e) { + return m_imp->m_kernel.user_propagate_register_expr(e); } void kernel::user_propagate_register_created(user_propagator::created_eh_t& r) { - m_imp->user_propagate_register_created(r); - } - - func_decl* kernel::user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { - return m_imp->user_propagate_declare(name, n, domain, range); + m_imp->m_kernel.user_propagate_register_created(r); } }; \ No newline at end of file diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index 0296c29a6..5c28d52fd 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -301,12 +301,10 @@ namespace smt { void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh); - unsigned user_propagate_register(expr* e); + unsigned user_propagate_register_expr(expr* e); void user_propagate_register_created(user_propagator::created_eh_t& r); - func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range); - /** \brief Return a reference to smt::context. This is a temporary hack to support user theories. diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index fe4aec944..f9ab54327 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -236,18 +236,14 @@ namespace { m_context.user_propagate_register_diseq(diseq_eh); } - unsigned user_propagate_register(expr* e) override { - return m_context.user_propagate_register(e); + unsigned user_propagate_register_expr(expr* e) override { + return m_context.user_propagate_register_expr(e); } void user_propagate_register_created(user_propagator::created_eh_t& c) override { m_context.user_propagate_register_created(c); } - func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { - return m_context.user_propagate_declare(name, n, domain, range); - } - struct scoped_minimize_core { smt_solver& s; expr_ref_vector m_assumptions; diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp index d67e430e2..c99e50393 100644 --- a/src/smt/tactic/smt_tactic_core.cpp +++ b/src/smt/tactic/smt_tactic_core.cpp @@ -449,7 +449,7 @@ public: unsigned i = 0; for (expr* v : m_vars) { - unsigned j = m_ctx->user_propagate_register(v); + unsigned j = m_ctx->user_propagate_register_expr(v); m_var2internal.setx(i, j, 0); m_internal2var.setx(j, i, 0); ++i; @@ -493,15 +493,11 @@ public: m_diseq_eh = diseq_eh; } - unsigned user_propagate_register(expr* e) override { + unsigned user_propagate_register_expr(expr* e) override { m_vars.push_back(e); return m_vars.size() - 1; } - func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) override { - return m_ctx->user_propagate_declare(name, n, domain, range); - } - void user_propagate_register_created(user_propagator::created_eh_t& created_eh) override { m_ctx->user_propagate_register_created(created_eh); } diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp index ac7968d45..200d9b946 100644 --- a/src/smt/theory_user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -23,7 +23,7 @@ Author: using namespace smt; theory_user_propagator::theory_user_propagator(context& ctx): - theory(ctx, ctx.get_manager().mk_family_id("user_propagator")) + theory(ctx, ctx.get_manager().mk_family_id(user_propagator::plugin::name())) {} theory_user_propagator::~theory_user_propagator() { @@ -173,16 +173,6 @@ void theory_user_propagator::propagate() { m_qhead = qhead; } -func_decl* theory_user_propagator::declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { - if (!m_created_eh) - throw default_exception("event handler for dynamic expressions has to be registered before functions can be created"); - // ensure that declaration plugin is registered with m. - if (!m.has_plugin(get_id())) - m.register_plugin(get_id(), alloc(user_propagator::plugin)); - - func_decl_info info(get_id(), user_propagator::plugin::kind_t::OP_USER_PROPAGATE); - return m.mk_func_decl(name, n, domain, range, info); -} bool theory_user_propagator::internalize_atom(app* atom, bool gate_ctx) { return internalize_term(atom); diff --git a/src/smt/theory_user_propagator.h b/src/smt/theory_user_propagator.h index 0189b13cb..0589a87a5 100644 --- a/src/smt/theory_user_propagator.h +++ b/src/smt/theory_user_propagator.h @@ -97,7 +97,6 @@ namespace smt { void register_eq(user_propagator::eq_eh_t& eq_eh) { m_eq_eh = eq_eh; } void register_diseq(user_propagator::eq_eh_t& diseq_eh) { m_diseq_eh = diseq_eh; } void register_created(user_propagator::created_eh_t& created_eh) { m_created_eh = created_eh; } - func_decl* declare(symbol const& name, unsigned n, sort* const* domain, sort* range); bool has_fixed() const { return (bool)m_fixed_eh; } diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 94f7fb336..15c9cab82 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -108,8 +108,8 @@ public: m_tactic->user_propagate_register_diseq(diseq_eh); } - unsigned user_propagate_register(expr* e) override { - return m_tactic->user_propagate_register(e); + unsigned user_propagate_register_expr(expr* e) override { + return m_tactic->user_propagate_register_expr(e); } void user_propagate_clear() override { diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index a5cbea932..a9f5ffcf8 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -892,7 +892,7 @@ public: m_num_elim_apps = 0; } - unsigned user_propagate_register(expr* e) override { + unsigned user_propagate_register_expr(expr* e) override { m_nonvars.insert(e); return 0; } diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index 436ee3272..607928f64 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -78,7 +78,7 @@ public: void operator()(goal_ref const & g, goal_ref_buffer & result) override; void cleanup() override; - unsigned user_propagate_register(expr* e) override; + unsigned user_propagate_register_expr(expr* e) override; void user_propagate_clear() override; }; @@ -502,7 +502,7 @@ void reduce_args_tactic::cleanup() { m_imp->m_vars.append(vars); } -unsigned reduce_args_tactic::user_propagate_register(expr* e) { +unsigned reduce_args_tactic::user_propagate_register_expr(expr* e) { m_imp->m_vars.push_back(e); return 0; } diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index 4c4b9358d..437c7f804 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -85,7 +85,7 @@ public: throw default_exception("tactic does not support user propagation"); } - unsigned user_propagate_register(expr* e) override { return 0; } + unsigned user_propagate_register_expr(expr* e) override { return 0; } virtual char const* name() const = 0; protected: diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 07fc88b37..fca2f8481 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -190,9 +190,9 @@ public: m_t2->user_propagate_register_diseq(diseq_eh); } - unsigned user_propagate_register(expr* e) override { - m_t1->user_propagate_register(e); - return m_t2->user_propagate_register(e); + unsigned user_propagate_register_expr(expr* e) override { + m_t1->user_propagate_register_expr(e); + return m_t2->user_propagate_register_expr(e); } void user_propagate_clear() override { @@ -204,10 +204,6 @@ public: m_t2->user_propagate_register_created(created_eh); } - func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) override { - return m_t2->user_propagate_declare(name, n, domain, range); - } - }; tactic * and_then(tactic * t1, tactic * t2) { @@ -833,7 +829,7 @@ public: void reset() override { m_t->reset(); } void set_logic(symbol const& l) override { m_t->set_logic(l); } void set_progress_callback(progress_callback * callback) override { m_t->set_progress_callback(callback); } - unsigned user_propagate_register(expr* e) override { return m_t->user_propagate_register(e); } + unsigned user_propagate_register_expr(expr* e) override { return m_t->user_propagate_register_expr(e); } void user_propagate_clear() override { m_t->user_propagate_clear(); } protected: diff --git a/src/tactic/user_propagator_base.h b/src/tactic/user_propagator_base.h index db9ca88fd..534b9dbc0 100644 --- a/src/tactic/user_propagator_base.h +++ b/src/tactic/user_propagator_base.h @@ -29,6 +29,8 @@ namespace user_propagator { class plugin : public decl_plugin { public: + static symbol name() { return symbol("user_propagator"); } + enum kind_t { OP_USER_PROPAGATE }; virtual ~plugin() {} @@ -79,19 +81,7 @@ namespace user_propagator { throw default_exception("user-propagators are only supported on the SMT solver"); } - virtual unsigned user_propagate_register(expr* e) { - throw default_exception("user-propagators are only supported on the SMT solver"); - } - - /** - * Create uninterpreted function for the user propagator. - * When expressions using the function are assigned values, generate a callback - * into a register_declared_eh(user_ctx, solver_ctx, declared_expr, declare_id) with arguments - * 1. context and callback context - * 2. declared_expr: expression using function that was declared at top. - * 3. declared_id: a unique identifier (unique within the current scope) to track the expression. - */ - virtual func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { + virtual unsigned user_propagate_register_expr(expr* e) { throw default_exception("user-propagators are only supported on the SMT solver"); } From 85e362277c251a2421452c29199b568d126ef52f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 18 Dec 2021 11:56:05 -0800 Subject: [PATCH 05/12] Update z3++.h with bindings for user propagate functions --- src/api/c++/z3++.h | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 6af9beae7..747244ca7 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -334,6 +334,7 @@ namespace z3 { func_decl recfun(char const * name, sort const & d1, sort const & d2, sort const & range); void recdef(func_decl, expr_vector const& args, expr const& body); + func_decl user_propagate_function(symbol const& name, unsigned arity, sort const* domain, sort const& range); expr constant(symbol const & name, sort const & s); expr constant(char const * name, sort const & s); @@ -3424,6 +3425,17 @@ namespace z3 { Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body); } + inline func_decl context::user_propagate_function(symbol const& name, unsigned arity, sort const* domain, sort const& range) { + array args(arity); + for (unsigned i = 0; i < arity; i++) { + check_context(domain[i], range); + args[i] = domain[i]; + } + Z3_func_decl f = Z3_user_propagate_declare(m_ctx, name, arity, args.ptr(), range); + check_error(); + return func_decl(*this, f); + } + inline expr context::constant(symbol const & name, sort const & s) { Z3_ast r = Z3_mk_const(m_ctx, name, s); check_error(); @@ -3877,10 +3889,12 @@ namespace z3 { typedef std::function fixed_eh_t; typedef std::function final_eh_t; typedef std::function eq_eh_t; + typedef std::function created_eh_t; final_eh_t m_final_eh; eq_eh_t m_eq_eh; fixed_eh_t m_fixed_eh; + created_eh_t m_created_eh; solver* s; Z3_context c; Z3_solver_callback cb { nullptr }; @@ -3929,6 +3943,14 @@ namespace z3 { static_cast(p)->m_final_eh(); } + static void created_eh(void* p, Z3_solver_callback cb, unsigned id, Z3_ast _e) { + user_propagator_base* p = static_cast(_p); + scoped_cb _cb(p, cb); + scoped_context ctx(p->ctx()); + expr e(ctx(), _e); + static_cast(p)->m_created_eh(id, e); + } + public: user_propagator_base(Z3_context c) : s(nullptr), c(c) {} @@ -4008,6 +4030,18 @@ namespace z3 { Z3_solver_propagate_final(ctx(), *s, final_eh); } + void register_created(created_eh_t& c) { + assert(s); + m_created_eh = c; + Z3_solver_propagate_created(c, *s, created_eh); + } + + void register_created() { + m_created_eh = [this](unsigned id, expr const& e) { + created(id, e); + }; + Z3_solver_propagate_created(c, *s, created_eh); + } virtual void fixed(unsigned /*id*/, expr const& /*e*/) { } @@ -4015,6 +4049,8 @@ namespace z3 { virtual void final() { } + virtual void created(unsigned /*id*/, expr const& /*e*/) {} + /** \brief tracks \c e by a unique identifier that is returned by the call. From 7441bd706b89021f733fe7cb3dc6107badbc2a58 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Dec 2021 10:57:42 -0800 Subject: [PATCH 06/12] na --- src/api/c++/z3++.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 747244ca7..941f7cc0b 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -4033,14 +4033,14 @@ namespace z3 { void register_created(created_eh_t& c) { assert(s); m_created_eh = c; - Z3_solver_propagate_created(c, *s, created_eh); + Z3_solver_propagate_created(ctx(), *s, created_eh); } void register_created() { m_created_eh = [this](unsigned id, expr const& e) { created(id, e); }; - Z3_solver_propagate_created(c, *s, created_eh); + Z3_solver_propagate_created(ctx(), *s, created_eh); } virtual void fixed(unsigned /*id*/, expr const& /*e*/) { } From bee742111a822151c3f47ef8b1c0fb1f19f2b189 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Dec 2021 11:05:19 -0800 Subject: [PATCH 07/12] na --- src/api/c++/z3++.h | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 941f7cc0b..1d44467f1 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -334,7 +334,7 @@ namespace z3 { func_decl recfun(char const * name, sort const & d1, sort const & d2, sort const & range); void recdef(func_decl, expr_vector const& args, expr const& body); - func_decl user_propagate_function(symbol const& name, unsigned arity, sort const* domain, sort const& range); + func_decl user_propagate_function(symbol const& name, sort_vector const& domain, sort const& range); expr constant(symbol const & name, sort const & s); expr constant(char const * name, sort const & s); @@ -3425,13 +3425,13 @@ namespace z3 { Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body); } - inline func_decl context::user_propagate_function(symbol const& name, unsigned arity, sort const* domain, sort const& range) { - array args(arity); - for (unsigned i = 0; i < arity; i++) { + inline func_decl context::user_propagate_function(symbol const& name, sort_vector const& domain, sort const& range) { + array args(domain.size()); + for (unsigned i = 0; i < domain.size(); i++) { check_context(domain[i], range); args[i] = domain[i]; } - Z3_func_decl f = Z3_user_propagate_declare(m_ctx, name, arity, args.ptr(), range); + Z3_func_decl f = Z3_solver_propagate_declare(range.ctx(), name, args.size(), args.ptr(), range); check_error(); return func_decl(*this, f); } @@ -3943,7 +3943,7 @@ namespace z3 { static_cast(p)->m_final_eh(); } - static void created_eh(void* p, Z3_solver_callback cb, unsigned id, Z3_ast _e) { + static void created_eh(void* _p, Z3_solver_callback cb, Z3_ast _e, unsigned id) { user_propagator_base* p = static_cast(_p); scoped_cb _cb(p, cb); scoped_context ctx(p->ctx()); From a7b1db611c62fd64aa7aeb1e108b2962f6611933 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Sun, 19 Dec 2021 11:09:55 -0800 Subject: [PATCH 08/12] State graph dgml update and fixes in condition simplifier (#5721) * improved generated dgml graph * fixed simplification of negated ranges and did some code cleanup * do not make loops with lower=upper=0, this is epsilon * do not add loops with lower=upper=1 * bug fix in normalization: forgotten eps case --- src/ast/rewriter/seq_rewriter.cpp | 295 +++++++++--------------------- src/ast/rewriter/seq_rewriter.h | 10 +- src/ast/seq_decl_plugin.cpp | 50 +++++ src/ast/seq_decl_plugin.h | 7 + src/util/state_graph.cpp | 26 ++- 5 files changed, 168 insertions(+), 220 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 13d8ef4fb..aef5eeacd 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2857,7 +2857,7 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) { return BR_REWRITE2; } else if (re().is_loop(r, r1, lo, hi)) { - result = re().mk_loop(re().mk_reverse(r1), lo, hi); + result = re().mk_loop_proper(re().mk_reverse(r1), lo, hi); return BR_REWRITE2; } else if (re().is_reverse(r, r1)) { @@ -3184,7 +3184,7 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref if ((lo == 0 && hi == 0) || hi < lo) result = nothing(); else - result = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), re().mk_loop(r1, (lo == 0 ? 0 : lo - 1), hi - 1)); + result = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), re().mk_loop_proper(r1, (lo == 0 ? 0 : lo - 1), hi - 1)); } else if (re().is_opt(r, r1)) result = mk_antimirov_deriv(e, r1, path); @@ -3350,6 +3350,8 @@ expr_ref seq_rewriter::mk_regex_inter_normalize(expr* r1, expr* r2) { SASSERT(m_util.is_re(r1)); SASSERT(m_util.is_re(r2)); expr_ref result(m()); + if (re().is_epsilon(r2)) + std::swap(r1, r2); std::function test = [&](expr* t, expr*& a, expr*& b) { return re().is_intersection(t, a, b); }; std::function compose = [&](expr* r1, expr* r2) { return re().mk_inter(r1, r2); }; if (r1 == r2 || re().is_empty(r1) || re().is_full_seq(r2)) @@ -3504,7 +3506,7 @@ expr_ref seq_rewriter::mk_regex_reverse(expr* r) { else if (re().is_loop(r, r1, lo)) result = re().mk_loop(mk_regex_reverse(r1), lo); else if (re().is_loop(r, r1, lo, hi)) - result = re().mk_loop(mk_regex_reverse(r1), lo, hi); + result = re().mk_loop_proper(mk_regex_reverse(r1), lo, hi); else if (re().is_opt(r, r1)) result = re().mk_opt(mk_regex_reverse(r1)); else if (re().is_complement(r, r1)) @@ -3517,8 +3519,9 @@ expr_ref seq_rewriter::mk_regex_reverse(expr* r) { } expr_ref seq_rewriter::mk_regex_concat(expr* r, expr* s) { - sort* seq_sort = nullptr; + sort* seq_sort = nullptr, * ele_sort = nullptr; VERIFY(m_util.is_re(r, seq_sort)); + VERIFY(u().is_seq(seq_sort, ele_sort)); SASSERT(r->get_sort() == s->get_sort()); expr_ref result(m()); expr* r1, * r2; @@ -3528,11 +3531,30 @@ expr_ref seq_rewriter::mk_regex_concat(expr* r, expr* s) { result = r; else if (re().is_full_seq(r) && re().is_full_seq(s)) result = r; + else if (re().is_full_char(r) && re().is_full_seq(s)) + // ..* = .+ + result = re().mk_plus(re().mk_full_char(ele_sort)); + else if (re().is_full_seq(r) && re().is_full_char(s)) + // .*. = .+ + result = re().mk_plus(re().mk_full_char(ele_sort)); else if (re().is_concat(r, r1, r2)) - //create the resulting concatenation in right-associative form + // create the resulting concatenation in right-associative form except for the following case + // TODO: maintain the followig invariant for A ++ B{m,n} + C + // concat(concat(A, B{m,n}), C) (if A != () and C != ()) + // concat(B{m,n}, C) (if A == () and C != ()) + // where A, B, C are regexes + // Using & below for Intersection and | for Union + // In other words, do not make A ++ B{m,n} into right-assoc form, but keep B{m,n} at the top + // This will help to identify this situation in the merge routine: + // concat(concat(A, B{0,m}), C) | concat(concat(A, B{0,n}), C) + // simplies to + // concat(concat(A, B{0,max(m,n)}), C) + // analogously: + // concat(concat(A, B{0,m}), C) & concat(concat(A, B{0,n}), C) + // simplies to + // concat(concat(A, B{0,min(m,n)}), C) result = mk_regex_concat(r1, mk_regex_concat(r2, s)); else { - //TODO: perhaps simplifiy some further cases such as .*. = ..* = .*.+ = .+.* = .+ result = re().mk_concat(r, s); } return result; @@ -3566,15 +3588,7 @@ expr_ref seq_rewriter::mk_in_antimirov_rec(expr* s, expr* d) { */ expr_ref seq_rewriter::simplify_path(expr* elem, expr* path) { expr_ref result(path, m()); - expr* h = nullptr, * t = nullptr; - if (m().is_and(path, h, t)) { - if (m().is_true(h)) - result = simplify_path(elem, t); - else if (m().is_true(t)) - result = simplify_path(elem, h); - else - elim_condition(elem, result); - } + elim_condition(elem, result); return result; } @@ -4027,7 +4041,7 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { return result; } else { - return mk_der_concat(result, re().mk_loop(r1, lo, hi)); + return mk_der_concat(result, re().mk_loop_proper(r1, lo, hi)); } } else if (re().is_full_seq(r) || @@ -4523,7 +4537,7 @@ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) { unsigned lo1, hi1, lo2, hi2; if (re().is_loop(a, a1, lo1, hi1) && lo1 <= hi1 && re().is_loop(b, b1, lo2, hi2) && lo2 <= hi2 && a1 == b1) { - result = re().mk_loop(a1, lo1 + lo2, hi1 + hi2); + result = re().mk_loop_proper(a1, lo1 + lo2, hi1 + hi2); return BR_DONE; } if (re().is_loop(a, a1, lo1) && re().is_loop(b, b1, lo2) && a1 == b1) { @@ -4631,79 +4645,13 @@ br_status seq_rewriter::mk_re_union0(expr* a, expr* b, expr_ref& result) { return BR_FAILED; } -/* - (a + a) = a - (a + eps) = a - (eps + a) = a -*/ +/* Creates a normalized union. */ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) { - br_status st = mk_re_union0(a, b, result); - if (st != BR_FAILED) - return st; - auto mk_full = [&]() { return re().mk_full_seq(a->get_sort()); }; - if (are_complements(a, b)) { - result = mk_full(); - return BR_DONE; - } - - //just keep the union normalized result = mk_regex_union_normalize(a, b); return BR_DONE; - - - expr* a1 = nullptr, *a2 = nullptr; - expr* b1 = nullptr, *b2 = nullptr; - // ensure union is right-associative - // and swap-sort entries - if (re().is_union(a, a1, a2)) { - result = re().mk_union(a1, re().mk_union(a2, b)); - return BR_REWRITE2; - } - - auto get_id = [&](expr* e) { re().is_complement(e, e); return e->get_id(); }; - if (re().is_union(b, b1, b2)) { - if (is_subset(a, b1)) { - result = b; - return BR_DONE; - } - if (is_subset(b1, a)) { - result = re().mk_union(a, b2); - return BR_REWRITE1; - } - if (are_complements(a, b1)) { - result = mk_full(); - return BR_DONE; - } - if (get_id(a) > get_id(b1)) { - result = re().mk_union(b1, re().mk_union(a, b2)); - return BR_REWRITE2; - } - } - else { - if (is_subset(a, b)) { - result = b; - return BR_DONE; - } - if (is_subset(b, a)) { - result = a; - return BR_DONE; - } - if (get_id(a) > get_id(b)) { - result = re().mk_union(b, a); - return BR_DONE; - } - } - return BR_FAILED; } -/* - comp(intersect e1 e2) -> union comp(e1) comp(e2) - comp(union e1 e2) -> intersect comp(e1) comp(e2) - comp(none) -> all - comp(all) -> none - comp(comp(e1)) -> e1 - comp(epsilon) -> .+ -*/ +/* Creates a normalized complement */ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) { expr *e1 = nullptr, *e2 = nullptr; if (re().is_intersection(a, e1, e2)) { @@ -4758,84 +4706,10 @@ br_status seq_rewriter::mk_re_inter0(expr* a, expr* b, expr_ref& result) { return BR_FAILED; } -/** - (r n r) = r - (emp n r) = emp - (r n emp) = emp - (all n r) = r - (r n all) = r - (r n comp(r)) = emp - (comp(r) n r) = emp - (r n to_re(s)) = ite (s in r) to_re(s) emp - (to_re(s) n r) = " - */ +/* Creates a normalized intersection. */ br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) { - br_status st = mk_re_inter0(a, b, result); - if (st != BR_FAILED) - return st; - auto mk_empty = [&]() { return re().mk_empty(a->get_sort()); }; - if (are_complements(a, b)) { - result = mk_empty(); - return BR_DONE; - } - - // intersect and normalize result = mk_regex_inter_normalize(a, b); return BR_DONE; - - expr* a1 = nullptr, *a2 = nullptr; - expr* b1 = nullptr, *b2 = nullptr; - - // the following rewrite rules do not seem to - // do the right thing when it comes to normalizing - - // ensure intersection is right-associative - // and swap-sort entries - if (re().is_intersection(a, a1, a2)) { - result = re().mk_inter(a1, re().mk_inter(a2, b)); - return BR_REWRITE2; - } - auto get_id = [&](expr* e) { re().is_complement(e, e); return e->get_id(); }; - if (re().is_intersection(b, b1, b2)) { - if (is_subset(b1, a)) { - result = b; - return BR_DONE; - } - if (is_subset(a, b1)) { - result = re().mk_inter(a, b2); - return BR_REWRITE1; - } - if (are_complements(a, b1)) { - result = mk_empty(); - return BR_DONE; - } - if (get_id(a) > get_id(b1)) { - result = re().mk_inter(b1, re().mk_inter(a, b2)); - return BR_REWRITE2; - } - } - else { - if (get_id(a) > get_id(b)) { - result = re().mk_inter(b, a); - return BR_DONE; - } - if (is_subset(a, b)) { - result = a; - return BR_DONE; - } - if (is_subset(b, a)) { - result = b; - return BR_DONE; - } - } - if (re().is_to_re(b)) - std::swap(a, b); - expr* s = nullptr; - if (re().is_to_re(a, s)) { - result = m().mk_ite(re().mk_in_re(s, b), a, re().mk_empty(a->get_sort())); - return BR_REWRITE2; - } - return BR_FAILED; } br_status seq_rewriter::mk_re_diff(expr* a, expr* b, expr_ref& result) { @@ -4873,7 +4747,7 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const* } // (loop (loop a l l) h h) = (loop a l*h l*h) if (re().is_loop(args[0], a, lo, hi) && np == 2 && lo == hi && lo2 == hi2) { - result = re().mk_loop(a, lo2 * lo, hi2 * hi); + result = re().mk_loop_proper(a, lo2 * lo, hi2 * hi); return BR_REWRITE1; } // (loop a 1 1) = a @@ -4900,7 +4774,7 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const* case 3: if (m_autil.is_numeral(args[1], n1) && n1.is_unsigned() && m_autil.is_numeral(args[2], n2) && n2.is_unsigned()) { - result = re().mk_loop(args[0], n1.get_unsigned(), n2.get_unsigned()); + result = re().mk_loop_proper(args[0], n1.get_unsigned(), n2.get_unsigned()); return BR_REWRITE1; } break; @@ -4912,7 +4786,7 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const* br_status seq_rewriter::mk_re_power(func_decl* f, expr* a, expr_ref& result) { unsigned p = f->get_parameter(0).get_int(); - result = re().mk_loop(a, p, p); + result = re().mk_loop_proper(a, p, p); return BR_REWRITE1; } @@ -5079,74 +4953,67 @@ void seq_rewriter::intersect(unsigned lo, unsigned hi, svector> ranges, ranges1; ranges.push_back(std::make_pair(0, u().max_char())); - auto exclude_char = [&](unsigned ch) { - if (ch == 0) { - intersect(1, u().max_char(), ranges); - } - else if (ch == u().max_char()) { - intersect(0, ch-1, ranges); + auto exclude_range = [&](unsigned lower, unsigned upper) { + SASSERT(lower <= upper); + if (lower == 0) { + if (upper == u().max_char()) + ranges.reset(); + else + intersect(upper + 1, u().max_char(), ranges); } + else if (upper == u().max_char()) + intersect(0, lower - 1, ranges); else { + // not(lower <= e <= upper) iff ((0 <= e <= lower-1) or (upper+1 <= e <= max)) + // Note that this transformation is correct only when lower <= upper ranges1.reset(); ranges1.append(ranges); - intersect(0, ch - 1, ranges); - intersect(ch + 1, u().max_char(), ranges1); + intersect(0, lower - 1, ranges); + intersect(upper + 1, u().max_char(), ranges1); ranges.append(ranges1); } }; bool all_ranges = true; + bool negated = false; for (expr* e : conds) { - if (m().is_eq(e, lhs, rhs) && elem == lhs && u().is_const_char(rhs, ch)) { - intersect(ch, ch, ranges); + if (u().is_char_const_range(elem, e, ch, ch2, negated)) { + if (ch > ch2) { + if (negated) + // !(ch <= elem <= ch2) is trivially true + continue; + else + // (ch <= elem <= ch2) is trivially false + ranges.reset(); + } + else if (negated) + exclude_range(ch, ch2); + else + intersect(ch, ch2, ranges); + conds_range.push_back(e); } - else if (m().is_eq(e, lhs, rhs) && elem == rhs && u().is_const_char(lhs, ch)) { - intersect(ch, ch, ranges); - } - else if (u().is_char_le(e, lhs, rhs) && elem == lhs && u().is_const_char(rhs, ch)) { - intersect(0, ch, ranges); - } - else if (u().is_char_le(e, lhs, rhs) && elem == rhs && u().is_const_char(lhs, ch)) { - intersect(ch, u().max_char(), ranges); - } - else if (m().is_not(e, e1) && m().is_eq(e1, lhs, rhs) && elem == lhs && u().is_const_char(rhs, ch)) { - exclude_char(ch); - } - else if (m().is_not(e, e1) && m().is_eq(e1, lhs, rhs) && elem == rhs && u().is_const_char(lhs, ch)) { - exclude_char(ch); - } - else if (m().is_not(e, e1) && u().is_char_le(e1, lhs, rhs) && elem == lhs && u().is_const_char(rhs, ch)) { - // not (e <= ch) - if (ch == u().max_char()) - ranges.reset(); - else - intersect(ch+1, u().max_char(), ranges); - } - else if (m().is_not(e, e1) && u().is_char_le(e1, lhs, rhs) && elem == rhs && u().is_const_char(lhs, ch)) { - // not (ch <= e) - if (ch == 0) - ranges.reset(); - else - intersect(0, ch-1, ranges); - } - else if (m().is_true(e) || (m().is_eq(e, lhs, rhs) && lhs == rhs)) { - // trivially true + // trivially true conditions + else if (m().is_true(e) || (m().is_eq(e, lhs, rhs) && lhs == rhs)) continue; - } - else if (m().is_not(e, e1) && m().is_eq(e1, lhs, rhs) && u().is_const_char(lhs, ch) && u().is_const_char(rhs, ch2) && ch != ch2) { - // trivially true + else if (m().is_not(e, e1) && m().is_eq(e1, lhs, rhs) && u().is_const_char(lhs, ch) && u().is_const_char(rhs, ch2) && ch != ch2) continue; - } - else if (m().is_false(e) || (m().is_not(e, e1) && m().is_eq(e1, lhs, rhs) && lhs == rhs)) { - // trivially false - cond = m().mk_false(); - return; - } + else if (u().is_char_le(e, lhs, rhs) && u().is_const_char(lhs, ch) && u().is_const_char(rhs, ch2) && ch <= ch2) + continue; + else if (m().is_not(e, e1) && u().is_char_le(e1, lhs, rhs) && u().is_const_char(lhs, ch) && u().is_const_char(rhs, ch2) && ch > ch2) + continue; + // trivially false conditions + else if (m().is_false(e) || (m().is_not(e, e1) && m().is_eq(e1, lhs, rhs) && lhs == rhs)) + ranges.reset(); + else if (u().is_char_le(e, lhs, rhs) && u().is_const_char(lhs, ch) && u().is_const_char(rhs, ch2) && ch > ch2) + ranges.reset(); + else if (m().is_not(e, e1) && u().is_char_le(e1, lhs, rhs) && u().is_const_char(lhs, ch) && u().is_const_char(rhs, ch2) && ch <= ch2) + ranges.reset(); else { all_ranges = false; break; @@ -5163,6 +5030,8 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) { cond = m().mk_true(); return; } + // removes all the trivially true conditions from conds + conds.set(conds_range); } } diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index c944e8f77..9357a2be8 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -223,11 +223,6 @@ class seq_rewriter { expr_ref merge_regex_sets(expr* r1, expr* r2, expr* unit, std::function& decompose, std::function& compose); - // Apply simplifications and keep the representation normalized - // Assuming r1 and r2 are normalized - expr_ref mk_regex_union_normalize(expr* r1, expr* r2); - expr_ref mk_regex_inter_normalize(expr* r1, expr* r2); - // elem is (:var 0) and path a condition that may have (:var 0) as a free variable // simplify path, e.g., (:var 0) = 'a' & (:var 0) = 'b' is simplified to false expr_ref simplify_path(expr* elem, expr* path); @@ -423,5 +418,10 @@ public: // heuristic elimination of element from condition that comes form a derivative. // special case optimization for conjunctions of equalities, disequalities and ranges. void elim_condition(expr* elem, expr_ref& cond); + + /* Apply simplifications to the union to keep the union normalized (r1 and r2 are not normalized)*/ + expr_ref mk_regex_union_normalize(expr* r1, expr* r2); + /* Apply simplifications to the intersection to keep it normalized (r1 and r2 are not normalized)*/ + expr_ref mk_regex_inter_normalize(expr* r1, expr* r2); }; diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 2044590aa..98a77c6b8 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -831,6 +831,39 @@ app* seq_util::mk_lt(expr* ch1, expr* ch2) const { return m.mk_not(mk_le(ch2, ch1)); } +bool seq_util::is_char_const_range(expr const* x, expr* e, unsigned& l, unsigned& u, bool& negated) const { + expr* a, * b, * e1, * e2, * lb, * ub; + e1 = e; + negated = (m.is_not(e, e1)) ? true : false; + if (m.is_eq(e1, a, b) && (a == x && is_const_char(b, l))) { + u = l; + return true; + } + if (is_char_le(e1, a, b) && a == x && is_const_char(b, u)) { + // (x <= u) + l = 0; + return true; + } + if (is_char_le(e1, a, b) && b == x && is_const_char(a, l)) { + // (l <= x) + u = max_char(); + return true; + } + if (m.is_and(e1, e1, e2) && is_char_le(e1, lb, a) && a == x && is_const_char(lb, l) && + is_char_le(e2, b, ub) && b == x && is_const_char(ub, u)) + // (l <= x) & (x <= u) + return true; + if (m.is_eq(e1, a, b) && b == x && is_const_char(a, l)) { + u = l; + return true; + } + if (m.is_and(e1, e2, e1) && is_char_le(e1, lb, a) && a == x && is_const_char(lb, l) && + is_char_le(e2, b, ub) && b == x && is_const_char(ub, u)) + // (x <= u) & (l <= x) + return true; + return false; +} + bool seq_util::str::is_string(func_decl const* f, zstring& s) const { if (is_string(f)) { s = f->get_parameter(0).get_zstring(); @@ -1030,6 +1063,23 @@ app* seq_util::rex::mk_loop(expr* r, unsigned lo, unsigned hi) { return m.mk_app(m_fid, OP_RE_LOOP, 2, params, 1, &r); } +expr* seq_util::rex::mk_loop_proper(expr* r, unsigned lo, unsigned hi) +{ + if (lo == 0 && hi == 0) { + sort* seq_sort = nullptr; + VERIFY(u.is_re(r, seq_sort)); + // avoid creating a loop with both bounds 0 + // such an expression is invalid as a loop + // it is BY DEFINITION = epsilon + return mk_epsilon(seq_sort); + } + if (lo == 1 && hi == 1) + // do not create a loop unless it actually is a loop + return r; + parameter params[2] = { parameter(lo), parameter(hi) }; + return m.mk_app(m_fid, OP_RE_LOOP, 2, params, 1, &r); +} + app* seq_util::rex::mk_loop(expr* r, expr* lo) { expr* rs[2] = { r, lo }; return m.mk_app(m_fid, OP_RE_LOOP, 0, nullptr, 2, rs); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index d6a1a0f29..9c76298b0 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -252,6 +252,12 @@ public: unsigned max_char() const { return seq.max_char(); } unsigned num_bits() const { return seq.num_bits(); } + /* + e has a form that is equivalent to l <= x <= u (then negated = false) + or e is equivalent to !(l <= x <= u) (then negated = true) + */ + bool is_char_const_range(expr const* x, expr * e, unsigned& l, unsigned& u, bool& negated) const; + app* mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range); bool is_skolem(expr const* e) const { return is_app_of(e, m_fid, _OP_SEQ_SKOLEM); } @@ -498,6 +504,7 @@ public: app* mk_opt(expr* r) { return m.mk_app(m_fid, OP_RE_OPTION, r); } app* mk_loop(expr* r, unsigned lo); app* mk_loop(expr* r, unsigned lo, unsigned hi); + expr* mk_loop_proper(expr* r, unsigned lo, unsigned hi); app* mk_loop(expr* r, expr* lo); app* mk_loop(expr* r, expr* lo, expr* hi); app* mk_full_char(sort* s); diff --git a/src/util/state_graph.cpp b/src/util/state_graph.cpp index 2cc4158c7..55de6d515 100644 --- a/src/util/state_graph.cpp +++ b/src/util/state_graph.cpp @@ -445,7 +445,7 @@ bool state_graph::write_dgml() { } r = m_state_ufind.next(r); } while (r != s); - dgml << " Category=\"State\">" << std::endl; + dgml << " Category=\"State\" Group=\"Collapsed\">" << std::endl; if (m_dead.contains(s)) dgml << "" << std::endl; if (m_live.contains(s)) @@ -453,18 +453,35 @@ bool state_graph::write_dgml() { if (m_unexplored.contains(s)) dgml << "" << std::endl; dgml << "" << std::endl; + dgml << "" << std::endl; + dgml << "" << std::endl; } } dgml << "" << std::endl; dgml << "" << std::endl; for (auto s : m_seen) { - if (m_state_ufind.is_root(s)) + if (m_state_ufind.is_root(s)) { for (auto t : m_targets[s]) { dgml << "" << std::endl; if (!m_sources_maybecycle[t].contains(s)) dgml << "" << std::endl; dgml << "" << std::endl; } + dgml << "" << std::endl; + dgml << "" << std::endl; + } } dgml << "" << std::endl; dgml << "" << std::endl @@ -494,6 +511,11 @@ bool state_graph::write_dgml() { << "" << std::endl << "" << std::endl << "" << std::endl + << "" << std::endl + << "" << std::endl + << "" << std::endl << "