na

Z3Prover · Dec 18, 2021 · 4856581 · 4856581
1 parent 8ca023d
commit 4856581
Show file tree

Hide file tree

Showing 12 changed files with 36 additions and 37 deletions.
diff --git 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
@@ -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
@@ -416,44 +416,44 @@ 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;
     }
 }
 
 paccessor_decl::paccessor_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, ptype const & r):
     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;
     }
     return false;
 }
 
 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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");
         }