diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index e6e7d5dc8..44ad9ccbc 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -53,11 +53,11 @@ def init_project_def():
     add_lib('fpa', ['core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa')
     add_lib('smt_tactic', ['smt'], 'smt/tactic')
     add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
-    # TODO: split muz_qe into muz, qe. Perhaps, we should also consider breaking muz into muz and pdr.
-    add_lib('muz_qe', ['smt', 'sat', 'smt2parser', 'aig_tactic'])
-    add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'muz_qe'], 'tactic/smtlogics')
+    add_lib('qe', ['smt','sat'], 'qe')
+    add_lib('muz', ['smt', 'sat', 'smt2parser', 'aig_tactic','qe'])
+    add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'muz','qe'], 'tactic/smtlogics')
     add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
-    add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'muz_qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
+    add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'muz', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
     add_lib('smtparser', ['portfolio'], 'parsers/smt')
     API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h']
     add_lib('api', ['portfolio', 'user_plugin', 'smtparser', 'realclosure'],
diff --git a/src/muz_qe/README b/src/muz/README
similarity index 100%
rename from src/muz_qe/README
rename to src/muz/README
diff --git a/src/muz_qe/aig_exporter.cpp b/src/muz/aig_exporter.cpp
old mode 100755
new mode 100644
similarity index 100%
rename from src/muz_qe/aig_exporter.cpp
rename to src/muz/aig_exporter.cpp
diff --git a/src/muz_qe/aig_exporter.h b/src/muz/aig_exporter.h
old mode 100755
new mode 100644
similarity index 100%
rename from src/muz_qe/aig_exporter.h
rename to src/muz/aig_exporter.h
diff --git a/src/muz_qe/arith_bounds_tactic.cpp b/src/muz/arith_bounds_tactic.cpp
similarity index 100%
rename from src/muz_qe/arith_bounds_tactic.cpp
rename to src/muz/arith_bounds_tactic.cpp
diff --git a/src/muz_qe/arith_bounds_tactic.h b/src/muz/arith_bounds_tactic.h
similarity index 100%
rename from src/muz_qe/arith_bounds_tactic.h
rename to src/muz/arith_bounds_tactic.h
diff --git a/src/muz_qe/clp_context.cpp b/src/muz/clp_context.cpp
similarity index 100%
rename from src/muz_qe/clp_context.cpp
rename to src/muz/clp_context.cpp
diff --git a/src/muz_qe/clp_context.h b/src/muz/clp_context.h
similarity index 100%
rename from src/muz_qe/clp_context.h
rename to src/muz/clp_context.h
diff --git a/src/muz_qe/datalog_parser.cpp b/src/muz/datalog_parser.cpp
similarity index 100%
rename from src/muz_qe/datalog_parser.cpp
rename to src/muz/datalog_parser.cpp
diff --git a/src/muz_qe/datalog_parser.h b/src/muz/datalog_parser.h
similarity index 100%
rename from src/muz_qe/datalog_parser.h
rename to src/muz/datalog_parser.h
diff --git a/src/muz_qe/dl_base.cpp b/src/muz/dl_base.cpp
similarity index 100%
rename from src/muz_qe/dl_base.cpp
rename to src/muz/dl_base.cpp
diff --git a/src/muz_qe/dl_base.h b/src/muz/dl_base.h
similarity index 100%
rename from src/muz_qe/dl_base.h
rename to src/muz/dl_base.h
diff --git a/src/muz_qe/dl_bmc_engine.cpp b/src/muz/dl_bmc_engine.cpp
similarity index 100%
rename from src/muz_qe/dl_bmc_engine.cpp
rename to src/muz/dl_bmc_engine.cpp
diff --git a/src/muz_qe/dl_bmc_engine.h b/src/muz/dl_bmc_engine.h
similarity index 100%
rename from src/muz_qe/dl_bmc_engine.h
rename to src/muz/dl_bmc_engine.h
diff --git a/src/muz_qe/dl_boogie_proof.cpp b/src/muz/dl_boogie_proof.cpp
similarity index 99%
rename from src/muz_qe/dl_boogie_proof.cpp
rename to src/muz/dl_boogie_proof.cpp
index e14512973..d11e4a932 100644
--- a/src/muz_qe/dl_boogie_proof.cpp
+++ b/src/muz/dl_boogie_proof.cpp
@@ -49,7 +49,7 @@ Example from Boogie:
 #include "model_pp.h"
 #include "proof_utils.h"
 #include "ast_pp.h"
-#include "dl_util.h"
+#include "qe_util.h"
 
 namespace datalog {
     
@@ -91,7 +91,7 @@ namespace datalog {
                 if (!m.is_implies(premise, l1, l2)) {
                     continue;
                 }
-                datalog::flatten_and(l1, literals);
+                qe::flatten_and(l1, literals);
                 positions2.reset();
                 premises2.reset();
                 premises2.push_back(premise);       
diff --git a/src/muz_qe/dl_boogie_proof.h b/src/muz/dl_boogie_proof.h
similarity index 100%
rename from src/muz_qe/dl_boogie_proof.h
rename to src/muz/dl_boogie_proof.h
diff --git a/src/muz_qe/dl_bound_relation.cpp b/src/muz/dl_bound_relation.cpp
similarity index 100%
rename from src/muz_qe/dl_bound_relation.cpp
rename to src/muz/dl_bound_relation.cpp
diff --git a/src/muz_qe/dl_bound_relation.h b/src/muz/dl_bound_relation.h
similarity index 100%
rename from src/muz_qe/dl_bound_relation.h
rename to src/muz/dl_bound_relation.h
diff --git a/src/muz_qe/dl_check_table.cpp b/src/muz/dl_check_table.cpp
similarity index 100%
rename from src/muz_qe/dl_check_table.cpp
rename to src/muz/dl_check_table.cpp
diff --git a/src/muz_qe/dl_check_table.h b/src/muz/dl_check_table.h
similarity index 100%
rename from src/muz_qe/dl_check_table.h
rename to src/muz/dl_check_table.h
diff --git a/src/muz_qe/dl_cmds.cpp b/src/muz/dl_cmds.cpp
similarity index 100%
rename from src/muz_qe/dl_cmds.cpp
rename to src/muz/dl_cmds.cpp
diff --git a/src/muz_qe/dl_cmds.h b/src/muz/dl_cmds.h
similarity index 100%
rename from src/muz_qe/dl_cmds.h
rename to src/muz/dl_cmds.h
diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz/dl_compiler.cpp
similarity index 100%
rename from src/muz_qe/dl_compiler.cpp
rename to src/muz/dl_compiler.cpp
diff --git a/src/muz_qe/dl_compiler.h b/src/muz/dl_compiler.h
similarity index 100%
rename from src/muz_qe/dl_compiler.h
rename to src/muz/dl_compiler.h
diff --git a/src/muz_qe/dl_context.cpp b/src/muz/dl_context.cpp
similarity index 100%
rename from src/muz_qe/dl_context.cpp
rename to src/muz/dl_context.cpp
index 7da9808e7..f5bfb6b5e 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz/dl_context.cpp
@@ -35,12 +35,6 @@ Revision History:
 #include"dl_mk_similarity_compressor.h"
 #include"dl_mk_unbound_compressor.h"
 #include"dl_mk_subsumption_checker.h"
-#include"dl_compiler.h"
-#include"dl_instruction.h"
-#include"dl_context.h"
-#include"for_each_expr.h"
-#include"ast_smt_pp.h"
-#include"ast_smt2_pp.h"
 #include"dl_mk_partial_equiv.h"
 #include"dl_mk_bit_blast.h"
 #include"dl_mk_array_blast.h"
@@ -49,6 +43,12 @@ Revision History:
 #include"dl_mk_quantifier_abstraction.h"
 #include"dl_mk_quantifier_instantiation.h"
 #include"dl_mk_scale.h"
+#include"dl_compiler.h"
+#include"dl_instruction.h"
+#include"dl_context.h"
+#include"for_each_expr.h"
+#include"ast_smt_pp.h"
+#include"ast_smt2_pp.h"
 #include"datatype_decl_plugin.h"
 
 
diff --git a/src/muz_qe/dl_context.h b/src/muz/dl_context.h
similarity index 100%
rename from src/muz_qe/dl_context.h
rename to src/muz/dl_context.h
diff --git a/src/muz_qe/dl_costs.cpp b/src/muz/dl_costs.cpp
similarity index 100%
rename from src/muz_qe/dl_costs.cpp
rename to src/muz/dl_costs.cpp
diff --git a/src/muz_qe/dl_costs.h b/src/muz/dl_costs.h
similarity index 100%
rename from src/muz_qe/dl_costs.h
rename to src/muz/dl_costs.h
diff --git a/src/muz_qe/dl_external_relation.cpp b/src/muz/dl_external_relation.cpp
similarity index 100%
rename from src/muz_qe/dl_external_relation.cpp
rename to src/muz/dl_external_relation.cpp
diff --git a/src/muz_qe/dl_external_relation.h b/src/muz/dl_external_relation.h
similarity index 100%
rename from src/muz_qe/dl_external_relation.h
rename to src/muz/dl_external_relation.h
diff --git a/src/muz_qe/dl_finite_product_relation.cpp b/src/muz/dl_finite_product_relation.cpp
similarity index 100%
rename from src/muz_qe/dl_finite_product_relation.cpp
rename to src/muz/dl_finite_product_relation.cpp
diff --git a/src/muz_qe/dl_finite_product_relation.h b/src/muz/dl_finite_product_relation.h
similarity index 100%
rename from src/muz_qe/dl_finite_product_relation.h
rename to src/muz/dl_finite_product_relation.h
diff --git a/src/muz_qe/dl_instruction.cpp b/src/muz/dl_instruction.cpp
similarity index 100%
rename from src/muz_qe/dl_instruction.cpp
rename to src/muz/dl_instruction.cpp
diff --git a/src/muz_qe/dl_instruction.h b/src/muz/dl_instruction.h
similarity index 100%
rename from src/muz_qe/dl_instruction.h
rename to src/muz/dl_instruction.h
diff --git a/src/muz_qe/dl_interval_relation.cpp b/src/muz/dl_interval_relation.cpp
similarity index 100%
rename from src/muz_qe/dl_interval_relation.cpp
rename to src/muz/dl_interval_relation.cpp
diff --git a/src/muz_qe/dl_interval_relation.h b/src/muz/dl_interval_relation.h
similarity index 100%
rename from src/muz_qe/dl_interval_relation.h
rename to src/muz/dl_interval_relation.h
diff --git a/src/muz_qe/dl_mk_array_blast.cpp b/src/muz/dl_mk_array_blast.cpp
similarity index 98%
rename from src/muz_qe/dl_mk_array_blast.cpp
rename to src/muz/dl_mk_array_blast.cpp
index 2bfb6807a..776a2da5b 100644
--- a/src/muz_qe/dl_mk_array_blast.cpp
+++ b/src/muz/dl_mk_array_blast.cpp
@@ -18,7 +18,7 @@ Revision History:
 --*/
 
 #include "dl_mk_array_blast.h"
-
+#include "qe_util.h"
 
 namespace datalog {
 
@@ -101,7 +101,7 @@ namespace datalog {
     
     bool mk_array_blast::ackermanize(rule const& r, expr_ref& body, expr_ref& head) {
         expr_ref_vector conjs(m);
-        flatten_and(body, conjs);
+        qe::flatten_and(body, conjs);
         m_defs.reset();
         m_sub.reset();
         m_next_var = 0;
@@ -207,7 +207,7 @@ namespace datalog {
         for (unsigned i = utsz; i < tsz; ++i) {
             conjs.push_back(r.get_tail(i));
         }
-        flatten_and(conjs);
+        qe::flatten_and(conjs);
         for (unsigned i = 0; i < conjs.size(); ++i) {
             expr* x, *y, *e = conjs[i].get();
             
diff --git a/src/muz_qe/dl_mk_array_blast.h b/src/muz/dl_mk_array_blast.h
similarity index 100%
rename from src/muz_qe/dl_mk_array_blast.h
rename to src/muz/dl_mk_array_blast.h
diff --git a/src/muz_qe/dl_mk_backwards.cpp b/src/muz/dl_mk_backwards.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_backwards.cpp
rename to src/muz/dl_mk_backwards.cpp
diff --git a/src/muz_qe/dl_mk_backwards.h b/src/muz/dl_mk_backwards.h
similarity index 100%
rename from src/muz_qe/dl_mk_backwards.h
rename to src/muz/dl_mk_backwards.h
diff --git a/src/muz_qe/dl_mk_bit_blast.cpp b/src/muz/dl_mk_bit_blast.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_bit_blast.cpp
rename to src/muz/dl_mk_bit_blast.cpp
diff --git a/src/muz_qe/dl_mk_bit_blast.h b/src/muz/dl_mk_bit_blast.h
similarity index 100%
rename from src/muz_qe/dl_mk_bit_blast.h
rename to src/muz/dl_mk_bit_blast.h
diff --git a/src/muz_qe/dl_mk_coalesce.cpp b/src/muz/dl_mk_coalesce.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_coalesce.cpp
rename to src/muz/dl_mk_coalesce.cpp
diff --git a/src/muz_qe/dl_mk_coalesce.h b/src/muz/dl_mk_coalesce.h
similarity index 100%
rename from src/muz_qe/dl_mk_coalesce.h
rename to src/muz/dl_mk_coalesce.h
diff --git a/src/muz_qe/dl_mk_coi_filter.cpp b/src/muz/dl_mk_coi_filter.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_coi_filter.cpp
rename to src/muz/dl_mk_coi_filter.cpp
diff --git a/src/muz_qe/dl_mk_coi_filter.h b/src/muz/dl_mk_coi_filter.h
similarity index 100%
rename from src/muz_qe/dl_mk_coi_filter.h
rename to src/muz/dl_mk_coi_filter.h
diff --git a/src/muz/dl_mk_different.h b/src/muz/dl_mk_different.h
new file mode 100644
index 000000000..2def011f9
--- /dev/null
+++ b/src/muz/dl_mk_different.h
@@ -0,0 +1,38 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    dl_mk_different_symbolic.h
+
+Abstract:
+
+    Create Horn clauses for different symbolic transformation.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-06-19
+
+Revision History:
+
+--*/
+#ifndef _DL_MK_DIFFERENT_SYMBOLIC_H_
+#define _DL_MK_DIFFERENT_SYMBOLIC_H_
+
+#include"dl_rule_transformer.h"
+
+namespace datalog {
+
+    class mk_different_symbolic : public rule_transformer::plugin {
+        ast_manager& m;
+        context&     m_ctx;
+    public:
+        mk_different_symbolic(context & ctx, unsigned priority = 33037);
+        ~mk_different_symbolic();        
+        rule_set * operator()(rule_set const & source);
+    };
+
+};
+
+#endif /* _DL_MK_DIFFERENT_SYMBOLIC_H_ */
+
diff --git a/src/muz_qe/dl_mk_explanations.cpp b/src/muz/dl_mk_explanations.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_explanations.cpp
rename to src/muz/dl_mk_explanations.cpp
diff --git a/src/muz_qe/dl_mk_explanations.h b/src/muz/dl_mk_explanations.h
similarity index 100%
rename from src/muz_qe/dl_mk_explanations.h
rename to src/muz/dl_mk_explanations.h
diff --git a/src/muz_qe/dl_mk_filter_rules.cpp b/src/muz/dl_mk_filter_rules.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_filter_rules.cpp
rename to src/muz/dl_mk_filter_rules.cpp
diff --git a/src/muz_qe/dl_mk_filter_rules.h b/src/muz/dl_mk_filter_rules.h
similarity index 100%
rename from src/muz_qe/dl_mk_filter_rules.h
rename to src/muz/dl_mk_filter_rules.h
diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp b/src/muz/dl_mk_interp_tail_simplifier.cpp
similarity index 99%
rename from src/muz_qe/dl_mk_interp_tail_simplifier.cpp
rename to src/muz/dl_mk_interp_tail_simplifier.cpp
index afd586627..b01b4326c 100644
--- a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp
+++ b/src/muz/dl_mk_interp_tail_simplifier.cpp
@@ -546,7 +546,7 @@ namespace datalog {
 
         if (modified) {
             m_conj.reset();
-            flatten_and(simp_res, m_conj);
+            qe::flatten_and(simp_res, m_conj);
             for (unsigned i = 0; i < m_conj.size(); ++i) {
                 expr* e = m_conj[i].get();
                 if (is_app(e)) {
diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.h b/src/muz/dl_mk_interp_tail_simplifier.h
similarity index 100%
rename from src/muz_qe/dl_mk_interp_tail_simplifier.h
rename to src/muz/dl_mk_interp_tail_simplifier.h
diff --git a/src/muz_qe/dl_mk_karr_invariants.cpp b/src/muz/dl_mk_karr_invariants.cpp
similarity index 99%
rename from src/muz_qe/dl_mk_karr_invariants.cpp
rename to src/muz/dl_mk_karr_invariants.cpp
index e4e5a1ff8..11bc850bb 100644
--- a/src/muz_qe/dl_mk_karr_invariants.cpp
+++ b/src/muz/dl_mk_karr_invariants.cpp
@@ -430,7 +430,7 @@ namespace datalog {
             var* v, *w;
             rational n1, n2;
             expr_ref_vector conjs(m);
-            datalog::flatten_and(cond, conjs);
+            qe::flatten_and(cond, conjs);
             matrix& M = get_ineqs();
             unsigned num_columns = get_signature().size();
 
diff --git a/src/muz_qe/dl_mk_karr_invariants.h b/src/muz/dl_mk_karr_invariants.h
similarity index 100%
rename from src/muz_qe/dl_mk_karr_invariants.h
rename to src/muz/dl_mk_karr_invariants.h
diff --git a/src/muz_qe/dl_mk_loop_counter.cpp b/src/muz/dl_mk_loop_counter.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_loop_counter.cpp
rename to src/muz/dl_mk_loop_counter.cpp
diff --git a/src/muz_qe/dl_mk_loop_counter.h b/src/muz/dl_mk_loop_counter.h
similarity index 100%
rename from src/muz_qe/dl_mk_loop_counter.h
rename to src/muz/dl_mk_loop_counter.h
diff --git a/src/muz_qe/dl_mk_magic_sets.cpp b/src/muz/dl_mk_magic_sets.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_magic_sets.cpp
rename to src/muz/dl_mk_magic_sets.cpp
diff --git a/src/muz_qe/dl_mk_magic_sets.h b/src/muz/dl_mk_magic_sets.h
similarity index 100%
rename from src/muz_qe/dl_mk_magic_sets.h
rename to src/muz/dl_mk_magic_sets.h
diff --git a/src/muz_qe/dl_mk_magic_symbolic.cpp b/src/muz/dl_mk_magic_symbolic.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_magic_symbolic.cpp
rename to src/muz/dl_mk_magic_symbolic.cpp
diff --git a/src/muz_qe/dl_mk_magic_symbolic.h b/src/muz/dl_mk_magic_symbolic.h
similarity index 100%
rename from src/muz_qe/dl_mk_magic_symbolic.h
rename to src/muz/dl_mk_magic_symbolic.h
diff --git a/src/muz_qe/dl_mk_partial_equiv.cpp b/src/muz/dl_mk_partial_equiv.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_partial_equiv.cpp
rename to src/muz/dl_mk_partial_equiv.cpp
diff --git a/src/muz_qe/dl_mk_partial_equiv.h b/src/muz/dl_mk_partial_equiv.h
similarity index 100%
rename from src/muz_qe/dl_mk_partial_equiv.h
rename to src/muz/dl_mk_partial_equiv.h
diff --git a/src/muz_qe/dl_mk_quantifier_abstraction.cpp b/src/muz/dl_mk_quantifier_abstraction.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_quantifier_abstraction.cpp
rename to src/muz/dl_mk_quantifier_abstraction.cpp
diff --git a/src/muz_qe/dl_mk_quantifier_abstraction.h b/src/muz/dl_mk_quantifier_abstraction.h
similarity index 100%
rename from src/muz_qe/dl_mk_quantifier_abstraction.h
rename to src/muz/dl_mk_quantifier_abstraction.h
diff --git a/src/muz_qe/dl_mk_quantifier_instantiation.cpp b/src/muz/dl_mk_quantifier_instantiation.cpp
similarity index 99%
rename from src/muz_qe/dl_mk_quantifier_instantiation.cpp
rename to src/muz/dl_mk_quantifier_instantiation.cpp
index ddbddca01..b24e3e81c 100644
--- a/src/muz_qe/dl_mk_quantifier_instantiation.cpp
+++ b/src/muz/dl_mk_quantifier_instantiation.cpp
@@ -48,7 +48,7 @@ namespace datalog {
         for (unsigned j = 0; j < tsz; ++j) {
             conjs.push_back(r.get_tail(j));            
         }
-        datalog::flatten_and(conjs);
+        qe::flatten_and(conjs);
         for (unsigned j = 0; j < conjs.size(); ++j) {
             expr* e = conjs[j].get();
             quantifier* q;
diff --git a/src/muz_qe/dl_mk_quantifier_instantiation.h b/src/muz/dl_mk_quantifier_instantiation.h
similarity index 100%
rename from src/muz_qe/dl_mk_quantifier_instantiation.h
rename to src/muz/dl_mk_quantifier_instantiation.h
diff --git a/src/muz_qe/dl_mk_rule_inliner.cpp b/src/muz/dl_mk_rule_inliner.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_rule_inliner.cpp
rename to src/muz/dl_mk_rule_inliner.cpp
diff --git a/src/muz_qe/dl_mk_rule_inliner.h b/src/muz/dl_mk_rule_inliner.h
similarity index 100%
rename from src/muz_qe/dl_mk_rule_inliner.h
rename to src/muz/dl_mk_rule_inliner.h
diff --git a/src/muz_qe/dl_mk_scale.cpp b/src/muz/dl_mk_scale.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_scale.cpp
rename to src/muz/dl_mk_scale.cpp
diff --git a/src/muz_qe/dl_mk_scale.h b/src/muz/dl_mk_scale.h
similarity index 100%
rename from src/muz_qe/dl_mk_scale.h
rename to src/muz/dl_mk_scale.h
diff --git a/src/muz_qe/dl_mk_similarity_compressor.cpp b/src/muz/dl_mk_similarity_compressor.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_similarity_compressor.cpp
rename to src/muz/dl_mk_similarity_compressor.cpp
diff --git a/src/muz_qe/dl_mk_similarity_compressor.h b/src/muz/dl_mk_similarity_compressor.h
similarity index 100%
rename from src/muz_qe/dl_mk_similarity_compressor.h
rename to src/muz/dl_mk_similarity_compressor.h
diff --git a/src/muz_qe/dl_mk_simple_joins.cpp b/src/muz/dl_mk_simple_joins.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_simple_joins.cpp
rename to src/muz/dl_mk_simple_joins.cpp
diff --git a/src/muz_qe/dl_mk_simple_joins.h b/src/muz/dl_mk_simple_joins.h
similarity index 100%
rename from src/muz_qe/dl_mk_simple_joins.h
rename to src/muz/dl_mk_simple_joins.h
diff --git a/src/muz_qe/dl_mk_slice.cpp b/src/muz/dl_mk_slice.cpp
similarity index 99%
rename from src/muz_qe/dl_mk_slice.cpp
rename to src/muz/dl_mk_slice.cpp
index 5b9d43acc..0df75324d 100644
--- a/src/muz_qe/dl_mk_slice.cpp
+++ b/src/muz/dl_mk_slice.cpp
@@ -619,7 +619,7 @@ namespace datalog {
         for (unsigned j = r.get_uninterpreted_tail_size(); j < r.get_tail_size(); ++j) {
             conjs.push_back(r.get_tail(j));
         }
-        datalog::flatten_and(conjs);
+        qe::flatten_and(conjs);
         return conjs;
     }
 
diff --git a/src/muz_qe/dl_mk_slice.h b/src/muz/dl_mk_slice.h
similarity index 100%
rename from src/muz_qe/dl_mk_slice.h
rename to src/muz/dl_mk_slice.h
diff --git a/src/muz_qe/dl_mk_subsumption_checker.cpp b/src/muz/dl_mk_subsumption_checker.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_subsumption_checker.cpp
rename to src/muz/dl_mk_subsumption_checker.cpp
diff --git a/src/muz_qe/dl_mk_subsumption_checker.h b/src/muz/dl_mk_subsumption_checker.h
similarity index 100%
rename from src/muz_qe/dl_mk_subsumption_checker.h
rename to src/muz/dl_mk_subsumption_checker.h
diff --git a/src/muz_qe/dl_mk_unbound_compressor.cpp b/src/muz/dl_mk_unbound_compressor.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_unbound_compressor.cpp
rename to src/muz/dl_mk_unbound_compressor.cpp
diff --git a/src/muz_qe/dl_mk_unbound_compressor.h b/src/muz/dl_mk_unbound_compressor.h
similarity index 100%
rename from src/muz_qe/dl_mk_unbound_compressor.h
rename to src/muz/dl_mk_unbound_compressor.h
diff --git a/src/muz_qe/dl_mk_unfold.cpp b/src/muz/dl_mk_unfold.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_unfold.cpp
rename to src/muz/dl_mk_unfold.cpp
diff --git a/src/muz_qe/dl_mk_unfold.h b/src/muz/dl_mk_unfold.h
similarity index 100%
rename from src/muz_qe/dl_mk_unfold.h
rename to src/muz/dl_mk_unfold.h
diff --git a/src/muz_qe/dl_product_relation.cpp b/src/muz/dl_product_relation.cpp
similarity index 100%
rename from src/muz_qe/dl_product_relation.cpp
rename to src/muz/dl_product_relation.cpp
diff --git a/src/muz_qe/dl_product_relation.h b/src/muz/dl_product_relation.h
similarity index 100%
rename from src/muz_qe/dl_product_relation.h
rename to src/muz/dl_product_relation.h
diff --git a/src/muz_qe/dl_relation_manager.cpp b/src/muz/dl_relation_manager.cpp
similarity index 100%
rename from src/muz_qe/dl_relation_manager.cpp
rename to src/muz/dl_relation_manager.cpp
diff --git a/src/muz_qe/dl_relation_manager.h b/src/muz/dl_relation_manager.h
similarity index 100%
rename from src/muz_qe/dl_relation_manager.h
rename to src/muz/dl_relation_manager.h
diff --git a/src/muz_qe/dl_rule.cpp b/src/muz/dl_rule.cpp
similarity index 99%
rename from src/muz_qe/dl_rule.cpp
rename to src/muz/dl_rule.cpp
index 455f2c244..5ac580cb8 100644
--- a/src/muz_qe/dl_rule.cpp
+++ b/src/muz/dl_rule.cpp
@@ -263,7 +263,7 @@ namespace datalog {
         if (m.is_implies(fml, e1, e2)) {
             expr_ref_vector es(m);
             head = ensure_app(e2);
-            datalog::flatten_and(e1, es);
+            qe::flatten_and(e1, es);
             for (unsigned i = 0; i < es.size(); ++i) {
                 body.push_back(ensure_app(es[i].get()));
             }
@@ -380,7 +380,7 @@ namespace datalog {
         for (unsigned i = 0; i < body.size(); ++i) {
             r.push_back(body[i].get());
         }
-        flatten_and(r);
+        qe::flatten_and(r);
         body.reset();
         for (unsigned i = 0; i < r.size(); ++i) {
             body.push_back(ensure_app(r[i].get()));
diff --git a/src/muz_qe/dl_rule.h b/src/muz/dl_rule.h
similarity index 100%
rename from src/muz_qe/dl_rule.h
rename to src/muz/dl_rule.h
diff --git a/src/muz_qe/dl_rule_set.cpp b/src/muz/dl_rule_set.cpp
similarity index 100%
rename from src/muz_qe/dl_rule_set.cpp
rename to src/muz/dl_rule_set.cpp
diff --git a/src/muz_qe/dl_rule_set.h b/src/muz/dl_rule_set.h
similarity index 100%
rename from src/muz_qe/dl_rule_set.h
rename to src/muz/dl_rule_set.h
diff --git a/src/muz_qe/dl_rule_subsumption_index.cpp b/src/muz/dl_rule_subsumption_index.cpp
similarity index 100%
rename from src/muz_qe/dl_rule_subsumption_index.cpp
rename to src/muz/dl_rule_subsumption_index.cpp
diff --git a/src/muz_qe/dl_rule_subsumption_index.h b/src/muz/dl_rule_subsumption_index.h
similarity index 100%
rename from src/muz_qe/dl_rule_subsumption_index.h
rename to src/muz/dl_rule_subsumption_index.h
diff --git a/src/muz_qe/dl_rule_transformer.cpp b/src/muz/dl_rule_transformer.cpp
similarity index 100%
rename from src/muz_qe/dl_rule_transformer.cpp
rename to src/muz/dl_rule_transformer.cpp
diff --git a/src/muz_qe/dl_rule_transformer.h b/src/muz/dl_rule_transformer.h
similarity index 100%
rename from src/muz_qe/dl_rule_transformer.h
rename to src/muz/dl_rule_transformer.h
diff --git a/src/muz_qe/dl_sieve_relation.cpp b/src/muz/dl_sieve_relation.cpp
similarity index 100%
rename from src/muz_qe/dl_sieve_relation.cpp
rename to src/muz/dl_sieve_relation.cpp
diff --git a/src/muz_qe/dl_sieve_relation.h b/src/muz/dl_sieve_relation.h
similarity index 100%
rename from src/muz_qe/dl_sieve_relation.h
rename to src/muz/dl_sieve_relation.h
diff --git a/src/muz_qe/dl_sparse_table.cpp b/src/muz/dl_sparse_table.cpp
similarity index 100%
rename from src/muz_qe/dl_sparse_table.cpp
rename to src/muz/dl_sparse_table.cpp
diff --git a/src/muz_qe/dl_sparse_table.h b/src/muz/dl_sparse_table.h
similarity index 100%
rename from src/muz_qe/dl_sparse_table.h
rename to src/muz/dl_sparse_table.h
diff --git a/src/muz_qe/dl_table.cpp b/src/muz/dl_table.cpp
similarity index 100%
rename from src/muz_qe/dl_table.cpp
rename to src/muz/dl_table.cpp
diff --git a/src/muz_qe/dl_table.h b/src/muz/dl_table.h
similarity index 100%
rename from src/muz_qe/dl_table.h
rename to src/muz/dl_table.h
diff --git a/src/muz_qe/dl_table_plugin.h b/src/muz/dl_table_plugin.h
similarity index 100%
rename from src/muz_qe/dl_table_plugin.h
rename to src/muz/dl_table_plugin.h
diff --git a/src/muz_qe/dl_table_relation.cpp b/src/muz/dl_table_relation.cpp
similarity index 100%
rename from src/muz_qe/dl_table_relation.cpp
rename to src/muz/dl_table_relation.cpp
diff --git a/src/muz_qe/dl_table_relation.h b/src/muz/dl_table_relation.h
similarity index 100%
rename from src/muz_qe/dl_table_relation.h
rename to src/muz/dl_table_relation.h
diff --git a/src/muz_qe/dl_util.cpp b/src/muz/dl_util.cpp
similarity index 83%
rename from src/muz_qe/dl_util.cpp
rename to src/muz/dl_util.cpp
index 1b1042345..0b88136e2 100644
--- a/src/muz_qe/dl_util.cpp
+++ b/src/muz/dl_util.cpp
@@ -40,118 +40,6 @@ namespace datalog {
         ptr->deallocate();
     }
 
-    void flatten_and(expr_ref_vector& result) {
-        ast_manager& m = result.get_manager();
-        expr* e1, *e2, *e3;
-        for (unsigned i = 0; i < result.size(); ++i) {
-            if (m.is_and(result[i].get())) {
-                app* a = to_app(result[i].get());
-                unsigned num_args = a->get_num_args();
-                for (unsigned j = 0; j < num_args; ++j) {
-                    result.push_back(a->get_arg(j));
-                }
-                result[i] = result.back();
-                result.pop_back();
-                --i;
-            }
-            else if (m.is_not(result[i].get(), e1) && m.is_not(e1, e2)) {
-                result[i] = e2;
-                --i;
-            }
-            else if (m.is_not(result[i].get(), e1) && m.is_or(e1)) {
-                app* a = to_app(e1);
-                unsigned num_args = a->get_num_args();
-                for (unsigned j = 0; j < num_args; ++j) {
-                    result.push_back(m.mk_not(a->get_arg(j)));
-                }
-                result[i] = result.back();
-                result.pop_back();
-                --i;                
-            }
-            else if (m.is_not(result[i].get(), e1) && m.is_implies(e1,e2,e3)) {
-                result.push_back(e2);
-                result[i] = m.mk_not(e3);
-                --i;
-            }
-            else if (m.is_true(result[i].get()) ||
-                     (m.is_not(result[i].get(), e1) &&
-                      m.is_false(e1))) {
-                result[i] = result.back();
-                result.pop_back();
-                --i;                
-            }
-            else if (m.is_false(result[i].get()) ||
-                     (m.is_not(result[i].get(), e1) &&
-                      m.is_true(e1))) {
-                result.reset();
-                result.push_back(m.mk_false());
-                return;
-            }
-        }
-    }
-
-    void flatten_and(expr* fml, expr_ref_vector& result) {
-        SASSERT(result.get_manager().is_bool(fml));
-        result.push_back(fml);        
-        flatten_and(result);
-    }
-
-    void flatten_or(expr_ref_vector& result) {
-        ast_manager& m = result.get_manager();
-        expr* e1, *e2, *e3;
-        for (unsigned i = 0; i < result.size(); ++i) {
-            if (m.is_or(result[i].get())) {
-                app* a = to_app(result[i].get());
-                unsigned num_args = a->get_num_args();
-                for (unsigned j = 0; j < num_args; ++j) {
-                    result.push_back(a->get_arg(j));
-                }
-                result[i] = result.back();
-                result.pop_back();
-                --i;
-            }
-            else if (m.is_not(result[i].get(), e1) && m.is_not(e1, e2)) {
-                result[i] = e2;
-                --i;
-            }
-            else if (m.is_not(result[i].get(), e1) && m.is_and(e1)) {
-                app* a = to_app(e1);
-                unsigned num_args = a->get_num_args();
-                for (unsigned j = 0; j < num_args; ++j) {
-                    result.push_back(m.mk_not(a->get_arg(j)));
-                }
-                result[i] = result.back();
-                result.pop_back();
-                --i;                
-            }
-            else if (m.is_implies(result[i].get(),e2,e3)) {
-                result.push_back(e3);
-                result[i] = m.mk_not(e2);
-                --i;
-            }
-            else if (m.is_false(result[i].get()) ||
-                     (m.is_not(result[i].get(), e1) &&
-                      m.is_true(e1))) {
-                result[i] = result.back();
-                result.pop_back();
-                --i;                
-            }
-            else if (m.is_true(result[i].get()) ||
-                     (m.is_not(result[i].get(), e1) &&
-                      m.is_false(e1))) {
-                result.reset();
-                result.push_back(m.mk_true());
-                return;
-            }
-        }        
-    }
-
-
-    void flatten_or(expr* fml, expr_ref_vector& result) {
-        SASSERT(result.get_manager().is_bool(fml));
-        result.push_back(fml);        
-        flatten_or(result);
-    }
 
     bool contains_var(expr * trm, unsigned var_idx) {
         ptr_vector<sort> vars;
diff --git a/src/muz_qe/dl_util.h b/src/muz/dl_util.h
similarity index 98%
rename from src/muz_qe/dl_util.h
rename to src/muz/dl_util.h
index b92a33d1a..debb4d3e2 100644
--- a/src/muz_qe/dl_util.h
+++ b/src/muz/dl_util.h
@@ -30,6 +30,7 @@ Revision History:
 #include"ast_counter.h"
 #include"statistics.h"
 #include"lbool.h"
+#include"qe_util.h"
 
 namespace datalog {
 
@@ -107,18 +108,6 @@ namespace datalog {
     typedef u_map<var *> varidx2var_map;
     typedef obj_hashtable<func_decl> func_decl_set; //!< Rule dependencies.
     typedef vector<std::string> string_vector;
-
-
-    /**
-       \brief Collect top-level conjunctions and disjunctions.
-    */
-    void flatten_and(expr_ref_vector& result);
-
-    void flatten_and(expr* fml, expr_ref_vector& result);
-
-    void flatten_or(expr_ref_vector& result);
-
-    void flatten_or(expr* fml, expr_ref_vector& result);
     
     bool contains_var(expr * trm, unsigned var_idx);
 
diff --git a/src/muz_qe/dl_vector_relation.h b/src/muz/dl_vector_relation.h
similarity index 100%
rename from src/muz_qe/dl_vector_relation.h
rename to src/muz/dl_vector_relation.h
diff --git a/src/muz_qe/equiv_proof_converter.cpp b/src/muz/equiv_proof_converter.cpp
similarity index 100%
rename from src/muz_qe/equiv_proof_converter.cpp
rename to src/muz/equiv_proof_converter.cpp
diff --git a/src/muz_qe/equiv_proof_converter.h b/src/muz/equiv_proof_converter.h
similarity index 100%
rename from src/muz_qe/equiv_proof_converter.h
rename to src/muz/equiv_proof_converter.h
diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz/fixedpoint_params.pyg
similarity index 100%
rename from src/muz_qe/fixedpoint_params.pyg
rename to src/muz/fixedpoint_params.pyg
diff --git a/src/muz_qe/heap_trie.h b/src/muz/heap_trie.h
similarity index 100%
rename from src/muz_qe/heap_trie.h
rename to src/muz/heap_trie.h
diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz/hilbert_basis.cpp
similarity index 100%
rename from src/muz_qe/hilbert_basis.cpp
rename to src/muz/hilbert_basis.cpp
diff --git a/src/muz_qe/hilbert_basis.h b/src/muz/hilbert_basis.h
similarity index 100%
rename from src/muz_qe/hilbert_basis.h
rename to src/muz/hilbert_basis.h
diff --git a/src/muz_qe/hnf.cpp b/src/muz/hnf.cpp
similarity index 99%
rename from src/muz_qe/hnf.cpp
rename to src/muz/hnf.cpp
index 36316cfa6..9d6f3c1ab 100644
--- a/src/muz_qe/hnf.cpp
+++ b/src/muz/hnf.cpp
@@ -214,7 +214,7 @@ private:
             m_body.push_back(e1);
             head = e2;
         }
-        datalog::flatten_and(m_body);
+        qe::flatten_and(m_body);
         if (premise) {
             p = m.mk_rewrite(fml0, mk_implies(m_body, head));
         }
diff --git a/src/muz_qe/hnf.h b/src/muz/hnf.h
similarity index 100%
rename from src/muz_qe/hnf.h
rename to src/muz/hnf.h
diff --git a/src/muz_qe/horn_subsume_model_converter.cpp b/src/muz/horn_subsume_model_converter.cpp
similarity index 100%
rename from src/muz_qe/horn_subsume_model_converter.cpp
rename to src/muz/horn_subsume_model_converter.cpp
diff --git a/src/muz_qe/horn_subsume_model_converter.h b/src/muz/horn_subsume_model_converter.h
similarity index 100%
rename from src/muz_qe/horn_subsume_model_converter.h
rename to src/muz/horn_subsume_model_converter.h
diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz/horn_tactic.cpp
similarity index 99%
rename from src/muz_qe/horn_tactic.cpp
rename to src/muz/horn_tactic.cpp
index 1916839f4..07a0e2568 100644
--- a/src/muz_qe/horn_tactic.cpp
+++ b/src/muz/horn_tactic.cpp
@@ -141,7 +141,7 @@ class horn_tactic : public tactic {
             expr_ref_vector args(m), body(m);
             expr_ref head(m);
             expr* a = 0, *a1 = 0;
-            datalog::flatten_or(tmp, args);
+            qe::flatten_or(tmp, args);
             for (unsigned i = 0; i < args.size(); ++i) {
                 a = args[i].get(); 
                 check_predicate(mark, a);
diff --git a/src/muz_qe/horn_tactic.h b/src/muz/horn_tactic.h
similarity index 100%
rename from src/muz_qe/horn_tactic.h
rename to src/muz/horn_tactic.h
diff --git a/src/muz_qe/model2expr.cpp b/src/muz/model2expr.cpp
similarity index 100%
rename from src/muz_qe/model2expr.cpp
rename to src/muz/model2expr.cpp
diff --git a/src/muz_qe/model2expr.h b/src/muz/model2expr.h
similarity index 100%
rename from src/muz_qe/model2expr.h
rename to src/muz/model2expr.h
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz/pdr_context.cpp
similarity index 99%
rename from src/muz_qe/pdr_context.cpp
rename to src/muz/pdr_context.cpp
index ff40be4f3..db85bc5a9 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz/pdr_context.cpp
@@ -45,6 +45,7 @@ Notes:
 #include "smt_value_sort.h"
 #include "proof_utils.h"
 #include "dl_boogie_proof.h"
+#include "qe_util.h"
 
 namespace pdr {
 
@@ -342,7 +343,7 @@ namespace pdr {
 
     void pred_transformer::add_property(expr* lemma, unsigned lvl) {
         expr_ref_vector lemmas(m);
-        datalog::flatten_and(lemma, lemmas);
+        qe::flatten_and(lemma, lemmas);
         for (unsigned i = 0; i < lemmas.size(); ++i) {
             expr* lemma_i = lemmas[i].get();
             if (add_property1(lemma_i, lvl)) {
@@ -587,7 +588,7 @@ namespace pdr {
         for (unsigned i = ut_size; i < t_size; ++i) {
             tail.push_back(rule.get_tail(i));
         }        
-        datalog::flatten_and(tail);
+        qe::flatten_and(tail);
         for (unsigned i = 0; i < tail.size(); ++i) {
             expr_ref tmp(m);
             var_subst(m, false)(tail[i].get(), var_reprs.size(), (expr*const*)var_reprs.c_ptr(), tmp);
@@ -778,7 +779,7 @@ namespace pdr {
         ast_manager& m = pt().get_manager();
         expr_ref_vector conjs(m);
         obj_map<expr,expr*> model;
-        datalog::flatten_and(state(), conjs);
+        qe::flatten_and(state(), conjs);
         for (unsigned i = 0; i < conjs.size(); ++i) {
             expr* e = conjs[i].get(), *e1, *e2;
             if (m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) {
@@ -1979,7 +1980,7 @@ namespace pdr {
         expr_ref_vector mdl(m), forms(m), Phi(m);
         forms.push_back(T);
         forms.push_back(phi);
-        datalog::flatten_and(forms);        
+        qe::flatten_and(forms);        
         ptr_vector<expr> forms1(forms.size(), forms.c_ptr());
         if (use_model_generalizer) {
             Phi.append(mev.minimize_model(forms1, M));
@@ -2035,7 +2036,7 @@ namespace pdr {
             TRACE("pdr", tout << "Projected:\n" << mk_pp(phi1, m) << "\n";);
         }
         Phi.reset();
-        datalog::flatten_and(phi1, Phi);
+        qe::flatten_and(phi1, Phi);
         unsigned_vector indices;
         vector<expr_ref_vector> child_states;
         child_states.resize(preds.size(), expr_ref_vector(m));
diff --git a/src/muz_qe/pdr_context.h b/src/muz/pdr_context.h
similarity index 100%
rename from src/muz_qe/pdr_context.h
rename to src/muz/pdr_context.h
diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz/pdr_dl_interface.cpp
similarity index 100%
rename from src/muz_qe/pdr_dl_interface.cpp
rename to src/muz/pdr_dl_interface.cpp
diff --git a/src/muz_qe/pdr_dl_interface.h b/src/muz/pdr_dl_interface.h
similarity index 100%
rename from src/muz_qe/pdr_dl_interface.h
rename to src/muz/pdr_dl_interface.h
diff --git a/src/muz_qe/pdr_farkas_learner.cpp b/src/muz/pdr_farkas_learner.cpp
similarity index 99%
rename from src/muz_qe/pdr_farkas_learner.cpp
rename to src/muz/pdr_farkas_learner.cpp
index 8bc77ecc6..6202c913d 100644
--- a/src/muz_qe/pdr_farkas_learner.cpp
+++ b/src/muz/pdr_farkas_learner.cpp
@@ -320,7 +320,7 @@ namespace pdr {
 
         expr_set bs;
         expr_ref_vector blist(m_pr);
-        datalog::flatten_and(B, blist);
+        qe::flatten_and(B, blist);
         for (unsigned i = 0; i < blist.size(); ++i) {
             bs.insert(blist[i].get());
         }
diff --git a/src/muz_qe/pdr_farkas_learner.h b/src/muz/pdr_farkas_learner.h
similarity index 100%
rename from src/muz_qe/pdr_farkas_learner.h
rename to src/muz/pdr_farkas_learner.h
diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz/pdr_generalizers.cpp
similarity index 99%
rename from src/muz_qe/pdr_generalizers.cpp
rename to src/muz/pdr_generalizers.cpp
index 8e15fa983..93a1c1844 100644
--- a/src/muz_qe/pdr_generalizers.cpp
+++ b/src/muz/pdr_generalizers.cpp
@@ -137,7 +137,7 @@ namespace pdr {
             C = pm.mk_or(Bs);
             TRACE("pdr", tout << "prop:\n" << mk_pp(A,m) << "\ngen:" << mk_pp(B, m) << "\nto: " << mk_pp(C, m) << "\n";);
             core.reset();
-            datalog::flatten_and(C, core);    
+            qe::flatten_and(C, core);    
             uses_level = true;
         }    
     }
@@ -157,7 +157,7 @@ namespace pdr {
     }
 
     void core_convex_hull_generalizer::operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores) {
-        // method3(n, core, uses_level, new_cores);
+        method3(n, core, uses_level, new_cores);
         method1(n, core, uses_level, new_cores);
     }
 
@@ -194,11 +194,11 @@ namespace pdr {
         }
         expr_ref fml = n.pt().get_formulas(n.level(), false);
         expr_ref_vector fmls(m);
-        datalog::flatten_and(fml, fmls);
+        qe::flatten_and(fml, fmls);
         for (unsigned i = 0; i < fmls.size(); ++i) {
             fml = m.mk_not(fmls[i].get());
             core2.reset();
-            datalog::flatten_and(fml, core2);
+            qe::flatten_and(fml, core2);
             if (!mk_convex(core2, 1, conv2)) {
                 IF_VERBOSE(0, verbose_stream() << "Non-convex: " << mk_pp(pm.mk_and(core2), m) << "\n";);
                 continue;
@@ -332,7 +332,7 @@ namespace pdr {
         for (unsigned i = 0; i < consequences.size(); ++i) {
             es.reset();
             tmp = m.mk_not(consequences[i].get());
-            datalog::flatten_and(tmp, es);
+            qe::flatten_and(tmp, es);
             if (!mk_convex(es, i, conv)) {
                 IF_VERBOSE(0, verbose_stream() << "Failed to create convex closure\n";);
                 return;
diff --git a/src/muz_qe/pdr_generalizers.h b/src/muz/pdr_generalizers.h
similarity index 100%
rename from src/muz_qe/pdr_generalizers.h
rename to src/muz/pdr_generalizers.h
diff --git a/src/muz_qe/pdr_manager.cpp b/src/muz/pdr_manager.cpp
similarity index 98%
rename from src/muz_qe/pdr_manager.cpp
rename to src/muz/pdr_manager.cpp
index 3e79e4f00..9eb10aba9 100644
--- a/src/muz_qe/pdr_manager.cpp
+++ b/src/muz/pdr_manager.cpp
@@ -56,7 +56,7 @@ namespace pdr {
 
     expr_ref inductive_property::fixup_clause(expr* fml) const {        
         expr_ref_vector disjs(m);
-        datalog::flatten_or(fml, disjs);
+        qe::flatten_or(fml, disjs);
         expr_ref result(m);
         bool_rewriter(m).mk_or(disjs.size(), disjs.c_ptr(), result);
         return result;
@@ -65,7 +65,7 @@ namespace pdr {
     expr_ref inductive_property::fixup_clauses(expr* fml) const {
         expr_ref_vector conjs(m);
         expr_ref result(m);
-        datalog::flatten_and(fml, conjs);
+        qe::flatten_and(fml, conjs);
         for (unsigned i = 0; i < conjs.size(); ++i) {
             conjs[i] = fixup_clause(conjs[i].get());
         }
@@ -238,7 +238,7 @@ namespace pdr {
     expr_ref manager::mk_not_and(expr_ref_vector const& conjs) {
         expr_ref result(m), e(m);
         expr_ref_vector es(conjs);
-        datalog::flatten_and(es);
+        qe::flatten_and(es);
         for (unsigned i = 0; i < es.size(); ++i) {
             m_brwr.mk_not(es[i].get(), e);
             es[i] = e;
diff --git a/src/muz_qe/pdr_manager.h b/src/muz/pdr_manager.h
similarity index 100%
rename from src/muz_qe/pdr_manager.h
rename to src/muz/pdr_manager.h
diff --git a/src/muz_qe/pdr_prop_solver.cpp b/src/muz/pdr_prop_solver.cpp
similarity index 99%
rename from src/muz_qe/pdr_prop_solver.cpp
rename to src/muz/pdr_prop_solver.cpp
index eb3c0ee96..d9b22e04e 100644
--- a/src/muz_qe/pdr_prop_solver.cpp
+++ b/src/muz/pdr_prop_solver.cpp
@@ -76,7 +76,7 @@ namespace pdr {
         }
 
         void mk_safe(expr_ref_vector& conjs) {
-            datalog::flatten_and(conjs);
+            qe::flatten_and(conjs);
             expand_literals(conjs);
             for (unsigned i = 0; i < conjs.size(); ++i) {
                 expr * lit = conjs[i].get();
diff --git a/src/muz_qe/pdr_prop_solver.h b/src/muz/pdr_prop_solver.h
similarity index 100%
rename from src/muz_qe/pdr_prop_solver.h
rename to src/muz/pdr_prop_solver.h
diff --git a/src/muz_qe/pdr_reachable_cache.cpp b/src/muz/pdr_reachable_cache.cpp
similarity index 100%
rename from src/muz_qe/pdr_reachable_cache.cpp
rename to src/muz/pdr_reachable_cache.cpp
diff --git a/src/muz_qe/pdr_reachable_cache.h b/src/muz/pdr_reachable_cache.h
similarity index 100%
rename from src/muz_qe/pdr_reachable_cache.h
rename to src/muz/pdr_reachable_cache.h
diff --git a/src/muz_qe/pdr_smt_context_manager.cpp b/src/muz/pdr_smt_context_manager.cpp
similarity index 100%
rename from src/muz_qe/pdr_smt_context_manager.cpp
rename to src/muz/pdr_smt_context_manager.cpp
diff --git a/src/muz_qe/pdr_smt_context_manager.h b/src/muz/pdr_smt_context_manager.h
similarity index 100%
rename from src/muz_qe/pdr_smt_context_manager.h
rename to src/muz/pdr_smt_context_manager.h
diff --git a/src/muz_qe/pdr_sym_mux.cpp b/src/muz/pdr_sym_mux.cpp
similarity index 100%
rename from src/muz_qe/pdr_sym_mux.cpp
rename to src/muz/pdr_sym_mux.cpp
diff --git a/src/muz_qe/pdr_sym_mux.h b/src/muz/pdr_sym_mux.h
similarity index 100%
rename from src/muz_qe/pdr_sym_mux.h
rename to src/muz/pdr_sym_mux.h
diff --git a/src/muz_qe/pdr_util.cpp b/src/muz/pdr_util.cpp
similarity index 99%
rename from src/muz_qe/pdr_util.cpp
rename to src/muz/pdr_util.cpp
index 3d93f8104..d23dc186e 100644
--- a/src/muz_qe/pdr_util.cpp
+++ b/src/muz/pdr_util.cpp
@@ -954,7 +954,7 @@ namespace pdr {
     void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) {
         ast_manager& m = fml.get_manager();
         expr_ref_vector conjs(m);
-        datalog::flatten_and(fml, conjs);
+        qe::flatten_and(fml, conjs);
         obj_map<expr, unsigned> diseqs;
         expr* n, *lhs, *rhs;
         for (unsigned i = 0; i < conjs.size(); ++i) {
diff --git a/src/muz_qe/pdr_util.h b/src/muz/pdr_util.h
similarity index 100%
rename from src/muz_qe/pdr_util.h
rename to src/muz/pdr_util.h
diff --git a/src/muz_qe/proof_utils.cpp b/src/muz/proof_utils.cpp
similarity index 100%
rename from src/muz_qe/proof_utils.cpp
rename to src/muz/proof_utils.cpp
diff --git a/src/muz_qe/proof_utils.h b/src/muz/proof_utils.h
similarity index 100%
rename from src/muz_qe/proof_utils.h
rename to src/muz/proof_utils.h
diff --git a/src/muz_qe/rel_context.cpp b/src/muz/rel_context.cpp
similarity index 100%
rename from src/muz_qe/rel_context.cpp
rename to src/muz/rel_context.cpp
diff --git a/src/muz_qe/rel_context.h b/src/muz/rel_context.h
similarity index 100%
rename from src/muz_qe/rel_context.h
rename to src/muz/rel_context.h
diff --git a/src/muz_qe/replace_proof_converter.cpp b/src/muz/replace_proof_converter.cpp
similarity index 100%
rename from src/muz_qe/replace_proof_converter.cpp
rename to src/muz/replace_proof_converter.cpp
diff --git a/src/muz_qe/replace_proof_converter.h b/src/muz/replace_proof_converter.h
similarity index 100%
rename from src/muz_qe/replace_proof_converter.h
rename to src/muz/replace_proof_converter.h
diff --git a/src/muz_qe/skip_list_base.h b/src/muz/skip_list_base.h
similarity index 100%
rename from src/muz_qe/skip_list_base.h
rename to src/muz/skip_list_base.h
diff --git a/src/muz_qe/tab_context.cpp b/src/muz/tab_context.cpp
similarity index 99%
rename from src/muz_qe/tab_context.cpp
rename to src/muz/tab_context.cpp
index 4f4c14cc7..a56d16a0e 100644
--- a/src/muz_qe/tab_context.cpp
+++ b/src/muz/tab_context.cpp
@@ -208,7 +208,7 @@ namespace tb {
                 fmls.push_back(m_predicates[i]);
             }
             fmls.push_back(m_constraint);
-            datalog::flatten_and(fmls);
+            qe::flatten_and(fmls);
             bool_rewriter(m).mk_and(fmls.size(), fmls.c_ptr(), fml);
             return fml;
         }
@@ -337,7 +337,7 @@ namespace tb {
             expr_ref tmp(m);
             substitution subst(m);
             subst.reserve(1, get_num_vars());
-            datalog::flatten_and(m_constraint, fmls);
+            qe::flatten_and(m_constraint, fmls);
             unsigned num_fmls = fmls.size();
             for (unsigned i = 0; i < num_fmls; ++i) {
                 if (get_subst(rw, subst, i, fmls)) {
@@ -664,7 +664,7 @@ namespace tb {
 
 
             m_qe(m_empty_set, false, fmls);
-            datalog::flatten_and(fmls);
+            qe::flatten_and(fmls);
             for (unsigned i = 0; i < fmls.size(); ++i) {
                 expr_ref n = normalize(fmls[i].get());
                 if (m_sat_lits.contains(n)) {
diff --git a/src/muz_qe/tab_context.h b/src/muz/tab_context.h
similarity index 100%
rename from src/muz_qe/tab_context.h
rename to src/muz/tab_context.h
diff --git a/src/muz_qe/unit_subsumption_tactic.cpp b/src/muz/unit_subsumption_tactic.cpp
similarity index 100%
rename from src/muz_qe/unit_subsumption_tactic.cpp
rename to src/muz/unit_subsumption_tactic.cpp
diff --git a/src/muz_qe/unit_subsumption_tactic.h b/src/muz/unit_subsumption_tactic.h
similarity index 100%
rename from src/muz_qe/unit_subsumption_tactic.h
rename to src/muz/unit_subsumption_tactic.h
diff --git a/src/muz_qe/vsubst_tactic.cpp b/src/muz/vsubst_tactic.cpp
similarity index 100%
rename from src/muz_qe/vsubst_tactic.cpp
rename to src/muz/vsubst_tactic.cpp
diff --git a/src/muz_qe/vsubst_tactic.h b/src/muz/vsubst_tactic.h
similarity index 100%
rename from src/muz_qe/vsubst_tactic.h
rename to src/muz/vsubst_tactic.h
diff --git a/src/muz_qe/nlarith_util.cpp b/src/qe/nlarith_util.cpp
similarity index 100%
rename from src/muz_qe/nlarith_util.cpp
rename to src/qe/nlarith_util.cpp
diff --git a/src/muz_qe/nlarith_util.h b/src/qe/nlarith_util.h
similarity index 100%
rename from src/muz_qe/nlarith_util.h
rename to src/qe/nlarith_util.h
diff --git a/src/muz_qe/qe.cpp b/src/qe/qe.cpp
similarity index 99%
rename from src/muz_qe/qe.cpp
rename to src/qe/qe.cpp
index 894a935b5..d0aafb896 100644
--- a/src/muz_qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -36,7 +36,7 @@ Revision History:
 #include "expr_functors.h"
 #include "quant_hoist.h"
 #include "bool_rewriter.h"
-#include "dl_util.h"
+#include "qe_util.h"
 #include "th_rewriter.h"
 #include "smt_kernel.h"
 #include "model_evaluator.h"
@@ -81,7 +81,7 @@ namespace qe {
             ptr_vector<expr> todo;
             ptr_vector<expr> conjs_closed, conjs_mixed, conjs_open;
             
-            datalog::flatten_and(fml, conjs);
+            qe::flatten_and(fml, conjs);
 
             for (unsigned i = 0; i < conjs.size(); ++i) {
                 todo.push_back(conjs[i].get());
@@ -306,7 +306,7 @@ namespace qe {
     // conj_enum
 
     conj_enum::conj_enum(ast_manager& m, expr* e): m(m), m_conjs(m) {
-        datalog::flatten_and(e, m_conjs);
+        qe::flatten_and(e, m_conjs);
     }
 
     void conj_enum::extract_equalities(expr_ref_vector& eqs) {
diff --git a/src/muz_qe/qe.h b/src/qe/qe.h
similarity index 100%
rename from src/muz_qe/qe.h
rename to src/qe/qe.h
diff --git a/src/muz_qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp
similarity index 100%
rename from src/muz_qe/qe_arith_plugin.cpp
rename to src/qe/qe_arith_plugin.cpp
diff --git a/src/muz_qe/qe_array_plugin.cpp b/src/qe/qe_array_plugin.cpp
similarity index 100%
rename from src/muz_qe/qe_array_plugin.cpp
rename to src/qe/qe_array_plugin.cpp
diff --git a/src/muz_qe/qe_bool_plugin.cpp b/src/qe/qe_bool_plugin.cpp
similarity index 100%
rename from src/muz_qe/qe_bool_plugin.cpp
rename to src/qe/qe_bool_plugin.cpp
diff --git a/src/muz_qe/qe_bv_plugin.cpp b/src/qe/qe_bv_plugin.cpp
similarity index 100%
rename from src/muz_qe/qe_bv_plugin.cpp
rename to src/qe/qe_bv_plugin.cpp
diff --git a/src/muz_qe/qe_cmd.cpp b/src/qe/qe_cmd.cpp
similarity index 100%
rename from src/muz_qe/qe_cmd.cpp
rename to src/qe/qe_cmd.cpp
diff --git a/src/muz_qe/qe_cmd.h b/src/qe/qe_cmd.h
similarity index 100%
rename from src/muz_qe/qe_cmd.h
rename to src/qe/qe_cmd.h
diff --git a/src/muz_qe/qe_datatype_plugin.cpp b/src/qe/qe_datatype_plugin.cpp
similarity index 100%
rename from src/muz_qe/qe_datatype_plugin.cpp
rename to src/qe/qe_datatype_plugin.cpp
diff --git a/src/muz_qe/qe_dl_plugin.cpp b/src/qe/qe_dl_plugin.cpp
similarity index 100%
rename from src/muz_qe/qe_dl_plugin.cpp
rename to src/qe/qe_dl_plugin.cpp
diff --git a/src/muz_qe/qe_lite.cpp b/src/qe/qe_lite.cpp
similarity index 99%
rename from src/muz_qe/qe_lite.cpp
rename to src/qe/qe_lite.cpp
index 01537b574..130673527 100644
--- a/src/muz_qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -30,9 +30,8 @@ Revision History:
 #include "bool_rewriter.h"
 #include "var_subst.h"
 #include "uint_set.h"
-#include "dl_util.h"
+#include "qe_util.h"
 #include "th_rewriter.h"
-#include "dl_util.h"
 #include "for_each_expr.h"
 #include "expr_safe_replace.h"
 #include "cooperate.h"
@@ -696,7 +695,7 @@ namespace eq {
                     m_subst(r, m_subst_map.size(), m_subst_map.c_ptr(), new_r);
                     m_rewriter(new_r);
                     conjs.reset();
-                    datalog::flatten_and(new_r, conjs);
+                    qe::flatten_and(new_r, conjs);
                     reduced = true;
                 }
             }
@@ -2387,7 +2386,7 @@ public:
 
     void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml) {
         expr_ref_vector disjs(m);
-        datalog::flatten_or(fml, disjs);
+        qe::flatten_or(fml, disjs);
         for (unsigned i = 0; i < disjs.size(); ++i) {
             expr_ref_vector conjs(m);
             conjs.push_back(disjs[i].get());
@@ -2400,7 +2399,7 @@ public:
 
 
     void operator()(uint_set const& index_set, bool index_of_bound, expr_ref_vector& fmls) {
-        datalog::flatten_and(fmls);
+        qe::flatten_and(fmls);
         unsigned index;
         if (has_unique_non_ground(fmls, index)) {
             expr_ref fml(m);
diff --git a/src/muz_qe/qe_lite.h b/src/qe/qe_lite.h
similarity index 100%
rename from src/muz_qe/qe_lite.h
rename to src/qe/qe_lite.h
diff --git a/src/muz_qe/qe_sat_tactic.cpp b/src/qe/qe_sat_tactic.cpp
similarity index 100%
rename from src/muz_qe/qe_sat_tactic.cpp
rename to src/qe/qe_sat_tactic.cpp
diff --git a/src/muz_qe/qe_sat_tactic.h b/src/qe/qe_sat_tactic.h
similarity index 100%
rename from src/muz_qe/qe_sat_tactic.h
rename to src/qe/qe_sat_tactic.h
diff --git a/src/muz_qe/qe_tactic.cpp b/src/qe/qe_tactic.cpp
similarity index 100%
rename from src/muz_qe/qe_tactic.cpp
rename to src/qe/qe_tactic.cpp
diff --git a/src/muz_qe/qe_tactic.h b/src/qe/qe_tactic.h
similarity index 100%
rename from src/muz_qe/qe_tactic.h
rename to src/qe/qe_tactic.h
diff --git a/src/qe/qe_util.cpp b/src/qe/qe_util.cpp
new file mode 100644
index 000000000..629fe4b56
--- /dev/null
+++ b/src/qe/qe_util.cpp
@@ -0,0 +1,116 @@
+#include "qe_util.h"
+
+namespace qe {
+    void flatten_and(expr_ref_vector& result) {
+        ast_manager& m = result.get_manager();
+        expr* e1, *e2, *e3;
+        for (unsigned i = 0; i < result.size(); ++i) {
+            if (m.is_and(result[i].get())) {
+                app* a = to_app(result[i].get());
+                unsigned num_args = a->get_num_args();
+                for (unsigned j = 0; j < num_args; ++j) {
+                    result.push_back(a->get_arg(j));
+                }
+                result[i] = result.back();
+                result.pop_back();
+                --i;
+            }
+            else if (m.is_not(result[i].get(), e1) && m.is_not(e1, e2)) {
+                result[i] = e2;
+                --i;
+            }
+            else if (m.is_not(result[i].get(), e1) && m.is_or(e1)) {
+                app* a = to_app(e1);
+                unsigned num_args = a->get_num_args();
+                for (unsigned j = 0; j < num_args; ++j) {
+                    result.push_back(m.mk_not(a->get_arg(j)));
+                }
+                result[i] = result.back();
+                result.pop_back();
+                --i;                
+            }
+            else if (m.is_not(result[i].get(), e1) && m.is_implies(e1,e2,e3)) {
+                result.push_back(e2);
+                result[i] = m.mk_not(e3);
+                --i;
+            }
+            else if (m.is_true(result[i].get()) ||
+                     (m.is_not(result[i].get(), e1) &&
+                      m.is_false(e1))) {
+                result[i] = result.back();
+                result.pop_back();
+                --i;                
+            }
+            else if (m.is_false(result[i].get()) ||
+                     (m.is_not(result[i].get(), e1) &&
+                      m.is_true(e1))) {
+                result.reset();
+                result.push_back(m.mk_false());
+                return;
+            }
+        }
+    }
+
+    void flatten_and(expr* fml, expr_ref_vector& result) {
+        SASSERT(result.get_manager().is_bool(fml));
+        result.push_back(fml);        
+        flatten_and(result);
+    }
+
+    void flatten_or(expr_ref_vector& result) {
+        ast_manager& m = result.get_manager();
+        expr* e1, *e2, *e3;
+        for (unsigned i = 0; i < result.size(); ++i) {
+            if (m.is_or(result[i].get())) {
+                app* a = to_app(result[i].get());
+                unsigned num_args = a->get_num_args();
+                for (unsigned j = 0; j < num_args; ++j) {
+                    result.push_back(a->get_arg(j));
+                }
+                result[i] = result.back();
+                result.pop_back();
+                --i;
+            }
+            else if (m.is_not(result[i].get(), e1) && m.is_not(e1, e2)) {
+                result[i] = e2;
+                --i;
+            }
+            else if (m.is_not(result[i].get(), e1) && m.is_and(e1)) {
+                app* a = to_app(e1);
+                unsigned num_args = a->get_num_args();
+                for (unsigned j = 0; j < num_args; ++j) {
+                    result.push_back(m.mk_not(a->get_arg(j)));
+                }
+                result[i] = result.back();
+                result.pop_back();
+                --i;                
+            }
+            else if (m.is_implies(result[i].get(),e2,e3)) {
+                result.push_back(e3);
+                result[i] = m.mk_not(e2);
+                --i;
+            }
+            else if (m.is_false(result[i].get()) ||
+                     (m.is_not(result[i].get(), e1) &&
+                      m.is_true(e1))) {
+                result[i] = result.back();
+                result.pop_back();
+                --i;                
+            }
+            else if (m.is_true(result[i].get()) ||
+                     (m.is_not(result[i].get(), e1) &&
+                      m.is_false(e1))) {
+                result.reset();
+                result.push_back(m.mk_true());
+                return;
+            }
+        }        
+    }
+
+
+    void flatten_or(expr* fml, expr_ref_vector& result) {
+        SASSERT(result.get_manager().is_bool(fml));
+        result.push_back(fml);        
+        flatten_or(result);
+    }
+}
diff --git a/src/qe/qe_util.h b/src/qe/qe_util.h
new file mode 100644
index 000000000..7e1fe7f79
--- /dev/null
+++ b/src/qe/qe_util.h
@@ -0,0 +1,37 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    qe_util.h
+
+Abstract:
+
+    Utilities for quantifiers.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-08-28
+
+Revision History:
+
+--*/
+#ifndef _QE_UTIL_H_
+#define _QE_UTIL_H_
+
+#include "ast.h"
+
+namespace qe {
+    /**
+       \brief Collect top-level conjunctions and disjunctions.
+    */
+    void flatten_and(expr_ref_vector& result);
+
+    void flatten_and(expr* fml, expr_ref_vector& result);
+
+    void flatten_or(expr_ref_vector& result);
+
+    void flatten_or(expr* fml, expr_ref_vector& result);
+
+}
+#endif