From c2e95bb0c5924f6f0ca019392cd76c6d6db03ac2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 31 Oct 2012 09:43:46 -0700 Subject: [PATCH] make front_end_params an optional argument in cmd_context Signed-off-by: Leonardo de Moura --- src/api/api_parsers.cpp | 4 ++-- src/ast/pattern/expr_pattern_match.cpp | 2 +- src/cmd_context/cmd_context.cpp | 20 +++++++++++++------- src/cmd_context/cmd_context.h | 13 +++++++------ src/parsers/smt/smtlib_solver.cpp | 2 +- src/shell/smtlib_frontend.cpp | 2 +- src/test/quant_solve.cpp | 2 +- 7 files changed, 26 insertions(+), 19 deletions(-) diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index 03e947c8a..0a76c710e 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -296,7 +296,7 @@ extern "C" { Z3_symbol const decl_names[], Z3_func_decl const decls[]) { Z3_TRY; - cmd_context ctx(mk_c(c)->fparams(), false, &(mk_c(c)->m())); + cmd_context ctx(&mk_c(c)->fparams(), false, &(mk_c(c)->m())); ctx.set_ignore_check(true); if (exec) { ctx.set_solver(alloc(z3_context_solver, *mk_c(c))); @@ -362,7 +362,7 @@ extern "C" { Z3_symbol decl_names[], Z3_func_decl decls[]) { Z3_TRY; - cmd_context ctx(mk_c(c)->fparams(), false, &(mk_c(c)->m())); + cmd_context ctx(&mk_c(c)->fparams(), false, &(mk_c(c)->m())); std::string s(str); std::istringstream is(s); // No logging for this one, since it private. diff --git a/src/ast/pattern/expr_pattern_match.cpp b/src/ast/pattern/expr_pattern_match.cpp index 3fe68c1ee..aca739949 100644 --- a/src/ast/pattern/expr_pattern_match.cpp +++ b/src/ast/pattern/expr_pattern_match.cpp @@ -404,7 +404,7 @@ expr_pattern_match::initialize(char const * spec_string) { std::istringstream is(spec_string); front_end_params p; - cmd_context ctx(p, true, &m_manager); + cmd_context ctx(&p, true, &m_manager); VERIFY(parse_smt2_commands(ctx, is)); ptr_vector::const_iterator it = ctx.begin_assertions(); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 5e80863de..e9a613d4e 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -300,12 +300,13 @@ public: } }; -cmd_context::cmd_context(front_end_params & params, bool main_ctx, ast_manager * m, symbol const & l): +cmd_context::cmd_context(front_end_params * params, bool main_ctx, ast_manager * m, symbol const & l): m_main_ctx(main_ctx), - m_params(params), + m_params(params == 0 ? alloc(front_end_params) : params), + m_params_owner(params == 0), m_logic(l), m_interactive_mode(false), - m_global_decls(!params.m_smtlib2_compliant), // SMTLIB 2.0 uses scoped decls. + m_global_decls(!this->params().m_smtlib2_compliant), // SMTLIB 2.0 uses scoped decls. m_print_success(false), // params.m_smtlib2_compliant), m_random_seed(0), m_produce_unsat_cores(false), @@ -340,6 +341,11 @@ cmd_context::~cmd_context() { finalize_cmds(); finalize_tactic_cmds(); finalize_probes(); + m_solver = 0; + m_check_sat_result = 0; + if (m_params_owner) { + dealloc(m_params); + } } cmd_context::check_sat_state cmd_context::cs_state() const { @@ -531,10 +537,10 @@ void cmd_context::init_manager() { SASSERT(m_manager == 0); SASSERT(m_pmanager == 0); m_check_sat_result = 0; - m_manager = alloc(ast_manager, m_params.m_proof_mode, m_params.m_trace_stream); + m_manager = alloc(ast_manager, params().m_proof_mode, params().m_trace_stream); m_pmanager = alloc(pdecl_manager, *m_manager); init_manager_core(true); - if (m_params.m_smtlib2_compliant) + if (params().m_smtlib2_compliant) m_manager->enable_int_real_coercions(false); } @@ -1240,7 +1246,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions init_manager(); if (m_solver) { m_check_sat_result = m_solver.get(); // solver itself stores the result. - m_solver->set_front_end_params(m_params); + m_solver->set_front_end_params(params()); m_solver->set_progress_callback(this); m_solver->set_produce_proofs(produce_proofs()); m_solver->set_produce_models(produce_models()); @@ -1390,7 +1396,7 @@ void cmd_context::validate_model() { void cmd_context::set_solver(solver * s) { m_check_sat_result = 0; m_solver = s; - m_solver->set_front_end_params(m_params); + m_solver->set_front_end_params(params()); if (has_manager() && s != 0) { m_solver->init(m(), m_logic); // assert formulas and create scopes in the new solver. diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index d730ba002..efbfbfb75 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -133,7 +133,8 @@ public: protected: bool m_main_ctx; - front_end_params & m_params; + front_end_params * m_params; + bool m_params_owner; symbol m_logic; bool m_interactive_mode; bool m_global_decls; @@ -246,9 +247,9 @@ protected: void print_unsupported_info(symbol const& s) { if (s != symbol::null) diagnostic_stream() << "; " << s << std::endl;} public: - cmd_context(front_end_params & params, bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null); + cmd_context(front_end_params * params = 0, bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null); ~cmd_context(); - bool is_smtlib2_compliant() const { return m_params.m_smtlib2_compliant; } + bool is_smtlib2_compliant() const { return params().m_smtlib2_compliant; } void set_logic(symbol const & s); bool has_logic() const { return m_logic != symbol::null; } symbol const & get_logic() const { return m_logic; } @@ -268,8 +269,8 @@ public: void set_global_decls(bool flag) { SASSERT(!has_manager()); m_global_decls = flag; } unsigned random_seed() const { return m_random_seed; } void set_random_seed(unsigned s) { m_random_seed = s; } - bool produce_models() const { return m_params.m_model; } - bool produce_proofs() const { return m_params.m_proof_mode != PGM_DISABLED; } + bool produce_models() const { return params().m_model; } + bool produce_proofs() const { return params().m_proof_mode != PGM_DISABLED; } bool produce_unsat_cores() const { return m_produce_unsat_cores; } void set_produce_unsat_cores(bool flag) { m_produce_unsat_cores = flag; } bool produce_assignments() const { return m_produce_assignments; } @@ -283,7 +284,7 @@ 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_params; } + front_end_params & params() const { return *m_params; } void set_solver(solver * s); solver * get_solver() const { return m_solver.get(); } diff --git a/src/parsers/smt/smtlib_solver.cpp b/src/parsers/smt/smtlib_solver.cpp index 1aff13a3d..77c2455dc 100644 --- a/src/parsers/smt/smtlib_solver.cpp +++ b/src/parsers/smt/smtlib_solver.cpp @@ -82,7 +82,7 @@ namespace smtlib { // Hack: it seems SMT-LIB allow benchmarks without any :formula benchmark.add_formula(m_ast_manager.mk_true()); } - m_ctx = alloc(cmd_context, m_params, true, &m_ast_manager, benchmark.get_logic()); + m_ctx = alloc(cmd_context, &m_params, true, &m_ast_manager, benchmark.get_logic()); m_ctx->set_solver(mk_smt_strategic_solver(*m_ctx)); theory::expr_iterator fit = benchmark.begin_formulas(); theory::expr_iterator fend = benchmark.end_formulas(); diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp index 1b1299971..dd8987529 100644 --- a/src/shell/smtlib_frontend.cpp +++ b/src/shell/smtlib_frontend.cpp @@ -97,7 +97,7 @@ unsigned read_smtlib2_commands(char const* file_name, front_end_params& front_en g_start_time = clock(); register_on_timeout_proc(on_timeout); signal(SIGINT, on_ctrl_c); - cmd_context ctx(front_end_params); + cmd_context ctx(&front_end_params); // temporary hack until strategic_solver is ported to new tactic framework if (front_end_params.m_nlsat) { diff --git a/src/test/quant_solve.cpp b/src/test/quant_solve.cpp index 2899522b3..fe3454336 100644 --- a/src/test/quant_solve.cpp +++ b/src/test/quant_solve.cpp @@ -98,7 +98,7 @@ static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, expr* static expr_ref parse_fml(ast_manager& m, char const* str) { expr_ref result(m); front_end_params fp; - cmd_context ctx(fp, false, &m); + cmd_context ctx(&fp, false, &m); ctx.set_ignore_check(true); std::ostringstream buffer; buffer << "(declare-const x Int)\n"