From d92efeb0c515eb03bb862d47f67774f4253d2925 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 18 Dec 2012 17:14:25 -0800 Subject: [PATCH] Make ast_manager::get_family_id(symbol const &) side-effect free. The version with side-effects is now called ast_manager::mk_family_id Signed-off-by: Leonardo de Moura --- src/api/api_context.cpp | 10 ++++----- src/ast/arith_decl_plugin.cpp | 2 +- src/ast/array_decl_plugin.cpp | 2 +- src/ast/ast.cpp | 28 +++++++++++++++--------- src/ast/ast.h | 24 +++++++++++++++----- src/ast/ast_smt_pp.cpp | 12 +++++----- src/ast/bv_decl_plugin.cpp | 8 +++---- src/ast/datatype_decl_plugin.cpp | 2 +- src/ast/decl_collector.cpp | 2 +- src/ast/dl_decl_plugin.cpp | 2 +- src/ast/float_decl_plugin.cpp | 6 ++--- src/ast/format.cpp | 2 +- src/ast/macros/macro_util.cpp | 4 ++-- src/ast/pattern/pattern_inference.cpp | 2 +- src/ast/pattern/pattern_inference.h | 2 +- src/ast/proof_checker/proof_checker.cpp | 2 +- src/ast/reg_decl_plugins.cpp | 14 ++++++------ src/ast/simplifier/bv_elim.cpp | 2 +- src/ast/simplifier/simplifier_plugin.h | 2 +- src/ast/static_features.cpp | 4 ++-- src/cmd_context/basic_cmds.cpp | 2 +- src/cmd_context/cmd_context.cpp | 2 +- src/cmd_context/pdecl.cpp | 2 +- src/muz_qe/dl_bmc_engine.cpp | 2 +- src/muz_qe/dl_cmds.cpp | 2 +- src/muz_qe/dl_rule.cpp | 2 +- src/muz_qe/proof_utils.cpp | 2 +- src/muz_qe/qe_arith_plugin.cpp | 4 ++-- src/muz_qe/qe_array_plugin.cpp | 2 +- src/muz_qe/qe_bv_plugin.cpp | 2 +- src/muz_qe/qe_datatype_plugin.cpp | 2 +- src/muz_qe/qe_dl_plugin.cpp | 2 +- src/parsers/smt/smtparser.cpp | 12 +++++----- src/parsers/util/pattern_validation.h | 3 +-- src/smt/proto_model/array_factory.cpp | 2 +- src/smt/proto_model/datatype_factory.cpp | 2 +- src/smt/proto_model/numeral_factory.cpp | 4 ++-- src/smt/proto_model/proto_model.cpp | 2 +- src/smt/proto_model/value_factory.cpp | 2 +- src/smt/smt_model_finder.cpp | 4 ++-- src/smt/smt_setup.cpp | 6 ++--- src/smt/theory_arith_core.h | 2 +- src/smt/theory_array_base.cpp | 2 +- src/smt/theory_bv.cpp | 2 +- src/smt/theory_datatype.cpp | 2 +- src/smt/theory_dense_diff_logic_def.h | 2 +- src/smt/theory_diff_logic.h | 2 +- src/smt/theory_dl.cpp | 4 ++-- src/smt/theory_seq_empty.h | 2 +- src/smt/user_plugin/user_smt_theory.cpp | 2 +- src/tactic/fpa/fpa2bv_converter.cpp | 2 +- src/tactic/probe.cpp | 2 +- src/test/bv_simplifier_plugin.cpp | 4 ++-- src/test/expr_rand.cpp | 4 ++-- src/test/fuzzing/expr_rand.cpp | 6 ++--- src/test/model_retrieval.cpp | 2 +- 56 files changed, 127 insertions(+), 108 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 7dc8d1a12..9ebc771f0 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -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(m().get_plugin(m_dt_fid)); if (!m_user_ref_count) { diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 093f6b346..f2dccf065 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -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) { } diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index be7bc6e2f..857cec105 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -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) { } diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 690c89229..486aa9646 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -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); } diff --git a/src/ast/ast.h b/src/ast/ast.h index 09784b301..3f03b86b9 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -188,10 +188,20 @@ class family_manager { svector 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& 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(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 & dom) const { m_family_manager.get_dom(dom); } diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 78a1caf68..66b467b92 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -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) {} diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 434bdaa11..9c5bccbc6 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -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(m.get_plugin(m.get_family_id("bv"))); + m_plugin = static_cast(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); } diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 5cf841b49..0714af28b 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -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) { } diff --git a/src/ast/decl_collector.cpp b/src/ast/decl_collector.cpp index a83bf6b99..b663a9df3 100644 --- a/src/ast/decl_collector.cpp +++ b/src/ast/decl_collector.cpp @@ -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) { diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp index 5b73f944a..8ac19c11c 100644 --- a/src/ast/dl_decl_plugin.cpp +++ b/src/ast/dl_decl_plugin.cpp @@ -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. diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index dbe7d5232..7f6d7f764 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -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(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(m.get_plugin(m_fid)); } diff --git a/src/ast/format.cpp b/src/ast/format.cpp index 68ba5ea9a..1a36ca8ae 100644 --- a/src/ast/format.cpp +++ b/src/ast/format.cpp @@ -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) { diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp index 86f30ed73..e9b9c831e 100644 --- a/src/ast/macros/macro_util.cpp +++ b/src/ast/macros/macro_util.cpp @@ -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(this)->m_arith_simp = static_cast(m_simplifier.get_plugin(m_manager.get_family_id("arith"))); + const_cast(this)->m_arith_simp = static_cast(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(this)->m_bv_simp = static_cast(m_simplifier.get_plugin(m_manager.get_family_id("bv"))); + const_cast(this)->m_bv_simp = static_cast(m_simplifier.get_plugin(m_manager.mk_family_id("bv"))); } SASSERT(m_bv_simp != 0); return m_bv_simp; diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp index 773b9a2f5..83362f5b3 100644 --- a/src/ast/pattern/pattern_inference.cpp +++ b/src/ast/pattern/pattern_inference.cpp @@ -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), diff --git a/src/ast/pattern/pattern_inference.h b/src/ast/pattern/pattern_inference.h index 1a179e794..97897835c 100644 --- a/src/ast/pattern/pattern_inference.h +++ b/src/ast/pattern/pattern_inference.h @@ -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); }; diff --git a/src/ast/proof_checker/proof_checker.cpp b/src/ast/proof_checker/proof_checker.cpp index 240504048..85e0cc791 100644 --- a/src/ast/proof_checker/proof_checker.cpp +++ b/src/ast/proof_checker/proof_checker.cpp @@ -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); } diff --git a/src/ast/reg_decl_plugins.cpp b/src/ast/reg_decl_plugins.cpp index fd4d49789..ab1844e07 100644 --- a/src/ast/reg_decl_plugins.cpp +++ b/src/ast/reg_decl_plugins.cpp @@ -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)); } } diff --git a/src/ast/simplifier/bv_elim.cpp b/src/ast/simplifier/bv_elim.cpp index 3238d13e7..5c19a245e 100644 --- a/src/ast/simplifier/bv_elim.cpp +++ b/src/ast/simplifier/bv_elim.cpp @@ -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 diff --git a/src/ast/simplifier/simplifier_plugin.h b/src/ast/simplifier/simplifier_plugin.h index d95547a69..8e176ea6e 100644 --- a/src/ast/simplifier/simplifier_plugin.h +++ b/src/ast/simplifier/simplifier_plugin.h @@ -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; } diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp index 234626365..f40eb2c75 100644 --- a/src/ast/static_features.cpp +++ b/src/ast/static_features.cpp @@ -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") { diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 8f65485ae..c1be7a69b 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -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; } diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 3f32c77d3..043dc45e6 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -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) diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index 6b55d4072..bafd76f0b 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -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() { diff --git a/src/muz_qe/dl_bmc_engine.cpp b/src/muz_qe/dl_bmc_engine.cpp index b5ffa808a..c7e53e581 100644 --- a/src/muz_qe/dl_bmc_engine.cpp +++ b/src/muz_qe/dl_bmc_engine.cpp @@ -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(m.get_plugin(dfid)); VERIFY (dtp->mk_datatypes(dts.size(), dts.c_ptr(), new_sorts)); diff --git a/src/muz_qe/dl_cmds.cpp b/src/muz_qe/dl_cmds.cpp index bf9c24203..c88e7346e 100644 --- a/src/muz_qe/dl_cmds.cpp +++ b/src/muz_qe/dl_cmds.cpp @@ -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(m_cmd.m().get_plugin(m.get_family_id(name))); + m_decl_plugin = static_cast(m_cmd.m().get_plugin(m.mk_family_id(name))); } else { m_decl_plugin = alloc(datalog::dl_decl_plugin); diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp index bd7131fea..d34f8a67f 100644 --- a/src/muz_qe/dl_rule.cpp +++ b/src/muz_qe/dl_rule.cpp @@ -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, diff --git a/src/muz_qe/proof_utils.cpp b/src/muz_qe/proof_utils.cpp index 1e837b578..e5a3ea437 100644 --- a/src/muz_qe/proof_utils.cpp +++ b/src/muz_qe/proof_utils.cpp @@ -450,7 +450,7 @@ static void permute_unit_resolution(expr_ref_vector& refs, obj_map 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); diff --git a/src/muz_qe/qe_arith_plugin.cpp b/src/muz_qe/qe_arith_plugin.cpp index 69c036639..4e158229b 100644 --- a/src/muz_qe/qe_arith_plugin.cpp +++ b/src/muz_qe/qe_arith_plugin.cpp @@ -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)), diff --git a/src/muz_qe/qe_array_plugin.cpp b/src/muz_qe/qe_array_plugin.cpp index c013f93f4..106a42338 100644 --- a/src/muz_qe/qe_array_plugin.cpp +++ b/src/muz_qe/qe_array_plugin.cpp @@ -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)) { } diff --git a/src/muz_qe/qe_bv_plugin.cpp b/src/muz_qe/qe_bv_plugin.cpp index 8712061d6..cae567111 100644 --- a/src/muz_qe/qe_bv_plugin.cpp +++ b/src/muz_qe/qe_bv_plugin.cpp @@ -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) {} diff --git a/src/muz_qe/qe_datatype_plugin.cpp b/src/muz_qe/qe_datatype_plugin.cpp index 3978a9ba4..0b51f26af 100644 --- a/src/muz_qe/qe_datatype_plugin.cpp +++ b/src/muz_qe/qe_datatype_plugin.cpp @@ -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) diff --git a/src/muz_qe/qe_dl_plugin.cpp b/src/muz_qe/qe_dl_plugin.cpp index 23f43759d..15e972e88 100644 --- a/src/muz_qe/qe_dl_plugin.cpp +++ b/src/muz_qe/qe_dl_plugin.cpp @@ -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) diff --git a/src/parsers/smt/smtparser.cpp b/src/parsers/smt/smtparser.cpp index d3b2feeb7..c1ebd251b 100644 --- a/src/parsers/smt/smtparser.cpp +++ b/src/parsers/smt/smtparser.cpp @@ -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); diff --git a/src/parsers/util/pattern_validation.h b/src/parsers/util/pattern_validation.h index d78502a8f..99024097e 100644 --- a/src/parsers/util/pattern_validation.h +++ b/src/parsers/util/pattern_validation.h @@ -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); } }; diff --git a/src/smt/proto_model/array_factory.cpp b/src/smt/proto_model/array_factory.cpp index b91857e40..a929f6d9a 100644 --- a/src/smt/proto_model/array_factory.cpp +++ b/src/smt/proto_model/array_factory.cpp @@ -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) { } /** diff --git a/src/smt/proto_model/datatype_factory.cpp b/src/smt/proto_model/datatype_factory.cpp index 0ea610869..5be802714 100644 --- a/src/smt/proto_model/datatype_factory.cpp +++ b/src/smt/proto_model/datatype_factory.cpp @@ -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) { } diff --git a/src/smt/proto_model/numeral_factory.cpp b/src/smt/proto_model/numeral_factory.cpp index 9653322e3..a67b6c075 100644 --- a/src/smt/proto_model/numeral_factory.cpp +++ b/src/smt/proto_model/numeral_factory.cpp @@ -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) { } diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index 92110bc1a..d7a06f14f 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -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); diff --git a/src/smt/proto_model/value_factory.cpp b/src/smt/proto_model/value_factory.cpp index 0b2aded9e..93294d898 100644 --- a/src/smt/proto_model/value_factory.cpp +++ b/src/smt/proto_model/value_factory.cpp @@ -51,7 +51,7 @@ expr * basic_factory::get_fresh_value(sort * s) { } user_sort_factory::user_sort_factory(ast_manager & m): - simple_factory(m, m.get_family_id("user-sort")) { + simple_factory(m, m.mk_family_id("user-sort")) { } void user_sort_factory::freeze_universe(sort * s) { diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 619a7d60c..e69b7a1b6 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -454,8 +454,8 @@ namespace smt { m_model(0), m_eval_cache_range(m), m_new_constraints(0) { - m_asimp = static_cast(s.get_plugin(m.get_family_id("arith"))); - m_bvsimp = static_cast(s.get_plugin(m.get_family_id("bv"))); + m_asimp = static_cast(s.get_plugin(m.mk_family_id("arith"))); + m_bvsimp = static_cast(s.get_plugin(m.mk_family_id("bv"))); } ~auf_solver() { diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index f0dc1f5a6..96673e67e 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -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)); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index b774fb3d9..fafe73a79 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -1294,7 +1294,7 @@ namespace smt { template theory_arith::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), diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index ca6449d1d..c2c50567f 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -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) { } diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index e425071d2..559ce155b 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -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), diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 65abfe238..8c6543eff 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -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), diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index 4d50bd8bf..21f1262ac 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -28,7 +28,7 @@ namespace smt { template theory_dense_diff_logic::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), diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h index 264ab9b2d..4140f683c 100644 --- a/src/smt/theory_diff_logic.h +++ b/src/smt/theory_diff_logic.h @@ -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), diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp index 402ab856c..758f78c2c 100644 --- a/src/smt/theory_dl.cpp +++ b/src/smt/theory_dl.cpp @@ -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(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) diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h index ef3924603..d5468df28 100644 --- a/src/smt/theory_seq_empty.h +++ b/src/smt/theory_seq_empty.h @@ -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) {} }; }; diff --git a/src/smt/user_plugin/user_smt_theory.cpp b/src/smt/user_plugin/user_smt_theory.cpp index ab4cc62c4..a2d1e4f37 100644 --- a/src/smt/user_plugin/user_smt_theory.cpp +++ b/src/smt/user_plugin/user_smt_theory.cpp @@ -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(); diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 8a4b31612..b53ad21eb 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -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(m.get_plugin(m.get_family_id("float"))); + m_plugin = static_cast(m.get_plugin(m.mk_family_id("float"))); } fpa2bv_converter::~fpa2bv_converter() { diff --git a/src/tactic/probe.cpp b/src/tactic/probe.cpp index 2940e93b9..1a696dc78 100644 --- a/src/tactic/probe.cpp +++ b/src/tactic/probe.cpp @@ -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; } diff --git a/src/test/bv_simplifier_plugin.cpp b/src/test/bv_simplifier_plugin.cpp index 4a472425e..635143021 100644 --- a/src/test/bv_simplifier_plugin.cpp +++ b/src/test/bv_simplifier_plugin.cpp @@ -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); diff --git a/src/test/expr_rand.cpp b/src/test/expr_rand.cpp index 1ceeba8b8..19a07e98a 100644 --- a/src/test/expr_rand.cpp +++ b/src/test/expr_rand.cpp @@ -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); diff --git a/src/test/fuzzing/expr_rand.cpp b/src/test/fuzzing/expr_rand.cpp index e1a7631c4..a2aca7e6e 100644 --- a/src/test/fuzzing/expr_rand.cpp +++ b/src/test/fuzzing/expr_rand.cpp @@ -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); diff --git a/src/test/model_retrieval.cpp b/src/test/model_retrieval.cpp index da6c3ddd0..f40f89d22 100644 --- a/src/test/model_retrieval.cpp +++ b/src/test/model_retrieval.cpp @@ -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