diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 6eeef935c..3eef9e3e8 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -24,12 +24,12 @@ def init_project_def():
     add_lib('parser_util', ['ast'], 'parsers/util')
     add_lib('grobner', ['ast'], 'math/grobner')
     add_lib('euclid', ['util'], 'math/euclid')
-    # Old (non-modular) parameter framework. It has been subsumed by util\params.h.
-    # However, it is still used by many old components.
-    add_lib('old_params', ['ast'])
+    # 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', 'old_params'], 'ast/simplifier')
+    add_lib('simplifier', ['rewriter', 'front_end_params'], 'ast/simplifier')
     add_lib('normal_forms', ['rewriter', 'simplifier'], 'ast/normal_forms')
     add_lib('core_tactics', ['tactic', 'normal_forms'], 'tactic/core')
     add_lib('sat_tactic', ['tactic', 'sat'], 'sat/tactic')
@@ -37,14 +37,15 @@ def init_project_def():
     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('cmd_context', ['tactic', 'rewriter', 'model', 'old_params'])
+    add_lib('solver', ['model', 'tactic', 'front_end_params'])
+    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')
     add_lib('pattern', ['normal_forms', 'smt2parser'], 'ast/pattern')
-    add_lib('macros', ['simplifier', 'old_params'], 'ast/macros')
-    add_lib('proof_checker', ['rewriter', 'old_params'], 'ast/proof_checker')
-    add_lib('bit_blaster', ['rewriter', 'simplifier', 'old_params'], 'ast/rewriter/bit_blaster')
-    add_lib('proto_model', ['model', 'simplifier', 'old_params'], 'smt/proto_model')
+    add_lib('macros', ['simplifier', 'front_end_params'], 'ast/macros')
+    add_lib('proof_checker', ['rewriter', 'front_end_params'], 'ast/proof_checker')
+    add_lib('bit_blaster', ['rewriter', 'simplifier', 'front_end_params'], 'ast/rewriter/bit_blaster')
+    add_lib('proto_model', ['model', 'simplifier', 'front_end_params'], 'smt/proto_model')
     add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model',
                     'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util'])
     add_lib('user_plugin', ['smt'], 'smt/user_plugin')
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 82865a4ac..3d316dcb8 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1086,7 +1086,8 @@ def mk_def_files():
 
 def cp_z3pyc_to_build():
     mk_dir(BUILD_DIR)
-    compileall.compile_dir(Z3PY_SRC_DIR, force=1)
+    if compileall.compile_dir(Z3PY_SRC_DIR, force=1) != 1:
+        raise MKException("failed to compile Z3Py sources")
     for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(Z3PY_SRC_DIR)):
         try:
             os.remove('%s/%s' % (BUILD_DIR, pyc))
diff --git a/scripts/update_api.py b/scripts/update_api.py
index 46251ea61..53159f10e 100644
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -670,6 +670,11 @@ mk_py_wrappers()
 mk_dotnet()
 mk_dotnet_wrappers()
 
+log_h.close()
+log_c.close()
+exe_c.close()
+core_py.close()
+
 if is_verbose():
     print "Generated '%s'" % ('%s/api_log_macros.h' % api_dir)
     print "Generated '%s'" % ('%s/api_log_macros.cpp' % api_dir)
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 71a24c534..9b3619a6e 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -80,7 +80,7 @@ extern "C" {
         LOG_Z3_mk_solver_from_tactic(c, t);
         RESET_ERROR_CODE();
         Z3_solver_ref * s = alloc(Z3_solver_ref);
-        s->m_solver       = alloc(tactic2solver_api, to_tactic_ref(t));
+        s->m_solver       = alloc(tactic2solver, to_tactic_ref(t));
         s->m_solver->set_front_end_params(mk_c(c)->fparams());
         s->m_solver->init(mk_c(c)->m(), symbol::null);
         mk_c(c)->save_object(s);
diff --git a/src/api/python/z3poly.py b/src/api/python/z3poly.py
deleted file mode 100644
index f8e6eb1f7..000000000
--- a/src/api/python/z3poly.py
+++ /dev/null
@@ -1,67 +0,0 @@
-############################################
-# Copyright (c) 2012 Microsoft Corporation
-# 
-# Z3 Polynomial interface
-#
-# Author: Leonardo de Moura (leonardo)
-############################################
-from z3 import *
-
-class PolynomialManager:
-    """Polynomial Manager.
-    """
-    def __init__(self, ctx=None):
-        self.ctx     = z3._get_ctx(ctx)
-        self.manager = Z3_mk_polynomial_manager(self.ctx_ref())
-        
-    def __del__(self):
-        Z3_del_polynomial_manager(self.ctx_ref(), self.manager)
-
-    def ctx_ref(self):
-        return self.ctx.ref()
-
-    def m(self):
-        return self.manager
-
-_main_pmanager = None
-def main_pmanager():
-    """Return a reference to the global Polynomial manager.
-    """
-    global _main_pmanager
-    if _main_pmanager == None:
-        _main_pmanager = PolynomialManager()
-    return _main_pmanager  
-
-def _get_pmanager(ctx):
-    if ctx == None:
-        return main_pmanager()
-    else:
-        return ctx
-
-class Polynomial:
-    """Multivariate polynomials.
-    """
-    def __init__(self, poly=None, m=None):
-        self.pmanager = _get_pmanager(m)
-        if poly == None:
-            self.poly = Z3_mk_zero_polynomial(self.ctx_ref(), self.m())
-        else:
-            self.poly = poly
-        Z3_polynomial_inc_ref(self.ctx_ref(), self.m(), self.poly)
-    
-    def __del__(self):
-        Z3_polynomial_dec_ref(self.ctx_ref(), self.m(), self.poly)
-
-    def m(self):
-        return self.pmanager.m()
-
-    def ctx_ref(self):
-        return self.pmanager.ctx_ref()
-    
-    def __repr__(self):
-        return Z3_polynomial_to_string(self.ctx_ref(), self.m(), self.poly)
-
-# test
-p = Polynomial()
-print p
-
diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index 879f8f4d3..c6fa7718c 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -27,6 +27,7 @@ Notes:
 #include"cmd_util.h"
 #include"simplify_cmd.h"
 #include"eval_cmd.h"
+#include"front_end_params.h"
 
 class help_cmd : public cmd {
     svector<symbol> m_cmds;
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index e9a613d4e..c56066827 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -348,6 +348,18 @@ cmd_context::~cmd_context() {
     }
 }
 
+bool cmd_context::is_smtlib2_compliant() const { 
+    return params().m_smtlib2_compliant; 
+}
+
+bool cmd_context::produce_models() const { 
+    return params().m_model; 
+}
+
+bool cmd_context::produce_proofs() const { 
+    return params().m_proof_mode != PGM_DISABLED; 
+}
+
 cmd_context::check_sat_state cmd_context::cs_state() const {
     if (m_check_sat_result.get() == 0)
         return css_clear;
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index efbfbfb75..9296f0735 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -249,7 +249,7 @@ protected:
 public:
     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 params().m_smtlib2_compliant; }
+    bool is_smtlib2_compliant() const;
     void set_logic(symbol const & s);
     bool has_logic() const { return m_logic != symbol::null; }
     symbol const & get_logic() const { return m_logic; }
@@ -269,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 params().m_model; }
-    bool produce_proofs() const { return params().m_proof_mode != PGM_DISABLED; }
+    bool produce_models() const;
+    bool produce_proofs() const;
     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; }
