* test/unit/context/context_black.h: Test CDList<>. In particular,
authorMorgan Deters <mdeters@gmail.com>
Fri, 26 Feb 2010 21:44:42 +0000 (21:44 +0000)
committerMorgan Deters <mdeters@gmail.com>
Fri, 26 Feb 2010 21:44:42 +0000 (21:44 +0000)
commit14c22833d05f632eb40eb68cc3c68345d891005c
treec596c6e91442a3393611e88b10dec3871992a207
parent3311e8276fb6221d9e100be2b1eec88d8f119fef
* 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).
52 files changed:
src/context/context.h
src/context/context_mm.h
src/expr/attribute.h
src/expr/expr_manager.cpp
src/expr/expr_manager.h
src/expr/node.h
src/expr/node_builder.h
src/expr/node_manager.h
src/expr/node_value.h
src/expr/type.h
src/include/cvc4_private.h [new file with mode: 0644]
src/include/cvc4parser_private.h [new file with mode: 0644]
src/parser/antlr_parser.h
src/parser/symbol_table.h
src/prop/cnf_conversion.h
src/prop/cnf_stream.h
src/prop/minisat/core/Solver.h
src/prop/minisat/core/SolverTypes.h
src/prop/minisat/simp/SimpSolver.h
src/prop/prop_engine.h
src/prop/sat.h
src/smt/smt_engine.h
src/theory/Makefile.am
src/theory/arith/theory_arith.h
src/theory/arith/theory_def.h
src/theory/arrays/Makefile [new file with mode: 0644]
src/theory/arrays/Makefile.am [new file with mode: 0644]
src/theory/arrays/kinds [new file with mode: 0644]
src/theory/arrays/theory_arrays.h [new file with mode: 0644]
src/theory/arrays/theory_def.h [new file with mode: 0644]
src/theory/booleans/theory_bool.h
src/theory/booleans/theory_def.h
src/theory/bv/Makefile [new file with mode: 0644]
src/theory/bv/Makefile.am [new file with mode: 0644]
src/theory/bv/kinds [new file with mode: 0644]
src/theory/bv/theory_bv.h [new file with mode: 0644]
src/theory/bv/theory_def.h [new file with mode: 0644]
src/theory/output_channel.h
src/theory/theory.h
src/theory/theory_engine.h
src/theory/theoryof_table_prologue.h
src/theory/uf/ecdata.h
src/theory/uf/theory_def.h
src/theory/uf/theory_uf.cpp
src/theory/uf/theory_uf.h
src/util/decision_engine.h
src/util/model.h
src/util/options.h
src/util/result.h
src/util/unique_id.h
test/unit/Makefile.am
test/unit/context/context_black.h