From 4856581b68d63929d8913240c9ce25360c0fba8f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
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 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<int> 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<int> 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<expr_ref_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<void*(void*, ast_manager&, context_obj*&)> fresh_eh_t;
typedef std::function<void(void*)> push_eh_t;
typedef std::function<void(void*,unsigned)> pop_eh_t;
- typedef std::function<void(void*, callback*, expr*, unsigned)> register_created_eh_t;
+ typedef std::function<void(void*, callback*, expr*, unsigned)> 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");
}