mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

added method for creating ast_manager based on context_params configuration

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-09 14:24:37 -08:00
parent 84e79035cb
commit 9b7946e52d
9 changed files with 51 additions and 41 deletions
Download patch file Download diff file Expand all files Collapse all files

44
src/api/api_context.cpp
View file

@ -82,13 +82,13 @@ namespace api {
context::context(context_params * p, bool user_ref_count):
m_params(p != 0 ? *p : context_params()),
m_user_ref_count(user_ref_count),
m_manager(m_params.m_proof ? PGM_FINE : PGM_DISABLED, m_params.m_trace ? m_params.m_trace_file_name.c_str() : 0),
m_plugins(m_manager),
m_arith_util(m_manager),
m_bv_util(m_manager),
m_datalog_util(m_manager),
m_last_result(m_manager),
m_ast_trail(m_manager),
m_manager(m_params.mk_ast_manager()),
m_plugins(m()),
m_arith_util(m()),
m_bv_util(m()),
m_datalog_util(m()),
m_last_result(m()),
m_ast_trail(m()),
m_replay_stack() {
m_solver = 0;
@ -102,22 +102,16 @@ namespace api {
m_smtlib_parser_has_decls = false;
z3_bound_num_procs();
//
// Configuration parameter settings.
//
if (m_params.m_debug_ref_count) {
m_manager.debug_ref_count();
}
m_error_handler = &default_error_handler;
m_basic_fid = m_manager.get_basic_family_id();
m_arith_fid = m_manager.get_family_id("arith");
m_bv_fid = m_manager.get_family_id("bv");
m_array_fid = m_manager.get_family_id("array");
m_dt_fid = m_manager.get_family_id("datatype");
m_datalog_fid = m_manager.get_family_id("datalog_relation");
m_dt_plugin = static_cast<datatype_decl_plugin*>(m_manager.get_plugin(m_dt_fid));
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_dt_plugin = static_cast<datatype_decl_plugin*>(m().get_plugin(m_dt_fid));
if (!m_user_ref_count) {
m_replay_stack.push_back(0);
@ -143,7 +137,7 @@ namespace api {
{
if (m_interruptable)
(*m_interruptable)();
m_manager.set_cancel(true);
m().set_cancel(true);
}
}
@ -196,12 +190,12 @@ namespace api {
expr * context::mk_and(unsigned num_exprs, expr * const * exprs) {
switch(num_exprs) {
case 0:
return m_manager.mk_true();
return m().mk_true();
case 1:
save_ast_trail(exprs[0]);
return exprs[0];
default: {
expr * a = m_manager.mk_and(num_exprs, exprs);
expr * a = m().mk_and(num_exprs, exprs);
save_ast_trail(a);
return a;
} }
@ -217,7 +211,7 @@ namespace api {
SASSERT(m_replay_stack.size() > num_scopes);
unsigned j = m_replay_stack.size() - num_scopes - 1;
if (!m_replay_stack[j]) {
m_replay_stack[j] = alloc(ast_ref_vector, m_manager);
m_replay_stack[j] = alloc(ast_ref_vector, m());
}
m_replay_stack[j]->push_back(n);
}
@ -325,7 +319,7 @@ namespace api {
smt::kernel & context::get_smt_kernel() {
if (!m_solver) {
m_fparams.updt_params(m_params);
m_solver = alloc(smt::kernel, m_manager, m_fparams);
m_solver = alloc(smt::kernel, m(), m_fparams);
}
return *m_solver;
}

6
src/api/api_context.h
View file

@ -46,7 +46,7 @@ namespace api {
struct add_plugins { add_plugins(ast_manager & m); };
context_params m_params;
bool m_user_ref_count; //!< if true, the user is responsible for managing referenc counters.
ast_manager m_manager;
scoped_ptr<ast_manager> m_manager;
add_plugins m_plugins;
arith_util m_arith_util;
@ -101,10 +101,10 @@ namespace api {
context(context_params * p, bool user_ref_count = false);
~context();
ast_manager & m() { return m_manager; }
ast_manager & m() const { return *(m_manager.get()); }
context_params & params() { return m_params; }
bool produce_proofs() const { return m_manager.proofs_enabled(); }
bool produce_proofs() const { return m().proofs_enabled(); }
bool produce_models() const { return m_params.m_model; }
bool produce_unsat_cores() const { return m_params.m_unsat_core; }
bool use_auto_config() const { return m_params.m_auto_config; }

7
src/cmd_context/cmd_context.cpp
View file

@ -592,14 +592,9 @@ void cmd_context::init_manager() {
SASSERT(m_manager == 0);
SASSERT(m_pmanager == 0);
m_check_sat_result = 0;
m_manager = alloc(ast_manager,
produce_proofs() ? PGM_FINE : PGM_DISABLED,
m_params.m_trace ? m_params.m_trace_file_name.c_str() : 0);
m_manager = m_params.mk_ast_manager();
m_pmanager = alloc(pdecl_manager, *m_manager);
init_manager_core(true);
// PARAM-TODO
// if (params().m_smtlib2_compliant)
// m_manager->enable_int_real_coercions(false);
}
void cmd_context::init_external_manager() {

16
src/cmd_context/context_params.cpp
View file

@ -79,6 +79,9 @@ void context_params::set(char const * param, char const * value) {
else if (p == "debug_ref_count") {
set_bool(m_debug_ref_count, param, value);
}
else if (p == "smtlib2_compliant") {
set_bool(m_smtlib2_compliant, param, value);
}
else {
throw default_exception("unknown parameter '%s'", p.c_str());
}
@ -99,6 +102,7 @@ void context_params::updt_params(params_ref const & p) {
m_trace_file_name = p.get_str("trace_file_name", "z3.log");
m_unsat_core = p.get_bool("unsat_core", false);
m_debug_ref_count = p.get_bool("debug_ref_count", false);
m_smtlib2_compliant = p.get_bool("smtlib2_compliant", false);
}
void context_params::collect_param_descrs(param_descrs & d) {
@ -113,6 +117,7 @@ void context_params::collect_param_descrs(param_descrs & d) {
d.insert("trace_file_name", CPK_STRING, "trace out file name (see option 'trace')", "z3.log");
d.insert("unsat_core", CPK_BOOL, "unsat-core generation for solvers, this parameter can be overwritten when creating a solver, not every solver in Z3 supports unsat core generation", "false");
d.insert("debug_ref_count", CPK_BOOL, "debug support for AST reference counting", "false");
d.insert("smtlib2_compliant", CPK_BOOL, "enable/disable SMT-LIB 2.0 compliance", "false");
}
params_ref context_params::merge_default_params(params_ref const & p) {
@ -133,4 +138,15 @@ void context_params::init_solver_params(ast_manager & m, solver & s, params_ref
s.updt_params(merge_default_params(p));
}
ast_manager * context_params::mk_ast_manager() {
ast_manager * r = alloc(ast_manager,
m_proof ? PGM_FINE : PGM_DISABLED,
m_trace ? m_trace_file_name.c_str() : 0);
if (m_smtlib2_compliant)
r->enable_int_real_coercions(false);
if (m_debug_ref_count)
r->debug_ref_count();
return r;
}

6
src/cmd_context/context_params.h
View file

@ -37,6 +37,7 @@ public:
bool m_model;
bool m_model_validate;
bool m_unsat_core;
bool m_smtlib2_compliant; // it must be here because it enable/disable the use of coercions in the ast_manager.
unsigned m_timeout;
context_params();
@ -63,6 +64,11 @@ public:
Example: auto_config
*/
params_ref merge_default_params(params_ref const & p);
/**
\brief Create an AST manager using this configuration.
*/
ast_manager * mk_ast_manager();
};

2
src/parsers/smt2/smt2parser.cpp
View file

@ -2365,7 +2365,7 @@ namespace smt2 {
parser(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & p):
m_ctx(ctx),
m_params(p),
m_scanner(ctx, is, interactive, p),
m_scanner(ctx, is, interactive),
m_curr(scanner::NULL_TOKEN),
m_curr_cmd(0),
m_num_bindings(0),

7
src/parsers/smt2/smt2scanner.cpp
View file

@ -242,7 +242,7 @@ namespace smt2 {
}
}
scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive, params_ref const & _p):
scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive):
m_ctx(ctx),
m_interactive(interactive),
m_spos(0),
@ -254,9 +254,8 @@ namespace smt2 {
m_bend(0),
m_stream(stream),
m_cache_input(false) {
parser_params p(_p);
m_smtlib2_compliant = p.smt2_compliant();
m_smtlib2_compliant = ctx.params().m_smtlib2_compliant;
for (int i = 0; i < 256; ++i) {
m_normalized[i] = (char) i;

2
src/parsers/smt2/smt2scanner.h
View file

@ -76,7 +76,7 @@ namespace smt2 {
EOF_TOKEN
};
scanner(cmd_context & ctx, std::istream& stream, bool interactive = false, params_ref const & p = params_ref());
scanner(cmd_context & ctx, std::istream& stream, bool interactive = false);
~scanner() {}

2
src/parsers/util/parser_params.pyg
View file

@ -3,4 +3,4 @@ def_module_params('parser',
params=(('ignore_user_patterns', BOOL, False, 'ignore patterns provided by the user'),
('ignore_bad_patterns', BOOL, True, 'ignore malformed patterns'),
('error_for_visual_studio', BOOL, False, 'display error messages in Visual Studio format'),
('smt2_compliant', BOOL, False, 'enable/disable SMT-LIB 2.0 compliance')))
))