From b7d2ba471eef5ee8dad37785e8b27d223f3e9f7a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Aug 2023 16:02:43 -0700 Subject: [PATCH] use namespace, add util with discriminators Signed-off-by: Nikolaj Bjorner --- src/ast/reg_decl_plugins.cpp | 2 +- src/ast/synth_decl_plugin.cpp | 56 +++++++++++++++++---------------- src/ast/synth_decl_plugin.h | 53 ++++++++++++++++++------------- src/cmd_context/cmd_context.cpp | 2 +- 4 files changed, 63 insertions(+), 50 deletions(-) diff --git a/src/ast/reg_decl_plugins.cpp b/src/ast/reg_decl_plugins.cpp index b42591a4c..5103ae901 100644 --- a/src/ast/reg_decl_plugins.cpp +++ b/src/ast/reg_decl_plugins.cpp @@ -55,5 +55,5 @@ void reg_decl_plugins(ast_manager & m) { if (!m.get_plugin(m.mk_family_id(symbol("specrels")))) m.register_plugin(symbol("specrels"), alloc(special_relations_decl_plugin)); if (!m.get_plugin(m.mk_family_id(symbol("synth")))) - m.register_plugin(symbol("synth"), alloc(synth_decl_plugin)); + m.register_plugin(symbol("synth"), alloc(synth::plugin)); } diff --git a/src/ast/synth_decl_plugin.cpp b/src/ast/synth_decl_plugin.cpp index 8934eefb2..35338265b 100644 --- a/src/ast/synth_decl_plugin.cpp +++ b/src/ast/synth_decl_plugin.cpp @@ -19,40 +19,42 @@ Author: #include "ast/synth_decl_plugin.h" +namespace synth { -synth_decl_plugin::synth_decl_plugin() {} + plugin::plugin() {} -func_decl * synth_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range) { - auto& m = *m_manager; - if (!range) - range = m.mk_bool_sort(); + func_decl * plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + auto& m = *m_manager; + if (!range) + range = m.mk_bool_sort(); - if (!m.is_bool(range)) - m.raise_exception("range of synthesis declaration is Bool"); + if (!m.is_bool(range)) + m.raise_exception("range of synthesis declaration is Bool"); - if (num_parameters > 0) - m.raise_exception("no parameters are expected"); + if (num_parameters > 0) + m.raise_exception("no parameters are expected"); - symbol name; - switch (k) { - case OP_SYNTH_DECLARE_OUTPUT: - name = "synthesiz3"; - break; - case OP_SYNTH_DECLARE_GRAMMAR: - default: - NOT_IMPLEMENTED_YET(); + symbol name; + switch (k) { + case OP_DECLARE_OUTPUT: + name = "synthesiz3"; + break; + case OP_DECLARE_GRAMMAR: + default: + NOT_IMPLEMENTED_YET(); + } + func_decl_info info(m_family_id, k, num_parameters, parameters); + return m.mk_func_decl(name, arity, domain, range, info); } - func_decl_info info(m_family_id, k, num_parameters, parameters); - return m.mk_func_decl(name, arity, domain, range, info); + + void plugin::get_op_names(svector & op_names, symbol const & logic) { + if (logic == symbol::null) { + op_names.push_back(builtin_name("synthesiz3", OP_DECLARE_OUTPUT)); + } + } + } -void synth_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { - if (logic == symbol::null) { - op_names.push_back(builtin_name("synthesiz3", OP_SYNTH_DECLARE_OUTPUT)); - } -} - - diff --git a/src/ast/synth_decl_plugin.h b/src/ast/synth_decl_plugin.h index 29a2d439d..01d606764 100644 --- a/src/ast/synth_decl_plugin.h +++ b/src/ast/synth_decl_plugin.h @@ -19,28 +19,39 @@ Author: #include "ast/ast.h" +namespace synth { -enum synth_op_kind { - OP_SYNTH_DECLARE_OUTPUT, - OP_SYNTH_DECLARE_GRAMMAR, - LAST_SYNTH_OP -}; - -class synth_decl_plugin : public decl_plugin { -public: - synth_decl_plugin(); - - decl_plugin * mk_fresh() override { - return alloc(synth_decl_plugin); - } + enum op_kind { + OP_DECLARE_OUTPUT, + OP_DECLARE_GRAMMAR, + LAST_OP + }; - func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range) override; - - void get_op_names(svector & op_names, symbol const & logic) override; + class plugin : public decl_plugin { + public: + plugin(); + + plugin * mk_fresh() override { + return alloc(plugin); + } + + func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) override; + + void get_op_names(svector & op_names, symbol const & logic) override; + + sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override { return nullptr; } + }; - sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override { return nullptr; } -}; - - + class util { + ast_manager& m; + family_id m_fid; + public: + util(ast_manager& m): m(m), m_fid(m.get_family_id("synth")) {} + + bool is_synthesiz3(expr* e) { return is_app_of(e, m_fid, OP_DECLARE_OUTPUT); } + bool is_grammar(expr* e) { return is_app_of(e, m_fid, OP_DECLARE_GRAMMAR); } + }; + +} diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index f9b851999..0b6775151 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -826,7 +826,7 @@ void cmd_context::init_manager_core(bool new_manager) { register_plugin(symbol("fpa"), alloc(fpa_decl_plugin), logic_has_fpa()); register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin), !has_logic()); register_plugin(symbol("specrels"), alloc(special_relations_decl_plugin), !has_logic()); - register_plugin(symbol("synth"), alloc(synth_decl_plugin), !has_logic()); + register_plugin(symbol("synth"), alloc(synth::plugin), !has_logic()); } else { // the manager was created by an external module