diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index d281af2bd..a6046a83e 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -26,6 +26,7 @@ Revision History:
#include"api_log_macros.h"
#include"api_util.h"
#include"install_tactics.h"
+#include"reg_decl_plugins.h"
namespace api {
@@ -60,7 +61,7 @@ namespace api {
}
context::add_plugins::add_plugins(ast_manager & m) {
- m.register_decl_plugins();
+ reg_decl_plugins(m);
}
// ------------------------
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 8e878165c..856060a52 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -25,13 +25,6 @@ Revision History:
#include"string_buffer.h"
#include"ast_util.h"
#include"ast_smt2_pp.h"
-#include"arith_decl_plugin.h"
-#include"array_decl_plugin.h"
-#include"bv_decl_plugin.h"
-#include"datatype_decl_plugin.h"
-#include"dl_decl_plugin.h"
-#include"seq_decl_plugin.h"
-#include"float_decl_plugin.h"
// -----------------------------------
//
@@ -1403,30 +1396,6 @@ void ast_manager::register_plugin(symbol const & s, decl_plugin * plugin) {
register_plugin(id, plugin);
}
-void ast_manager::register_decl_plugins() {
- if (!get_plugin(get_family_id(symbol("arith")))) {
- register_plugin(symbol("arith"), alloc(arith_decl_plugin));
- }
- if (!get_plugin(get_family_id(symbol("bv")))) {
- register_plugin(symbol("bv"), alloc(bv_decl_plugin));
- }
- if (!get_plugin(get_family_id(symbol("array")))) {
- register_plugin(symbol("array"), alloc(array_decl_plugin));
- }
- if (!get_plugin(get_family_id(symbol("datatype")))) {
- register_plugin(symbol("datatype"), alloc(datatype_decl_plugin));
- }
- if (!get_plugin(get_family_id(symbol("datalog_relation")))) {
- register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin));
- }
- if (!get_plugin(get_family_id(symbol("seq")))) {
- register_plugin(symbol("seq"), alloc(seq_decl_plugin));
- }
- if (!get_plugin(get_family_id(symbol("float")))) {
- register_plugin(symbol("float"), alloc(float_decl_plugin));
- }
-}
-
decl_plugin * ast_manager::get_plugin(family_id fid) const {
return m_plugins.get(fid, 0);
}
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 8de390ee0..17b4d2dac 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1283,8 +1283,6 @@ enum proof_gen_mode {
//
// -----------------------------------
-class arith_decl_plugin;
-
class ast_manager {
protected:
protected:
@@ -1411,8 +1409,6 @@ public:
void register_plugin(family_id id, decl_plugin * plugin);
- void register_decl_plugins();
-
decl_plugin * get_plugin(family_id fid) const;
bool has_plugin(family_id fid) const { return get_plugin(fid) != 0; }
diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp
index db1fbd1dc..76f34f316 100644
--- a/src/ast/dl_decl_plugin.cpp
+++ b/src/ast/dl_decl_plugin.cpp
@@ -23,6 +23,7 @@ Revision History:
#include "datatype_decl_plugin.h"
#include "dl_decl_plugin.h"
#include "warning.h"
+#include "reg_decl_plugins.h"
namespace datalog {
@@ -621,7 +622,7 @@ namespace datalog {
dl_decl_util::ast_plugin_registrator::ast_plugin_registrator(ast_manager& m)
{
// ensure required plugins are installed into the ast_manager
- m.register_decl_plugins();
+ reg_decl_plugins(m);
}
dl_decl_util::dl_decl_util(ast_manager& m):
diff --git a/src/ast/reg_decl_plugins.cpp b/src/ast/reg_decl_plugins.cpp
new file mode 100644
index 000000000..042d51e23
--- /dev/null
+++ b/src/ast/reg_decl_plugins.cpp
@@ -0,0 +1,51 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+ reg_decl_plugins
+
+Abstract:
+
+ Goodie for installing all available declarations
+ plugins in an ast_manager
+
+Author:
+
+ Leonardo de Moura (leonardo) 2012-10-24.
+
+Revision History:
+
+--*/
+#include"ast.h"
+#include"arith_decl_plugin.h"
+#include"array_decl_plugin.h"
+#include"bv_decl_plugin.h"
+#include"datatype_decl_plugin.h"
+#include"dl_decl_plugin.h"
+#include"seq_decl_plugin.h"
+#include"float_decl_plugin.h"
+
+void reg_decl_plugins(ast_manager & m) {
+ if (!get_plugin(get_family_id(symbol("arith")))) {
+ register_plugin(symbol("arith"), alloc(arith_decl_plugin));
+ }
+ if (!get_plugin(get_family_id(symbol("bv")))) {
+ register_plugin(symbol("bv"), alloc(bv_decl_plugin));
+ }
+ if (!get_plugin(get_family_id(symbol("array")))) {
+ register_plugin(symbol("array"), alloc(array_decl_plugin));
+ }
+ if (!get_plugin(get_family_id(symbol("datatype")))) {
+ register_plugin(symbol("datatype"), alloc(datatype_decl_plugin));
+ }
+ if (!get_plugin(get_family_id(symbol("datalog_relation")))) {
+ register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin));
+ }
+ if (!get_plugin(get_family_id(symbol("seq")))) {
+ register_plugin(symbol("seq"), alloc(seq_decl_plugin));
+ }
+ if (!get_plugin(get_family_id(symbol("float")))) {
+ register_plugin(symbol("float"), alloc(float_decl_plugin));
+ }
+}
diff --git a/src/ast/reg_decl_plugins.h b/src/ast/reg_decl_plugins.h
new file mode 100644
index 000000000..57185181e
--- /dev/null
+++ b/src/ast/reg_decl_plugins.h
@@ -0,0 +1,27 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+ reg_decl_plugins
+
+Abstract:
+
+ Goodie for installing all available declarations
+ plugins in an ast_manager
+
+Author:
+
+ Leonardo de Moura (leonardo) 2012-10-24.
+
+Revision History:
+
+--*/
+#ifndef _REG_DECL_PLUGINS_H_
+#define _REG_DECL_PLUGINS_H_
+
+class ast_manager;
+
+void reg_decl_plugins(ast_manager & m);
+
+#endif
diff --git a/src/muz_qe/pdr_farkas_learner.cpp b/src/muz_qe/pdr_farkas_learner.cpp
index 1dd46cbdf..00bb5d723 100644
--- a/src/muz_qe/pdr_farkas_learner.cpp
+++ b/src/muz_qe/pdr_farkas_learner.cpp
@@ -33,6 +33,7 @@ Revision History:
#include "ast_ll_pp.h"
#include "arith_bounds_tactic.h"
#include "proof_utils.h"
+#include "reg_decl_plugins.h"
#define PROOF_MODE PGM_FINE
//#define PROOF_MODE PGM_COARSE
@@ -249,7 +250,7 @@ namespace pdr {
p2o(m_pr, outer_mgr),
o2p(outer_mgr, m_pr)
{
- m_pr.register_decl_plugins();
+ reg_decl_plugins(m_pr);
m_ctx = alloc(smt::solver, m_pr, m_proof_params);
}
@@ -800,7 +801,7 @@ namespace pdr {
bool res;
ast_manager m;
- m.register_decl_plugins();
+ reg_decl_plugins(m);
arith_util a(m);
pdr::farkas_learner fl(params, m);
expr_ref_vector lemmas(m);
@@ -864,7 +865,7 @@ namespace pdr {
return;
}
ast_manager m;
- m.register_decl_plugins();
+ reg_decl_plugins(m);
scoped_ptr<smtlib::parser> p = smtlib::parser::create(m);
p->initialize_smtlib();
diff --git a/src/smt/default_solver.cpp b/src/smt/default_solver.cpp
index 16db274e9..ad611763b 100644
--- a/src/smt/default_solver.cpp
+++ b/src/smt/default_solver.cpp
@@ -18,6 +18,7 @@ Notes:
--*/
#include"solver.h"
#include"smt_solver.h"
+#include"reg_decl_plugins.h"
class default_solver : public solver {
front_end_params * m_params;
@@ -43,7 +44,7 @@ public:
virtual void collect_param_descrs(param_descrs & r) {
if (m_context == 0) {
ast_manager m;
- m.register_decl_plugins();
+ reg_decl_plugins(m);
front_end_params p;
smt::solver s(m, p);
s.collect_param_descrs(r);
diff --git a/src/test/arith_rewriter.cpp b/src/test/arith_rewriter.cpp
index 04b018646..0933e9d11 100644
--- a/src/test/arith_rewriter.cpp
+++ b/src/test/arith_rewriter.cpp
@@ -1,10 +1,11 @@
#include "arith_rewriter.h"
#include "bv_decl_plugin.h"
#include "ast_pp.h"
+#include "reg_decl_plugins.h"
void tst_arith_rewriter() {
ast_manager m;
- m.register_decl_plugins();
+ reg_decl_plugins(m);
arith_rewriter ar(m);
arith_util au(m);
expr_ref t1(m), t2(m), result(m);
diff --git a/src/test/bv_simplifier_plugin.cpp b/src/test/bv_simplifier_plugin.cpp
index 9c9a7100b..271d1a534 100644
--- a/src/test/bv_simplifier_plugin.cpp
+++ b/src/test/bv_simplifier_plugin.cpp
@@ -1,6 +1,7 @@
#include "bv_simplifier_plugin.h"
#include "arith_decl_plugin.h"
#include "ast_pp.h"
+#include "reg_decl_plugins.h"
class tst_bv_simplifier_plugin_cls {
ast_manager m_manager;
@@ -79,7 +80,7 @@ public:
m_arith(m_manager),
m_simp(m_manager, m_bsimp, m_bv_params),
m_fid(m_manager.get_family_id("bv")) {
- m_manager.register_decl_plugins();
+ reg_decl_plugins(m_manager);
}
~tst_bv_simplifier_plugin_cls() {}
diff --git a/src/test/check_assumptions.cpp b/src/test/check_assumptions.cpp
index dce982345..033e3fdc9 100644
--- a/src/test/check_assumptions.cpp
+++ b/src/test/check_assumptions.cpp
@@ -4,13 +4,14 @@
#include "arith_decl_plugin.h"
#include "bv_decl_plugin.h"
#include "smt_context.h"
+#include "reg_decl_plugins.h"
void tst_check_assumptions()
{
memory::initialize(0);
front_end_params params;
ast_manager mgr;
- mgr.register_decl_plugins();
+ reg_decl_plugins(mgr);
sort_ref b(mgr.mk_bool_sort(), mgr);
func_decl_ref pPred(mgr.mk_func_decl(symbol("p"), 0, static_cast<sort * const *>(0), b), mgr);
diff --git a/src/test/datalog_parser.cpp b/src/test/datalog_parser.cpp
index 489808aba..2d8a04225 100644
--- a/src/test/datalog_parser.cpp
+++ b/src/test/datalog_parser.cpp
@@ -3,6 +3,7 @@
#include "arith_decl_plugin.h"
#include "dl_context.h"
#include "front_end_params.h"
+#include "reg_decl_plugins.h"
using namespace datalog;
@@ -10,7 +11,7 @@ using namespace datalog;
static void dparse_string(char const* str) {
ast_manager m;
front_end_params params;
- m.register_decl_plugins();
+ reg_decl_plugins(m);
context ctx(m, params);
parser* p = parser::create(ctx,m);
@@ -37,7 +38,7 @@ static void dparse_string(char const* str) {
static void dparse_file(char const* file) {
ast_manager m;
front_end_params params;
- m.register_decl_plugins();
+ reg_decl_plugins(m);
context ctx(m, params);
parser* p = parser::create(ctx,m);
diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp
index 9d99c6ee6..469797bf0 100644
--- a/src/test/dl_query.cpp
+++ b/src/test/dl_query.cpp
@@ -3,7 +3,8 @@
#include "dl_table_relation.h"
#include "dl_context.h"
#include "front_end_params.h"
-#include"stopwatch.h"
+#include "stopwatch.h"
+#include "reg_decl_plugins.h"
using namespace datalog;
@@ -127,7 +128,7 @@ void dl_query_test(ast_manager & m, front_end_params & fparams, params_ref& para
void dl_query_test_wpa(front_end_params & fparams, params_ref& params) {
params.set_bool(":magic-sets-for-queries", true);
ast_manager m;
- m.register_decl_plugins();
+ reg_decl_plugins(m);
arith_util arith(m);
const char * problem_dir = "C:\\tvm\\src\\z3_2\\debug\\test\\w0.datalog";
dl_decl_util dl_util(m);
diff --git a/src/test/dl_smt_relation.cpp b/src/test/dl_smt_relation.cpp
index bf34688ea..0a473a7f9 100644
--- a/src/test/dl_smt_relation.cpp
+++ b/src/test/dl_smt_relation.cpp
@@ -3,13 +3,14 @@
#include "dl_context.h"
#include "z3.h"
#include "z3_private.h"
+#include "reg_decl_plugins.h"
namespace datalog {
void test_smt_relation_unit() {
ast_manager m;
- m.register_decl_plugins();
+ reg_decl_plugins(m);
arith_util a(m);
sort* int_sort = a.mk_int();
sort* real_sort = a.mk_real();
diff --git a/src/test/expr_context_simplifier.cpp b/src/test/expr_context_simplifier.cpp
index 91bd29ca7..1ff4944d8 100644
--- a/src/test/expr_context_simplifier.cpp
+++ b/src/test/expr_context_simplifier.cpp
@@ -1,6 +1,7 @@
#include "expr_context_simplifier.h"
#include "smtparser.h"
#include "ast_pp.h"
+#include "reg_decl_plugins.h"
static void simplify_formula(ast_manager& m, expr* e) {
expr_ref result(m);
@@ -19,7 +20,7 @@ void tst_expr_context_simplifier() {
ast_manager m;
smtlib::parser* parser = smtlib::parser::create(m);
- m.register_decl_plugins();
+ reg_decl_plugins(m);
parser->initialize_smtlib();
diff --git a/src/test/expr_pattern_match.cpp b/src/test/expr_pattern_match.cpp
index 4e1fef1ed..e7088913e 100644
--- a/src/test/expr_pattern_match.cpp
+++ b/src/test/expr_pattern_match.cpp
@@ -4,10 +4,11 @@
#include "arith_decl_plugin.h"
#include "bv_decl_plugin.h"
#include "array_decl_plugin.h"
+#include "reg_decl_plugins.h"
void tst_expr_pattern_match() {
ast_manager manager;
- manager.register_decl_plugins();
+ reg_decl_plugins(manager);
expr_pattern_match apm(manager);
diff --git a/src/test/expr_rand.cpp b/src/test/expr_rand.cpp
index fec4e5d3f..1ceeba8b8 100644
--- a/src/test/expr_rand.cpp
+++ b/src/test/expr_rand.cpp
@@ -6,12 +6,13 @@
#include "ast_smt_pp.h"
#include <iostream>
#include <sstream>
+#include "reg_decl_plugins.h"
static unsigned rand_seed = 1;
void tst_expr_arith(unsigned num_files) {
ast_manager m;
- m.register_decl_plugins();
+ reg_decl_plugins(m);
expr_rand er(m);
er.seed(rand_seed);
diff --git a/src/test/factor_rewriter.cpp b/src/test/factor_rewriter.cpp
index 110df86a3..625710fe1 100644
--- a/src/test/factor_rewriter.cpp
+++ b/src/test/factor_rewriter.cpp
@@ -1,10 +1,11 @@
#include "factor_rewriter.h"
#include "bv_decl_plugin.h"
#include "ast_pp.h"
+#include "reg_decl_plugins.h"
void tst_factor_rewriter() {
ast_manager m;
- m.register_decl_plugins();
+ reg_decl_plugins(m);
factor_rewriter_star fw(m);
arith_util a(m);
diff --git a/src/test/grobner.cpp b/src/test/grobner.cpp
index 92ba2c854..89aea5049 100644
--- a/src/test/grobner.cpp
+++ b/src/test/grobner.cpp
@@ -24,6 +24,7 @@ Revision History:
#include"arith_simplifier_plugin.h"
#include"front_end_params.h"
#include"grobner.h"
+#include"reg_decl_plugins.h"
void display_eqs(grobner & gb, v_dependency_manager & dep_m) {
std::cerr << "RESULT:\n";
@@ -55,7 +56,7 @@ void tst_grobner(char ** argv, int argc, int & i) {
ast_manager m;
smtlib::parser* parser = smtlib::parser::create(m);
- m.register_decl_plugins();
+ reg_decl_plugins(m);
parser->initialize_smtlib();
if (!parser->parse_file(file_path)) {
diff --git a/src/test/horn_subsume_model_converter.cpp b/src/test/horn_subsume_model_converter.cpp
index c99a50c87..28359b954 100644
--- a/src/test/horn_subsume_model_converter.cpp
+++ b/src/test/horn_subsume_model_converter.cpp
@@ -2,10 +2,11 @@
#include "horn_subsume_model_converter.h"
#include "arith_decl_plugin.h"
#include "model_smt2_pp.h"
+#include "reg_decl_plugins.h"
void tst_horn_subsume_model_converter() {
ast_manager m;
- m.register_decl_plugins();
+ reg_decl_plugins(m);
arith_util a(m);
ptr_vector<sort> ints;
diff --git a/src/test/model2expr.cpp b/src/test/model2expr.cpp
index 3040ddadc..abca706c1 100644
--- a/src/test/model2expr.cpp
+++ b/src/test/model2expr.cpp
@@ -2,10 +2,11 @@
#include "ast_pp.h"
#include "arith_decl_plugin.h"
#include "model_smt2_pp.h"
+#include "reg_decl_plugins.h"
void tst_model2expr() {
ast_manager m;
- m.register_decl_plugins();
+ reg_decl_plugins(m);
arith_util a(m);
ptr_vector<sort> ints;
diff --git a/src/test/model_retrieval.cpp b/src/test/model_retrieval.cpp
index 96d956b0e..2fa1cb24f 100644
--- a/src/test/model_retrieval.cpp
+++ b/src/test/model_retrieval.cpp
@@ -6,6 +6,7 @@
#include "bv_decl_plugin.h"
#include "array_decl_plugin.h"
#include "model_v2_pp.h"
+#include "reg_decl_plugins.h"
void tst_model_retrieval()
{
@@ -15,7 +16,7 @@ void tst_model_retrieval()
ast_manager m;
- m.register_decl_plugins();
+ reg_decl_plugins(m);
family_id array_fid = m.get_family_id(symbol("array"));
array_util au(m);
diff --git a/src/test/nlarith_util.cpp b/src/test/nlarith_util.cpp
index 87d5f9594..f08fa020e 100644
--- a/src/test/nlarith_util.cpp
+++ b/src/test/nlarith_util.cpp
@@ -1,10 +1,11 @@
#include "nlarith_util.h"
#include "arith_decl_plugin.h"
#include "ast_pp.h"
+#include "reg_decl_plugins.h"
void tst_nlarith_util() {
ast_manager M;
- M.register_decl_plugins();
+ reg_decl_plugins(M);
arith_util A(M);
sort_ref R(A.mk_real(), M);
app_ref one(A.mk_numeral(rational(1), false), M);
diff --git a/src/test/qe_defs.cpp b/src/test/qe_defs.cpp
index 0620a3b59..d1c8232d8 100644
--- a/src/test/qe_defs.cpp
+++ b/src/test/qe_defs.cpp
@@ -2,6 +2,7 @@
#include "qe.h"
#include "ast_pp.h"
#include "smtparser.h"
+#include "reg_decl_plugins.h"
static void test_defs(ast_manager& m, expr* _fml) {
@@ -48,7 +49,7 @@ static void test_defs_all(ast_manager& m, expr* _fml) {
static void test_defs(char const* str) {
ast_manager m;
- m.register_decl_plugins();
+ reg_decl_plugins(m);
scoped_ptr<smtlib::parser> parser = smtlib::parser::create(m);
parser->initialize_smtlib();
std::ostringstream buffer;
diff --git a/src/test/quant_elim.cpp b/src/test/quant_elim.cpp
index 0947b5583..3e8e8b16f 100644
--- a/src/test/quant_elim.cpp
+++ b/src/test/quant_elim.cpp
@@ -11,6 +11,7 @@
#include "smtparser.h"
#include "lbool.h"
#include <sstream>
+#include "reg_decl_plugins.h"
static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char const* option) {
@@ -52,7 +53,7 @@ static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char cons
static void test_formula(lbool expected_outcome, char const* fml) {
ast_manager m;
- m.register_decl_plugins();
+ reg_decl_plugins(m);
scoped_ptr<smtlib::parser> parser = smtlib::parser::create(m);
parser->initialize_smtlib();
diff --git a/src/test/quant_solve.cpp b/src/test/quant_solve.cpp
index 096ae33de..003ae26b4 100644
--- a/src/test/quant_solve.cpp
+++ b/src/test/quant_solve.cpp
@@ -7,6 +7,7 @@
#include <sstream>
#include "expr_replacer.h"
#include "smt_solver.h"
+#include "reg_decl_plugins.h"
static void validate_quant_solution(ast_manager& m, app* x, expr* fml, expr* t, expr* new_fml) {
// verify:
@@ -86,7 +87,7 @@ static void test_quant_solve1() {
ast_manager m;
arith_util ar(m);
- m.register_decl_plugins();
+ reg_decl_plugins(m);
sort* i = ar.mk_int();
app_ref x(m.mk_const(symbol("x"),i), m);
app_ref y(m.mk_const(symbol("y"),i), m);
diff --git a/src/test/simple_parser.cpp b/src/test/simple_parser.cpp
index 189fcd2cf..a5d4d8def 100644
--- a/src/test/simple_parser.cpp
+++ b/src/test/simple_parser.cpp
@@ -22,10 +22,11 @@ Revision History:
#include"ast_pp.h"
#include"well_sorted.h"
#include"warning.h"
+#include"reg_decl_plugins.h"
void tst_simple_parser() {
ast_manager m;
- m.register_decl_plugins();
+ reg_decl_plugins(m);
arith_util m_util(m);
cost_parser p(m);
var_ref_vector vs(m);
diff --git a/src/test/smt_context.cpp b/src/test/smt_context.cpp
index 48ac71077..853bde068 100644
--- a/src/test/smt_context.cpp
+++ b/src/test/smt_context.cpp
@@ -1,11 +1,12 @@
#include "smt_context.h"
+#include "reg_decl_plugins.h"
void tst_smt_context()
{
front_end_params params;
ast_manager m;
- m.register_decl_plugins();
+ reg_decl_plugins(m);
smt::context ctx(m, params);
diff --git a/src/test/smtparser.cpp b/src/test/smtparser.cpp
index 6aa6f0e06..dc4f0eb74 100644
--- a/src/test/smtparser.cpp
+++ b/src/test/smtparser.cpp
@@ -7,7 +7,7 @@
#include "for_each_file.h"
#include "array_decl_plugin.h"
#include "bv_decl_plugin.h"
-
+#include "reg_decl_plugins.h"
class for_each_file_smt : public for_each_file_proc {
public:
@@ -19,7 +19,7 @@ public:
ast_manager ast_manager;
smtlib::parser* parser = smtlib::parser::create(ast_manager);
- ast_manager.register_decl_plugins();
+ reg_decl_plugins(ast_manager);
parser->initialize_smtlib();
diff --git a/src/test/substitution.cpp b/src/test/substitution.cpp
index 80549c72d..38f85bb11 100644
--- a/src/test/substitution.cpp
+++ b/src/test/substitution.cpp
@@ -5,7 +5,7 @@
#include "bv_decl_plugin.h"
#include "ast_pp.h"
#include "arith_decl_plugin.h"
-
+#include "reg_decl_plugins.h"
void tst_substitution()
{
@@ -16,7 +16,7 @@ void tst_substitution()
enable_trace("subst_bug");
ast_manager m;
- m.register_decl_plugins();
+ reg_decl_plugins(m);
var_ref v1(m.mk_var(0, m.mk_bool_sort()), m);
var_ref v2(m.mk_var(1, m.mk_bool_sort()), m);
diff --git a/src/test/symmetry.cpp b/src/test/symmetry.cpp
index ff0a84dff..d296a346c 100644
--- a/src/test/symmetry.cpp
+++ b/src/test/symmetry.cpp
@@ -5,6 +5,7 @@
#include "nat_set.h"
#include "stream_buffer.h"
#include "obj_hashtable.h"
+#include "reg_decl_plugins.h"
class partition {
public:
@@ -723,7 +724,7 @@ public:
void parse_file(char const* file_path, char const* file_tmp) {
smtlib::parser* parser = smtlib::parser::create(m_mgr);
- m_mgr.register_decl_plugins();
+ reg_decl_plugins(m_mgr);
parser->initialize_smtlib();
if (!parser->parse_file(file_path)) {
diff --git a/src/test/theory_dl.cpp b/src/test/theory_dl.cpp
index 9d5796963..d07ec34af 100644
--- a/src/test/theory_dl.cpp
+++ b/src/test/theory_dl.cpp
@@ -2,6 +2,7 @@
#include "dl_decl_plugin.h"
#include "ast_pp.h"
#include "model_v2_pp.h"
+#include "reg_decl_plugins.h"
void tst_theory_dl() {
ast_manager m;
@@ -9,7 +10,7 @@ void tst_theory_dl() {
params.m_model = true;
datalog::dl_decl_util u(m);
smt::context ctx(m, params);
- m.register_decl_plugins();
+ reg_decl_plugins(m);
expr_ref a(m), b(m), c(m);
sort_ref s(m);
s = u.mk_sort(symbol("S"),111);
diff --git a/src/test/var_subst.cpp b/src/test/var_subst.cpp
index ec8078025..efc4555fe 100644
--- a/src/test/var_subst.cpp
+++ b/src/test/var_subst.cpp
@@ -23,6 +23,7 @@ Revision History:
#include"bv_decl_plugin.h"
#include"array_decl_plugin.h"
#include"for_each_expr.h"
+#include"reg_decl_plugins.h"
namespace find_q {
struct proc {
@@ -101,7 +102,7 @@ void tst_subst(ast_manager& m) {
void tst_var_subst() {
ast_manager m;
- m.register_decl_plugins();
+ reg_decl_plugins(m);
tst_subst(m);
scoped_ptr<smtlib::parser> parser = smtlib::parser::create(m);