From 92acd6d4ee5d5ac62414e8f012f3e27582f4db6e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 1 Dec 2012 18:19:02 -0800 Subject: [PATCH] removed front_end_params from cmd_context Signed-off-by: Leonardo de Moura --- scripts/mk_project.py | 14 ++++---- src/cmd_context/basic_cmds.cpp | 21 ++++++------ src/cmd_context/cmd_context.cpp | 60 ++++++++++++++++++++------------- src/cmd_context/cmd_context.h | 6 ++-- src/cmd_context/tactic_cmds.cpp | 3 -- src/muz_qe/dl_cmds.cpp | 4 ++- src/solver/strategic_solver.cpp | 19 +++++------ src/solver/strategic_solver.h | 5 +-- src/solver/tactic2solver.cpp | 3 -- src/solver/tactic2solver.h | 3 +- 10 files changed, 71 insertions(+), 67 deletions(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 27120c89d..ac6f44a83 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -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') diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 43507ed3f..d3861257b 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -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 ""; } 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", "", "assert term.")); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 42abd2b2c..7a06f30bf 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -16,7 +16,6 @@ Notes: --*/ #include -#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; diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 1b15c0b60..c2acba0dc 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -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(this)->init_manager(); return *m_pmanager; } sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast(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(); } diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index d44ef196d..ba1193b20 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -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()); diff --git a/src/muz_qe/dl_cmds.cpp b/src/muz_qe/dl_cmds.cpp index d89b8d80d..deb4dc7ec 100644 --- a/src/muz_qe/dl_cmds.cpp +++ b/src/muz_qe/dl_cmds.cpp @@ -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"); diff --git a/src/solver/strategic_solver.cpp b/src/solver/strategic_solver.cpp index 8968f862a..8ce098c51 100644 --- a/src/solver/strategic_solver.cpp +++ b/src/solver/strategic_solver.cpp @@ -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()); diff --git a/src/solver/strategic_solver.h b/src/solver/strategic_solver.h index 7cdda80d5..1883a88cd 100644 --- a/src/solver/strategic_solver.h +++ b/src/solver/strategic_solver.h @@ -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(); diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 0dd55a26b..e630f9c78 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -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); diff --git a/src/solver/tactic2solver.h b/src/solver/tactic2solver.h index 854956d80..0a057b04b 100644 --- a/src/solver/tactic2solver.h +++ b/src/solver/tactic2solver.h @@ -43,13 +43,12 @@ class tactic2solver_core : public solver_na2as { ast_manager & m() const { return m_assertions.m(); } }; scoped_ptr 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;