From 4856581b68d63929d8913240c9ce25360c0fba8f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 17 Dec 2021 16:40:19 -0800 Subject: [PATCH] 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 bb5ab975219..222fe7061ea 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 dd07e8baf37..70447ff671f 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 e34c7e38af0..7a93382e95b 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 e5b630902d3..3a1db06c1c6 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 ba800548478..85f59d26c48 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 13f7da7dc55..b26823291cd 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 e8fdbc64804..0296c29a687 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 a755fe5ae71..fe4aec944ac 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 93ce81976ba..d67e430e2db 100644 --- a/src/smt/tactic/smt_tactic_core.cpp +++ b/src/smt/tactic/smt_tactic_core.cpp @@ -319,7 +319,7 @@ class smt_tactic : public tactic { 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 @@ class smt_tactic : public tactic { 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 @@ class smt_tactic : public tactic { 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 a9b340d4ab1..0189b13cb44 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 171a8314d6a..07fc88b374c 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -200,7 +200,7 @@ class and_then_tactical : public binary_tactical { 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 e5a2d282f5b..db9ca88fd23 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"); }