diff --git a/mk_make.py b/mk_make.py
index 1ae145066..9481e10b9 100644
--- a/mk_make.py
+++ b/mk_make.py
@@ -8,16 +8,13 @@
 ############################################
 from mk_util import *
 
-BUILD_DIR='build-test'
-SRC_DIR='src'
-MODES=['Debug', 'Release']
-PLATFORMS=['Win32', 'x64']
-VS_COMMON_OPTIONS='WIN32;_WINDOWS;ASYNC_COMMANDS'
-VS_DBG_OPTIONS='Z3DEBUG;_TRACE;_DEBUG'
-VS_RELEASE_OPTIONS='NDEBUG;_EXTERNAL_RELEASE'
-
-# Initialization
-mk_dir(BUILD_DIR)
+set_build_dir('build-test')
+set_src_dir('src')
+set_modes(['Debug', 'Release'])
+set_platforms(['Win32', 'x64'])
+set_vs_options('WIN32;_WINDOWS;ASYNC_COMMANDS',
+               'Z3DEBUG;_TRACE;_DEBUG',
+               'NDEBUG;_EXTERNAL_RELEASE')
 
 add_lib('util', [])
 add_lib('polynomial', ['util'])
@@ -32,5 +29,8 @@ add_lib('simplifier', ['util', 'ast', 'rewriter'])
 # Model module should not depend on simplifier module. 
 # We must replace all occurrences of simplifier with rewriter.
 add_lib('model', ['util', 'ast', 'rewriter', 'simplifier'])
-add_lib('tactic', ['util', 'ast'])
+# 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', ['util', 'ast', 'simplifier', 'model'])
+add_lib('framework', ['util', 'ast', 'model', 'old_params', 'simplifier', 'rewriter'])
 
diff --git a/mk_util.py b/mk_util.py
index 5073504c6..191c9787f 100644
--- a/mk_util.py
+++ b/mk_util.py
@@ -9,6 +9,38 @@
 import os
 import glob
 
+BUILD_DIR='build'
+SRC_DIR='src'
+MODES=[]
+PLATFORMS=[]
+
+def set_build_dir(d):
+    global BUILD_DIR
+    BUILD_DIR = d
+    mk_dir(BUILD_DIR)
+
+def set_src_dir(d):
+    global SRC_DIR
+    SRC_DIR = d
+
+def set_modes(l):
+    global MODES
+    MODES=l
+
+def set_platforms(l):
+    global PLATFORMS
+    PLATFORMS=l
+
+VS_COMMON_OPTIONS='WIN32'
+VS_DBG_OPTIONS='_DEBUG'
+VS_RELEASE_OPTIONS='NDEBUG'
+
+def set_vs_options(common, dbg, release):
+    global VS_COMMON_OPTIONS, VS_DBG_OPTIONS, VS_RELEASE_OPTIONS
+    VS_COMMON_OPTIONS = common
+    VS_DBG_OPTIONS = dbg
+    VS_RELEASE_OPTIONS = release
+
 def is_debug(mode):
     return mode == 'Debug'
 
diff --git a/src/framework/README b/src/framework/README
new file mode 100644
index 000000000..695db970b
--- /dev/null
+++ b/src/framework/README
@@ -0,0 +1 @@
+tactic and command context frameworks.
\ No newline at end of file
diff --git a/lib/basic_cmds.cpp b/src/framework/basic_cmds.cpp
similarity index 99%
rename from lib/basic_cmds.cpp
rename to src/framework/basic_cmds.cpp
index d05c69baa..879f8f4d3 100644
--- a/lib/basic_cmds.cpp
+++ b/src/framework/basic_cmds.cpp
@@ -27,7 +27,6 @@ Notes:
 #include"cmd_util.h"
 #include"simplify_cmd.h"
 #include"eval_cmd.h"
