more reorg

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

src/api/api_solver.cpp

@@ -39,7 +39,6 @@ extern "C" {
         s->m_solver->set_produce_proofs(m.proofs_enabled());
         s->m_solver->set_produce_unsat_cores(s->m_params.get_bool("unsat_core", false));
         s->m_solver->set_produce_models(s->m_params.get_bool("model", true));
-        s->m_solver->set_front_end_params(mk_c(c)->fparams());
         s->m_solver->updt_params(s->m_params);
         s->m_solver->init(m, s->m_logic);
         s->m_initialized = true;

src/ast/pattern/expr_pattern_match.cpp

@@ -36,7 +36,6 @@ Notes:
 #include"ast_pp.h"
 #include"cmd_context.h"
 #include"smt2parser.h"
-#include"front_end_params.h"
 
 expr_pattern_match::expr_pattern_match(ast_manager & manager):
     m_manager(manager), m_precompiled(manager) {        

src/ast/pattern/expr_pattern_match.h

@@ -22,7 +22,6 @@ Notes:
 
 #include"ast.h"
 #include"map.h"
-#include"front_end_params.h"
 
 class expr_pattern_match {
 

src/cmd_context/cmd_context.cpp

@@ -1301,7 +1301,6 @@ 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(params());
         m_solver->set_progress_callback(this);
         scoped_watch sw(*this);
         cancel_eh<solver> eh(*m_solver);
@@ -1445,7 +1444,6 @@ 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(params());
     if (has_manager() && s != 0) {
         m_solver->set_produce_unsat_cores(m_produce_unsat_cores);
         m_solver->set_produce_models(params().m_model);

src/cmd_context/tactic_cmds.cpp

@@ -189,7 +189,6 @@ public:
         params_ref p = ps();
         front_end_params2params(ctx.params(), p);
         tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p);
-        tref->set_front_end_params(ctx.params());
         tref->set_logic(ctx.get_logic());
         ast_manager & m = ctx.m();
         unsigned timeout   = p.get_uint("timeout", UINT_MAX);

src/front_end_params/front_end_params.cpp

@@ -51,10 +51,6 @@ void front_end_params::register_params(ini_params & p) {
         p.register_bool_param("debug_ref_count", m_debug_ref_count);
     });
 
-    // temporary hack until strategic_solver is ported to new tactic framework
-    PRIVATE_PARAMS({
-        p.register_bool_param("nlsat", m_nlsat);
-    });
 }
 
 #endif

src/front_end_params/front_end_params.h

@@ -20,14 +20,9 @@ Revision History:
 #define _FRONT_END_PARAMS_H_
 
 #include"ast.h"
-#include"preprocessor_params.h"
 #include"smt_params.h"
-#include"arith_simplifier_params.h"
 
-struct front_end_params : public preprocessor_params, public smt_params, 
+struct front_end_params : public smt_params {
-                          public arith_simplifier_params {
-    bool                m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples.
-    bool                m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples.
     bool                m_well_sorted_check;
     unsigned            m_memory_high_watermark;
     unsigned            m_memory_max_size;
@@ -39,13 +34,9 @@ struct front_end_params : public preprocessor_params, public smt_params,
     std::string         m_trace_file_name;
     std::fstream*       m_trace_stream;
     bool                m_display_config;
-    bool                m_nlsat; // temporary hack until strategic_solver is ported to new tactic framework
-
     bool                m_dump_goal_as_smt;
 
     front_end_params():
-        m_at_labels_cex(false),
-        m_check_at_labels(false),
         m_well_sorted_check(true),
         m_memory_high_watermark(0),
         m_memory_max_size(0),
@@ -60,7 +51,6 @@ struct front_end_params : public preprocessor_params, public smt_params,
         m_trace_file_name("z3.log"),
         m_trace_stream(NULL),
         m_display_config(false),
-        m_nlsat(false),
         m_dump_goal_as_smt(false) {
     }
 

src/front_end_params/preprocessor_params.h

@@ -22,6 +22,7 @@ Revision History:
 #include"pattern_inference_params.h"
 #include"bit_blaster_params.h"
 #include"bv_simplifier_params.h"
+#include"arith_simplifier_params.h"
 
 enum lift_ite_kind {
     LI_NONE,
@@ -30,7 +31,9 @@ enum lift_ite_kind {
 };
 
 struct preprocessor_params : public pattern_inference_params, 
-                             public bit_blaster_params, public bv_simplifier_params {
+                             public bit_blaster_params, 
+                             public bv_simplifier_params, 
+                             public arith_simplifier_params {
     lift_ite_kind   m_lift_ite;
     lift_ite_kind   m_ng_lift_ite;  // lift ite for non ground terms
     bool            m_pull_cheap_ite_trees;
@@ -81,6 +84,7 @@ public:
         pattern_inference_params::register_params(p);
         bit_blaster_params::register_params(p);
         bv_simplifier_params::register_params(p);
+        arith_simplifier_params::register_params(p);
         p.register_int_param("lift_ite", 0, 2, reinterpret_cast<int&>(m_lift_ite), "ite term lifting: 0 - no lifting, 1 - conservative, 2 - full");
         p.register_int_param("ng_lift_ite", 0, 2, reinterpret_cast<int&>(m_ng_lift_ite), "ite (non-ground) term lifting: 0 - no lifting, 1 - conservative, 2 - full");
         p.register_bool_param("elim_term_ite", m_eliminate_term_ite, "eliminate term if-then-else in the preprocessor");

src/front_end_params/smt_params.h

@@ -25,6 +25,7 @@ Revision History:
 #include"theory_array_params.h"
 #include"theory_bv_params.h"
 #include"theory_datatype_params.h"
+#include"preprocessor_params.h"
 
 enum phase_selection { 
     PS_ALWAYS_FALSE,
@@ -65,7 +66,12 @@ enum case_split_strategy {
     CS_RELEVANCY_GOAL, // based on relevancy and the current goal
 };
 
-struct smt_params : public dyn_ack_params, public qi_params, public theory_arith_params, public theory_array_params, public theory_bv_params, 
+struct smt_params : public preprocessor_params, 
+                    public dyn_ack_params, 
+                    public qi_params, 
+                    public theory_arith_params, 
+                    public theory_array_params, 
+                    public theory_bv_params, 
                     public theory_datatype_params {
     bool             m_display_proof;
     bool             m_display_dot_proof;
@@ -196,7 +202,9 @@ struct smt_params : public dyn_ack_params, public qi_params, public theory_arith
     bool                m_user_theory_preprocess_axioms;
     bool                m_user_theory_persist_axioms;
     unsigned            m_soft_timeout;
-    
+    bool                m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples.
+    bool                m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples.    
+
     smt_params():
         m_display_proof(false),
         m_display_dot_proof(false),
@@ -260,7 +268,9 @@ struct smt_params : public dyn_ack_params, public qi_params, public theory_arith
         m_preprocess(true), // temporary hack for disabling all preprocessing..
         m_user_theory_preprocess_axioms(false),
         m_user_theory_persist_axioms(false),
-        m_soft_timeout(0)
+        m_soft_timeout(0),
+        m_at_labels_cex(false),
+        m_check_at_labels(false)
     {
 
     }

src/shell/smtlib_frontend.cpp

@@ -98,16 +98,9 @@ unsigned read_smtlib2_commands(char const* file_name, front_end_params& front_en
     signal(SIGINT, on_ctrl_c);
     cmd_context ctx;
 
-    // temporary hack until strategic_solver is ported to new tactic framework
+    solver * s = mk_smt_strategic_solver(false);
-    if (front_end_params.m_nlsat) {
+    ctx.set_solver(s);
-        tactic_factory2solver * s = alloc(tactic_factory2solver);
+
-        s->set_tactic(alloc(qfnra_nlsat_fct));
-        ctx.set_solver(s);
-    }
-    else {
-        solver * s = mk_smt_strategic_solver(false);
-        ctx.set_solver(s);
-    }
     install_dl_cmds(ctx);
     install_dbg_cmds(ctx);
     install_polynomial_cmds(ctx);

src/smt/smt_model_generator.cpp

@@ -48,7 +48,7 @@ namespace smt {
 
     void model_generator::init_model() {
         SASSERT(!m_model);
-        // PARAM-TODO
+        // PARAM-TODO smt_params ---> params_ref
         m_model = alloc(proto_model, m_manager, m_context->get_simplifier()); // , m_context->get_fparams());
         ptr_vector<theory>::const_iterator it  = m_context->begin_theories();
         ptr_vector<theory>::const_iterator end = m_context->end_theories();

src/smt/smt_solver.cpp

@@ -24,22 +24,19 @@ Notes:
 namespace smt {
 
     class solver : public solver_na2as {
-        front_end_params *  m_params;
+        front_end_params    m_params;
         smt::kernel *       m_context;
         progress_callback * m_callback;
     public:
-        solver():m_params(0), m_context(0), m_callback(0) {}
+        solver():m_context(0), m_callback(0) {}
 
         virtual ~solver() {
             if (m_context != 0)
                 dealloc(m_context);
         }
 
-        virtual void set_front_end_params(front_end_params & p) {
-            m_params = &p;
-        }
-
         virtual void updt_params(params_ref const & p) {
+            // PARAM-TODO copy p --> m_params
             if (m_context == 0)
                 return;
             m_context->updt_params(p);
@@ -49,8 +46,7 @@ namespace smt {
             if (m_context == 0) {
                 ast_manager m;
                 reg_decl_plugins(m);
-                front_end_params p;
+                smt::kernel s(m, m_params);
-                smt::kernel s(m, p);
                 s.collect_param_descrs(r);
             }
             else {
@@ -59,11 +55,10 @@ namespace smt {
         }
 
         virtual void init_core(ast_manager & m, symbol const & logic) {
-            SASSERT(m_params);
             reset();
 #pragma omp critical (solver)
             {
-                m_context = alloc(smt::kernel, m, *m_params);
+                m_context = alloc(smt::kernel, m, m_params);
                 if (m_callback)
                     m_context->set_progress_callback(m_callback);
             }

src/smt/tactic/smt_tactic.cpp

@@ -24,7 +24,7 @@ Notes:
 #include"rewriter_types.h"
 
 class smt_tactic : public tactic {
-    scoped_ptr<front_end_params> m_params;
+    front_end_params             m_params;
     params_ref                   m_params_ref;
     statistics                   m_stats;
     std::string                  m_failure;
@@ -52,11 +52,7 @@ public:
     }
 
     front_end_params & fparams() {
-        if (!m_params) {
+        return m_params;
-            m_params = alloc(front_end_params);
-            params2front_end_params(m_params_ref, fparams());
-        }
-        return *m_params;
     }
 
     void updt_params_core(params_ref const & p) {
@@ -68,6 +64,7 @@ public:
         TRACE("smt_tactic", tout << this << "\nupdt_params: " << p << "\n";);
         updt_params_core(p);
         m_params_ref = p;
+        // PARAM-TODO update params2front_end_params p ---> m_params
         params2front_end_params(m_params_ref, fparams());
         SASSERT(p.get_bool("auto_config", fparams().m_auto_config) == fparams().m_auto_config);
     }
@@ -97,14 +94,6 @@ public:
         m_stats.reset();
     }
     
-    // for backward compatibility
-    virtual void set_front_end_params(front_end_params & p) {
-        m_params = alloc(front_end_params, p);
-        SASSERT(m_params.get() == &fparams());
-        // must propagate the params_ref to fparams
-        params2front_end_params(m_params_ref, fparams());
-    }
-
     virtual void set_logic(symbol const & l) {
         m_logic = l;
     }

src/solver/solver.h

@@ -41,15 +41,6 @@ struct front_end_params;
 class solver : public check_sat_result {
 public:
     virtual ~solver() {}
-    
-    /**
-       \brief This method is invoked to allow the solver to access the front_end_params (environment parameters).
-       
-       \warning This method is used for backward compatibility. The first solver implemented in Z3 used
-       front_end_params to store its configuration parameters. 
-    */
-    virtual void set_front_end_params(front_end_params & p) {} 
-
     /**
        \brief Update the solver internal settings. 
     */

src/solver/strategic_solver.cpp

@@ -191,7 +191,6 @@ void strategic_solver::init_inc_solver() {
     m_inc_solver->set_produce_proofs(m_produce_proofs);
     m_inc_solver->set_produce_models(m_produce_models);
     m_inc_solver->set_produce_unsat_cores(m_produce_unsat_cores);
-    m_inc_solver->set_front_end_params(*m_fparams);
     m_inc_solver->init(m(), m_logic);
     unsigned sz = get_num_assertions();
     if (m_produce_unsat_cores) {
@@ -329,7 +328,6 @@ struct strategic_solver::mk_tactic {
         params_ref p;
         front_end_params2params(*s->m_fparams, p);
         tactic * tct = (*f)(m, p);
-        tct->set_front_end_params(*s->m_fparams);
         tct->set_logic(s->m_logic);
         if (s->m_callback)
             tct->set_progress_callback(s->m_callback);

src/solver/strategic_solver.h

@@ -118,8 +118,6 @@ public:
     void set_inc_unknown_behavior(inc_unknown_behavior b) { m_inc_unknown_behavior = b; }
     void force_tactic(bool f) { m_force_tactic = f; }
 
-    virtual void set_front_end_params(front_end_params & p) { m_fparams = &p; }
-
     virtual void updt_params(params_ref const & p);
     virtual void collect_param_descrs(param_descrs & r);
 

src/solver/tactic2solver.cpp

@@ -107,8 +107,6 @@ lbool tactic2solver_core::check_sat_core(unsigned num_assumptions, expr * const
         return l_undef;
     tactic & t                       = *(m_ctx->m_tactic);
     simple_check_sat_result & result = *(m_ctx->m_result);
-    if (m_fparams)
-        t.set_front_end_params(*m_fparams);
     goal_ref g = alloc(goal, m, m_produce_proofs, m_produce_models, m_produce_unsat_cores);
     t.set_logic(m_ctx->m_logic);
     unsigned sz = m_ctx->m_assertions.size();

src/solver/tactic2solver.h

@@ -54,8 +54,6 @@ public:
 
     virtual tactic * get_tactic(ast_manager & m, params_ref const & p) = 0;
     
-    virtual void set_front_end_params(front_end_params & p) { m_fparams = &p; } 
-
     virtual void updt_params(params_ref const & p);
     virtual void collect_param_descrs(param_descrs & r);
 

src/tactic/tactic.h

@@ -92,7 +92,6 @@ public:
     virtual void reset() { cleanup(); }
 
     // for backward compatibility
-    virtual void set_front_end_params(front_end_params & p) {}
     virtual void set_logic(symbol const & l) {}
     virtual void set_progress_callback(progress_callback * callback) {}
 

src/tactic/tactical.cpp

@@ -87,11 +87,6 @@ public:
         m_t2->reset();
     }
 
-    virtual void set_front_end_params(front_end_params & p) {
-        m_t1->set_front_end_params(p);
-        m_t2->set_front_end_params(p);
-    }
-
     virtual void set_logic(symbol const & l) {
         m_t1->set_logic(l);
         m_t2->set_logic(l);
@@ -380,13 +375,6 @@ public:
             (*it)->reset();
     }
 
-    virtual void set_front_end_params(front_end_params & p) {
-        ptr_vector<tactic>::iterator it  = m_ts.begin();
-        ptr_vector<tactic>::iterator end = m_ts.end();
-        for (; it != end; ++it)
-            (*it)->set_front_end_params(p);
-    }
-
     virtual void set_logic(symbol const & l) {
         ptr_vector<tactic>::iterator it  = m_ts.begin();
         ptr_vector<tactic>::iterator end = m_ts.end();
@@ -992,7 +980,6 @@ public:
     virtual void cleanup(void) { m_t->cleanup(); }
     virtual void collect_statistics(statistics & st) const { m_t->collect_statistics(st); }
     virtual void reset_statistics() { m_t->reset_statistics(); }    
-    virtual void set_front_end_params(front_end_params & p) { m_t->set_front_end_params(p); }
     virtual void updt_params(params_ref const & p) { m_t->updt_params(p); }
     virtual void collect_param_descrs(param_descrs & r) { m_t->collect_param_descrs(r); }
     virtual void reset() { m_t->reset(); }