diff --git a/lib/lockless_queue.h b/lib/lockless_queue.h
deleted file mode 100644
index 83d9226c4..000000000
--- a/lib/lockless_queue.h
+++ /dev/null
@@ -1,115 +0,0 @@
-/*++
-Copyright (c) 2008 Microsoft Corporation
-
-Module Name:
-
-    lockless_queue.h
-
-Abstract:
-
-    A queue that doesn't require locking, as long as only 
-    one thread pushes and another thread pops.
-
-Author:
-
-    Christoph Wintersteiger (t-cwinte) 2008-12-26
-
-Revision History:
-
---*/
-
-#ifndef _LOCKLESS_QUEUE_H_
-#define _LOCKLESS_QUEUE_H_
-
-#include <new> 
-#include "debug.h"
-
-template<typename T>
-class lockless_queue {
-protected:
-    unsigned m_head;
-    unsigned m_tail;
-    unsigned m_size;
-    T *m_items;
-public:
-    typedef T value_type;
-
-    lockless_queue(unsigned size=4096) : 
-        m_head(0), 
-        m_tail(0), 
-        m_size(size),
-        m_items(0) { 
-        if(m_size>0) {
-            m_items = alloc_vect<T>(m_size);
-            SASSERT(m_items!=0);
-        }
-    }
-
-    lockless_queue(const lockless_queue &other) {
-        m_items = 0;
-        m_size = m_head = m_tail = 0;
-        this->operator=(other);
-    }
-
-    ~lockless_queue() { 
-        if(m_items) {
-            dealloc_vect(m_items, m_size);
-            m_items=0;
-        }
-    }
-
-    inline bool push(const T& elem) {
-        volatile unsigned head = m_head;
-
-        if(((head+1)%m_size) == m_tail)
-            return false; // queue is full.
-
-        m_items[head++] = elem;
-        head %= m_size;
-        m_head = head;
-        return true;
-    }
-
-    inline bool pop() {
-        volatile unsigned tail = m_tail;
-
-        if(tail == m_head)
-            return false; // queue is empty.
-
-        tail = (tail+1) % m_size;
-        m_tail = tail;
-        return true;
-    }
-
-    inline T& back() const {
-        SASSERT(!empty());
-        return m_items[m_tail]; 
-    }
-
-    inline bool empty() const {
-        return (m_tail == m_head);
-    }
-
-	inline bool full() const {
-        return (m_tail == ((m_head+1)%m_size));
-    }
-
-    lockless_queue& operator=(const lockless_queue &other) {
-        if(m_size!=other.m_size) {
-            if(m_items) dealloc_vect(m_items, m_size);
-            m_items = alloc_vect<T>(other.m_size);
-            m_size = other.m_size;
-        }
-
-        for(size_t cur = other.m_tail; cur!=other.m_head; cur = (cur+1)%m_size)
-            m_items[cur] = other.m_items[cur];
-
-        m_tail = other.m_tail;
-        m_head = other.m_head;
-
-        return *this;
-    }
-
-};
-
-#endif
diff --git a/mk_make.py b/mk_make.py
index 0bf3ecb80..de60d621f 100644
--- a/mk_make.py
+++ b/mk_make.py
@@ -160,4 +160,8 @@ add_lib('util', [])
 add_lib('polynomial', ['util'])
 add_lib('sat', ['util', 'sat_core'])
 add_lib('nlsat', ['util', 'sat_core', 'polynomial'])
+add_lib('subpaving', ['util'])
 add_lib('ast', ['util', 'polynomial'])
