make front_end_params an optional argument in cmd_context

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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.

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<expr>::const_iterator it  = ctx.begin_assertions();

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.

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_models() const { return params().m_model; }
-    bool produce_proofs() const { return m_params.m_proof_mode != PGM_DISABLED; }
+    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<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_params; }
+    front_end_params & params() const { return *m_params; }
  
     void set_solver(solver * s);
     solver * get_solver() const { return m_solver.get(); }

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

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

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"