From 14c22833d05f632eb40eb68cc3c68345d891005c Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 26 Feb 2010 21:44:42 +0000 Subject: * 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). --- src/prop/cnf_conversion.h | 2 ++ src/prop/cnf_stream.h | 3 ++- src/prop/minisat/core/Solver.h | 2 ++ src/prop/minisat/core/SolverTypes.h | 2 ++ src/prop/minisat/simp/SimpSolver.h | 2 ++ src/prop/prop_engine.h | 2 ++ src/prop/sat.h | 2 ++ 7 files changed, 14 insertions(+), 1 deletion(-) (limited to 'src/prop') 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 -- cgit v1.2.3