Flatten libcvc4 build structure; remove some #include interdependences

42 files changed, 74 insertions, 545 deletions

diff --git a/src/theory/Makefile b/src/theory/Makefile
deleted file mode 100644
index da7d0e6b9..000000000
--- a/src/theory/Makefile
+++ /dev/null
@@ -1,4 +0,0 @@
-topdir = ../..
-srcdir = src/theory
-
-include $(topdir)/Makefile.subdir
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
deleted file mode 100644
index 860075aa8..000000000
--- a/src/theory/Makefile.am
+++ /dev/null
@@ -1,111 +0,0 @@
-AM_CPPFLAGS = \
-	-D__BUILDING_CVC4LIB \
-	-I@builddir@/.. -I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
-
-SUBDIRS = builtin booleans uf arith bv arrays datatypes quantifiers rewriterules idl strings
-DIST_SUBDIRS = $(SUBDIRS) example
-
-noinst_LTLIBRARIES = libtheory.la
-
-libtheory_la_SOURCES = \
-	decision_attributes.h \
-	logic_info.h \
-	logic_info.cpp \
-	output_channel.h \
-	interrupted.h \
-	type_enumerator.h \
-	theory_engine.h \
-	theory_engine.cpp \
-	theory_test_utils.h \
-	theory.h \
-	theory.cpp \
-	theoryof_mode.h \
-	theory_registrar.h \
-	rewriter.h \
-	rewriter_attributes.h \
-	rewriter.cpp \
-	substitutions.h \
-	substitutions.cpp \
-	valuation.h \
-	valuation.cpp \
-	shared_terms_database.h \
-	shared_terms_database.cpp \
-	term_registration_visitor.h \
-	term_registration_visitor.cpp \
-	ite_simplifier.h \
-	ite_simplifier.cpp \
-	unconstrained_simplifier.h \
-	unconstrained_simplifier.cpp \
-	quantifiers_engine.h \
-	quantifiers_engine.cpp \
-	model.h \
-	model.cpp \
-	rep_set.h \
-	rep_set.cpp \
-	atom_requests.h \
-	atom_requests.cpp
-
-nodist_libtheory_la_SOURCES = \
-	rewriter_tables.h \
-	theory_traits.h \
-	type_enumerator.cpp
-
-libtheory_la_LIBADD = \
-	@builddir@/builtin/libbuiltin.la \
-	@builddir@/booleans/libbooleans.la \
-	@builddir@/uf/libuf.la \
-	@builddir@/arith/libarith.la \
-	@builddir@/arrays/libarrays.la \
-	@builddir@/bv/libbv.la \
-	@builddir@/datatypes/libdatatypes.la \
-	@builddir@/quantifiers/libquantifiers.la \
-	@builddir@/rewriterules/librewriterules.la \
-	@builddir@/idl/libidl.la \
-	@builddir@/strings/libstrings.la
-
-EXTRA_DIST = \
-	logic_info.i \
-	options_handlers.h \
-	rewriter_tables_template.h \
-	theory_traits_template.h \
-	type_enumerator_template.cpp \
-	mktheorytraits \
-	mkrewriter \
-	Makefile.subdirs
-
-BUILT_SOURCES = \
-	rewriter_tables.h \
-	theory_traits.h \
-	type_enumerator.cpp
-
-CLEANFILES = \
-	rewriter_tables.h \
-	theory_traits.h \
-	type_enumerator.cpp
-
-include @top_srcdir@/src/theory/Makefile.subdirs
-
-rewriter_tables.h: rewriter_tables_template.h mkrewriter @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
-	$(AM_V_at)chmod +x @srcdir@/mkrewriter
-	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
-	$(AM_V_GEN)(@srcdir@/mkrewriter \
-		$< \
-		`cat @top_builddir@/src/theory/.subdirs` \
-	> $@) || (rm -f $@ && exit 1)
-
-theory_traits.h: theory_traits_template.h mktheorytraits @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
-	$(AM_V_at)chmod +x @srcdir@/mktheorytraits
-	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
-	$(AM_V_GEN)(@srcdir@/mktheorytraits \
-		$< \
-		`cat @top_builddir@/src/theory/.subdirs` \
-	> $@) || (rm -f $@ && exit 1)
-
-type_enumerator.cpp: type_enumerator_template.cpp mktheorytraits @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
-	$(AM_V_at)chmod +x @srcdir@/mktheorytraits
-	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
-	$(AM_V_GEN)(@srcdir@/mktheorytraits \
-		$< \
-		`cat @top_builddir@/src/theory/.subdirs` \
-	> $@) || (rm -f $@ && exit 1)
diff --git a/src/theory/Makefile.subdirs b/src/theory/Makefile.subdirs
index 99adc7d0d..9dbe458df 100644
--- a/src/theory/Makefile.subdirs
+++ b/src/theory/Makefile.subdirs
@@ -1,5 +1,5 @@
-$(top_builddir)/src/theory/.subdirs: $(top_srcdir)/src/theory/Makefile.am
-	$(AM_V_at)grep '^SUBDIRS = ' $(top_srcdir)/src/theory/Makefile.am | cut -d' ' -f3- | tr ' ' "\n" | xargs -I__D__ echo $(top_srcdir)/src/theory/__D__/kinds >$(top_builddir)/src/theory/.subdirs.tmp
+$(top_builddir)/src/theory/.subdirs: $(top_srcdir)/src/Makefile.am
+	$(AM_V_at)grep '^THEORIES = ' $(top_srcdir)/src/Makefile.am | cut -d' ' -f3- | tr ' ' "\n" | xargs -I__D__ echo $(top_srcdir)/src/theory/__D__/kinds >$(top_builddir)/src/theory/.subdirs.tmp
 	@if ! diff -q $(top_builddir)/src/theory/.subdirs $(top_builddir)/src/theory/.subdirs.tmp &>/dev/null; then \
 		echo "  GEN   " $@; \
 		$(am__mv) $(top_builddir)/src/theory/.subdirs.tmp $(top_builddir)/src/theory/.subdirs; \
