diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-26 21:44:42 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-26 21:44:42 +0000 |
commit | 14c22833d05f632eb40eb68cc3c68345d891005c (patch) | |
tree | c596c6e91442a3393611e88b10dec3871992a207 /src/util | |
parent | 3311e8276fb6221d9e100be2b1eec88d8f119fef (diff) |
* 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).
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/decision_engine.h | 4 | ||||
-rw-r--r-- | src/util/model.h | 2 | ||||
-rw-r--r-- | src/util/options.h | 2 | ||||
-rw-r--r-- | src/util/result.h | 2 | ||||
-rw-r--r-- | src/util/unique_id.h | 2 |
5 files changed, 8 insertions, 4 deletions
diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h index 72943ee99..ac9fc5ffd 100644 --- a/src/util/decision_engine.h +++ b/src/util/decision_engine.h @@ -13,6 +13,8 @@ ** A decision engine for CVC4. **/ +#include "cvc4_private.h" + #ifndef __CVC4__DECISION_ENGINE_H #define __CVC4__DECISION_ENGINE_H @@ -27,7 +29,7 @@ namespace CVC4 { /** * A decision mechanism for the next decision. */ -class CVC4_PUBLIC DecisionEngine { +class DecisionEngine { public: /** * Destructor. diff --git a/src/util/model.h b/src/util/model.h index 65c919dd2..d2a51e447 100644 --- a/src/util/model.h +++ b/src/util/model.h @@ -18,7 +18,7 @@ namespace CVC4 { -class Model { +class CVC4_PUBLIC Model { };/* class Model */ }/* CVC4 namespace */ diff --git a/src/util/options.h b/src/util/options.h index 404700a85..d2b19a20b 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -22,7 +22,7 @@ namespace CVC4 { -struct Options { +struct CVC4_PUBLIC Options { std::string binary_name; diff --git a/src/util/result.h b/src/util/result.h index 49ba7c697..7557cece8 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -29,7 +29,7 @@ namespace CVC4 { /** * Three-valued, immutable SMT result, with optional explanation. */ -class Result { +class CVC4_PUBLIC Result { public: enum SAT { UNSAT = 0, diff --git a/src/util/unique_id.h b/src/util/unique_id.h index 244b8a5dd..54e56da96 100644 --- a/src/util/unique_id.h +++ b/src/util/unique_id.h @@ -13,6 +13,8 @@ ** A mechanism for getting a compile-time unique ID. **/ +#include "cvc4_private.h" + #ifndef __CVC4__UNIQUE_ID_H #define __CVC4__UNIQUE_ID_H |