* 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).

2 files changed, 48 insertions, 0 deletions

diff --git a/src/include/cvc4_private.h b/src/include/cvc4_private.h
new file mode 100644
index 000000000..df5dd4a0b
--- /dev/null
+++ b/src/include/cvc4_private.h
@@ -0,0 +1,24 @@
+/*********************                                                        */
+/** cvc4_private.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** #inclusion of this file marks a header as private and generates a
+ ** warning when the file is included improperly.
+ **/
+
+#ifndef __CVC4_PRIVATE_H
+#define __CVC4_PRIVATE_H
+
+#if ! (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST))
+#  warning A private CVC4 header was included when not building the library or private unit test code.
+#endif /* ! (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */
+
+#endif /* __CVC4_PRIVATE_H */
diff --git a/src/include/cvc4parser_private.h b/src/include/cvc4parser_private.h
new file mode 100644
index 000000000..72d942ef0
--- /dev/null
+++ b/src/include/cvc4parser_private.h
@@ -0,0 +1,24 @@
+/*********************                                                        */
+/** cvc4parser_private.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** #inclusion of this file marks a header as private and generates a
+ ** warning when the file is included improperly.
+ **/
+
+#ifndef __CVC4PARSER_PRIVATE_H
+#define __CVC4PARSER_PRIVATE_H
+
+#if ! (defined(__BUILDING_CVC4PARSERLIB) || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST))
+#  warning A private CVC4 parser header was included when not building the parser library or private unit test code.
+#endif /* ! (__BUILDING_CVC4PARSERLIB || __BUILDING_CVC4PARSERLIB_UNIT_TEST) */
+
+#endif /* __CVC4PARSER_PRIVATE_H */