-#include"qe_cmd.h"
 
 class help_cmd : public cmd {
     svector<symbol> m_cmds;
@@ -770,5 +769,4 @@ void install_ext_basic_cmds(cmd_context & ctx) {
     ctx.insert(alloc(builtin_cmd, "reset", 0, "reset the shell (all declarations and assertions will be erased)"));
     install_simplify_cmd(ctx);
     install_eval_cmd(ctx);
-    install_qe_cmd(ctx);
 }
diff --git a/lib/basic_cmds.h b/src/framework/basic_cmds.h
similarity index 100%
rename from lib/basic_cmds.h
rename to src/framework/basic_cmds.h
diff --git a/lib/check_logic.cpp b/src/framework/check_logic.cpp
similarity index 99%
rename from lib/check_logic.cpp
rename to src/framework/check_logic.cpp
index 550240a71..820ef59a4 100644
--- a/lib/check_logic.cpp
+++ b/src/framework/check_logic.cpp
@@ -21,6 +21,7 @@ Revision History:
 #include"array_decl_plugin.h"
 #include"bv_decl_plugin.h"
 #include"ast_pp.h"
+#include"for_each_expr.h"
 
 struct check_logic::imp {
     ast_manager & m;
diff --git a/lib/check_logic.h b/src/framework/check_logic.h
similarity index 95%
rename from lib/check_logic.h
rename to src/framework/check_logic.h
index 8521ed57b..6fdfc5654 100644
--- a/lib/check_logic.h
+++ b/src/framework/check_logic.h
@@ -19,7 +19,7 @@ Revision History:
 #ifndef _CHECK_LOGIC_H_
 #define _CHECK_LOGIC_H_
 
-#include"assertion_set.h"
+#include"ast.h"
 
 class check_logic {
     struct imp;
diff --git a/lib/check_sat_result.h b/src/framework/check_sat_result.h
similarity index 100%
rename from lib/check_sat_result.h
rename to src/framework/check_sat_result.h
diff --git a/lib/cmd_context.cpp b/src/framework/cmd_context.cpp
similarity index 99%
rename from lib/cmd_context.cpp
rename to src/framework/cmd_context.cpp
index 333e53b3a..1eb0f63e7 100644
--- a/lib/cmd_context.cpp
+++ b/src/framework/cmd_context.cpp
@@ -16,6 +16,7 @@ Notes:
 
 --*/
 #include<signal.h>
+#include"front_end_params.h"
 #include"tptr.h"
 #include"cmd_context.h"
 #include"func_decl_dependencies.h"
@@ -36,6 +37,7 @@ Notes:
 #include"decl_collector.h"
 #include"well_sorted.h"
 #include"model_evaluator.h"
+#include"for_each_expr.h"
 
 func_decls::func_decls(ast_manager & m, func_decl * f):
     m_decls(TAG(func_decl*, f, 0)) {
@@ -321,7 +323,7 @@ cmd_context::cmd_context(front_end_params & params, bool main_ctx, ast_manager *
     SASSERT(m != 0 || !has_manager());
     install_basic_cmds(*this);
     install_ext_basic_cmds(*this);
-    install_tactic_cmds(*this);
+    install_core_tactic_cmds(*this);
     SASSERT(m != 0 || !has_manager());
     if (m)
         init_external_manager();
diff --git a/lib/cmd_context.h b/src/framework/cmd_context.h
similarity index 99%
rename from lib/cmd_context.h
rename to src/framework/cmd_context.h
index 381abce1c..017f26428 100644
--- a/lib/cmd_context.h
+++ b/src/framework/cmd_context.h
@@ -24,7 +24,6 @@ Notes:
 #include<sstream>
 #include"ast.h"
 #include"pdecl.h"
-#include"front_end_params.h"
 #include"dictionary.h"
 #include"solver.h"
 #include"datatype_decl_plugin.h"
@@ -37,6 +36,8 @@ Notes:
 #include"progress_callback.h"
 #include"scoped_ptr_vector.h"
 
+struct front_end_params;
+
 class func_decls {
     func_decl * m_decls;
 public:
diff --git a/lib/cmd_util.cpp b/src/framework/cmd_util.cpp
similarity index 100%
rename from lib/cmd_util.cpp
rename to src/framework/cmd_util.cpp
diff --git a/lib/cmd_util.h b/src/framework/cmd_util.h
similarity index 100%
rename from lib/cmd_util.h
rename to src/framework/cmd_util.h
diff --git a/lib/converter.h b/src/framework/converter.h
similarity index 100%
rename from lib/converter.h
rename to src/framework/converter.h
diff --git a/lib/eval_cmd.cpp b/src/framework/eval_cmd.cpp
similarity index 100%
rename from lib/eval_cmd.cpp
rename to src/framework/eval_cmd.cpp
diff --git a/lib/eval_cmd.h b/src/framework/eval_cmd.h
similarity index 100%
rename from lib/eval_cmd.h
rename to src/framework/eval_cmd.h
diff --git a/src/tactic/goal.cpp b/src/framework/goal.cpp
similarity index 100%
rename from src/tactic/goal.cpp
rename to src/framework/goal.cpp
diff --git a/src/tactic/goal.h b/src/framework/goal.h
similarity index 100%
rename from src/tactic/goal.h
rename to src/framework/goal.h
diff --git a/lib/goal_util.cpp b/src/framework/goal_util.cpp
similarity index 100%
rename from lib/goal_util.cpp
rename to src/framework/goal_util.cpp
diff --git a/lib/goal_util.h b/src/framework/goal_util.h
similarity index 100%
rename from lib/goal_util.h
rename to src/framework/goal_util.h
diff --git a/lib/model_converter.cpp b/src/framework/model_converter.cpp
similarity index 100%
rename from lib/model_converter.cpp
rename to src/framework/model_converter.cpp
diff --git a/lib/model_converter.h b/src/framework/model_converter.h
similarity index 100%
rename from lib/model_converter.h
rename to src/framework/model_converter.h
diff --git a/lib/parametric_cmd.cpp b/src/framework/parametric_cmd.cpp
similarity index 100%
rename from lib/parametric_cmd.cpp
rename to src/framework/parametric_cmd.cpp
diff --git a/lib/parametric_cmd.h b/src/framework/parametric_cmd.h
similarity index 86%
rename from lib/parametric_cmd.h
rename to src/framework/parametric_cmd.h
index 4acf41b9e..762d6bd72 100644
--- a/lib/parametric_cmd.h
+++ b/src/framework/parametric_cmd.h
@@ -58,16 +58,19 @@ public:
         m_last = symbol::null; 
     }
     virtual void set_next_arg(cmd_context & ctx, sort * s) { 
-        m_params.set_sort(m_last, s); 
-        m_last = symbol::null; 
+        NOT_IMPLEMENTED_YET();
+        // m_params.set_sort(m_last, s); 
+        // m_last = symbol::null; 
     }
     virtual void set_next_arg(cmd_context & ctx, expr * t) { 
-        m_params.set_expr(m_last, t); 
-        m_last = symbol::null; 
+        NOT_IMPLEMENTED_YET();
+        // m_params.set_expr(m_last, t); 
+        // m_last = symbol::null; 
     }
     virtual void set_next_arg(cmd_context & ctx, func_decl * f) { 
-        m_params.set_func_decl(m_last, f); 
-        m_last = symbol::null; 
+        NOT_IMPLEMENTED_YET();
+        // m_params.set_func_decl(m_last, f); 
+        // m_last = symbol::null; 
     }
 };
 
diff --git a/lib/pdecl.cpp b/src/framework/pdecl.cpp
similarity index 100%
rename from lib/pdecl.cpp
rename to src/framework/pdecl.cpp
diff --git a/lib/pdecl.h b/src/framework/pdecl.h
similarity index 100%
rename from lib/pdecl.h
rename to src/framework/pdecl.h
diff --git a/lib/probe.cpp b/src/framework/probe.cpp
similarity index 100%
rename from lib/probe.cpp
rename to src/framework/probe.cpp
diff --git a/lib/probe.h b/src/framework/probe.h
similarity index 100%
rename from lib/probe.h
rename to src/framework/probe.h
diff --git a/lib/progress_callback.h b/src/framework/progress_callback.h
similarity index 100%
rename from lib/progress_callback.h
rename to src/framework/progress_callback.h
diff --git a/lib/proof_converter.cpp b/src/framework/proof_converter.cpp
similarity index 100%
rename from lib/proof_converter.cpp
rename to src/framework/proof_converter.cpp
diff --git a/lib/proof_converter.h b/src/framework/proof_converter.h
similarity index 100%
rename from lib/proof_converter.h
rename to src/framework/proof_converter.h
diff --git a/lib/simplify_cmd.cpp b/src/framework/simplify_cmd.cpp
similarity index 100%
rename from lib/simplify_cmd.cpp
rename to src/framework/simplify_cmd.cpp
diff --git a/lib/simplify_cmd.h b/src/framework/simplify_cmd.h
similarity index 100%
rename from lib/simplify_cmd.h
rename to src/framework/simplify_cmd.h
diff --git a/lib/solver.cpp b/src/framework/solver.cpp
similarity index 99%
rename from lib/solver.cpp
rename to src/framework/solver.cpp
index fd2be70d3..12f1b76f3 100644
--- a/lib/solver.cpp
+++ b/src/framework/solver.cpp
@@ -17,7 +17,7 @@ Notes:
 
 --*/
 #include"solver.h"
-#include"smt_solver.h"
+// #include"smt_solver.h"
 
 unsigned solver::get_num_assertions() const {
     NOT_IMPLEMENTED_YET();
@@ -33,6 +33,7 @@ void solver::display(std::ostream & out) const {
     out << "(solver)";
 }
 
+#if 0
 class default_solver : public solver {
     front_end_params * m_params;
     smt::solver *     m_context;
@@ -191,3 +192,4 @@ public:
 solver * mk_default_solver() {
     return alloc(default_solver);
 }
+#endif
diff --git a/lib/solver.h b/src/framework/solver.h
similarity index 100%
rename from lib/solver.h
rename to src/framework/solver.h
diff --git a/lib/tactic.cpp b/src/framework/tactic.cpp
similarity index 100%
rename from lib/tactic.cpp
rename to src/framework/tactic.cpp
diff --git a/lib/tactic.h b/src/framework/tactic.h
similarity index 100%
rename from lib/tactic.h
rename to src/framework/tactic.h
diff --git a/lib/tactic_cmds.cpp b/src/framework/tactic_cmds.cpp
similarity index 99%
rename from lib/tactic_cmds.cpp
rename to src/framework/tactic_cmds.cpp
index f0b255696..c7351d455 100644
--- a/lib/tactic_cmds.cpp
+++ b/src/framework/tactic_cmds.cpp
@@ -20,7 +20,6 @@ Notes:
 #include"cmd_context.h"
 #include"cmd_util.h"
 #include"parametric_cmd.h"
-#include"install_tactics.h"
 #include"scoped_timer.h"
 #include"scoped_ctrl_c.h"
 #include"cancel_eh.h"
@@ -390,13 +389,12 @@ public:
 };
 
            
-void install_tactic_cmds(cmd_context & ctx) {
+void install_core_tactic_cmds(cmd_context & ctx) {
     ctx.insert(alloc(declare_tactic_cmd));
     ctx.insert(alloc(get_user_tactics_cmd));
     ctx.insert(alloc(help_tactic_cmd));
     ctx.insert(alloc(check_sat_using_tactict_cmd));
     ctx.insert(alloc(apply_tactic_cmd));
-    install_tactics(ctx);
 }
 
 static tactic * mk_and_then(cmd_context & ctx, sexpr * n) {
diff --git a/lib/tactic_cmds.h b/src/framework/tactic_cmds.h
similarity index 96%
rename from lib/tactic_cmds.h
rename to src/framework/tactic_cmds.h
index 10f1d6276..c44078a90 100644
--- a/lib/tactic_cmds.h
+++ b/src/framework/tactic_cmds.h
@@ -45,7 +45,7 @@ public:
     tactic * mk(ast_manager & m);
 };
 
-void install_tactic_cmds(cmd_context & ctx);
+void install_core_tactic_cmds(cmd_context & ctx);
 tactic * sexpr2tactic(cmd_context & ctx, sexpr * n);
 
 class probe_info {
diff --git a/lib/tactic_manager.cpp b/src/framework/tactic_manager.cpp
similarity index 100%
rename from lib/tactic_manager.cpp
rename to src/framework/tactic_manager.cpp
diff --git a/lib/tactic_manager.h b/src/framework/tactic_manager.h
similarity index 100%
rename from lib/tactic_manager.h
rename to src/framework/tactic_manager.h
diff --git a/lib/tactical.cpp b/src/framework/tactical.cpp
similarity index 100%
rename from lib/tactical.cpp
rename to src/framework/tactical.cpp
diff --git a/lib/tactical.h b/src/framework/tactical.h
similarity index 100%
rename from lib/tactical.h
rename to src/framework/tactical.h
diff --git a/lib/bit_blaster_params.h b/src/old_params/bit_blaster_params.h
similarity index 100%
rename from lib/bit_blaster_params.h
rename to src/old_params/bit_blaster_params.h
diff --git a/lib/cnf_params.cpp b/src/old_params/cnf_params.cpp
similarity index 100%
rename from lib/cnf_params.cpp
rename to src/old_params/cnf_params.cpp
diff --git a/lib/cnf_params.h b/src/old_params/cnf_params.h
similarity index 100%
rename from lib/cnf_params.h
rename to src/old_params/cnf_params.h
diff --git a/lib/dyn_ack_params.cpp b/src/old_params/dyn_ack_params.cpp
similarity index 100%
rename from lib/dyn_ack_params.cpp
rename to src/old_params/dyn_ack_params.cpp
diff --git a/lib/dyn_ack_params.h b/src/old_params/dyn_ack_params.h
similarity index 100%
rename from lib/dyn_ack_params.h
rename to src/old_params/dyn_ack_params.h
diff --git a/lib/front_end_params.cpp b/src/old_params/front_end_params.cpp
similarity index 100%
rename from lib/front_end_params.cpp
rename to src/old_params/front_end_params.cpp
diff --git a/lib/front_end_params.h b/src/old_params/front_end_params.h
similarity index 100%
rename from lib/front_end_params.h
rename to src/old_params/front_end_params.h
diff --git a/lib/nnf_params.cpp b/src/old_params/nnf_params.cpp
similarity index 100%
rename from lib/nnf_params.cpp
rename to src/old_params/nnf_params.cpp
diff --git a/lib/nnf_params.h b/src/old_params/nnf_params.h
similarity index 100%
rename from lib/nnf_params.h
rename to src/old_params/nnf_params.h
diff --git a/lib/order_params.cpp b/src/old_params/order_params.cpp
similarity index 100%
rename from lib/order_params.cpp
rename to src/old_params/order_params.cpp
diff --git a/lib/order_params.h b/src/old_params/order_params.h
similarity index 100%
rename from lib/order_params.h
rename to src/old_params/order_params.h
diff --git a/lib/params2front_end_params.cpp b/src/old_params/params2front_end_params.cpp
similarity index 100%
rename from lib/params2front_end_params.cpp
rename to src/old_params/params2front_end_params.cpp
diff --git a/lib/params2front_end_params.h b/src/old_params/params2front_end_params.h
similarity index 100%
rename from lib/params2front_end_params.h
rename to src/old_params/params2front_end_params.h
diff --git a/lib/parser_params.cpp b/src/old_params/parser_params.cpp
similarity index 100%
rename from lib/parser_params.cpp
rename to src/old_params/parser_params.cpp
diff --git a/lib/parser_params.h b/src/old_params/parser_params.h
similarity index 100%
rename from lib/parser_params.h
rename to src/old_params/parser_params.h
diff --git a/lib/pattern_inference_params.h b/src/old_params/pattern_inference_params.h
similarity index 100%
rename from lib/pattern_inference_params.h
rename to src/old_params/pattern_inference_params.h
diff --git a/lib/preprocessor_params.h b/src/old_params/preprocessor_params.h
similarity index 100%
rename from lib/preprocessor_params.h
rename to src/old_params/preprocessor_params.h
diff --git a/lib/qi_params.h b/src/old_params/qi_params.h
similarity index 100%
rename from lib/qi_params.h
rename to src/old_params/qi_params.h
diff --git a/lib/smt_params.cpp b/src/old_params/smt_params.cpp
similarity index 100%
rename from lib/smt_params.cpp
rename to src/old_params/smt_params.cpp
diff --git a/lib/smt_params.h b/src/old_params/smt_params.h
similarity index 100%
rename from lib/smt_params.h
rename to src/old_params/smt_params.h
diff --git a/lib/spc_params.cpp b/src/old_params/spc_params.cpp
similarity index 100%
rename from lib/spc_params.cpp
rename to src/old_params/spc_params.cpp
diff --git a/lib/spc_params.h b/src/old_params/spc_params.h
similarity index 100%
rename from lib/spc_params.h
rename to src/old_params/spc_params.h
diff --git a/lib/theory_arith_params.cpp b/src/old_params/theory_arith_params.cpp
similarity index 100%
rename from lib/theory_arith_params.cpp
rename to src/old_params/theory_arith_params.cpp
diff --git a/lib/theory_arith_params.h b/src/old_params/theory_arith_params.h
similarity index 100%
rename from lib/theory_arith_params.h
rename to src/old_params/theory_arith_params.h
diff --git a/lib/theory_array_params.h b/src/old_params/theory_array_params.h
similarity index 100%
rename from lib/theory_array_params.h
rename to src/old_params/theory_array_params.h
diff --git a/lib/theory_bv_params.h b/src/old_params/theory_bv_params.h
similarity index 100%
rename from lib/theory_bv_params.h
rename to src/old_params/theory_bv_params.h
diff --git a/lib/theory_datatype_params.h b/src/old_params/theory_datatype_params.h
similarity index 100%
rename from lib/theory_datatype_params.h
rename to src/old_params/theory_datatype_params.h
diff --git a/lib/z3_solver_params.cpp b/src/old_params/z3_solver_params.cpp
similarity index 100%
rename from lib/z3_solver_params.cpp
rename to src/old_params/z3_solver_params.cpp
diff --git a/lib/z3_solver_params.h b/src/old_params/z3_solver_params.h
similarity index 100%
rename from lib/z3_solver_params.h
rename to src/old_params/z3_solver_params.h
diff --git a/src/simplifier/README b/src/simplifier/README
new file mode 100644
index 000000000..4725d9de9
--- /dev/null
+++ b/src/simplifier/README
@@ -0,0 +1,2 @@
+Simplifier module is now obsolete.
+It is still being used in many places, but we will eventually replace all occurrences with the new rewriter module.
diff --git a/lib/smt_solver.cpp b/src/smt/smt_solver.cpp
similarity index 100%
rename from lib/smt_solver.cpp
rename to src/smt/smt_solver.cpp
diff --git a/lib/smt_solver.h b/src/smt/smt_solver.h
similarity index 100%
rename from lib/smt_solver.h
rename to src/smt/smt_solver.h