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

removed front_end_params from cmd_context

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-01 18:19:02 -08:00
parent 29cf179364
commit 92acd6d4ee
10 changed files with 71 additions and 67 deletions
Download patch file Download diff file Expand all files Collapse all files

14
scripts/mk_project.py
View file

@ -25,22 +25,22 @@ def init_project_def():
add_lib('parser_util', ['ast'], 'parsers/util')
add_lib('grobner', ['ast'], 'math/grobner')
add_lib('euclid', ['util'], 'math/euclid')
# Front-end-params module still contain a lot of parameters for smt solver component.
# This should be fixed
add_lib('front_end_params', ['ast'])
# Simplifier module will be deleted in the future.
# It has been replaced with rewriter module.
add_lib('simplifier', ['rewriter', 'front_end_params'], 'ast/simplifier')
add_lib('core_tactics', ['tactic', 'normal_forms'], 'tactic/core')
add_lib('sat_tactic', ['tactic', 'sat'], 'sat/tactic')
add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith')
add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic')
add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic')
add_lib('aig_tactic', ['tactic'], 'tactic/aig')
add_lib('solver', ['model', 'tactic', 'front_end_params'])
add_lib('solver', ['model', 'tactic'])
add_lib('cmd_context', ['solver', 'rewriter'])
add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds')
add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
# Front-end-params module still contain a lot of parameters for smt solver component.
# This should be fixed
add_lib('front_end_params', ['ast'])
# Simplifier module will be deleted in the future.
# It has been replaced with rewriter module.
add_lib('simplifier', ['rewriter', 'front_end_params'], 'ast/simplifier')
add_lib('pattern', ['normal_forms', 'smt2parser', 'simplifier'], 'ast/pattern')
add_lib('macros', ['simplifier', 'front_end_params'], 'ast/macros')
add_lib('proof_checker', ['rewriter', 'front_end_params'], 'ast/proof_checker')

21
src/cmd_context/basic_cmds.cpp
View file

