mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

use namespace, add util with discriminators

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-08-08 16:02:43 -07:00
parent 78b8072bb4
commit b7d2ba471e
4 changed files with 63 additions and 50 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/reg_decl_plugins.cpp
View file

@ -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));
}

56
src/ast/synth_decl_plugin.cpp
View file

@ -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<builtin_name> & 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<builtin_name> & op_names, symbol const & logic) {
if (logic == symbol::null) {
op_names.push_back(builtin_name("synthesiz3", OP_SYNTH_DECLARE_OUTPUT));
}
}

53
src/ast/synth_decl_plugin.h
View file

@ -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<builtin_name> & 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<builtin_name> & 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); }
};
}

2
src/cmd_context/cmd_context.cpp
View file

@ -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