+add_lib('rewriter', ['util', 'ast', 'polynomial'])
+add_lib('tactic', ['util', 'ast'])
+
diff --git a/lib/act_cache.cpp b/src/ast/act_cache.cpp
similarity index 100%
rename from lib/act_cache.cpp
rename to src/ast/act_cache.cpp
diff --git a/lib/act_cache.h b/src/ast/act_cache.h
similarity index 100%
rename from lib/act_cache.h
rename to src/ast/act_cache.h
diff --git a/lib/ast_dag_pp.cpp b/src/ast/ast_dag_pp.cpp
similarity index 100%
rename from lib/ast_dag_pp.cpp
rename to src/ast/ast_dag_pp.cpp
diff --git a/lib/ast_dag_pp.h b/src/ast/ast_dag_pp.h
similarity index 100%
rename from lib/ast_dag_pp.h
rename to src/ast/ast_dag_pp.h
diff --git a/lib/ast_lt.cpp b/src/ast/ast_lt.cpp
similarity index 100%
rename from lib/ast_lt.cpp
rename to src/ast/ast_lt.cpp
diff --git a/lib/ast_lt.h b/src/ast/ast_lt.h
similarity index 100%
rename from lib/ast_lt.h
rename to src/ast/ast_lt.h
diff --git a/lib/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
similarity index 100%
rename from lib/ast_smt_pp.cpp
rename to src/ast/ast_smt_pp.cpp
diff --git a/lib/ast_smt_pp.h b/src/ast/ast_smt_pp.h
similarity index 100%
rename from lib/ast_smt_pp.h
rename to src/ast/ast_smt_pp.h
diff --git a/lib/ast_translation.cpp b/src/ast/ast_translation.cpp
similarity index 100%
rename from lib/ast_translation.cpp
rename to src/ast/ast_translation.cpp
diff --git a/lib/ast_translation.h b/src/ast/ast_translation.h
similarity index 100%
rename from lib/ast_translation.h
rename to src/ast/ast_translation.h
diff --git a/lib/decl_collector.cpp b/src/ast/decl_collector.cpp
similarity index 100%
rename from lib/decl_collector.cpp
rename to src/ast/decl_collector.cpp
diff --git a/lib/decl_collector.h b/src/ast/decl_collector.h
similarity index 100%
rename from lib/decl_collector.h
rename to src/ast/decl_collector.h
diff --git a/lib/expr_delta_pair.h b/src/ast/expr_delta_pair.h
similarity index 100%
rename from lib/expr_delta_pair.h
rename to src/ast/expr_delta_pair.h
diff --git a/lib/expr_substitution.cpp b/src/ast/expr_substitution.cpp
similarity index 100%
rename from lib/expr_substitution.cpp
rename to src/ast/expr_substitution.cpp
diff --git a/lib/expr_substitution.h b/src/ast/expr_substitution.h
similarity index 100%
rename from lib/expr_substitution.h
rename to src/ast/expr_substitution.h
diff --git a/lib/used_vars.cpp b/src/ast/used_vars.cpp
similarity index 100%
rename from lib/used_vars.cpp
rename to src/ast/used_vars.cpp
diff --git a/lib/used_vars.h b/src/ast/used_vars.h
similarity index 100%
rename from lib/used_vars.h
rename to src/ast/used_vars.h
diff --git a/lib/rpolynomial.cpp b/src/polynomial/rpolynomial.cpp
similarity index 100%
rename from lib/rpolynomial.cpp
rename to src/polynomial/rpolynomial.cpp
diff --git a/lib/rpolynomial.h b/src/polynomial/rpolynomial.h
similarity index 100%
rename from lib/rpolynomial.h
rename to src/polynomial/rpolynomial.h
diff --git a/lib/arith_rewriter.cpp b/src/rewriter/arith_rewriter.cpp
similarity index 100%
rename from lib/arith_rewriter.cpp
rename to src/rewriter/arith_rewriter.cpp
diff --git a/lib/arith_rewriter.h b/src/rewriter/arith_rewriter.h
similarity index 100%
rename from lib/arith_rewriter.h
rename to src/rewriter/arith_rewriter.h
diff --git a/lib/array_rewriter.cpp b/src/rewriter/array_rewriter.cpp
similarity index 100%
rename from lib/array_rewriter.cpp
rename to src/rewriter/array_rewriter.cpp
diff --git a/lib/array_rewriter.h b/src/rewriter/array_rewriter.h
similarity index 100%
rename from lib/array_rewriter.h
rename to src/rewriter/array_rewriter.h
diff --git a/lib/bool_rewriter.cpp b/src/rewriter/bool_rewriter.cpp
similarity index 100%
rename from lib/bool_rewriter.cpp
rename to src/rewriter/bool_rewriter.cpp
diff --git a/lib/bool_rewriter.h b/src/rewriter/bool_rewriter.h
similarity index 100%
rename from lib/bool_rewriter.h
rename to src/rewriter/bool_rewriter.h
diff --git a/lib/bv_rewriter.cpp b/src/rewriter/bv_rewriter.cpp
similarity index 100%
rename from lib/bv_rewriter.cpp
rename to src/rewriter/bv_rewriter.cpp
diff --git a/lib/bv_rewriter.h b/src/rewriter/bv_rewriter.h
similarity index 100%
rename from lib/bv_rewriter.h
rename to src/rewriter/bv_rewriter.h
diff --git a/lib/datatype_rewriter.cpp b/src/rewriter/datatype_rewriter.cpp
similarity index 100%
rename from lib/datatype_rewriter.cpp
rename to src/rewriter/datatype_rewriter.cpp
diff --git a/lib/datatype_rewriter.h b/src/rewriter/datatype_rewriter.h
similarity index 100%
rename from lib/datatype_rewriter.h
rename to src/rewriter/datatype_rewriter.h
diff --git a/lib/dl_rewriter.cpp b/src/rewriter/dl_rewriter.cpp
similarity index 100%
rename from lib/dl_rewriter.cpp
rename to src/rewriter/dl_rewriter.cpp
diff --git a/lib/dl_rewriter.h b/src/rewriter/dl_rewriter.h
similarity index 100%
rename from lib/dl_rewriter.h
rename to src/rewriter/dl_rewriter.h
diff --git a/lib/float_rewriter.cpp b/src/rewriter/float_rewriter.cpp
similarity index 100%
rename from lib/float_rewriter.cpp
rename to src/rewriter/float_rewriter.cpp
diff --git a/lib/float_rewriter.h b/src/rewriter/float_rewriter.h
similarity index 100%
rename from lib/float_rewriter.h
rename to src/rewriter/float_rewriter.h
diff --git a/lib/poly_rewriter.h b/src/rewriter/poly_rewriter.h
similarity index 100%
rename from lib/poly_rewriter.h
rename to src/rewriter/poly_rewriter.h
diff --git a/lib/poly_rewriter_def.h b/src/rewriter/poly_rewriter_def.h
similarity index 100%
rename from lib/poly_rewriter_def.h
rename to src/rewriter/poly_rewriter_def.h
diff --git a/lib/rewriter.cpp b/src/rewriter/rewriter.cpp
similarity index 100%
rename from lib/rewriter.cpp
rename to src/rewriter/rewriter.cpp
diff --git a/lib/rewriter.h b/src/rewriter/rewriter.h
similarity index 100%
rename from lib/rewriter.h
rename to src/rewriter/rewriter.h
diff --git a/lib/rewriter_def.h b/src/rewriter/rewriter_def.h
similarity index 100%
rename from lib/rewriter_def.h
rename to src/rewriter/rewriter_def.h
diff --git a/lib/rewriter_types.h b/src/rewriter/rewriter_types.h
similarity index 100%
rename from lib/rewriter_types.h
rename to src/rewriter/rewriter_types.h
diff --git a/lib/th_rewriter.cpp b/src/rewriter/th_rewriter.cpp
similarity index 100%
rename from lib/th_rewriter.cpp
rename to src/rewriter/th_rewriter.cpp
diff --git a/lib/th_rewriter.h b/src/rewriter/th_rewriter.h
similarity index 100%
rename from lib/th_rewriter.h
rename to src/rewriter/th_rewriter.h
diff --git a/lib/var_subst.cpp b/src/rewriter/var_subst.cpp
similarity index 100%
rename from lib/var_subst.cpp
rename to src/rewriter/var_subst.cpp
diff --git a/lib/var_subst.h b/src/rewriter/var_subst.h
similarity index 100%
rename from lib/var_subst.h
rename to src/rewriter/var_subst.h
diff --git a/lib/subpaving.cpp b/src/subpaving/subpaving.cpp
similarity index 100%
rename from lib/subpaving.cpp
rename to src/subpaving/subpaving.cpp
diff --git a/lib/subpaving.h b/src/subpaving/subpaving.h
similarity index 100%
rename from lib/subpaving.h
rename to src/subpaving/subpaving.h
diff --git a/lib/subpaving_hwf.cpp b/src/subpaving/subpaving_hwf.cpp
similarity index 100%
rename from lib/subpaving_hwf.cpp
rename to src/subpaving/subpaving_hwf.cpp
diff --git a/lib/subpaving_hwf.h b/src/subpaving/subpaving_hwf.h
similarity index 100%
rename from lib/subpaving_hwf.h
rename to src/subpaving/subpaving_hwf.h
diff --git a/lib/subpaving_mpf.cpp b/src/subpaving/subpaving_mpf.cpp
similarity index 100%
rename from lib/subpaving_mpf.cpp
rename to src/subpaving/subpaving_mpf.cpp
diff --git a/lib/subpaving_mpf.h b/src/subpaving/subpaving_mpf.h
similarity index 100%
rename from lib/subpaving_mpf.h
rename to src/subpaving/subpaving_mpf.h
diff --git a/lib/subpaving_mpff.cpp b/src/subpaving/subpaving_mpff.cpp
similarity index 100%
rename from lib/subpaving_mpff.cpp
rename to src/subpaving/subpaving_mpff.cpp
diff --git a/lib/subpaving_mpff.h b/src/subpaving/subpaving_mpff.h
similarity index 100%
rename from lib/subpaving_mpff.h
rename to src/subpaving/subpaving_mpff.h
diff --git a/lib/subpaving_mpfx.cpp b/src/subpaving/subpaving_mpfx.cpp
similarity index 100%
rename from lib/subpaving_mpfx.cpp
rename to src/subpaving/subpaving_mpfx.cpp
diff --git a/lib/subpaving_mpfx.h b/src/subpaving/subpaving_mpfx.h
similarity index 100%
rename from lib/subpaving_mpfx.h
rename to src/subpaving/subpaving_mpfx.h
diff --git a/lib/subpaving_mpq.cpp b/src/subpaving/subpaving_mpq.cpp
similarity index 100%
rename from lib/subpaving_mpq.cpp
rename to src/subpaving/subpaving_mpq.cpp
diff --git a/lib/subpaving_mpq.h b/src/subpaving/subpaving_mpq.h
similarity index 100%
rename from lib/subpaving_mpq.h
rename to src/subpaving/subpaving_mpq.h
diff --git a/lib/subpaving_t.h b/src/subpaving/subpaving_t.h
similarity index 100%
rename from lib/subpaving_t.h
rename to src/subpaving/subpaving_t.h
diff --git a/lib/subpaving_t_def.h b/src/subpaving/subpaving_t_def.h
similarity index 100%
rename from lib/subpaving_t_def.h
rename to src/subpaving/subpaving_t_def.h
diff --git a/lib/subpaving_types.h b/src/subpaving/subpaving_types.h
similarity index 100%
rename from lib/subpaving_types.h
rename to src/subpaving/subpaving_types.h
diff --git a/lib/goal.cpp b/src/tactic/goal.cpp
similarity index 100%
rename from lib/goal.cpp
rename to src/tactic/goal.cpp
diff --git a/lib/goal.h b/src/tactic/goal.h
similarity index 100%
rename from lib/goal.h
rename to src/tactic/goal.h