Flatten libcvc4 build structure; remove some #include interdependences

5 files changed, 59 insertions, 40 deletions

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;
   }