diff --git a/src/theory/arith/Makefile b/src/theory/arith/Makefile
deleted file mode 100644
index 5016522e8..000000000
--- a/src/theory/arith/Makefile
+++ /dev/null
@@ -1,4 +0,0 @@
-topdir = ../../..
-srcdir = src/theory/arith
-
-include $(topdir)/Makefile.subdir
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
deleted file mode 100644
index 620b8a121..000000000
--- a/src/theory/arith/Makefile.am
+++ /dev/null
@@ -1,72 +0,0 @@
-AM_CPPFLAGS = \
-	-D__BUILDING_CVC4LIB \
-	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
-
-noinst_LTLIBRARIES = libarith.la
-
-libarith_la_SOURCES = \
-	theory_arith_type_rules.h \
-	type_enumerator.h \
-	arithvar.h \
-	arithvar.cpp \
-	bound_counts.h \
-	arith_rewriter.h \
-	arith_rewriter.cpp \
-	arith_static_learner.h \
-	arith_static_learner.cpp \
-	constraint_forward.h \
-	constraint.h \
-	constraint.cpp \
-	congruence_manager.h \
-	congruence_manager.cpp \
-	normal_form.h\
-	normal_form.cpp \
-	arith_utilities.h \
-	delta_rational.h \
-	delta_rational.cpp \
-	partial_model.h \
-	partial_model.cpp \
-	linear_equality.h \
-	linear_equality.cpp \
-	simplex_update.h \
-	simplex_update.cpp \
-	callbacks.h \
-	callbacks.cpp \
-	matrix.h \
-	matrix.cpp \
-	tableau.h \
-	tableau.cpp \
-	tableau_sizes.h \
-	tableau_sizes.cpp \
-	error_set.h \
-	error_set.cpp \
-	simplex.h \
-	simplex.cpp \
-	dual_simplex.h \
-	dual_simplex.cpp \
-	fc_simplex.h \
-	fc_simplex.cpp \
-	soi_simplex.h \
-	soi_simplex.cpp \
-	approx_simplex.h \
-	approx_simplex.cpp \
-	attempt_solution_simplex.h \
-	attempt_solution_simplex.cpp \
-	theory_arith.h \
-	theory_arith.cpp \
-	theory_arith_private_forward.h \
-	theory_arith_private.h \
-	theory_arith_private.cpp \
-	dio_solver.h \
-	dio_solver.cpp \
-	arith_heuristic_pivot_rule.h \
-	arith_heuristic_pivot_rule.cpp \
-	arith_unate_lemma_mode.h \
-	arith_unate_lemma_mode.cpp \
-	arith_propagation_mode.h \
-	arith_propagation_mode.cpp
-
-EXTRA_DIST = \
-	kinds \
-	options_handlers.h
diff --git a/src/theory/arrays/Makefile b/src/theory/arrays/Makefile
deleted file mode 100644
index bce529db0..000000000
--- a/src/theory/arrays/Makefile
+++ /dev/null
@@ -1,4 +0,0 @@
-topdir = ../../..
-srcdir = src/theory/arrays
-
-include $(topdir)/Makefile.subdir
diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am
deleted file mode 100644
index 77f102cf8..000000000
--- a/src/theory/arrays/Makefile.am
+++ /dev/null
@@ -1,22 +0,0 @@
-AM_CPPFLAGS = \
-	-D__BUILDING_CVC4LIB \
-	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
-
-noinst_LTLIBRARIES = libarrays.la
-
-libarrays_la_SOURCES = \
-	theory_arrays_type_rules.h \
-	type_enumerator.h \
-	theory_arrays_rewriter.h \
-	theory_arrays.h \
-	theory_arrays.cpp \
-	union_find.h \
-	union_find.cpp \
-	array_info.h \
-	array_info.cpp \
-	static_fact_manager.h \
-	static_fact_manager.cpp
-
-EXTRA_DIST = \
-	kinds
diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp
new file mode 100644
index 000000000..d926cd7a2
--- /dev/null
+++ b/src/theory/arrays/theory_arrays_rewriter.cpp
@@ -0,0 +1,49 @@
+/*********************                                                        */
+/*! \file theory_arrays_rewriter.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "expr/attribute.h"
+#include "theory/arrays/theory_arrays_rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+namespace attr {
+  struct ArrayConstantMostFrequentValueTag { };
+  struct ArrayConstantMostFrequentValueCountTag { };
+}/* CVC4::theory::arrays::attr namespace */
+
+typedef expr::Attribute<attr::ArrayConstantMostFrequentValueCountTag, uint64_t> ArrayConstantMostFrequentValueCountAttr;
+typedef expr::Attribute<attr::ArrayConstantMostFrequentValueTag, Node> ArrayConstantMostFrequentValueAttr;
+
+Node getMostFrequentValue(TNode store) {
+  return store.getAttribute(ArrayConstantMostFrequentValueAttr());
+}
+uint64_t getMostFrequentValueCount(TNode store) {
+  return store.getAttribute(ArrayConstantMostFrequentValueCountAttr());
+}
+
+void setMostFrequentValue(TNode store, TNode value) {
+  return store.setAttribute(ArrayConstantMostFrequentValueAttr(), value);
+}
+void setMostFrequentValueCount(TNode store, uint64_t count) {
+  return store.setAttribute(ArrayConstantMostFrequentValueCountAttr(), count);
+}
+
+}/* CVC4::theory::arrays namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 5df06bda8..388769412 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -22,19 +22,15 @@
 
 #include "theory/rewriter.h"
 #include "theory/type_enumerator.h"
-#include "expr/attribute.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arrays {
 
-namespace attr {
-  struct ArrayConstantMostFrequentValueTag { };
-  struct ArrayConstantMostFrequentValueCountTag { };
-}/* CVC4::theory::arrays::attr namespace */
-
-typedef expr::Attribute<attr::ArrayConstantMostFrequentValueCountTag, uint64_t> ArrayConstantMostFrequentValueCountAttr;
-typedef expr::Attribute<attr::ArrayConstantMostFrequentValueTag, Node> ArrayConstantMostFrequentValueAttr;
+Node getMostFrequentValue(TNode store);
+uint64_t getMostFrequentValueCount(TNode store);
+void setMostFrequentValue(TNode store, TNode value);
+void setMostFrequentValueCount(TNode store, uint64_t count);
 
 static inline Node mkEqNode(Node a, Node b) {
   return a.getType().isBoolean() ? a.iffNode(b) : a.eqNode(b);
@@ -132,8 +128,8 @@ public:
     unsigned mostFrequentValueCount = 0;
     store = node[0];
     if (store.getKind() == kind::STORE) {
-      mostFrequentValue = store.getAttribute(ArrayConstantMostFrequentValueAttr());
-      mostFrequentValueCount = store.getAttribute(ArrayConstantMostFrequentValueCountAttr());
+      mostFrequentValue = getMostFrequentValue(store);
+      mostFrequentValueCount = getMostFrequentValueCount(store);
     }
 
     // Compute the most frequently written value for n
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index b16b62f69..9f7bdfd4a 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -127,8 +127,8 @@ struct ArrayStoreTypeRule {
     unsigned mostFrequentValueCount = 0;
     store = n[0];
     if (store.getKind() == kind::STORE) {
-      mostFrequentValue = store.getAttribute(ArrayConstantMostFrequentValueAttr());
-      mostFrequentValueCount = store.getAttribute(ArrayConstantMostFrequentValueCountAttr());
+      mostFrequentValue = getMostFrequentValue(store);
+      mostFrequentValueCount = getMostFrequentValueCount(store);
     }
 
     // Compute the most frequently written value for n
@@ -145,8 +145,8 @@ struct ArrayStoreTypeRule {
         (compare == Cardinality::EQUAL && (!(defaultValue < mostFrequentValue)))) {
       return false;
     }
-    n.setAttribute(ArrayConstantMostFrequentValueAttr(), mostFrequentValue);
-    n.setAttribute(ArrayConstantMostFrequentValueCountAttr(), mostFrequentValueCount);
+    setMostFrequentValue(n, mostFrequentValue);
+    setMostFrequentValueCount(n, mostFrequentValueCount);
     return true;
   }
 
diff --git a/src/theory/booleans/Makefile b/src/theory/booleans/Makefile
deleted file mode 100644
index a74a72d83..000000000
--- a/src/theory/booleans/Makefile
+++ /dev/null
@@ -1,4 +0,0 @@
-topdir = ../../..
-srcdir = src/theory/bool
-
-include $(topdir)/Makefile.subdir
diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am
deleted file mode 100644
index 9d58ffa75..000000000
--- a/src/theory/booleans/Makefile.am
+++ /dev/null
@@ -1,22 +0,0 @@
-AM_CPPFLAGS = \
-	-D__BUILDING_CVC4LIB \
-	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
-
-noinst_LTLIBRARIES = libbooleans.la
-
-libbooleans_la_SOURCES = \
-	type_enumerator.h \
-	theory_bool.h \
-	theory_bool.cpp \
-	theory_bool_type_rules.h \
-	theory_bool_rewriter.h \
-	theory_bool_rewriter.cpp \
-	circuit_propagator.h \
-	circuit_propagator.cpp \
-	boolean_term_conversion_mode.h \
-	boolean_term_conversion_mode.cpp
-
-EXTRA_DIST = \
-	kinds \
-	options_handlers.h
diff --git a/src/theory/builtin/Makefile b/src/theory/builtin/Makefile
deleted file mode 100644
index 1dfd8a113..000000000
--- a/src/theory/builtin/Makefile
+++ /dev/null
@@ -1,4 +0,0 @@
-topdir = ../../..
-srcdir = src/theory/builtin
-
-include $(topdir)/Makefile.subdir
diff --git a/src/theory/builtin/Makefile.am b/src/theory/builtin/Makefile.am
deleted file mode 100644
index 6ff00feb6..000000000
--- a/src/theory/builtin/Makefile.am
+++ /dev/null
@@ -1,17 +0,0 @@
-AM_CPPFLAGS = \
-	-D__BUILDING_CVC4LIB \
-	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
-
-noinst_LTLIBRARIES = libbuiltin.la
-
-libbuiltin_la_SOURCES = \
-	theory_builtin_type_rules.h \
-	type_enumerator.h \
-	theory_builtin_rewriter.h \
-	theory_builtin_rewriter.cpp \
-	theory_builtin.h \
-	theory_builtin.cpp
-
-EXTRA_DIST = \
-	kinds
diff --git a/src/theory/bv/Makefile b/src/theory/bv/Makefile
deleted file mode 100644
index 797408368..000000000
--- a/src/theory/bv/Makefile
+++ /dev/null
@@ -1,4 +0,0 @@
-topdir = ../../..
-srcdir = src/theory/bv
-
-include $(topdir)/Makefile.subdir
diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am
deleted file mode 100644
index 8651f280b..000000000
--- a/src/theory/bv/Makefile.am
+++ /dev/null
@@ -1,44 +0,0 @@
-AM_CPPFLAGS = \
-	-D__BUILDING_CVC4LIB \
-	-D __STDC_LIMIT_MACROS \
-	-D __STDC_FORMAT_MACROS \
-	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
-
-noinst_LTLIBRARIES = libbv.la
-
-libbv_la_SOURCES = \
-	theory_bv_utils.h \
-	type_enumerator.h \
-	bitblaster.h \
-	bitblaster.cpp \
-	bv_to_bool.h \
-	bv_to_bool.cpp \
-	bv_subtheory.h \
-	bv_subtheory_core.h \
-	bv_subtheory_core.cpp \
-	bv_subtheory_bitblast.h \
-	bv_subtheory_bitblast.cpp \
-	bv_subtheory_inequality.h \
-	bv_subtheory_inequality.cpp \
-	bv_inequality_graph.h \
-	bv_inequality_graph.cpp \
-	bitblast_strategies.h \
-	bitblast_strategies.cpp \
-	slicer.h \
-	slicer.cpp \
-	theory_bv.h \
-	theory_bv.cpp \
-	theory_bv_rewrite_rules.h \
-	theory_bv_rewrite_rules_core.h \
-	theory_bv_rewrite_rules_operator_elimination.h \
-	theory_bv_rewrite_rules_constant_evaluation.h \
-	theory_bv_rewrite_rules_normalization.h \
-	theory_bv_rewrite_rules_simplification.h \
-	theory_bv_type_rules.h \
-	theory_bv_rewriter.h \
-	theory_bv_rewriter.cpp \
-	cd_set_collection.h
-
-EXTRA_DIST = \
-	kinds
diff --git a/src/theory/datatypes/Makefile b/src/theory/datatypes/Makefile
deleted file mode 100644
index cb3da4be3..000000000
--- a/src/theory/datatypes/Makefile
+++ /dev/null
@@ -1,4 +0,0 @@
-topdir = ../../..
-srcdir = src/theory/datatypes
-
-include $(topdir)/Makefile.subdir
diff --git a/src/theory/datatypes/Makefile.am b/src/theory/datatypes/Makefile.am
deleted file mode 100644
index 8b788b73b..000000000
--- a/src/theory/datatypes/Makefile.am
+++ /dev/null
@@ -1,16 +0,0 @@
-AM_CPPFLAGS = \
-	-D__BUILDING_CVC4LIB \
-	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
-
-noinst_LTLIBRARIES = libdatatypes.la
-
-libdatatypes_la_SOURCES = \
-	theory_datatypes_type_rules.h \
-	type_enumerator.h \
-	theory_datatypes.h \
-	datatypes_rewriter.h \
-	theory_datatypes.cpp 
-	
-EXTRA_DIST = \
-	kinds
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 0bbef1601..37a656555 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -22,6 +22,7 @@
 #include "theory/rewriter.h"
 #include "theory/datatypes/options.h"
 #include "theory/type_enumerator.h"
+#include "expr/node_manager_attributes.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index d3efc636f..527d110e0 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -20,7 +20,7 @@
 #define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
 
 #include "util/matcher.h"
-#include "expr/attribute.h"
+//#include "expr/attribute.h"
 
 namespace CVC4 {
 
diff --git a/src/theory/example/Makefile b/src/theory/example/Makefile
deleted file mode 100644
index be6721f80..000000000
--- a/src/theory/example/Makefile
+++ /dev/null
@@ -1,4 +0,0 @@
-topdir = ../../..
-srcdir = src/theory/example
-
-include $(topdir)/Makefile.subdir
diff --git a/src/theory/example/Makefile.am b/src/theory/example/Makefile.am
deleted file mode 100644
index 801a048a8..000000000
--- a/src/theory/example/Makefile.am
+++ /dev/null
@@ -1,14 +0,0 @@
-AM_CPPFLAGS = \
-	-D__BUILDING_CVC4LIB \
-	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
-
-noinst_LTLIBRARIES = libexample.la
-
-libexample_la_SOURCES = \
-	ecdata.h \
-	ecdata.cpp \
-	theory_uf_tim.h \
-	theory_uf_tim.cpp
-
-EXTRA_DIST =
diff --git a/src/theory/idl/Makefile b/src/theory/idl/Makefile
deleted file mode 100644
index 75ae33c7e..000000000
--- a/src/theory/idl/Makefile
+++ /dev/null
@@ -1,4 +0,0 @@
-topdir = ../../..
-srcdir = src/theory/idl
-
-include $(topdir)/Makefile.subdir
diff --git a/src/theory/idl/Makefile.am b/src/theory/idl/Makefile.am
deleted file mode 100644
index 4297e3bdb..000000000
--- a/src/theory/idl/Makefile.am
+++ /dev/null
@@ -1,19 +0,0 @@
-AM_CPPFLAGS = \
-	-D__BUILDING_CVC4LIB \
-	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
-
-noinst_LTLIBRARIES = libidl.la
-
-libidl_la_SOURCES = \
-	idl_model.h \
-	idl_model.cpp \
-	idl_assertion.h \
-	idl_assertion.cpp \
-	idl_assertion_db.h \
-	idl_assertion_db.cpp \
-	theory_idl.h \
-	theory_idl.cpp
-
-EXTRA_DIST = \
-	kinds 
diff --git a/src/theory/quantifiers/Makefile b/src/theory/quantifiers/Makefile
deleted file mode 100644
index 8ffdfb575..000000000
--- a/src/theory/quantifiers/Makefile
+++ /dev/null
@@ -1,4 +0,0 @@
-topdir = ../../..
-srcdir = src/theory/quantifiers
-
-include $(topdir)/Makefile.subdir
diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
deleted file mode 100644
index be24d6c67..000000000
--- a/src/theory/quantifiers/Makefile.am
+++ /dev/null
@@ -1,62 +0,0 @@
-AM_CPPFLAGS = \
-	-D__BUILDING_CVC4LIB \
-	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
-
-noinst_LTLIBRARIES = libquantifiers.la
-
-libquantifiers_la_SOURCES = \
-	theory_quantifiers_type_rules.h \
-	theory_quantifiers.h \
-	quantifiers_rewriter.h \
-	quantifiers_rewriter.cpp \
-	theory_quantifiers.cpp \
-	instantiation_engine.h \
-	instantiation_engine.cpp \
-	trigger.h \
-	trigger.cpp \
-	candidate_generator.h \
-	candidate_generator.cpp \
-	inst_match.h \
-	inst_match.cpp \
-	model_engine.h \
-	model_engine.cpp \
-	modes.cpp \
-	modes.h \
-	term_database.h \
-	term_database.cpp \
-	first_order_model.h \
-	first_order_model.cpp \
-	model_builder.h \
-	model_builder.cpp \
-	quantifiers_attributes.h \
-	quantifiers_attributes.cpp \
-	inst_gen.h \
-	inst_gen.cpp \
-	quant_util.h \
-	quant_util.cpp \
-	inst_match_generator.h \
-	inst_match_generator.cpp \
-	macros.h \
-	macros.cpp \
-	inst_strategy_e_matching.h \
-	inst_strategy_e_matching.cpp \
-	inst_strategy_cbqi.h \
-	inst_strategy_cbqi.cpp \
-	full_model_check.h \
-	full_model_check.cpp \
-	bounded_integers.h \
-	bounded_integers.cpp \
-	first_order_reasoning.h \
-	first_order_reasoning.cpp \
-	rewrite_engine.h \
-	rewrite_engine.cpp \
-	relevant_domain.h \
-	relevant_domain.cpp \
-	symmetry_breaking.h \
-	symmetry_breaking.cpp
-
-
-EXTRA_DIST = \
-	kinds \
-	options_handlers.h
diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h
index 05461d378..7f6855fea 100755
--- a/src/theory/quantifiers/symmetry_breaking.h
+++ b/src/theory/quantifiers/symmetry_breaking.h
@@ -29,6 +29,7 @@
 #include "util/sort_inference.h"
 #include "context/context.h"
 #include "context/context_mm.h"
+#include "context/cdhashmap.h"
 #include "context/cdchunk_list.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 1688479f3..177d8b230 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -17,6 +17,7 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
 #define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
 
+#include "expr/attribute.h"
 #include "theory/theory.h"
 
 #include <map>
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index fb599e2a0..8ebde136d 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -19,6 +19,7 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
 #define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
 
+#include "context/cdhashmap.h"
 #include "theory/theory.h"
 #include "util/hash.h"
 #include "util/statistics_registry.h"
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index 4245ad6f9..e05d97c05 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -19,7 +19,7 @@
 #pragma once
 
 #include "expr/node.h"
-#include "expr/attribute.h"
+//#include "expr/attribute.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/rewriter_attributes.h b/src/theory/rewriter_attributes.h
index 45e83aa63..4c4e33fc6 100644
--- a/src/theory/rewriter_attributes.h
+++ b/src/theory/rewriter_attributes.h
@@ -18,6 +18,8 @@
 
 #pragma once
 
+#include "expr/attribute.h"
+
 namespace CVC4 {
 namespace theory {
 
diff --git a/src/theory/rewriterules/Makefile b/src/theory/rewriterules/Makefile
deleted file mode 100644
index 4b1d4fc55..000000000
--- a/src/theory/rewriterules/Makefile
+++ /dev/null
@@ -1,4 +0,0 @@
-topdir = ../../..
-srcdir = src/theory/rewriterules
-
-include $(topdir)/Makefile.subdir
diff --git a/src/theory/rewriterules/Makefile.am b/src/theory/rewriterules/Makefile.am
deleted file mode 100644
index a1e5771b9..000000000
--- a/src/theory/rewriterules/Makefile.am
+++ /dev/null
@@ -1,28 +0,0 @@
-AM_CPPFLAGS = \
-	-D__BUILDING_CVC4LIB \
-	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
-
-noinst_LTLIBRARIES = librewriterules.la
-
-librewriterules_la_SOURCES = \
-	theory_rewriterules_rules.h \
-	theory_rewriterules_rules.cpp \
-	theory_rewriterules.h \
-	theory_rewriterules.cpp \
-	theory_rewriterules_rewriter.h \
-	theory_rewriterules_type_rules.h \
-	theory_rewriterules_preprocess.h \
-	theory_rewriterules_params.h \
-	rr_inst_match.h \
-	rr_inst_match_impl.h \
-	rr_inst_match.cpp \
-	rr_trigger.h \
-	rr_trigger.cpp \
-	rr_candidate_generator.h \
-	rr_candidate_generator.cpp \
-	efficient_e_matching.h \
-	efficient_e_matching.cpp
-
-EXTRA_DIST = \
-	kinds
diff --git a/src/theory/strings/Makefile b/src/theory/strings/Makefile
deleted file mode 100644
index e92c24ab7..000000000
--- a/src/theory/strings/Makefile
+++ /dev/null
@@ -1,4 +0,0 @@
-topdir = ../../..
-srcdir = src/theory/strings
-
-include $(topdir)/Makefile.subdir
diff --git a/src/theory/strings/Makefile.am b/src/theory/strings/Makefile.am
deleted file mode 100644
index d5e5d1a23..000000000
--- a/src/theory/strings/Makefile.am
+++ /dev/null
@@ -1,21 +0,0 @@
-AM_CPPFLAGS = \
-	-D__BUILDING_CVC4LIB \
-	-I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
-AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
-
-noinst_LTLIBRARIES = libstrings.la
-
-libstrings_la_SOURCES = \
-	theory_strings.h \
-	theory_strings.cpp \
-	theory_strings_rewriter.h \
-	theory_strings_rewriter.cpp \
-	theory_strings_type_rules.h \
-	type_enumerator.h \
-	theory_strings_preprocess.h \
-	theory_strings_preprocess.cpp \
-	regexp_operation.h \
-	regexp_operation.cpp
-
-EXTRA_DIST = \
-	kinds
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 21a5aacf5..fdd2d0518 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -20,7 +20,7 @@
 #define __CVC4__THEORY__THEORY_H
 
 #include "expr/node.h"
-#include "expr/attribute.h"
+//#include "expr/attribute.h"
 #include "expr/command.h"
 #include "theory/valuation.h"
 #include "theory/output_channel.h"
diff --git a/src/theory/uf/Makefile b/src/theory/uf/Makefile
deleted file mode 100644
index c3c641384..000000000
--- a/src/theory/uf/Makefile
+++ /dev/null
@@ -1,4 +0,0 @@
-topdir = ../../..
-srcdir = src/theory/uf
-
-include $(topdir)/Makefile.subdir
diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am
deleted file mode 100644
index 50c508092..000000000
--- a/src/theory/uf/Makefile.am
+++ /dev/null
@@ -1,25 +0,0 @@
-AM_CPPFLAGS = \
-	-D__BUILDING_CVC4LIB \
-	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
-
-noinst_LTLIBRARIES = libuf.la
-
-libuf_la_SOURCES = \
-	theory_uf.h \
-	theory_uf.cpp \
-	theory_uf_type_rules.h \
-	theory_uf_rewriter.h \
-	equality_engine.h \
-	equality_engine_types.h \
-	equality_engine.cpp \
-	symmetry_breaker.h \
-	symmetry_breaker.cpp \
-	theory_uf_strong_solver.h \
-	theory_uf_strong_solver.cpp \
-	theory_uf_model.h \
-	theory_uf_model.cpp 
-
-EXTRA_DIST = \
-	kinds \
-	options_handlers.h
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 8d1b6f1d9..a9294dc69 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -27,6 +27,7 @@
 #include "expr/node.h"
 #include "expr/kind_map.h"
 #include "context/cdo.h"
+#include "context/cdhashmap.h"
 #include "util/output.h"
 #include "util/statistics_registry.h"
 #include "theory/rewriter.h"
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 9ca146bde..2c9b4b7d5 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -21,7 +21,7 @@
 #define __CVC4__THEORY__UF__THEORY_UF_H
 
 #include "expr/node.h"
-#include "expr/attribute.h"
+//#include "expr/attribute.h"
 
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index 284212ba9..bf41a256d 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -12,6 +12,7 @@
  ** \brief Implementation of Theory UF Model
  **/
 
+#include "expr/attribute.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/theory_uf_model.h"
 #include "theory/uf/equality_engine.h"
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 9111ec6a7..079a03c36 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -21,6 +21,7 @@
 
 #include "context/context.h"
 #include "context/context_mm.h"
+#include "context/cdhashmap.h"
 #include "context/cdchunk_list.h"
 
 #include "util/statistics_registry.h"