mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

Make ast_manager::get_family_id(symbol const &) side-effect free. The version with side-effects is now called ast_manager::mk_family_id

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-18 17:14:25 -08:00
parent 3ddb1a85f1
commit d92efeb0c5
56 changed files with 127 additions and 108 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/api/api_context.cpp
View file

@ -106,11 +106,11 @@ namespace api {
m_error_handler = &default_error_handler;
m_basic_fid = m().get_basic_family_id();
m_arith_fid = m().get_family_id("arith");
m_bv_fid = m().get_family_id("bv");
m_array_fid = m().get_family_id("array");
m_dt_fid = m().get_family_id("datatype");
m_datalog_fid = m().get_family_id("datalog_relation");
m_arith_fid = m().mk_family_id("arith");
m_bv_fid = m().mk_family_id("bv");
m_array_fid = m().mk_family_id("array");
m_dt_fid = m().mk_family_id("datatype");
m_datalog_fid = m().mk_family_id("datalog_relation");
m_dt_plugin = static_cast<datatype_decl_plugin*>(m().get_plugin(m_dt_fid));
if (!m_user_ref_count) {

2
src/ast/arith_decl_plugin.cpp
View file

@ -583,7 +583,7 @@ bool arith_recognizers::is_numeral(expr const * n, rational & val, bool & is_int
}
arith_util::arith_util(ast_manager & m):
arith_recognizers(m.get_family_id("arith")),
arith_recognizers(m.mk_family_id("arith")),
m_manager(m),
m_plugin(0) {
}

2
src/ast/array_decl_plugin.cpp
View file

@ -548,7 +548,7 @@ func_decl * array_recognizers::get_as_array_func_decl(app * n) const {
}
array_util::array_util(ast_manager& m):
array_recognizers(m.get_family_id("array")),
array_recognizers(m.mk_family_id("array")),
m_manager(m) {
}

28
src/ast/ast.cpp
View file

@ -137,7 +137,7 @@ void display_parameters(std::ostream & out, unsigned n, parameter const * p) {
//
// -----------------------------------
family_id family_manager::get_family_id(symbol const & s) {
family_id family_manager::mk_family_id(symbol const & s) {
family_id r;
if (m_families.find(s, r)) {
return r;
@ -149,7 +149,15 @@ family_id family_manager::get_family_id(symbol const & s) {
return r;
}
bool family_manager::has_family(symbol const & s) {
family_id family_manager::get_family_id(symbol const & s) const {
family_id r;
if (m_families.find(s, r))
return r;
else
return null_family_id;
}
bool family_manager::has_family(symbol const & s) const {
return m_families.contains(s);
}
@ -1297,12 +1305,12 @@ void ast_manager::init() {
m_expr_id_gen.reset(0);
m_decl_id_gen.reset(c_first_decl_id);
m_some_value_proc = 0;
m_basic_family_id = get_family_id("basic");
m_label_family_id = get_family_id("label");
m_pattern_family_id = get_family_id("pattern");
m_model_value_family_id = get_family_id("model-value");
m_user_sort_family_id = get_family_id("user-sort");
m_arith_family_id = get_family_id("arith");
m_basic_family_id = mk_family_id("basic");
m_label_family_id = mk_family_id("label");
m_pattern_family_id = mk_family_id("pattern");
m_model_value_family_id = mk_family_id("model-value");
m_user_sort_family_id = mk_family_id("user-sort");
m_arith_family_id = mk_family_id("arith");
basic_decl_plugin * plugin = alloc(basic_decl_plugin);
register_plugin(m_basic_family_id, plugin);
m_bool_sort = plugin->mk_bool_sort();
@ -1435,7 +1443,7 @@ void ast_manager::copy_families_plugins(ast_manager const & from) {
<< ", target has_family: " << m_family_manager.has_family(fid) << "\n";
if (m_family_manager.has_family(fid)) tout << get_family_id(fid_name) << "\n";);
if (!m_family_manager.has_family(fid)) {
family_id new_fid = get_family_id(fid_name);
family_id new_fid = mk_family_id(fid_name);
TRACE("copy_families_plugins", tout << "new target fid created: " << new_fid << " fid_name: " << fid_name << "\n";);
}
TRACE("copy_families_plugins", tout << "target fid: " << get_family_id(fid_name) << "\n";);
@ -1472,7 +1480,7 @@ void ast_manager::set_next_expr_id(unsigned id) {
unsigned ast_manager::get_node_size(ast const * n) { return ::get_node_size(n); }
void ast_manager::register_plugin(symbol const & s, decl_plugin * plugin) {
family_id id = m_family_manager.get_family_id(s);
family_id id = m_family_manager.mk_family_id(s);
SASSERT(is_format_manager() || s != symbol("format"));
register_plugin(id, plugin);
}

24
src/ast/ast.h
View file

@ -188,10 +188,20 @@ class family_manager {
svector<symbol> m_names;
public:
family_manager():m_next_id(0) {}
/**
\brief Return the family_id for s, a new id is created if !has_family(s)
If has_family(s), then this method is equivalent to get_family_id(s)
*/
family_id mk_family_id(symbol const & s);
/**
\brief Return the family_id for s, return null_family_id if s was not registered in the manager.
*/
family_id get_family_id(symbol const & s) const;
family_id get_family_id(symbol const & s);
bool has_family(symbol const & s);
bool has_family(symbol const & s) const;
void get_dom(svector<symbol>& dom) const { m_families.get_dom(dom); }
@ -1483,8 +1493,10 @@ public:
small_object_allocator & get_allocator() { return m_alloc; }
family_id get_family_id(symbol const & s) const { return const_cast<ast_manager*>(this)->m_family_manager.get_family_id(s); }
family_id mk_family_id(symbol const & s) { return m_family_manager.mk_family_id(s); }
family_id mk_family_id(char const * s) { return mk_family_id(symbol(s)); }
family_id get_family_id(symbol const & s) const { return m_family_manager.get_family_id(s); }
family_id get_family_id(char const * s) const { return get_family_id(symbol(s)); }
symbol const & get_family_name(family_id fid) const { return m_family_manager.get_name(fid); }
@ -1507,7 +1519,7 @@ public:
bool has_plugin(family_id fid) const { return get_plugin(fid) != 0; }
bool has_plugin(symbol const & s) const { return has_plugin(get_family_id(s)); }
bool has_plugin(symbol const & s) const { return m_family_manager.has_family(s) && has_plugin(m_family_manager.get_family_id(s)); }
void get_dom(svector<symbol> & dom) const { m_family_manager.get_dom(dom); }

12
src/ast/ast_smt_pp.cpp
View file

@ -795,11 +795,11 @@ public:
m_simplify_implies(simplify_implies)
{
m_basic_fid = m.get_basic_family_id();
m_label_fid = m.get_family_id("label");
m_bv_fid = m.get_family_id("bv");
m_arith_fid = m.get_family_id("arith");
m_array_fid = m.get_family_id("array");
m_dt_fid = m.get_family_id("datatype");
m_label_fid = m.mk_family_id("label");
m_bv_fid = m.mk_family_id("bv");
m_arith_fid = m.mk_family_id("arith");
m_array_fid = m.mk_family_id("array");
m_dt_fid = m.mk_family_id("datatype");
}
void operator()(expr* n) {
@ -1009,7 +1009,7 @@ ast_smt_pp::ast_smt_pp(ast_manager& m):
m_status("unknown"),
m_category(),
m_logic(),
m_dt_fid(m.get_family_id("datatype")),
m_dt_fid(m.mk_family_id("datatype")),
m_is_declared(&m_is_declared_default),
m_simplify_implies(true)
{}

8
src/ast/bv_decl_plugin.cpp
View file

@ -59,7 +59,7 @@ void bv_decl_plugin::set_manager(ast_manager * m, family_id id) {
m_xor3 = m_manager->mk_func_decl(symbol("xor3"), 3, d, b, func_decl_info(m_family_id, OP_XOR3));
m_manager->inc_ref(m_xor3);
m_int_sort = m_manager->mk_sort(m_manager->get_family_id("arith"), INT_SORT);
m_int_sort = m_manager->mk_sort(m_manager->mk_family_id("arith"), INT_SORT);
SASSERT(m_int_sort != 0); // arith_decl_plugin must be installed before bv_decl_plugin.
m_manager->inc_ref(m_int_sort);
}
@ -801,10 +801,10 @@ bool bv_recognizers::mult_inverse(rational const & n, unsigned bv_size, rational
}
bv_util::bv_util(ast_manager & m):
bv_recognizers(m.get_family_id(symbol("bv"))),
bv_recognizers(m.mk_family_id(symbol("bv"))),
m_manager(m) {
SASSERT(m.has_plugin(symbol("bv")));
m_plugin = static_cast<bv_decl_plugin*>(m.get_plugin(m.get_family_id("bv")));
m_plugin = static_cast<bv_decl_plugin*>(m.get_plugin(m.mk_family_id("bv")));
}
app * bv_util::mk_numeral(rational const & val, sort* s) {
@ -827,7 +827,7 @@ sort * bv_util::mk_sort(unsigned bv_size) {
}
app * bv_util::mk_bv2int(expr* e) {
sort* s = m_manager.mk_sort(m_manager.get_family_id("arith"), INT_SORT);
sort* s = m_manager.mk_sort(m_manager.mk_family_id("arith"), INT_SORT);
parameter p(s);
return m_manager.mk_app(get_fid(), OP_BV2INT, 1, &p, 1, &e);
}

2
src/ast/datatype_decl_plugin.cpp
View file

@ -673,7 +673,7 @@ bool datatype_decl_plugin::is_value(app * e) const {
datatype_util::datatype_util(ast_manager & m):
m_manager(m),
m_family_id(m.get_family_id("datatype")),
m_family_id(m.mk_family_id("datatype")),
m_asts(m) {
}

2
src/ast/decl_collector.cpp
View file

@ -45,7 +45,7 @@ decl_collector::decl_collector(ast_manager & m, bool preds):
m_manager(m),
m_sep_preds(preds) {
m_basic_fid = m_manager.get_basic_family_id();
m_dt_fid = m_manager.get_family_id("datatype");
m_dt_fid = m_manager.mk_family_id("datatype");
}
void decl_collector::visit(ast* n) {

2
src/ast/dl_decl_plugin.cpp
View file

@ -629,7 +629,7 @@ namespace datalog {
m(m),
m_arith(m),
m_bv(m),
m_fid(m.get_family_id(symbol("datalog_relation")))
m_fid(m.mk_family_id(symbol("datalog_relation")))
{}
// create a constant belonging to a given finite domain.

6
src/ast/float_decl_plugin.cpp
View file

@ -31,7 +31,7 @@ float_decl_plugin::float_decl_plugin():
void float_decl_plugin::set_manager(ast_manager * m, family_id id) {
decl_plugin::set_manager(m, id);
family_id aid = m_manager->get_family_id("arith");
family_id aid = m_manager->mk_family_id("arith");
m_real_sort = m_manager->mk_sort(aid, REAL_SORT);
SASSERT(m_real_sort != 0); // arith_decl_plugin must be installed before float_decl_plugin.
m_manager->inc_ref(m_real_sort);
@ -42,7 +42,7 @@ void float_decl_plugin::set_manager(ast_manager * m, family_id id) {
if (m_manager->has_plugin(symbol("bv"))) {
// bv plugin is optional, so m_bv_plugin may be 0
m_bv_fid = m_manager->get_family_id("bv");
m_bv_fid = m_manager->mk_family_id("bv");
m_bv_plugin = static_cast<bv_decl_plugin*>(m_manager->get_plugin(m_bv_fid));
}
}
@ -512,7 +512,7 @@ bool float_decl_plugin::is_value(app * e) const {
float_util::float_util(ast_manager & m):
m_manager(m),
m_fid(m.get_family_id("float")),
m_fid(m.mk_family_id("float")),
m_a_util(m) {
m_plugin = static_cast<float_decl_plugin*>(m.get_plugin(m_fid));
}

2
src/ast/format.cpp
View file

@ -103,7 +103,7 @@ namespace format_ns {
symbol f("format");
if (!fm(m).has_plugin(f))
fm(m).register_plugin(f, alloc(format_decl_plugin));
return fm(m).get_family_id(f);
return fm(m).mk_family_id(f);
}
static family_id fid(ast_manager & m) {

4
src/ast/macros/macro_util.cpp
View file

@ -41,7 +41,7 @@ macro_util::macro_util(ast_manager & m, simplifier & s):
arith_simplifier_plugin * macro_util::get_arith_simp() const {
if (m_arith_simp == 0) {
const_cast<macro_util*>(this)->m_arith_simp = static_cast<arith_simplifier_plugin*>(m_simplifier.get_plugin(m_manager.get_family_id("arith")));
const_cast<macro_util*>(this)->m_arith_simp = static_cast<arith_simplifier_plugin*>(m_simplifier.get_plugin(m_manager.mk_family_id("arith")));
}
SASSERT(m_arith_simp != 0);
return m_arith_simp;
@ -49,7 +49,7 @@ arith_simplifier_plugin * macro_util::get_arith_simp() const {
bv_simplifier_plugin * macro_util::get_bv_simp() const {
if (m_bv_simp == 0) {
const_cast<macro_util*>(this)->m_bv_simp = static_cast<bv_simplifier_plugin*>(m_simplifier.get_plugin(m_manager.get_family_id("bv")));
const_cast<macro_util*>(this)->m_bv_simp = static_cast<bv_simplifier_plugin*>(m_simplifier.get_plugin(m_manager.mk_family_id("bv")));
}
SASSERT(m_bv_simp != 0);
return m_bv_simp;

2
src/ast/pattern/pattern_inference.cpp
View file

@ -91,7 +91,7 @@ pattern_inference::pattern_inference(ast_manager & m, pattern_inference_params &
simplifier(m),
m_params(params),
m_bfid(m.get_basic_family_id()),
m_afid(m.get_family_id("arith")),
m_afid(m.mk_family_id("arith")),
m_le(m),
m_nested_arith_only(true),
m_block_loop_patterns(params.m_pi_block_loop_patterns),

2
src/ast/pattern/pattern_inference.h
View file

@ -150,7 +150,7 @@ class pattern_inference : public simplifier {
void save_candidate(expr * n, unsigned delta);
void reset();
public:
collect(ast_manager & m, pattern_inference & o):m_manager(m), m_owner(o), m_afid(m.get_family_id("arith")) {}
collect(ast_manager & m, pattern_inference & o):m_manager(m), m_owner(o), m_afid(m.mk_family_id("arith")) {}
void operator()(expr * n, unsigned num_bindings);
};

2
src/ast/proof_checker/proof_checker.cpp
View file

@ -85,7 +85,7 @@ proof_checker::proof_checker(ast_manager& m) : m(m), m_todo(m), m_marked(), m_pi
if (!m.has_plugin(fam_name)) {
m.register_plugin(fam_name, alloc(hyp_decl_plugin));
}
m_hyp_fid = m.get_family_id(fam_name);
m_hyp_fid = m.mk_family_id(fam_name);
// m_spc_fid = m.get_family_id("spc");
m_nil = m.mk_const(m_hyp_fid, OP_NIL);
}

14
src/ast/reg_decl_plugins.cpp
View file

@ -27,25 +27,25 @@ Revision History:
#include"float_decl_plugin.h"
void reg_decl_plugins(ast_manager & m) {
if (!m.get_plugin(m.get_family_id(symbol("arith")))) {
if (!m.get_plugin(m.mk_family_id(symbol("arith")))) {
m.register_plugin(symbol("arith"), alloc(arith_decl_plugin));
}
if (!m.get_plugin(m.get_family_id(symbol("bv")))) {
if (!m.get_plugin(m.mk_family_id(symbol("bv")))) {
m.register_plugin(symbol("bv"), alloc(bv_decl_plugin));
}
if (!m.get_plugin(m.get_family_id(symbol("array")))) {
if (!m.get_plugin(m.mk_family_id(symbol("array")))) {
m.register_plugin(symbol("array"), alloc(array_decl_plugin));
}
if (!m.get_plugin(m.get_family_id(symbol("datatype")))) {
if (!m.get_plugin(m.mk_family_id(symbol("datatype")))) {
m.register_plugin(symbol("datatype"), alloc(datatype_decl_plugin));
}
if (!m.get_plugin(m.get_family_id(symbol("datalog_relation")))) {
if (!m.get_plugin(m.mk_family_id(symbol("datalog_relation")))) {
m.register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin));
}
if (!m.get_plugin(m.get_family_id(symbol("seq")))) {
if (!m.get_plugin(m.mk_family_id(symbol("seq")))) {
m.register_plugin(symbol("seq"), alloc(seq_decl_plugin));
}
if (!m.get_plugin(m.get_family_id(symbol("float")))) {
if (!m.get_plugin(m.mk_family_id(symbol("float")))) {
m.register_plugin(symbol("float"), alloc(float_decl_plugin));
}
}

2
src/ast/simplifier/bv_elim.cpp
View file

@ -15,7 +15,7 @@ void bv_elim::elim(quantifier* q, quantifier_ref& r) {
expr_ref new_body(m_manager);
expr* old_body = q->get_expr();
unsigned num_decls = q->get_num_decls();
family_id bfid = m_manager.get_family_id("bv");
family_id bfid = m_manager.mk_family_id("bv");
//
// Traverse sequence of bound variables to eliminate

2
src/ast/simplifier/simplifier_plugin.h
View file

@ -37,7 +37,7 @@ protected:
void set_reduce_invoked() { m_reduce_invoked = true; }
public:
simplifier_plugin(symbol const & fname, ast_manager & m):m_manager(m), m_fid(m.get_family_id(fname)), m_presimp(false), m_reduce_invoked(false) {}
simplifier_plugin(symbol const & fname, ast_manager & m):m_manager(m), m_fid(m.mk_family_id(fname)), m_presimp(false), m_reduce_invoked(false) {}
bool reduce_invoked() const { return m_reduce_invoked; }

4
src/ast/static_features.cpp
View file

@ -23,8 +23,8 @@ static_features::static_features(ast_manager & m):
m_manager(m),
m_autil(m),
m_bfid(m.get_basic_family_id()),
m_afid(m.get_family_id("arith")),
m_lfid(m.get_family_id("label")),
m_afid(m.mk_family_id("arith")),
m_lfid(m.mk_family_id("label")),
m_label_sym("label"),
m_pattern_sym("pattern"),
m_expr_list_sym("expr-list") {

2
src/cmd_context/basic_cmds.cpp
View file

@ -643,7 +643,7 @@ public:
family_id get_array_fid(cmd_context & ctx) {
if (m_array_fid == null_family_id) {
m_array_fid = ctx.m().get_family_id("array");
m_array_fid = ctx.m().mk_family_id("array");
}
return m_array_fid;
}

2
src/cmd_context/cmd_context.cpp
View file

@ -1386,7 +1386,7 @@ void cmd_context::set_diagnostic_stream(char const * name) {
struct contains_array_op_proc {
struct found {};
family_id m_array_fid;
contains_array_op_proc(ast_manager & m):m_array_fid(m.get_family_id("array")) {}
contains_array_op_proc(ast_manager & m):m_array_fid(m.mk_family_id("array")) {}
void operator()(var * n) {}
void operator()(app * n) {
if (n->get_family_id() != m_array_fid)

2
src/cmd_context/pdecl.cpp
View file

@ -765,7 +765,7 @@ pdecl_manager::pdecl_manager(ast_manager & m):
m_allocator(m.get_allocator()),
m_new_dt_eh(0) {
m_list = 0;
m_datatype_fid = m.get_family_id("datatype");
m_datatype_fid = m.mk_family_id("datatype");
}
pdecl_manager::~pdecl_manager() {

2
src/muz_qe/dl_bmc_engine.cpp
View file

@ -963,7 +963,7 @@ namespace datalog {
sort_ref_vector new_sorts(m);
family_id dfid = m.get_family_id("datatype");
family_id dfid = m.mk_family_id("datatype");
datatype_decl_plugin* dtp = static_cast<datatype_decl_plugin*>(m.get_plugin(dfid));
VERIFY (dtp->mk_datatypes(dts.size(), dts.c_ptr(), new_sorts));

2
src/muz_qe/dl_cmds.cpp
View file

@ -75,7 +75,7 @@ struct dl_context {
if (!m_decl_plugin) {
symbol name("datalog_relation");
if (m.has_plugin(name)) {
m_decl_plugin = static_cast<datalog::dl_decl_plugin*>(m_cmd.m().get_plugin(m.get_family_id(name)));
m_decl_plugin = static_cast<datalog::dl_decl_plugin*>(m_cmd.m().get_plugin(m.mk_family_id(name)));
}
else {
m_decl_plugin = alloc(datalog::dl_decl_plugin);

2
src/muz_qe/dl_rule.cpp
View file

@ -74,7 +74,7 @@ namespace datalog {
class remove_label_cfg : public default_rewriter_cfg {
family_id m_label_fid;
public:
remove_label_cfg(ast_manager& m): m_label_fid(m.get_family_id("label")) {}
remove_label_cfg(ast_manager& m): m_label_fid(m.get_label_family_id()) {}
virtual ~remove_label_cfg() {}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result,

2
src/muz_qe/proof_utils.cpp
View file

@ -450,7 +450,7 @@ static void permute_unit_resolution(expr_ref_vector& refs, obj_map<proof,proof*>
parameter const* params = thLemma->get_decl()->get_parameters();
unsigned num_params = thLemma->get_decl()->get_num_parameters();
SASSERT(params[0].is_symbol());
family_id tid = m.get_family_id(params[0].get_symbol());
family_id tid = m.mk_family_id(params[0].get_symbol());
SASSERT(tid != null_family_id);
prNew = m.mk_th_lemma(tid, m.get_fact(pr),
premises.size(), premises.c_ptr(), num_params-1, params+1);

4
src/muz_qe/qe_arith_plugin.cpp
View file

@ -1512,7 +1512,7 @@ public:
public:
arith_plugin(i_solver_context& ctx, ast_manager& m, smt_params& p):
qe_solver_plugin(m, m.get_family_id("arith"), ctx),
qe_solver_plugin(m, m.mk_family_id("arith"), ctx),
m_util(m, p, ctx),
m_trail(m)
{}
@ -2403,7 +2403,7 @@ public:
bool m_produce_models;
public:
nlarith_plugin(i_solver_context& ctx, ast_manager& m, bool produce_models) :
qe_solver_plugin(m, m.get_family_id("arith"), ctx),
qe_solver_plugin(m, m.mk_family_id("arith"), ctx),
m_rewriter(m),
m_util(m),
m_replacer(mk_default_expr_replacer(m)),

2
src/muz_qe/qe_array_plugin.cpp
View file

@ -16,7 +16,7 @@ namespace qe {
public:
array_plugin(i_solver_context& ctx, ast_manager& m) :
qe_solver_plugin(m, m.get_family_id("array"), ctx),
qe_solver_plugin(m, m.mk_family_id("array"), ctx),
m_replace(mk_default_expr_replacer(m))
{
}

2
src/muz_qe/qe_bv_plugin.cpp
View file

@ -32,7 +32,7 @@ namespace qe {
bv_util m_bv;
public:
bv_plugin(i_solver_context& ctx, ast_manager& m):
qe_solver_plugin(m, m.get_family_id("bv"), ctx),
qe_solver_plugin(m, m.mk_family_id("bv"), ctx),
m_replace(mk_default_expr_replacer(m)),
m_bv(m)
{}

2
src/muz_qe/qe_datatype_plugin.cpp
View file

@ -422,7 +422,7 @@ namespace qe {
public:
datatype_plugin(i_solver_context& ctx, ast_manager& m) :
qe_solver_plugin(m, m.get_family_id("datatype"), ctx),
qe_solver_plugin(m, m.mk_family_id("datatype"), ctx),
m_datatype_util(m),
m_replace(mk_default_expr_replacer(m)),
m_trail(m)

2
src/muz_qe/qe_dl_plugin.cpp
View file

@ -45,7 +45,7 @@ namespace qe {
public:
dl_plugin(i_solver_context& ctx, ast_manager& m) :
qe_solver_plugin(m, m.get_family_id("datalog_relation"), ctx),
qe_solver_plugin(m, m.mk_family_id("datalog_relation"), ctx),
m_replace(mk_default_expr_replacer(m)),
m_util(m),
m_trail(m)

12
src/parsers/smt/smtparser.cpp
View file

@ -483,13 +483,13 @@ public:
class array_sort : public builtin_sort_builder {
public:
array_sort(ast_manager& m) :
builtin_sort_builder(m, m.get_family_id("array"), ARRAY_SORT) {}
builtin_sort_builder(m, m.mk_family_id("array"), ARRAY_SORT) {}
};
class bv_sort : public builtin_sort_builder {
public:
bv_sort(ast_manager& m) :
builtin_sort_builder(m, m.get_family_id("bv"), BV_SORT) {}
builtin_sort_builder(m, m.mk_family_id("bv"), BV_SORT) {}
};
class user_sort : public sort_builder {
@ -538,7 +538,7 @@ class smtparser : public parser {
public:
add_plugins(ast_manager& m) {
#define REGISTER_PLUGIN(NAME, MK) { \
family_id fid = m.get_family_id(symbol(NAME)); \
family_id fid = m.mk_family_id(symbol(NAME)); \
if (!m.has_plugin(fid)) { \
m.register_plugin(fid, MK); \
} \
@ -681,7 +681,7 @@ public:
smtlib::symtable* table = m_benchmark.get_symtable();
symbol arith("arith");
family_id afid = m_manager.get_family_id(arith);
family_id afid = m_manager.mk_family_id(arith);
m_arith_fid = afid;
add_builtin_type("Int", afid, INT_SORT);
@ -694,7 +694,7 @@ public:
add_builtins(afid);
symbol bv("bv");
family_id bfid = m_manager.get_family_id(bv);
family_id bfid = m_manager.mk_family_id(bv);
m_bv_fid = bfid;
add_builtins(bfid);
@ -702,7 +702,7 @@ public:
add_builtin_type("BitVec", bfid, BV_SORT);
symbol array("array");
afid = m_manager.get_family_id(array);
afid = m_manager.mk_family_id(array);
m_array_fid = afid;
add_builtins(afid);

3
src/parsers/util/pattern_validation.h
View file

@ -32,11 +32,10 @@ class pattern_validator {
public:
pattern_validator(ast_manager const & m):
m_bfid(m.get_basic_family_id()),
m_lfid(m.get_family_id("label")) {
m_lfid(m.get_label_family_id()) {
}
bool operator()(unsigned num_bindings, unsigned num_new_bindings, expr * n);
bool operator()(unsigned num_new_bindings, expr * n) { return operator()(UINT_MAX, num_new_bindings, n); }
};

2
src/smt/proto_model/array_factory.cpp
View file

@ -34,7 +34,7 @@ func_decl * mk_aux_decl_for_array_sort(ast_manager & m, sort * s) {
}
array_factory::array_factory(ast_manager & m, proto_model & md):
struct_factory(m, m.get_family_id("array"), md) {
struct_factory(m, m.mk_family_id("array"), md) {
}
/**

2
src/smt/proto_model/datatype_factory.cpp
View file

@ -22,7 +22,7 @@ Revision History:
#include"ast_ll_pp.h"
datatype_factory::datatype_factory(ast_manager & m, proto_model & md):
struct_factory(m, m.get_family_id("datatype"), md),
struct_factory(m, m.mk_family_id("datatype"), md),
m_util(m) {
}

4
src/smt/proto_model/numeral_factory.cpp
View file

@ -24,7 +24,7 @@ app * arith_factory::mk_value_core(rational const & val, sort * s) {
}
arith_factory::arith_factory(ast_manager & m):
numeral_factory(m, m.get_family_id("arith")),
numeral_factory(m, m.mk_family_id("arith")),
m_util(m) {
}
@ -36,7 +36,7 @@ app * arith_factory::mk_value(rational const & val, bool is_int) {
}
bv_factory::bv_factory(ast_manager & m):
numeral_factory(m, m.get_family_id("bv")),
numeral_factory(m, m.mk_family_id("bv")),
m_util(m) {
}

2
src/smt/proto_model/proto_model.cpp
View file

@ -31,7 +31,7 @@ proto_model::proto_model(ast_manager & m, simplifier & s, params_ref const & p):
model_core(m),
m_asts(m),
m_simplifier(s),
m_afid(m.get_family_id(symbol("array"))) {
m_afid(m.mk_family_id(symbol("array"))) {
register_factory(alloc(basic_factory, m));
m_user_sort_factory = alloc(user_sort_factory, m);
register_factory(m_user_sort_factory);

2
src/smt/proto_model/value_factory.cpp
View file

@ -51,7 +51,7 @@ expr * basic_factory::get_fresh_value(sort * s) {
}
user_sort_factory::user_sort_factory(ast_manager & m):
simple_factory<unsigned>(m, m.get_family_id("user-sort")) {
simple_factory<unsigned>(m, m.mk_family_id("user-sort")) {
}
void user_sort_factory::freeze_universe(sort * s) {

4
src/smt/smt_model_finder.cpp
View file

@ -454,8 +454,8 @@ namespace smt {
m_model(0),
m_eval_cache_range(m),
m_new_constraints(0) {
m_asimp = static_cast<arith_simplifier_plugin*>(s.get_plugin(m.get_family_id("arith")));
m_bvsimp = static_cast<bv_simplifier_plugin*>(s.get_plugin(m.get_family_id("bv")));
m_asimp = static_cast<arith_simplifier_plugin*>(s.get_plugin(m.mk_family_id("arith")));
m_bvsimp = static_cast<bv_simplifier_plugin*>(s.get_plugin(m.mk_family_id("bv")));
}
~auf_solver() {

6
src/smt/smt_setup.cpp
View file

@ -692,7 +692,7 @@ namespace smt {
void setup::setup_arith() {
switch(m_params.m_arith_mode) {
case AS_NO_ARITH:
m_context.register_plugin(alloc(smt::theory_dummy, m_manager.get_family_id("arith"), "no arithmetic"));
m_context.register_plugin(alloc(smt::theory_dummy, m_manager.mk_family_id("arith"), "no arithmetic"));
break;
case AS_DIFF_LOGIC:
if (m_params.m_arith_fixnum) {
@ -734,7 +734,7 @@ namespace smt {
void setup::setup_bv() {
switch(m_params.m_bv_mode) {
case BS_NO_BV:
m_context.register_plugin(alloc(smt::theory_dummy, m_manager.get_family_id("bv"), "no bit-vector"));
m_context.register_plugin(alloc(smt::theory_dummy, m_manager.mk_family_id("bv"), "no bit-vector"));
break;
case BS_BLASTER:
m_context.register_plugin(alloc(smt::theory_bv, m_manager, m_params, m_params));
@ -745,7 +745,7 @@ namespace smt {
void setup::setup_arrays() {
switch(m_params.m_array_mode) {
case AR_NO_ARRAY:
m_context.register_plugin(alloc(smt::theory_dummy, m_manager.get_family_id("array"), "no array"));
m_context.register_plugin(alloc(smt::theory_dummy, m_manager.mk_family_id("array"), "no array"));
break;
case AR_SIMPLE:
m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params));

2
src/smt/theory_arith_core.h
View file

@ -1294,7 +1294,7 @@ namespace smt {
template<typename Ext>
theory_arith<Ext>::theory_arith(ast_manager & m, theory_arith_params & params):
theory(m.get_family_id("arith")),
theory(m.mk_family_id("arith")),
m_params(params),
m_util(m),
m_arith_eq_solver(m),

2
src/smt/theory_array_base.cpp
View file

@ -27,7 +27,7 @@ Revision History:
namespace smt {
theory_array_base::theory_array_base(ast_manager & m):
theory(m.get_family_id("array")),
theory(m.mk_family_id("array")),
m_found_unsupported_op(false)
{
}

2
src/smt/theory_bv.cpp
View file

@ -1239,7 +1239,7 @@ namespace smt {
}
theory_bv::theory_bv(ast_manager & m, theory_bv_params const & params, bit_blaster_params const & bb_params):
theory(m.get_family_id("bv")),
theory(m.mk_family_id("bv")),
m_params(params),
m_util(m),
m_autil(m),

2
src/smt/theory_datatype.cpp
View file

@ -454,7 +454,7 @@ namespace smt {
}
theory_datatype::theory_datatype(ast_manager & m, theory_datatype_params & p):
theory(m.get_family_id("datatype")),
theory(m.mk_family_id("datatype")),
m_params(p),
m_util(m),
m_find(*this),

2
src/smt/theory_dense_diff_logic_def.h
View file

@ -28,7 +28,7 @@ namespace smt {
template<typename Ext>
theory_dense_diff_logic<Ext>::theory_dense_diff_logic(ast_manager & m, theory_arith_params & p):
theory(m.get_family_id("arith")),
theory(m.mk_family_id("arith")),
m_params(p),
m_autil(m),
m_arith_eq_adapter(*this, p, m_autil),

2
src/smt/theory_diff_logic.h
View file

@ -306,7 +306,7 @@ namespace smt {
public:
theory_diff_logic(ast_manager& m, smt_params & params):
theory(m.get_family_id("arith")),
theory(m.mk_family_id("arith")),
m_params(params),
m_util(m),
m_arith_eq_adapter(*this, params, m_util),

4
src/smt/theory_dl.cpp
View file

@ -88,7 +88,7 @@ namespace smt {
m_th.get_rep(s, r, v);
app_ref rep_of(m_th.m());
rep_of = m_th.m().mk_app(r, m_node->get_owner());
theory_id bv_id = m_th.m().get_family_id("bv");
theory_id bv_id = m_th.m().mk_family_id("bv");
theory_bv* th_bv = dynamic_cast<theory_bv*>(ctx.get_theory(bv_id));
SASSERT(th_bv);
rational val;
@ -106,7 +106,7 @@ namespace smt {
public:
theory_dl(ast_manager& m):
theory(m.get_family_id("datalog_relation")),
theory(m.mk_family_id("datalog_relation")),
m_util(m),
m_bv(m),
m_trail(m)

2
src/smt/theory_seq_empty.h
View file

@ -32,7 +32,7 @@ namespace smt {
virtual theory* mk_fresh(context*) { return alloc(theory_seq_empty, get_manager()); }
virtual char const * get_name() const { return "seq-empty"; }
public:
theory_seq_empty(ast_manager& m):theory(m.get_family_id("seq")), m_used(false) {}
theory_seq_empty(ast_manager& m):theory(m.mk_family_id("seq")), m_used(false) {}
};
};

2
src/smt/user_plugin/user_smt_theory.cpp
View file

@ -646,7 +646,7 @@ namespace smt {
context & ctx = _s.get_context(); // HACK
symbol _name(name);
ast_manager & m = ctx.get_manager();
family_id fid = m.get_family_id(_name);
family_id fid = m.mk_family_id(_name);
user_decl_plugin * dp = alloc(user_decl_plugin);
m.register_plugin(fid, dp);
simplifier & s = ctx.get_simplifier();

2
src/tactic/fpa/fpa2bv_converter.cpp
View file

@ -32,7 +32,7 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
m_mpz_manager(m_mpf_manager.mpz_manager()),
m_bv_util(m),
extra_assertions(m) {
m_plugin = static_cast<float_decl_plugin*>(m.get_plugin(m.get_family_id("float")));
m_plugin = static_cast<float_decl_plugin*>(m.get_plugin(m.mk_family_id("float")));
}
fpa2bv_converter::~fpa2bv_converter() {

2
src/tactic/probe.cpp
View file

@ -326,7 +326,7 @@ class num_consts_probe : public probe {
unsigned m_counter;
proc(ast_manager & _m, bool b, char const * family):m(_m), m_bool(b), m_counter(0) {
if (family != 0)
m_fid = m.get_family_id(family);
m_fid = m.mk_family_id(family);
else
m_fid = null_family_id;
}

4
src/test/bv_simplifier_plugin.cpp
View file

@ -79,7 +79,7 @@ public:
m_arith(m_manager),
m_simp(m_manager, m_bsimp, m_bv_params),
m_bv_util(m_manager),
m_fid(m_manager.get_family_id("bv")) {
m_fid(m_manager.mk_family_id("bv")) {
reg_decl_plugins(m_manager);
}
@ -139,7 +139,7 @@ public:
m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e);
SASSERT(((a >> 8) | (a << 24)) == u32(e.get()));
params[0] = parameter(m_manager.mk_sort(m_manager.get_family_id("arith"), INT_SORT));
params[0] = parameter(m_manager.mk_sort(m_manager.mk_family_id("arith"), INT_SORT));
ar = m_manager.mk_app(m_fid, OP_BV2INT, 1, params, 1, es);
expr* es2[1] = { ar.get() };
params[0] = parameter(32);

4
src/test/expr_rand.cpp
View file

@ -18,7 +18,7 @@ void tst_expr_arith(unsigned num_files) {
er.seed(rand_seed);
er.initialize_arith(20);
family_id fid = m.get_family_id("arith");
family_id fid = m.mk_family_id("arith");
sort* int_ty = m.mk_sort(fid, INT_SORT, 0, 0);
sort* real_ty = m.mk_sort(fid, REAL_SORT, 0, 0);
@ -56,7 +56,7 @@ void tst_expr_rand(unsigned num_files) {
parameter p2(2);
parameter p8(8);
parameter p32(32);
family_id bvfid = m.get_family_id("bv");
family_id bvfid = m.mk_family_id("bv");
sort* bv1 = m.mk_sort(bvfid, BV_SORT, 1, &p1);
sort* bv2 = m.mk_sort(bvfid, BV_SORT, 1, &p2);
sort* bv8 = m.mk_sort(bvfid, BV_SORT, 1, &p8);

6
src/test/fuzzing/expr_rand.cpp
View file

@ -82,7 +82,7 @@ expr* expr_rand::choose_expr(sort* s) {
void expr_rand::initialize_arith(unsigned num_vars) {
arith_util u(m_manager);
family_id afid = m_manager.get_family_id("arith");
family_id afid = m_manager.mk_family_id("arith");
sort* i_ty = m_manager.mk_sort(afid, INT_SORT, 0, 0);
for(unsigned i = 0; i < num_vars; ++i) {
add_var(i_ty);
@ -106,7 +106,7 @@ void expr_rand::initialize_arith(unsigned num_vars) {
void expr_rand::initialize_bv(unsigned num_vars) {
bv_util u(m_manager);
family_id bfid = m_manager.get_basic_family_id();
family_id bvfid = m_manager.get_family_id("bv");
family_id bvfid = m_manager.mk_family_id("bv");
const unsigned num_sizes = 6;
@ -237,7 +237,7 @@ void expr_rand::initialize_bv(unsigned num_vars) {
}
void expr_rand::initialize_array(unsigned num_vars, sort* dom, sort* rng) {
family_id afid = m_manager.get_family_id("array");
family_id afid = m_manager.mk_family_id("array");
parameter p1(dom), p2(rng);
parameter ps[2] = { p1, p2 };
sort* a = m_manager.mk_sort(afid, ARRAY_SORT, 2, ps);

2
src/test/model_retrieval.cpp
View file

@ -18,7 +18,7 @@ void tst_model_retrieval()
ast_manager m;
reg_decl_plugins(m);
family_id array_fid = m.get_family_id(symbol("array"));
family_id array_fid = m.mk_family_id(symbol("array"));
array_util au(m);
// arr_s and select_fn creation copy-pasted from z3.cpp