diff --git a/src/cmd_context/solver.h b/src/cmd_context/solver.h
deleted file mode 100644
index 373f878bb..000000000
--- a/src/cmd_context/solver.h
+++ /dev/null
@@ -1,61 +0,0 @@
-/*++
-Copyright (c) 2011 Microsoft Corporation
-
-Module Name:
-
-    solver.h
-
-Abstract:
-
-    abstract solver interface
-
-Author:
-
-    Leonardo (leonardo) 2011-03-19
-
-Notes:
-
---*/
-#ifndef _SOLVER_H_
-#define _SOLVER_H_
-
-#include"check_sat_result.h"
-#include"front_end_params.h"
-#include"progress_callback.h"
-#include"params.h"
-
-class solver : public check_sat_result {
-public:
-    virtual ~solver() {}
-    
-    // for backward compatibility
-    virtual void set_front_end_params(front_end_params & p) {} 
-
-    virtual void updt_params(params_ref const & p) {}
-    virtual void collect_param_descrs(param_descrs & r) {}
-
-    virtual void set_produce_proofs(bool f) {}
-    virtual void set_produce_models(bool f) {}
-    virtual void set_produce_unsat_cores(bool f) {}
-    
-    virtual void init(ast_manager & m, symbol const & logic) = 0;
-    virtual void reset() = 0;
-    virtual void assert_expr(expr * t) = 0;
-    virtual void push() = 0;
-    virtual void pop(unsigned n) = 0;
-    virtual unsigned get_scope_level() const = 0;
-    virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) = 0;
-
-    virtual void set_cancel(bool f) {}
-    void cancel() { set_cancel(true); }
-    void reset_cancel() { set_cancel(false); }
-
-    virtual void set_progress_callback(progress_callback * callback) = 0;
-
-    virtual unsigned get_num_assertions() const;
-    virtual expr * get_assertion(unsigned idx) const;
-
-    virtual void display(std::ostream & out) const;
-};
-
-#endif
diff --git a/src/cmd_context/strategic_solver_cmd.cpp b/src/cmd_context/strategic_solver_cmd.cpp
new file mode 100644
index 000000000..3bb820e0d
--- /dev/null
+++ b/src/cmd_context/strategic_solver_cmd.cpp
@@ -0,0 +1,34 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    strategic_solver_cmd.h
+
+Abstract:
+
+    Specialization of the strategic solver that
+    used cmd_context to access the assertion set.
+
+Author:
+
+    Leonardo (leonardo) 2012-11-01
+
+Notes:
+
+--*/
+#include"strategic_solver_cmd.h"
+#include"cmd_context.h"
+
+strategic_solver_cmd::strategic_solver_cmd(cmd_context & ctx):
+    m_ctx(ctx) {
+}
+
+unsigned strategic_solver_cmd::get_num_assertions() const {
+    return static_cast<unsigned>(m_ctx.end_assertions() - m_ctx.begin_assertions());
+}
+
+expr * strategic_solver_cmd::get_assertion(unsigned idx) const {
+    SASSERT(idx < get_num_assertions());
+    return m_ctx.begin_assertions()[idx];
+}
diff --git a/src/cmd_context/strategic_solver_cmd.h b/src/cmd_context/strategic_solver_cmd.h
new file mode 100644
index 000000000..014d2dee6
--- /dev/null
+++ b/src/cmd_context/strategic_solver_cmd.h
@@ -0,0 +1,40 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    strategic_solver_cmd.h
+
+Abstract:
+
+    Specialization of the strategic solver that
+    used cmd_context to access the assertion set.
+
+Author:
+
+    Leonardo (leonardo) 2012-11-01
+
+Notes:
+
+--*/
+#ifndef _STRATEGIC_SOLVER_CMD_H_
+#define _STRATEGIC_SOLVER_CMD_H_
+
+#include"strategic_solver.h"
+
+class cmd_context;
+
+/**
+   Specialization for the SMT 2.0 command language frontend.
+
+   The strategic solver does not have to maintain a copy of the assertion set in the cmd_context.
+*/
+class strategic_solver_cmd : public strategic_solver_core {
+    cmd_context &        m_ctx;
+public:
+    strategic_solver_cmd(cmd_context & ctx);
+    virtual unsigned get_num_assertions() const;
+    virtual expr * get_assertion(unsigned idx) const;
+};
+
+#endif 
diff --git a/src/old_params/arith_simplifier_params.cpp b/src/front_end_params/arith_simplifier_params.cpp
similarity index 100%
rename from src/old_params/arith_simplifier_params.cpp
rename to src/front_end_params/arith_simplifier_params.cpp
diff --git a/src/old_params/arith_simplifier_params.h b/src/front_end_params/arith_simplifier_params.h
similarity index 100%
rename from src/old_params/arith_simplifier_params.h
rename to src/front_end_params/arith_simplifier_params.h
diff --git a/src/old_params/bit_blaster_params.h b/src/front_end_params/bit_blaster_params.h
similarity index 100%
rename from src/old_params/bit_blaster_params.h
rename to src/front_end_params/bit_blaster_params.h
diff --git a/src/old_params/bv_simplifier_params.h b/src/front_end_params/bv_simplifier_params.h
similarity index 100%
rename from src/old_params/bv_simplifier_params.h
rename to src/front_end_params/bv_simplifier_params.h
diff --git a/src/old_params/cnf_params.cpp b/src/front_end_params/cnf_params.cpp
similarity index 100%
rename from src/old_params/cnf_params.cpp
rename to src/front_end_params/cnf_params.cpp
diff --git a/src/old_params/cnf_params.h b/src/front_end_params/cnf_params.h
similarity index 100%
rename from src/old_params/cnf_params.h
rename to src/front_end_params/cnf_params.h
diff --git a/src/old_params/dyn_ack_params.cpp b/src/front_end_params/dyn_ack_params.cpp
similarity index 100%
rename from src/old_params/dyn_ack_params.cpp
rename to src/front_end_params/dyn_ack_params.cpp
diff --git a/src/old_params/dyn_ack_params.h b/src/front_end_params/dyn_ack_params.h
similarity index 100%
rename from src/old_params/dyn_ack_params.h
rename to src/front_end_params/dyn_ack_params.h
diff --git a/src/old_params/front_end_params.cpp b/src/front_end_params/front_end_params.cpp
similarity index 100%
rename from src/old_params/front_end_params.cpp
rename to src/front_end_params/front_end_params.cpp
diff --git a/src/old_params/front_end_params.h b/src/front_end_params/front_end_params.h
similarity index 100%
rename from src/old_params/front_end_params.h
rename to src/front_end_params/front_end_params.h
diff --git a/src/old_params/model_params.cpp b/src/front_end_params/model_params.cpp
similarity index 100%
rename from src/old_params/model_params.cpp
rename to src/front_end_params/model_params.cpp
diff --git a/src/old_params/model_params.h b/src/front_end_params/model_params.h
similarity index 100%
rename from src/old_params/model_params.h
rename to src/front_end_params/model_params.h
diff --git a/src/old_params/nnf_params.cpp b/src/front_end_params/nnf_params.cpp
similarity index 100%
rename from src/old_params/nnf_params.cpp
rename to src/front_end_params/nnf_params.cpp
diff --git a/src/old_params/nnf_params.h b/src/front_end_params/nnf_params.h
similarity index 100%
rename from src/old_params/nnf_params.h
rename to src/front_end_params/nnf_params.h
diff --git a/src/old_params/order_params.cpp b/src/front_end_params/order_params.cpp
similarity index 100%
rename from src/old_params/order_params.cpp
rename to src/front_end_params/order_params.cpp
diff --git a/src/old_params/order_params.h b/src/front_end_params/order_params.h
similarity index 100%
rename from src/old_params/order_params.h
rename to src/front_end_params/order_params.h
diff --git a/src/old_params/params2front_end_params.cpp b/src/front_end_params/params2front_end_params.cpp
similarity index 100%
rename from src/old_params/params2front_end_params.cpp
rename to src/front_end_params/params2front_end_params.cpp
diff --git a/src/old_params/params2front_end_params.h b/src/front_end_params/params2front_end_params.h
similarity index 100%
rename from src/old_params/params2front_end_params.h
rename to src/front_end_params/params2front_end_params.h
diff --git a/src/old_params/parser_params.cpp b/src/front_end_params/parser_params.cpp
similarity index 100%
rename from src/old_params/parser_params.cpp
rename to src/front_end_params/parser_params.cpp
diff --git a/src/old_params/parser_params.h b/src/front_end_params/parser_params.h
similarity index 100%
rename from src/old_params/parser_params.h
rename to src/front_end_params/parser_params.h
diff --git a/src/old_params/pattern_inference_params.cpp b/src/front_end_params/pattern_inference_params.cpp
similarity index 100%
rename from src/old_params/pattern_inference_params.cpp
rename to src/front_end_params/pattern_inference_params.cpp
diff --git a/src/old_params/pattern_inference_params.h b/src/front_end_params/pattern_inference_params.h
similarity index 100%
rename from src/old_params/pattern_inference_params.h
rename to src/front_end_params/pattern_inference_params.h
diff --git a/src/old_params/preprocessor_params.h b/src/front_end_params/preprocessor_params.h
similarity index 100%
rename from src/old_params/preprocessor_params.h
rename to src/front_end_params/preprocessor_params.h
diff --git a/src/old_params/qi_params.h b/src/front_end_params/qi_params.h
similarity index 100%
rename from src/old_params/qi_params.h
rename to src/front_end_params/qi_params.h
diff --git a/src/old_params/smt_params.cpp b/src/front_end_params/smt_params.cpp
similarity index 100%
rename from src/old_params/smt_params.cpp
rename to src/front_end_params/smt_params.cpp
diff --git a/src/old_params/smt_params.h b/src/front_end_params/smt_params.h
similarity index 100%
rename from src/old_params/smt_params.h
rename to src/front_end_params/smt_params.h
diff --git a/src/old_params/spc_params.cpp b/src/front_end_params/spc_params.cpp
similarity index 100%
rename from src/old_params/spc_params.cpp
rename to src/front_end_params/spc_params.cpp
diff --git a/src/old_params/spc_params.h b/src/front_end_params/spc_params.h
similarity index 100%
rename from src/old_params/spc_params.h
rename to src/front_end_params/spc_params.h
diff --git a/src/old_params/theory_arith_params.cpp b/src/front_end_params/theory_arith_params.cpp
similarity index 100%
rename from src/old_params/theory_arith_params.cpp
rename to src/front_end_params/theory_arith_params.cpp
diff --git a/src/old_params/theory_arith_params.h b/src/front_end_params/theory_arith_params.h
similarity index 100%
rename from src/old_params/theory_arith_params.h
rename to src/front_end_params/theory_arith_params.h
diff --git a/src/old_params/theory_array_params.h b/src/front_end_params/theory_array_params.h
similarity index 100%
rename from src/old_params/theory_array_params.h
rename to src/front_end_params/theory_array_params.h
diff --git a/src/old_params/theory_bv_params.h b/src/front_end_params/theory_bv_params.h
similarity index 100%
rename from src/old_params/theory_bv_params.h
rename to src/front_end_params/theory_bv_params.h
diff --git a/src/old_params/theory_datatype_params.h b/src/front_end_params/theory_datatype_params.h
similarity index 100%
rename from src/old_params/theory_datatype_params.h
rename to src/front_end_params/theory_datatype_params.h
diff --git a/src/old_params/z3_solver_params.cpp b/src/front_end_params/z3_solver_params.cpp
similarity index 100%
rename from src/old_params/z3_solver_params.cpp
rename to src/front_end_params/z3_solver_params.cpp
diff --git a/src/old_params/z3_solver_params.h b/src/front_end_params/z3_solver_params.h
similarity index 100%
rename from src/old_params/z3_solver_params.h
rename to src/front_end_params/z3_solver_params.h
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index 3b5044b7d..c544d9edf 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -1325,7 +1325,7 @@ namespace pdr {
             for (; it != end; ++it) {
                 ptr_vector<datalog::rule> const& rules = it->m_value->rules();
                 for (unsigned i = 0; i < rules.size(); ++i) {
-                    datalog::rule* rule = rules[i];
+                    // datalog::rule* rule = rules[i];
                     // vs(rule->get_head(), 
                     // apply interpretation of predicates to rule.
                     // create formula and check for unsat.
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index ab32b384a..f288c526e 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -28,6 +28,7 @@ Revision History:
 #include"rewriter.h"
 #include"has_free_vars.h"
 #include"ast_smt2_pp.h"
+#include"front_end_params.h"
 
 namespace smt2 {
     typedef cmd_exception parser_exception;
diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp
index dd8987529..6711158fd 100644
--- a/src/shell/smtlib_frontend.cpp
+++ b/src/shell/smtlib_frontend.cpp
@@ -101,7 +101,7 @@ unsigned read_smtlib2_commands(char const* file_name, front_end_params& front_en
 
     // temporary hack until strategic_solver is ported to new tactic framework
     if (front_end_params.m_nlsat) {
-        tactic2solver_cmd * s = alloc(tactic2solver_cmd);
+        tactic_factory2solver * s = alloc(tactic_factory2solver);
         s->set_tactic(alloc(qfnra_nlsat_fct));
         ctx.set_solver(s);
     }
diff --git a/src/smt/default_solver.cpp b/src/smt/default_solver.cpp
index ad611763b..73ce084f3 100644
--- a/src/smt/default_solver.cpp
+++ b/src/smt/default_solver.cpp
@@ -19,6 +19,7 @@ Notes:
 #include"solver.h"
 #include"smt_solver.h"
 #include"reg_decl_plugins.h"
+#include"front_end_params.h"
 
 class default_solver : public solver {
     front_end_params * m_params;
diff --git a/src/solver/check_sat_result.cpp b/src/solver/check_sat_result.cpp
new file mode 100644
index 000000000..7a248e8b1
--- /dev/null
+++ b/src/solver/check_sat_result.cpp
@@ -0,0 +1,54 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    check_sat_result.cpp
+
+Abstract:
+    Abstract interface for storing the result produced by 
+    a check_sat like command
+
+Author:
+
+    Leonardo (leonardo) 2012-11-01
+
+Notes:
+
+--*/
+#include"check_sat_result.h"
+
+simple_check_sat_result::simple_check_sat_result(ast_manager & m):
+    m_core(m),
+    m_proof(m) {
+    }
+
+simple_check_sat_result::~simple_check_sat_result() {
+}
+
+void simple_check_sat_result::collect_statistics(statistics & st) const { 
+    st.copy(m_stats); 
+}
+
+void simple_check_sat_result::get_unsat_core(ptr_vector<expr> & r) { 
+    if (m_status == l_false) 
+        r.append(m_core.size(), m_core.c_ptr()); 
+}
+ 
+void simple_check_sat_result::get_model(model_ref & m) { 
+    if (m_status != l_false) 
+        m = m_model; 
+    else 
+        m = 0; 
+}
+
+proof * simple_check_sat_result::get_proof() { 
+    return m_status == l_false ? m_proof.get() : 0; 
+}
+
+std::string simple_check_sat_result::reason_unknown() const { 
+    return m_unknown; 
+}
+
+void simple_check_sat_result::get_labels(svector<symbol> & r) {
+}
diff --git a/src/cmd_context/check_sat_result.h b/src/solver/check_sat_result.h
similarity index 56%
rename from src/cmd_context/check_sat_result.h
rename to src/solver/check_sat_result.h
index fcb42acb7..ce0525fc9 100644
--- a/src/cmd_context/check_sat_result.h
+++ b/src/solver/check_sat_result.h
@@ -23,6 +23,18 @@ Notes:
 #include"lbool.h"
 #include"statistics.h"
 
+/**
+   \brief Abstract interface for the result of a (check-sat) like command.
+   It encapsulates information such as:
+      - the actual result: l_true (satisfiable), l_false (unsatisfiable), l_undef (unknown)
+      - statistics
+      - model (if the result is satisfiable)
+      - proof (if the result is unsatisfiable)
+      - unsat-core (if the result is unsatisfiable)
+      - reason-unknown (if the result is unknown, i.e., the solver failed to solve the problem)
+      - label (if the result is satisfiable) this is legacy for Boogie
+      
+*/
 class check_sat_result {
 protected:
     unsigned    m_ref_count;
@@ -42,6 +54,9 @@ public:
     virtual void get_labels(svector<symbol> & r) = 0;
 };
 
+/**
+   \brief Very simple implementation of the check_sat_result object.
+*/
 struct simple_check_sat_result : public check_sat_result {
     statistics      m_stats;
     model_ref       m_model;
@@ -49,21 +64,14 @@ struct simple_check_sat_result : public check_sat_result {
     proof_ref       m_proof;
     std::string     m_unknown;
 
-    simple_check_sat_result(ast_manager & m):
-        m_core(m),
-        m_proof(m) {
-    }
-    virtual ~simple_check_sat_result() {}
-    virtual void collect_statistics(statistics & st) const { st.copy(m_stats); }
-    virtual void get_unsat_core(ptr_vector<expr> & r) { if (m_status == l_false) r.append(m_core.size(), m_core.c_ptr()); }
-    virtual void get_model(model_ref & m) { 
-        if (m_status != l_false) m = m_model; else m = 0; 
-    }
-    virtual proof * get_proof() { return m_status == l_false ? m_proof.get() : 0; }
-    virtual std::string reason_unknown() const { 
-        return m_unknown; 
-    }
-    virtual void get_labels(svector<symbol> & r) {}
+    simple_check_sat_result(ast_manager & m);
+    virtual ~simple_check_sat_result();
+    virtual void collect_statistics(statistics & st) const;
+    virtual void get_unsat_core(ptr_vector<expr> & r);
+    virtual void get_model(model_ref & m);
+    virtual proof * get_proof();
+    virtual std::string reason_unknown() const;
+    virtual void get_labels(svector<symbol> & r);
 };
 
 #endif
diff --git a/src/cmd_context/progress_callback.h b/src/solver/progress_callback.h
similarity index 60%
rename from src/cmd_context/progress_callback.h
rename to src/solver/progress_callback.h
index 6397d7bc4..fab054671 100644
--- a/src/cmd_context/progress_callback.h
+++ b/src/solver/progress_callback.h
@@ -23,11 +23,11 @@ class progress_callback {
 public:
     virtual ~progress_callback() {}
     
-    // Called approx. every m_progress_sampling_freq miliseconds
-    virtual void slow_progress_sample() { }
-    
-    // Called on every check for reqsource limit exceeded (mach more frequent).
-    virtual void fast_progress_sample() { }
+    // Called on every check for resource limit exceeded (much more frequent).
+    virtual void fast_progress_sample() {}
+
+    // Less frequent invoked.
+    virtual void slow_progress_sample() {}
 };
 
 #endif
diff --git a/src/cmd_context/solver.cpp b/src/solver/solver.cpp
similarity index 100%
rename from src/cmd_context/solver.cpp
rename to src/solver/solver.cpp
diff --git a/src/solver/solver.h b/src/solver/solver.h
new file mode 100644
index 000000000..e8823df4f
--- /dev/null
+++ b/src/solver/solver.h
@@ -0,0 +1,153 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    solver.h
+
+Abstract:
+
+    abstract solver interface
+
+Author:
+
+    Leonardo (leonardo) 2011-03-19
+
+Notes:
+
+--*/
+#ifndef _SOLVER_H_
+#define _SOLVER_H_
+
+#include"check_sat_result.h"
+#include"progress_callback.h"
+#include"params.h"
+
+struct front_end_params;
+
+/**
+   \brief Abstract interface for making solvers available in the Z3
+   API and front-ends such as SMT 2.0 and (legacy) SMT 1.0.
+
+   It provides the basic functionality for incremental solvers.
+     - assertions
+     - push/pop
+     - parameter setting (updt_params)
+     - statistics
+     - results based on check_sat_result API
+     - interruption (set_cancel)
+     - resets 
+*/
+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. 
+    */
+    virtual void updt_params(params_ref const & p) {}
+
+    /**
+       \brief Store in \c r a description of the configuration
+       parameters available in this solver.
+    */
+    virtual void collect_param_descrs(param_descrs & r) {}
+    
+    /**
+       \brief Enable/Disable proof production for this solver object.
+    
+       It is invoked before init(m, logic).
+    */
+    virtual void set_produce_proofs(bool f) {}
+    /**
+       \brief Enable/Disable model generation for this solver object.
+
+       It is invoked before init(m, logic).
+    */
+    virtual void set_produce_models(bool f) {}
+    /**
+       \brief Enable/Disable unsat core generation for this solver object.
+
+       It is invoked before init(m, logic).
+    */
+    virtual void set_produce_unsat_cores(bool f) {}
+    
+    /**
+       \brief Initialize the solver object with the given ast_manager and logic.
+    */
+    virtual void init(ast_manager & m, symbol const & logic) = 0;
+    
+    /**
+       \brief Reset the solver internal state. All assertions should be removed.
+    */
+    virtual void reset() = 0;
+
+    /**
+       \brief Add a new formula to the assertion stack.
+    */
+    virtual void assert_expr(expr * t) = 0;
+
+    /**
+       \brief Create a backtracking point.
+    */
+    virtual void push() = 0;
+
+    /**
+       \brief Remove \c n backtracking points. All assertions between the pop and matching push are removed. 
+    */
+    virtual void pop(unsigned n) = 0;
+
+    /**
+       \brief Return the number of backtracking points.
+    */
+    virtual unsigned get_scope_level() const = 0;
+
+    /**
+       \brief Check if the set of assertions in the assertion stack is satisfiable modulo the given assumptions.
+       
+       If it is unsatisfiable, and unsat-core generation is enabled. Then, the unsat-core is a subset of these assumptions.
+    */
+    virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) = 0;
+
+    virtual void set_cancel(bool f) {}
+    /**
+       \brief Interrupt this solver.
+    */
+    void cancel() { set_cancel(true); }
+    /**
+       \brief Reset the interruption.
+    */
+    void reset_cancel() { set_cancel(false); }
+
+    /**
+       \brief Set a progress callback procedure that is invoked by this solver during check_sat.
+       
+       This is essentially for backward compatibility and integration with VCC tools.
+    */
+    virtual void set_progress_callback(progress_callback * callback) = 0;
+    
+    /**
+       \brief Return the number of assertions in the assertion stack.
+    */
+    virtual unsigned get_num_assertions() const;
+
+    /**
+       \brief Return the assertion at position idx in the assertion stack.
+    */
+    virtual expr * get_assertion(unsigned idx) const;
+
+    /**
+       \brief Display the content of this solver.
+    */
+    virtual void display(std::ostream & out) const;
+};
+
+#endif
diff --git a/src/cmd_context/strategic_solver.cpp b/src/solver/strategic_solver.cpp
similarity index 80%
rename from src/cmd_context/strategic_solver.cpp
rename to src/solver/strategic_solver.cpp
index c8d5c6fcb..a32aec2b1 100644
--- a/src/cmd_context/strategic_solver.cpp
+++ b/src/solver/strategic_solver.cpp
@@ -17,15 +17,15 @@ Notes:
 
 --*/
 #include"strategic_solver.h"
-#include"cmd_context.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
 #define PS_VB_LVL 15
 
-strategic_solver::strategic_solver():
+strategic_solver_core::strategic_solver_core():
     m_manager(0),
     m_fparams(0),
     m_force_tactic(false),
@@ -45,7 +45,7 @@ strategic_solver::strategic_solver():
     m_produce_unsat_cores = false;
 }
 
-strategic_solver::~strategic_solver() {
+strategic_solver_core::~strategic_solver_core() {
     SASSERT(!m_curr_tactic);
     dictionary<tactic_factory*>::iterator it  = m_logic2fct.begin();
     dictionary<tactic_factory*>::iterator end = m_logic2fct.end();
@@ -56,7 +56,7 @@ strategic_solver::~strategic_solver() {
         m().dec_ref(m_proof);
 }
 
-bool strategic_solver::has_quantifiers() const {
+bool strategic_solver_core::has_quantifiers() const {
     unsigned sz = get_num_assertions();
     for (unsigned i = 0; i < sz; i++) {
         if (::has_quantifiers(get_assertion(i)))
@@ -68,7 +68,7 @@ bool strategic_solver::has_quantifiers() const {
 /**
    \brief Return true if a tactic should be used when the incremental solver returns unknown.
 */
-bool strategic_solver::use_tactic_when_undef() const {
+bool strategic_solver_core::use_tactic_when_undef() const {
     switch (m_inc_unknown_behavior) {
     case IUB_RETURN_UNDEF: return false;
     case IUB_USE_TACTIC_IF_QF: return !has_quantifiers();
@@ -79,7 +79,7 @@ bool strategic_solver::use_tactic_when_undef() const {
     }
 }
 
-void strategic_solver::set_inc_solver(solver * s) {
+void strategic_solver_core::set_inc_solver(solver * s) {
     SASSERT(m_inc_solver == 0);
     SASSERT(m_num_scopes == 0);
     m_inc_solver = s;
@@ -87,7 +87,7 @@ void strategic_solver::set_inc_solver(solver * s) {
         m_inc_solver->set_progress_callback(m_callback);
 }
 
-void strategic_solver::updt_params(params_ref const & p) {
+void strategic_solver_core::updt_params(params_ref const & p) {
     if (m_inc_solver)
         m_inc_solver->updt_params(p);
     if (m_fparams)
@@ -95,7 +95,7 @@ void strategic_solver::updt_params(params_ref const & p) {
 }
 
 
-void strategic_solver::collect_param_descrs(param_descrs & r) {
+void strategic_solver_core::collect_param_descrs(param_descrs & r) {
     if (m_inc_solver)
         m_inc_solver->collect_param_descrs(r);
 }
@@ -105,7 +105,7 @@ void strategic_solver::collect_param_descrs(param_descrs & r) {
    timeout == UINT_MAX means infinite
    After the timeout a strategy is used.
 */
-void strategic_solver::set_inc_solver_timeout(unsigned timeout) {
+void strategic_solver_core::set_inc_solver_timeout(unsigned timeout) {
     m_inc_solver_timeout = timeout;
 }
 
@@ -113,14 +113,14 @@ void strategic_solver::set_inc_solver_timeout(unsigned timeout) {
    \brief Set the default tactic factory.
    It is used if there is no tactic for a given logic.
 */
-void strategic_solver::set_default_tactic(tactic_factory * fct) {
+void strategic_solver_core::set_default_tactic(tactic_factory * fct) {
     m_default_fct = fct;
 }
 
 /**
    \brief Set a tactic factory for a given logic.
 */
-void strategic_solver::set_tactic_for(symbol const & logic, tactic_factory * fct) {
+void strategic_solver_core::set_tactic_for(symbol const & logic, tactic_factory * fct) {
     tactic_factory * old_fct;
     if (m_logic2fct.find(logic, old_fct)) {
         dealloc(old_fct);
@@ -128,7 +128,7 @@ void strategic_solver::set_tactic_for(symbol const & logic, tactic_factory * fct
     m_logic2fct.insert(logic, fct);
 }
 
-void strategic_solver::init(ast_manager & m, symbol const & logic) {
+void strategic_solver_core::init(ast_manager & m, symbol const & logic) {
     m_manager = &m;
     m_logic   = logic;
     if (m_inc_mode) {
@@ -138,7 +138,7 @@ void strategic_solver::init(ast_manager & m, symbol const & logic) {
 }
 
 // delayed inc solver initialization
-void strategic_solver::init_inc_solver() {
+void strategic_solver_core::init_inc_solver() {
     if (m_inc_mode) 
         return; // solver was already initialized
     if (!m_inc_solver)
@@ -152,7 +152,7 @@ void strategic_solver::init_inc_solver() {
     }
 }
 
-void strategic_solver::collect_statistics(statistics & st) const {
+void strategic_solver_core::collect_statistics(statistics & st) const {
     if (m_use_inc_solver_results) {
         SASSERT(m_inc_solver);
         m_inc_solver->collect_statistics(st);
@@ -165,7 +165,7 @@ void strategic_solver::collect_statistics(statistics & st) const {
     }
 }
 
-void strategic_solver::reset() {
+void strategic_solver_core::reset() {
     m_logic    = symbol::null;
     m_inc_mode = false;
     m_check_sat_executed = false;
@@ -176,7 +176,7 @@ void strategic_solver::reset() {
     reset_results();
 }
 
-void strategic_solver::reset_results() {
+void strategic_solver_core::reset_results() {
     m_use_inc_solver_results = false;
     m_model = 0;
     if (m_proof) {
@@ -187,7 +187,7 @@ void strategic_solver::reset_results() {
     m_stats.reset();
 }
 
-void strategic_solver::assert_expr(expr * t) {
+void strategic_solver_core::assert_expr(expr * t) {
     if (m_check_sat_executed && !m_inc_mode) {
         // a check sat was already executed --> switch to incremental mode
         init_inc_solver();
@@ -199,14 +199,14 @@ void strategic_solver::assert_expr(expr * t) {
     }
 }
 
-void strategic_solver::push() {
+void strategic_solver_core::push() {
     DEBUG_CODE(m_num_scopes++;);
     init_inc_solver();
     if (m_inc_solver)
         m_inc_solver->push();
 }
 
-void strategic_solver::pop(unsigned n) {
+void strategic_solver_core::pop(unsigned n) {
     DEBUG_CODE({
             SASSERT(n <= m_num_scopes);
             m_num_scopes -= n;
@@ -216,7 +216,7 @@ void strategic_solver::pop(unsigned n) {
         m_inc_solver->pop(n);
 }
 
-unsigned strategic_solver::get_scope_level() const {
+unsigned strategic_solver_core::get_scope_level() const {
     if (m_inc_solver)
         return m_inc_solver->get_scope_level();
     else
@@ -233,10 +233,10 @@ struct aux_timeout_eh : public event_handler {
     }
 };
 
-struct strategic_solver::mk_tactic {
-    strategic_solver *  m_solver;
+struct strategic_solver_core::mk_tactic {
+    strategic_solver_core *  m_solver;
 
-    mk_tactic(strategic_solver * s, tactic_factory * f):m_solver(s) {
+    mk_tactic(strategic_solver_core * s, tactic_factory * f):m_solver(s) {
         ast_manager & m = s->m();
         params_ref p;
         front_end_params2params(*s->m_fparams, p);
@@ -259,14 +259,14 @@ struct strategic_solver::mk_tactic {
     }
 };
 
-tactic_factory * strategic_solver::get_tactic_factory() const {
+tactic_factory * strategic_solver_core::get_tactic_factory() const {
     tactic_factory * f = 0;
     if (m_logic2fct.find(m_logic, f))
         return f;
     return m_default_fct.get();
 }
 
-lbool strategic_solver::check_sat_with_assumptions(unsigned num_assumptions, expr * const * assumptions) {
+lbool strategic_solver_core::check_sat_with_assumptions(unsigned num_assumptions, expr * const * assumptions) {
     if (!m_inc_solver) {
         IF_VERBOSE(PS_VB_LVL, verbose_stream() << "incremental solver was not installed, returning unknown...\n";);
         m_use_inc_solver_results = false;
@@ -278,7 +278,7 @@ lbool strategic_solver::check_sat_with_assumptions(unsigned num_assumptions, exp
     return m_inc_solver->check_sat(num_assumptions, assumptions);
 }
 
-lbool strategic_solver::check_sat(unsigned num_assumptions, expr * const * assumptions) {
+lbool strategic_solver_core::check_sat(unsigned num_assumptions, expr * const * assumptions) {
     reset_results();
     m_check_sat_executed = true;
     if (num_assumptions > 0 || // assumptions were provided
@@ -351,7 +351,7 @@ lbool strategic_solver::check_sat(unsigned num_assumptions, expr * const * assum
     return r;
 }
 
-void strategic_solver::set_cancel(bool f) {
+void strategic_solver_core::set_cancel(bool f) {
     if (m_inc_solver)
         m_inc_solver->set_cancel(f);
     #pragma omp critical (strategic_solver)
@@ -361,14 +361,14 @@ void strategic_solver::set_cancel(bool f) {
     }
 }
 
-void strategic_solver::get_unsat_core(ptr_vector<expr> & r) {
+void strategic_solver_core::get_unsat_core(ptr_vector<expr> & r) {
     if (m_use_inc_solver_results) {
         SASSERT(m_inc_solver);
         m_inc_solver->get_unsat_core(r); 
     }
 }
 
-void strategic_solver::get_model(model_ref & m) {
+void strategic_solver_core::get_model(model_ref & m) {
     if (m_use_inc_solver_results) {
         SASSERT(m_inc_solver);
         m_inc_solver->get_model(m);
@@ -378,7 +378,7 @@ void strategic_solver::get_model(model_ref & m) {
     }
 }
 
-proof * strategic_solver::get_proof() {
+proof * strategic_solver_core::get_proof() {
     if (m_use_inc_solver_results) {
         SASSERT(m_inc_solver);
         return m_inc_solver->get_proof();
@@ -388,7 +388,7 @@ proof * strategic_solver::get_proof() {
     }
 }
 
-std::string strategic_solver::reason_unknown() const {
+std::string strategic_solver_core::reason_unknown() const {
     if (m_use_inc_solver_results) {
         SASSERT(m_inc_solver);
         return m_inc_solver->reason_unknown();
@@ -396,20 +396,20 @@ std::string strategic_solver::reason_unknown() const {
     return m_reason_unknown;
 }
 
-void strategic_solver::get_labels(svector<symbol> & r) {
+void strategic_solver_core::get_labels(svector<symbol> & r) {
     if (m_use_inc_solver_results) {
         SASSERT(m_inc_solver);
         m_inc_solver->get_labels(r);
     }
 }
 
-void strategic_solver::set_progress_callback(progress_callback * callback) { 
+void strategic_solver_core::set_progress_callback(progress_callback * callback) { 
     m_callback = callback; 
     if (m_inc_solver)
         m_inc_solver->set_progress_callback(callback);
 }
 
-void strategic_solver::display(std::ostream & out) const {
+void strategic_solver_core::display(std::ostream & out) const {
     if (m_manager) {
         unsigned num = get_num_assertions();
         out << "(solver";
@@ -423,62 +423,50 @@ void strategic_solver::display(std::ostream & out) const {
     }
 }
 
-strategic_solver_cmd::strategic_solver_cmd(cmd_context & ctx):
-    m_ctx(ctx) {
+
+strategic_solver::ctx::ctx(ast_manager & m):m_assertions(m) {
 }
 
-unsigned strategic_solver_cmd::get_num_assertions() const {
-    return static_cast<unsigned>(m_ctx.end_assertions() - m_ctx.begin_assertions());
-}
-
-expr * strategic_solver_cmd::get_assertion(unsigned idx) const {
-    SASSERT(idx < get_num_assertions());
-    return m_ctx.begin_assertions()[idx];
-}
-
-strategic_solver_api::ctx::ctx(ast_manager & m):m_assertions(m) {
-}
-
-void strategic_solver_api::init(ast_manager & m, symbol const & logic) {
-    strategic_solver::init(m, logic);
+void strategic_solver::init(ast_manager & m, symbol const & logic) {
+    strategic_solver_core::init(m, logic);
     m_ctx = alloc(ctx, m);
 }
 
-unsigned strategic_solver_api::get_num_assertions() const {
+unsigned strategic_solver::get_num_assertions() const {
     if (m_ctx == 0)
         return 0;
     return m_ctx->m_assertions.size();
 }
 
-expr * strategic_solver_api::get_assertion(unsigned idx) const {
+expr * strategic_solver::get_assertion(unsigned idx) const {
     SASSERT(m_ctx);
     return m_ctx->m_assertions.get(idx);
 }
 
-void strategic_solver_api::assert_expr(expr * t) {
+void strategic_solver::assert_expr(expr * t) {
     SASSERT(m_ctx);
-    strategic_solver::assert_expr(t);
+    strategic_solver_core::assert_expr(t);
     m_ctx->m_assertions.push_back(t);
 }
 
-void strategic_solver_api::push() {
+void strategic_solver::push() {
     SASSERT(m_ctx);
-    strategic_solver::push();
+    strategic_solver_core::push();
     m_ctx->m_scopes.push_back(m_ctx->m_assertions.size());
 }
 
-void strategic_solver_api::pop(unsigned n) {
+void strategic_solver::pop(unsigned n) {
     SASSERT(m_ctx);
     unsigned new_lvl = m_ctx->m_scopes.size() - n;
     unsigned old_sz  = m_ctx->m_scopes[new_lvl];
     m_ctx->m_assertions.shrink(old_sz);
     m_ctx->m_scopes.shrink(new_lvl);
-    strategic_solver::pop(n);
+    strategic_solver_core::pop(n);
 }
 
-void strategic_solver_api::reset() {
+void strategic_solver::reset() {
     m_ctx = 0;
-    strategic_solver::reset();
+    strategic_solver_core::reset();
 }
 
 
diff --git a/src/cmd_context/strategic_solver.h b/src/solver/strategic_solver.h
similarity index 80%
rename from src/cmd_context/strategic_solver.h
rename to src/solver/strategic_solver.h
index b145da5f7..4d4a47388 100644
--- a/src/cmd_context/strategic_solver.h
+++ b/src/solver/strategic_solver.h
@@ -25,7 +25,28 @@ Notes:
 class progress_callback;
 struct front_end_params;
 
-class strategic_solver : public solver {
+/**
+   \brief Implementation of the solver API that supports:
+       - a different tactic for each logic 
+       - a general purpose tactic
+       - a default incremental solver
+
+   The strategic solver has two modes:
+       - non-incremental
+       - incremental
+   In non-incremental mode, tactics are used.
+   In incremental model, the incremental (general purpose) solver is used.
+   
+   A timeout for the incremental solver can be specified.
+   If the timeout is reached, then the strategic_solver tries to solve the problem using tactics.
+
+   The strategic_solver switches to incremental when:
+       - push is used
+       - assertions are peformed after a check_sat
+   It goes back to non_incremental mode when:
+       - reset is invoked.
+*/
+class strategic_solver_core : public solver {
 public:
     // Behavior when the incremental solver returns unknown.
     enum inc_unknown_behavior {
@@ -76,8 +97,8 @@ private:
     bool use_tactic_when_undef() const;
 
 public:
-    strategic_solver();
-    ~strategic_solver();
+    strategic_solver_core();
+    ~strategic_solver_core();
 
     ast_manager & m() const { SASSERT(m_manager); return *m_manager; }
 
@@ -119,17 +140,10 @@ public:
     virtual void set_progress_callback(progress_callback * callback);
 };
 
-// Specialization for the SMT 2.0 command language frontend
-class strategic_solver_cmd : public strategic_solver {
-    cmd_context &        m_ctx;
-public:
-    strategic_solver_cmd(cmd_context & ctx);
-    virtual unsigned get_num_assertions() const;
-    virtual expr * get_assertion(unsigned idx) const;
-};
-
-// Specialization for Z3 API
-class strategic_solver_api : public strategic_solver {
+/**
+   \brief Default implementation of strategic_solver_core
+*/
+class strategic_solver : public strategic_solver_core {
     struct ctx {
         expr_ref_vector              m_assertions;
         unsigned_vector              m_scopes;
@@ -137,7 +151,7 @@ class strategic_solver_api : public strategic_solver {
     };
     scoped_ptr<ctx>            m_ctx;
 public:
-    strategic_solver_api() {}
+    strategic_solver() {}
 
     virtual void init(ast_manager & m, symbol const & logic);
 
diff --git a/src/cmd_context/tactic2solver.cpp b/src/solver/tactic2solver.cpp
similarity index 72%
rename from src/cmd_context/tactic2solver.cpp
rename to src/solver/tactic2solver.cpp
index 6b67faae1..0747c7c9d 100644
--- a/src/cmd_context/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -23,26 +23,26 @@ Notes:
 #include"params2front_end_params.h"
 #include"ast_smt2_pp.h"
 
-tactic2solver::ctx::ctx(ast_manager & m, symbol const & logic):
+tactic2solver_core::ctx::ctx(ast_manager & m, symbol const & logic):
     m_logic(logic),
     m_assertions(m) {
 }
 
-tactic2solver::~tactic2solver() {
+tactic2solver_core::~tactic2solver_core() {
 }
 
-void tactic2solver::init(ast_manager & m, symbol const & logic) {
+void tactic2solver_core::init(ast_manager & m, symbol const & logic) {
     m_ctx = alloc(ctx, m, logic);
 }
 
-void tactic2solver::updt_params(params_ref const & p) {
+void tactic2solver_core::updt_params(params_ref const & p) {
     m_params = p;
 }
 
-void tactic2solver::collect_param_descrs(param_descrs & r) {
+void tactic2solver_core::collect_param_descrs(param_descrs & r) {
     if (m_ctx) {
         if (!m_ctx->m_tactic) {
-            #pragma omp critical (tactic2solver)
+            #pragma omp critical (tactic2solver_core)
             {
                 m_ctx->m_tactic = get_tactic(m_ctx->m(), m_params);
             }
@@ -51,7 +51,7 @@ void tactic2solver::collect_param_descrs(param_descrs & r) {
                 m_ctx->m_tactic->collect_param_descrs(r);
             }
 
-            #pragma omp critical (tactic2solver)
+            #pragma omp critical (tactic2solver_core)
             {
                 m_ctx->m_tactic = 0;
             }
@@ -62,26 +62,26 @@ void tactic2solver::collect_param_descrs(param_descrs & r) {
     }
 }
 
-void tactic2solver::reset() {
+void tactic2solver_core::reset() {
     SASSERT(m_ctx);
     m_ctx->m_assertions.reset();
     m_ctx->m_scopes.reset();
     m_ctx->m_result = 0;
 }
 
-void tactic2solver::assert_expr(expr * t) {
+void tactic2solver_core::assert_expr(expr * t) {
     SASSERT(m_ctx);
     m_ctx->m_assertions.push_back(t);
     m_ctx->m_result = 0;
 }
 
-void tactic2solver::push() {
+void tactic2solver_core::push() {
     SASSERT(m_ctx);
     m_ctx->m_scopes.push_back(m_ctx->m_assertions.size());
     m_ctx->m_result = 0;
 }
 
-void tactic2solver::pop(unsigned n) {
+void tactic2solver_core::pop(unsigned n) {
     SASSERT(m_ctx);
     unsigned new_lvl = m_ctx->m_scopes.size() - n;
     unsigned old_sz  = m_ctx->m_scopes[new_lvl];
@@ -90,18 +90,18 @@ void tactic2solver::pop(unsigned n) {
     m_ctx->m_result = 0;
 }
 
-unsigned tactic2solver::get_scope_level() const {
+unsigned tactic2solver_core::get_scope_level() const {
     SASSERT(m_ctx);
     return m_ctx->m_scopes.size();
 }
 
-lbool tactic2solver::check_sat(unsigned num_assumptions, expr * const * assumptions) {
+lbool tactic2solver_core::check_sat(unsigned num_assumptions, expr * const * assumptions) {
     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)
+    #pragma omp critical (tactic2solver_core)
     {
         m_ctx->m_tactic = get_tactic(m, p);
         if (m_ctx->m_tactic) {
@@ -147,7 +147,7 @@ lbool tactic2solver::check_sat(unsigned num_assumptions, expr * const * assumpti
         throw ex;
     }
     catch (z3_exception & ex) {
-        TRACE("tactic2solver", tout << "exception: " << ex.msg() << "\n";);
+        TRACE("tactic2solver_core", tout << "exception: " << ex.msg() << "\n";);
         result.set_status(l_undef);
         result.m_unknown = ex.msg();
     }
@@ -160,63 +160,63 @@ lbool tactic2solver::check_sat(unsigned num_assumptions, expr * const * assumpti
         result.m_core.append(core_elems.size(), core_elems.c_ptr());
     }
     
-    #pragma omp critical (tactic2solver)
+    #pragma omp critical (tactic2solver_core)
     {
         m_ctx->m_tactic = 0;
     }
     return result.status();
 }
 
-void tactic2solver::set_cancel(bool f) {
-    #pragma omp critical (tactic2solver)
+void tactic2solver_core::set_cancel(bool f) {
+    #pragma omp critical (tactic2solver_core)
     {
         if (m_ctx && m_ctx->m_tactic)
             m_ctx->m_tactic->set_cancel(f);
     }
 }
 
-void tactic2solver::collect_statistics(statistics & st) const {
+void tactic2solver_core::collect_statistics(statistics & st) const {
     if (m_ctx->m_result.get())
         m_ctx->m_result->collect_statistics(st);
 }
 
-void tactic2solver::get_unsat_core(ptr_vector<expr> & r) {
+void tactic2solver_core::get_unsat_core(ptr_vector<expr> & r) {
     if (m_ctx->m_result.get())
         m_ctx->m_result->get_unsat_core(r);
 }
 
-void tactic2solver::get_model(model_ref & m) {
+void tactic2solver_core::get_model(model_ref & m) {
     if (m_ctx->m_result.get())
         m_ctx->m_result->get_model(m);
 }
 
-proof * tactic2solver::get_proof() {
+proof * tactic2solver_core::get_proof() {
     if (m_ctx->m_result.get())
         return m_ctx->m_result->get_proof();
     else
         return 0;
 }
 
-std::string tactic2solver::reason_unknown() const {
+std::string tactic2solver_core::reason_unknown() const {
     if (m_ctx->m_result.get())
         return m_ctx->m_result->reason_unknown();
     else
         return std::string("unknown");
 }
 
-unsigned tactic2solver::get_num_assertions() const {
+unsigned tactic2solver_core::get_num_assertions() const {
     if (m_ctx) 
         return m_ctx->m_assertions.size();
     else
         return 0;
 }
 
-expr * tactic2solver::get_assertion(unsigned idx) const {
+expr * tactic2solver_core::get_assertion(unsigned idx) const {
     SASSERT(m_ctx);
     return m_ctx->m_assertions.get(idx);
 }
 
-void tactic2solver::display(std::ostream & out) const {
+void tactic2solver_core::display(std::ostream & out) const {
     if (m_ctx) {
         ast_manager & m = m_ctx->m_assertions.m();
         unsigned num = m_ctx->m_assertions.size();
@@ -231,19 +231,28 @@ void tactic2solver::display(std::ostream & out) const {
     }
 }
 
-void tactic2solver_cmd::set_tactic(tactic_factory * f) {
-    m_tactic_factory = f;
+tactic2solver::tactic2solver(tactic * t):
+    m_tactic(t) {
 }
 
-tactic * tactic2solver_cmd::get_tactic(ast_manager & m, params_ref const & p) {
-    if (m_tactic_factory == 0)
-        return 0;
-    return (*m_tactic_factory)(m, p);
+tactic2solver::~tactic2solver() {
 }
 
-tactic * tactic2solver_api::get_tactic(ast_manager & m, params_ref const & p) {
+tactic * tactic2solver::get_tactic(ast_manager & m, params_ref const & p) {
     m_tactic->cleanup();
     m_tactic->updt_params(p);
     return m_tactic.get();
 }
 
+tactic_factory2solver::~tactic_factory2solver() {
+}
+
+void tactic_factory2solver::set_tactic(tactic_factory * f) {
+    m_tactic_factory = f;
+}
+
+tactic * tactic_factory2solver::get_tactic(ast_manager & m, params_ref const & p) {
+    if (m_tactic_factory == 0)
+        return 0;
+    return (*m_tactic_factory)(m, p);
+}
diff --git a/src/cmd_context/tactic2solver.h b/src/solver/tactic2solver.h
similarity index 82%
rename from src/cmd_context/tactic2solver.h
rename to src/solver/tactic2solver.h
index 954dda041..fe92f3a7d 100644
--- a/src/cmd_context/tactic2solver.h
+++ b/src/solver/tactic2solver.h
@@ -25,7 +25,14 @@ Notes:
 #include"solver.h"
 #include"tactic.h"
 
-class tactic2solver : public solver {
+/**
+   \brief Simulates the incremental solver interface using a tactic.
+
+   Every query will be solved from scratch.  So, this is not a good
+   option for applications trying to solve many easy queries that a
+   similar to each other.
+*/
+class tactic2solver_core : public solver {
     struct ctx {
         symbol                       m_logic;
         expr_ref_vector              m_assertions;
@@ -42,8 +49,8 @@ class tactic2solver : public solver {
     bool                       m_produce_proofs;
     bool                       m_produce_unsat_cores;
 public:
-    tactic2solver():m_ctx(0), m_fparams(0), m_produce_models(false), m_produce_proofs(false), m_produce_unsat_cores(false) {}
-    virtual ~tactic2solver();
+    tactic2solver_core():m_ctx(0), m_fparams(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;
     
@@ -81,13 +88,19 @@ public:
     virtual void display(std::ostream & out) const;
 };
 
-/**
-   \brief Specialization for cmd_context
-*/
-class tactic2solver_cmd : public tactic2solver {
+class tactic2solver : public tactic2solver_core {
+    tactic_ref m_tactic;
+public:
+    tactic2solver(tactic * t);
+    virtual ~tactic2solver();
+    virtual tactic * get_tactic(ast_manager & m, params_ref const & p);
+};
+
+
+class tactic_factory2solver : public tactic2solver_core {
     scoped_ptr<tactic_factory> m_tactic_factory;
 public:
-    virtual ~tactic2solver_cmd() {}
+    virtual ~tactic_factory2solver();
     /**
        \brief Set tactic that will be used to process the satisfiability queries.
     */
@@ -95,16 +108,5 @@ public:
     virtual tactic * get_tactic(ast_manager & m, params_ref const & p);
 };
 
-/**
-   \brief Specialization for API
-*/
-class tactic2solver_api : public tactic2solver {
-    tactic_ref m_tactic;
-public:
-    tactic2solver_api(tactic * t):m_tactic(t) {}
-    virtual ~tactic2solver_api() {}
-    virtual tactic * get_tactic(ast_manager & m, params_ref const & p);
-};
-
 
 #endif
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index caf67084d..52762edc4 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -19,7 +19,7 @@ Notes:
 --*/
 #include"cmd_context.h"
 #include"ni_solver.h"
-#include"strategic_solver.h"
+#include"strategic_solver_cmd.h"
 #include"qfbv_tactic.h"
 #include"qflia_tactic.h"
 #include"qfnia_tactic.h"
@@ -56,7 +56,7 @@ MK_SIMPLE_TACTIC_FACTORY(qfnra_fct, mk_qfnra_tactic(m, p));
 MK_SIMPLE_TACTIC_FACTORY(qffpa_fct, mk_qffpa_tactic(m, p));
 MK_SIMPLE_TACTIC_FACTORY(ufbv_fct, mk_ufbv_tactic(m, p));
 
-static void init(strategic_solver * s) {
+static void init(strategic_solver_core * s) {
     s->set_default_tactic(alloc(default_fct));
     s->set_tactic_for(symbol("QF_UF"),     alloc(qfuf_fct));
     s->set_tactic_for(symbol("QF_BV"),     alloc(qfbv_fct));
@@ -81,14 +81,14 @@ static void init(strategic_solver * s) {
 }
 
 solver * mk_smt_strategic_solver(cmd_context & ctx) {
-    strategic_solver * s = alloc(strategic_solver_cmd, ctx);
+    strategic_solver_cmd * s = alloc(strategic_solver_cmd, ctx);
     s->set_inc_solver(mk_quasi_incremental_smt_solver(ctx));
     init(s);
     return s;
 }
 
 solver * mk_smt_strategic_solver(bool force_tactic) {
-    strategic_solver * s = alloc(strategic_solver_api);
+    strategic_solver * s = alloc(strategic_solver);
     s->force_tactic(force_tactic);
     s->set_inc_solver(mk_default_solver());
     init(s);