@ -27,7 +27,6 @@ Notes:
#include"cmd_util.h"
#include"simplify_cmd.h"
#include"eval_cmd.h"
#include"front_end_params.h"
#include"gparams.h"
#include"model_params.hpp"
@ -159,7 +158,7 @@ public:
};
ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", {
if (ctx.params().m_proof_mode == PGM_DISABLED)
if (!ctx.produce_proofs())
throw cmd_exception("proof construction is not enabled, use command (set-option :produce-proofs true)");
if (!ctx.has_manager() ||
ctx.cs_state() != cmd_context::css_unsat)
@ -253,7 +252,7 @@ protected:
}
public:
set_get_option_cmd(char const * name, front_end_params & params):
set_get_option_cmd(char const * name):
cmd(name),
m_true("true"),
m_false("false"),
@ -375,8 +374,8 @@ class set_option_cmd : public set_get_option_cmd {
}
public:
set_option_cmd(front_end_params & params):
set_get_option_cmd("set-option", params),
set_option_cmd():
set_get_option_cmd("set-option"),
m_unsupported(false) {
}
@ -454,8 +453,8 @@ class get_option_cmd : public set_get_option_cmd {
}
public:
get_option_cmd(front_end_params & params):
set_get_option_cmd("get-option", params) {
get_option_cmd():
set_get_option_cmd("get-option") {
}
virtual char const * get_usage() const { return "<keyword>"; }
virtual char const * get_descr(cmd_context & ctx) const { return "get configuration option."; }
@ -476,13 +475,13 @@ public:
print_bool(ctx, ctx.interactive_mode());
}
else if (opt == m_produce_proofs) {
print_bool(ctx, ctx.params().m_proof_mode != PGM_DISABLED);
print_bool(ctx, ctx.produce_proofs());
}
else if (opt == m_produce_unsat_cores) {
print_bool(ctx, ctx.produce_unsat_cores());
}
else if (opt == m_produce_models) {
print_bool(ctx, ctx.params().m_model);
print_bool(ctx, ctx.produce_models());
}
else if (opt == m_produce_assignments) {
print_bool(ctx, ctx.produce_assignments());
@ -711,8 +710,8 @@ void install_basic_cmds(cmd_context & ctx) {
ctx.insert(alloc(get_assertions_cmd));
ctx.insert(alloc(get_proof_cmd));
ctx.insert(alloc(get_unsat_core_cmd));
ctx.insert(alloc(set_option_cmd, ctx.params()));
ctx.insert(alloc(get_option_cmd, ctx.params()));
ctx.insert(alloc(set_option_cmd));
ctx.insert(alloc(get_option_cmd));
ctx.insert(alloc(get_info_cmd));
ctx.insert(alloc(set_info_cmd));
ctx.insert(alloc(builtin_cmd, "assert", "<term>", "assert term."));

60
src/cmd_context/cmd_context.cpp
View file

@ -16,7 +16,6 @@ Notes:
--*/
#include<signal.h>
#include"front_end_params.h"
#include"tptr.h"
#include"cmd_context.h"
#include"func_decl_dependencies.h"
@ -318,7 +317,6 @@ public:
cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
m_main_ctx(main_ctx),
m_fparams(alloc(front_end_params)),
m_logic(l),
m_interactive_mode(false),
m_global_decls(false), // :global-decls is false by default.
@ -358,11 +356,11 @@ cmd_context::~cmd_context() {
finalize_probes();
m_solver = 0;
m_check_sat_result = 0;
dealloc(m_fparams);
}
void cmd_context::set_produce_models(bool f) {
params().m_model = f;
// PARAM-TODO
// params().m_model = f;
if (m_solver)
m_solver->set_produce_models(f);
}
@ -374,19 +372,35 @@ void cmd_context::set_produce_unsat_cores(bool f) {
}
void cmd_context::set_produce_proofs(bool f) {
// PARAM-TODO
// can only be set before initialization
SASSERT(!has_manager());
params().m_proof_mode = f ? PGM_FINE : PGM_DISABLED;
// params().m_proof_mode = f ? PGM_FINE : PGM_DISABLED;
}
bool cmd_context::produce_models() const {
return params().m_model;
// PARAM-TODO
// return params().m_model;
return true;
}
bool cmd_context::produce_proofs() const {
return params().m_proof_mode != PGM_DISABLED;
// PARAM-TODO
// return params().m_proof_mode != PGM_DISABLED;
return false;
}
bool cmd_context::well_sorted_check_enabled() const {
// PARAM-TODO
return true;
}
bool cmd_context::validate_model_enabled() const {
// PARAM-TODO
return false;
}
cmd_context::check_sat_state cmd_context::cs_state() const {
if (m_check_sat_result.get() == 0)
return css_clear;
@ -579,9 +593,9 @@ void cmd_context::init_manager_core(bool new_manager) {
insert(pm().mk_plist_decl());
}
if (m_solver) {
m_solver->set_produce_unsat_cores(m_produce_unsat_cores);
m_solver->set_produce_models(params().m_model);
m_solver->set_produce_proofs(params().m_proof_mode == PGM_FINE);
m_solver->set_produce_unsat_cores(produce_unsat_cores());
m_solver->set_produce_models(produce_models());
m_solver->set_produce_proofs(produce_proofs());
m_solver->init(m(), m_logic);
}
m_check_logic.set_logic(m(), m_logic);
@ -591,7 +605,7 @@ void cmd_context::init_manager() {
SASSERT(m_manager == 0);
SASSERT(m_pmanager == 0);
m_check_sat_result = 0;
m_manager = alloc(ast_manager, params().m_proof_mode, params().m_trace_stream);
m_manager = alloc(ast_manager, produce_proofs() ? PGM_FINE : PGM_DISABLED); // PARAM-TODO , params().m_trace_stream);
m_pmanager = alloc(pdecl_manager, *m_manager);
init_manager_core(true);
// PARAM-TODO
@ -855,7 +869,7 @@ object_ref * cmd_context::find_object_ref(symbol const & s) const {
return r;
}
#define CHECK_SORT(T) if (params().m_well_sorted_check) m().check_sorts_core(T)
#define CHECK_SORT(T) if (well_sorted_check_enabled()) m().check_sorts_core(T)
void cmd_context::mk_const(symbol const & s, expr_ref & result) const {
mk_app(s, 0, 0, 0, 0, 0, result);
@ -895,13 +909,13 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
return;
}
SASSERT(num_args > 0);
TRACE("macro_bug", tout << "m_well_sorted_check: " << params().m_well_sorted_check << "\n";
TRACE("macro_bug", tout << "well_sorted_check_enabled(): " << well_sorted_check_enabled() << "\n";
tout << "s: " << s << "\n";
tout << "body:\n" << mk_ismt2_pp(_m.second, m()) << "\n";
tout << "args:\n"; for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(args[i], m()) << "\n" << mk_pp(m().get_sort(args[i]), m()) << "\n";);
var_subst subst(m());
subst(_m.second, num_args, args, result);
if (params().m_well_sorted_check && !is_well_sorted(m(), result))
if (well_sorted_check_enabled() && !is_well_sorted(m(), result))
throw cmd_exception("invalid macro application, sort mismatch ", s);
return;
}
@ -930,7 +944,7 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
func_decl * f = fs.find(m(), num_args, args, range);
if (f == 0)
throw cmd_exception("unknown constant ", s);
if (params().m_well_sorted_check)
if (well_sorted_check_enabled())
m().check_sort(f, num_args, args);
result = m().mk_app(f, num_args, args);
return;
@ -1151,7 +1165,7 @@ void cmd_context::assert_expr(expr * t) {
m_check_sat_result = 0;
m().inc_ref(t);
m_assertions.push_back(t);
if (m_produce_unsat_cores)
if (produce_unsat_cores())
m_assertion_names.push_back(0);
if (m_solver)
m_solver->assert_expr(t);
@ -1160,7 +1174,7 @@ void cmd_context::assert_expr(expr * t) {
void cmd_context::assert_expr(symbol const & name, expr * t) {
if (!m_check_logic(t))
throw cmd_exception(m_check_logic.get_last_error());
if (!m_produce_unsat_cores || name == symbol::null) {
if (!produce_unsat_cores() || name == symbol::null) {
assert_expr(t);
return;
}
@ -1266,7 +1280,7 @@ void cmd_context::restore_assertions(unsigned old_sz) {
SASSERT(old_sz <= m_assertions.size());
SASSERT(!m_interactive_mode || m_assertions.size() == m_assertion_strings.size());
restore(m(), m_assertions, old_sz);
if (m_produce_unsat_cores)
if (produce_unsat_cores())
restore(m(), m_assertion_names, old_sz);
if (m_interactive_mode)
m_assertion_strings.shrink(old_sz);
@ -1398,7 +1412,7 @@ struct contains_array_op_proc {
\brief Check if the current model satisfies the quantifier free formulas.
*/
void cmd_context::validate_model() {
if (!params().m_model_validate)
if (!validate_model_enabled())
return;
if (!is_model_available())
return;
@ -1445,9 +1459,9 @@ void cmd_context::set_solver(solver * s) {
m_check_sat_result = 0;
m_solver = s;
if (has_manager() && s != 0) {
m_solver->set_produce_unsat_cores(m_produce_unsat_cores);
m_solver->set_produce_models(params().m_model);
m_solver->set_produce_proofs(params().m_proof_mode == PGM_FINE);
m_solver->set_produce_unsat_cores(produce_unsat_cores());
m_solver->set_produce_models(produce_models());
m_solver->set_produce_proofs(produce_proofs());
m_solver->init(m(), m_logic);
// assert formulas and create scopes in the new solver.
unsigned lim = 0;
@ -1502,7 +1516,7 @@ void cmd_context::display_assertions() {
}
bool cmd_context::is_model_available() const {
if (params().m_model &&
if (produce_models() &&
has_manager() &&
(cs_state() == css_sat || cs_state() == css_unknown)) {
model_ref md;

6
src/cmd_context/cmd_context.h
View file

@ -42,8 +42,6 @@ Notes:
*/
std::string smt2_keyword_to_param(symbol const & k);
struct front_end_params;
class func_decls {
func_decl * m_decls;
public:
@ -138,7 +136,6 @@ public:
protected:
bool m_main_ctx;
front_end_params * m_fparams;
symbol m_logic;
bool m_interactive_mode;
bool m_global_decls;
@ -274,6 +271,8 @@ public:
bool produce_models() const;
bool produce_proofs() const;
bool produce_unsat_cores() const { return m_produce_unsat_cores; }
bool well_sorted_check_enabled() const;
bool validate_model_enabled() const;
void set_produce_models(bool flag);
void set_produce_unsat_cores(bool flag);
void set_produce_proofs(bool flag);
@ -288,7 +287,6 @@ public:
virtual ast_manager & get_ast_manager() { return m(); }
pdecl_manager & pm() const { if (!m_pmanager) const_cast<cmd_context*>(this)->init_manager(); return *m_pmanager; }
sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast<cmd_context*>(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; }
front_end_params & params() const { return *m_fparams; }
void set_solver(solver * s);
solver * get_solver() const { return m_solver.get(); }

3
src/cmd_context/tactic_cmds.cpp
View file

@ -24,7 +24,6 @@ Notes:
#include"scoped_ctrl_c.h"
#include"cancel_eh.h"
#include"model_smt2_pp.h"
#include"params2front_end_params.h"
#include"ast_smt2_pp.h"
#include"tactic.h"
#include"tactical.h"
@ -187,7 +186,6 @@ public:
virtual void execute(cmd_context & ctx) {
params_ref p = ps();
front_end_params2params(ctx.params(), p);
tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p);
tref->set_logic(ctx.get_logic());
ast_manager & m = ctx.m();
@ -298,7 +296,6 @@ public:
virtual void execute(cmd_context & ctx) {
params_ref p = ps();
front_end_params2params(ctx.params(), p);
tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p);
{
tactic & t = *(tref.get());

4
src/muz_qe/dl_cmds.cpp
View file

@ -33,6 +33,8 @@ Notes:
class dl_context {
// PARAM-TODO temp HACK: added m_params field because cmd_context does not have front_end_params anymore
front_end_params m_params;
cmd_context & m_cmd;
dl_collected_cmds* m_collected_cmds;
unsigned m_ref_count;
@ -62,7 +64,7 @@ public:
void init() {
ast_manager& m = m_cmd.m();
if (!m_context) {
m_context = alloc(datalog::context, m, m_cmd.params());
m_context = alloc(datalog::context, m, m_params);
}
if (!m_decl_plugin) {
symbol name("datalog_relation");

19
src/solver/strategic_solver.cpp
View file

@ -18,8 +18,6 @@ Notes:
--*/
#include"strategic_solver.h"
#include"scoped_timer.h"
#include"front_end_params.h"
#include"params2front_end_params.h"
#include"ast_smt2_pp.h"
// minimum verbosity level for portfolio verbose messages
@ -33,7 +31,6 @@ strategic_solver::ctx::ctx(ast_manager & m):
strategic_solver::strategic_solver():
m_manager(0),
m_fparams(0),
m_force_tactic(false),
m_inc_mode(false),
m_check_sat_executed(false),
@ -50,6 +47,7 @@ strategic_solver::strategic_solver():
m_produce_proofs = false;
m_produce_models = false;
m_produce_unsat_cores = false;
m_auto_config = true;
}
strategic_solver::~strategic_solver() {
@ -99,11 +97,12 @@ void strategic_solver::set_inc_solver(solver * s) {
void strategic_solver::updt_params(params_ref const & p) {
if (m_inc_solver)
m_inc_solver->updt_params(p);
if (m_fparams)
params2front_end_params(p, *m_fparams);
m_params = p;
m_auto_config = p.get_bool("auto_config", true);
// PARAM-TODO
// PROOFS, MODELS, UNSATCORES
}
void strategic_solver::collect_param_descrs(param_descrs & r) {
if (m_inc_solver)
m_inc_solver->collect_param_descrs(r);
@ -323,10 +322,8 @@ struct aux_timeout_eh : public event_handler {
struct strategic_solver::mk_tactic {
strategic_solver * m_solver;
mk_tactic(strategic_solver * s, tactic_factory * f):m_solver(s) {
mk_tactic(strategic_solver * s, tactic_factory * f, params_ref const & p):m_solver(s) {
ast_manager & m = s->m();
params_ref p;
front_end_params2params(*s->m_fparams, p);
tactic * tct = (*f)(m, p);
tct->set_logic(s->m_logic);
if (s->m_callback)
@ -374,7 +371,7 @@ lbool strategic_solver::check_sat(unsigned num_assumptions, expr * const * assum
reset_results();
m_check_sat_executed = true;
if (num_assumptions > 0 || // assumptions were provided
(!m_fparams->m_auto_config && !m_force_tactic) // auto config and force_tactic are turned off
(!m_auto_config && !m_force_tactic) // auto config and force_tactic are turned off
) {
// must use incremental solver
return check_sat_with_assumptions(num_assumptions, assumptions);
@ -438,7 +435,7 @@ lbool strategic_solver::check_sat(unsigned num_assumptions, expr * const * assum
TRACE("strategic_solver", tout << "using goal...\n"; g->display_with_dependencies(tout););
mk_tactic tct_maker(this, factory);
mk_tactic tct_maker(this, factory, m_params);
SASSERT(m_curr_tactic);
proof_ref pr(m());

5
src/solver/strategic_solver.h
View file

@ -23,7 +23,6 @@ Notes:
#include"tactic.h"
class progress_callback;
struct front_end_params;
/**
\brief Implementation of the solver API that supports:
@ -57,7 +56,7 @@ public:
private:
ast_manager * m_manager;
front_end_params * m_fparams;
params_ref m_params;
symbol m_logic;
bool m_force_tactic; // use tactics even when auto_config = false
bool m_inc_mode;
@ -93,6 +92,8 @@ private:
bool m_produce_models;
bool m_produce_unsat_cores;
bool m_auto_config;
progress_callback * m_callback;
void reset_results();

3
src/solver/tactic2solver.cpp
View file

@ -20,7 +20,6 @@ Notes:
--*/
#include"tactic2solver.h"
#include"params2front_end_params.h"
#include"ast_smt2_pp.h"
tactic2solver_core::ctx::ctx(ast_manager & m, symbol const & logic):
@ -94,8 +93,6 @@ lbool tactic2solver_core::check_sat_core(unsigned num_assumptions, expr * const
SASSERT(m_ctx);
ast_manager & m = m_ctx->m();
params_ref p = m_params;
if (m_fparams)
front_end_params2params(*m_fparams, p);
#pragma omp critical (tactic2solver_core)
{
m_ctx->m_tactic = get_tactic(m, p);

3
src/solver/tactic2solver.h
View file

@ -43,13 +43,12 @@ class tactic2solver_core : public solver_na2as {
ast_manager & m() const { return m_assertions.m(); }
};
scoped_ptr<ctx> m_ctx;
front_end_params * m_fparams;
params_ref m_params;
bool m_produce_models;
bool m_produce_proofs;
bool m_produce_unsat_cores;
public:
tactic2solver_core():m_ctx(0), m_fparams(0), m_produce_models(false), m_produce_proofs(false), m_produce_unsat_cores(false) {}
tactic2solver_core():m_ctx(0), m_produce_models(false), m_produce_proofs(false), m_produce_unsat_cores(false) {}
virtual ~tactic2solver_core();
virtual tactic * get_tactic(ast_manager & m, params_ref const & p) = 0;