* test/unit/context/context_black.h: Test CDList<>. In particular,

  test behavior of grow(), which was previously very broken, fixed by
  Tim earlier this afternoon.

* add the notion of a "private header".  Private header files (those
  not intended for distribution) should now #include "cvc4_private.h"
  (or "cvc4parser_private.h" for the parser code).  When not actually
  building libcvc4 (resp. libcvc4parser), or associated unit tests, a
  warning is emitted by the preprocessor.  This should make it easier
  to notice (and disentangle early) any unwanted public/private
  mixing.  Currently the warning identifies a couple places where we
  need to fix things.

* added directory infrastructure for arrays and BV theories.

* the Theory inheritance hierarchy makes some assumptions about the
  way inheritance is done.  These are checked at runtime when
  CVC4_ASSERTIONS is on.  See src/theory/theory.h's TheoryImpl<>
  definition for details.

* src/theory/booleans/theory_bool.h, src/theory/booleans/theory_def.h,
  src/theory/arith/theory_arith.h, src/theory/arith/theory_def.h,
  src/theory/uf/theory_uf.h, src/theory/uf/theory_def.h,
  src/parser/antlr_parser.h: minor code formatting fixes as per
  policy.

* src/theory/uf/theory_uf.cpp: fix for non-debug builds.

* src/util/options.h, src/util/model.h, src/util/result.h,
  src/expr/type.h: make CVC4_PUBLIC.

* src/util/decision_engine.h: no longer CVC4_PUBLIC.

* src/expr/expr_manager.cpp: ExprManager::booleanType() and
  ExprManager::kindType() weren't returning a value ?!  Fixed.

* src/expr/expr_manager.h, src/expr/node_manager.h: ExprManager no
  longer depends on NodeManager (public/private interface mixing).
  ExprManagerScope is an internal implementation detail, and is moved
  to node_manager.h.

* src/expr/node.h: mark gdb debug routines as "used" so that GCC
  always emits code for them (even though its static analysis shows
  they're unused).

7 files changed, 14 insertions, 1 deletions

diff --git a/src/prop/cnf_conversion.h b/src/prop/cnf_conversion.h
index 4ddfd3c06..d66e721db 100644
--- a/src/prop/cnf_conversion.h
+++ b/src/prop/cnf_conversion.h
@@ -13,6 +13,8 @@
  ** A type for describing possible CNF conversions.
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__CNF_CONVERSION_H
 #define __CVC4__CNF_CONVERSION_H
 
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 83a6aa68f..da3f7b1ed 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -19,10 +19,11 @@
  ** internals such as the representation and translation of 
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__CNF_STREAM_H
 #define __CVC4__CNF_STREAM_H
 
-
 #include "expr/node.h"
 #include "prop/sat.h"
 
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 5e51e5f5a..44499246e 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__PROP__MINISAT__SOLVER_H
 #define __CVC4__PROP__MINISAT__SOLVER_H
 
diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index 8860693e6..fd6a78ab0 100644
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__PROP__MINISAT__SOLVERTYPES_H
 #define __CVC4__PROP__MINISAT__SOLVERTYPES_H
 
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index f9e9b0387..223b21998 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__PROP__MINISAT__SIMP_SOLVER_H
 #define __CVC4__PROP__MINISAT__SIMP_SOLVER_H
 
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 4ea5e3b78..f57161fde 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -14,6 +14,8 @@
  ** between CVC4's SMT infrastructure and the SAT solver.
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__PROP_ENGINE_H
 #define __CVC4__PROP_ENGINE_H
 
diff --git a/src/prop/sat.h b/src/prop/sat.h
index a9696162a..65752f20b 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -13,6 +13,8 @@
  ** SAT Solver.
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__PROP__SAT_H
 #define __CVC4__PROP__SAT_H