From d03fdf5fedd6cd040b62745fa44c7ec0b091e128 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 15 Mar 2021 15:48:33 -0700 Subject: [PATCH] more descriptive naming convention --- scripts/mk_project.py | 4 ++-- src/api/api_config_params.cpp | 6 +++--- src/api/api_context.cpp | 8 ++++---- src/api/api_context.h | 6 +++--- src/api/api_solver.cpp | 2 +- src/cmd_context/cmd_context.cpp | 2 +- src/cmd_context/cmd_context.h | 4 ++-- 7 files changed, 16 insertions(+), 16 deletions(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 853c05f70..4af2da3e2 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -23,12 +23,12 @@ def init_project_def(): add_lib('realclosure', ['interval'], 'math/realclosure') add_lib('subpaving', ['interval'], 'math/subpaving') add_lib('ast', ['util', 'polynomial']) - add_lib('params', ['util']) add_lib('euf', ['ast', 'util'], 'ast/euf') + add_lib('params', ['util']) + add_lib('smt_params', ['params'], 'smt/params') add_lib('grobner', ['ast', 'dd', 'simplex'], 'math/grobner') add_lib('sat', ['util', 'dd', 'grobner']) add_lib('nlsat', ['polynomial', 'sat']) - add_lib('smt_params', ['params'], 'smt/params') add_lib('lp', ['util', 'nlsat', 'grobner', 'interval', 'smt_params'], 'math/lp') add_lib('rewriter', ['ast', 'polynomial', 'automata', 'params'], 'ast/rewriter') add_lib('macros', ['rewriter'], 'ast/macros') diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp index ce59170c5..211e2abde 100644 --- a/src/api/api_config_params.cpp +++ b/src/api/api_config_params.cpp @@ -70,7 +70,7 @@ extern "C" { try { memory::initialize(UINT_MAX); LOG_Z3_mk_config(); - Z3_config r = reinterpret_cast(alloc(ast_context)); + Z3_config r = reinterpret_cast(alloc(ast_context_params)); RETURN_Z3(r); } catch (z3_exception & ex) { // The error handler is only available for contexts @@ -82,13 +82,13 @@ extern "C" { void Z3_API Z3_del_config(Z3_config c) { LOG_Z3_del_config(c); - dealloc((reinterpret_cast(c))); + dealloc((reinterpret_cast(c))); } void Z3_API Z3_set_param_value(Z3_config c, char const * param_id, char const * param_value) { LOG_Z3_set_param_value(c, param_id, param_value); try { - ast_context * p = reinterpret_cast(c); + ast_context_params * p = reinterpret_cast(c); p->set(param_id, param_value); } catch (z3_exception & ex) { diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 2355d4837..756633048 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -70,8 +70,8 @@ namespace api { // // ------------------------ - context::context(ast_context * p, bool user_ref_count): - m_params(p != nullptr ? *p : ast_context()), + context::context(ast_context_params * p, bool user_ref_count): + m_params(p != nullptr ? *p : ast_context_params()), m_user_ref_count(user_ref_count), m_manager(m_params.mk_ast_manager()), m_plugins(m()), @@ -343,7 +343,7 @@ extern "C" { Z3_TRY; LOG_Z3_mk_context(c); memory::initialize(UINT_MAX); - Z3_context r = reinterpret_cast(alloc(api::context, reinterpret_cast(c), false)); + Z3_context r = reinterpret_cast(alloc(api::context, reinterpret_cast(c), false)); RETURN_Z3(r); Z3_CATCH_RETURN_NO_HANDLE(nullptr); } @@ -352,7 +352,7 @@ extern "C" { Z3_TRY; LOG_Z3_mk_context_rc(c); memory::initialize(UINT_MAX); - Z3_context r = reinterpret_cast(alloc(api::context, reinterpret_cast(c), true)); + Z3_context r = reinterpret_cast(alloc(api::context, reinterpret_cast(c), true)); RETURN_Z3(r); Z3_CATCH_RETURN_NO_HANDLE(nullptr); } diff --git a/src/api/api_context.h b/src/api/api_context.h index b2dc816dd..83f569767 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -73,7 +73,7 @@ namespace api { class context : public tactic_manager { struct add_plugins { add_plugins(ast_manager & m); }; - ast_context m_params; + ast_context_params m_params; bool m_user_ref_count; //!< if true, the user is responsible for managing reference counters. scoped_ptr m_manager; scoped_ptr m_cmd; @@ -135,11 +135,11 @@ namespace api { // // ------------------------ - context(ast_context * p, bool user_ref_count = false); + context(ast_context_params * p, bool user_ref_count = false); ~context(); ast_manager & m() const { return *(m_manager.get()); } - ast_context & params() { m_params.updt_params(); return m_params; } + ast_context_params & params() { m_params.updt_params(); return m_params; } scoped_ptr& cmd() { return m_cmd; } bool produce_proofs() const { return m().proofs_enabled(); } bool produce_models() const { return m_params.m_model; } diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 64132f9a4..577ff934c 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -876,7 +876,7 @@ extern "C" { solver::push_eh_t _push = push_eh; solver::pop_eh_t _pop = pop_eh; solver::fresh_eh_t _fresh = [&](void * user_ctx, ast_manager& m, solver::context_obj*& _ctx) { - ast_context params; + ast_context_params params; params.set_foreign_manager(&m); auto* ctx = alloc(api::context, ¶ms, false); _ctx = alloc(api_context_obj, ctx); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index bcf4225a2..9c4b2ce40 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -280,7 +280,7 @@ void macro_decls::erase_last(ast_manager& m) { m_decls->pop_back(); } -ast_manager * ast_context::mk_ast_manager() { +ast_manager * ast_context_params::mk_ast_manager() { if (m_manager) return m_manager; ast_manager * r = alloc(ast_manager, diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 4eb81b911..2cbe30a72 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -160,7 +160,7 @@ public: virtual void updt_params(params_ref const& p) = 0; }; -class ast_context : public context_params { +class ast_context_params : public context_params { ast_manager* m_manager { nullptr }; public: /** @@ -194,7 +194,7 @@ public: protected: - ast_context m_params; + ast_context_params m_params; bool m_main_ctx; symbol m_logic; bool m_interactive_mode;