3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00

Isolating reg_decl_plugins

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-24 11:27:50 -07:00
parent 69ce24a6ce
commit 641db30660
33 changed files with 140 additions and 70 deletions

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

@ -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() {}

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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