From 4375b60d5df794b2c6193f3892185ea181a0748d Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 30 Jun 2010 11:12:14 +0000 Subject: * theory "tree" rewriting implemented and works * added TheoryArith::preRewrite() to test and demonstrate the use of pre-rewriting. * array types and type checking now supported * array type checking now supported * theoryOf() dispatching properly to arrays now * theories now required to implement a (simple) identify() function that returns a string identifying them for debugging/user output purposes * added "builtin" theory to hold all built-in kinds and their type rules and rewriting (currently only exploding distinct) * fixed production build failure (regarding NodeSetDepth) * removed an errant "using namespace std" in util/bitvector.h (and made associated trivial fixes elsewhere) * fixes to make unexpected exceptions more verbose in debug builds * fixes to make multiple, cascading assertion fails simpler * minor other fixes to comments etc. --- src/util/bitvector.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/util/bitvector.h') diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 746d9aaaf..0febfddfd 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -17,6 +17,8 @@ ** \todo document this file **/ +#include "cvc4_public.h" + #ifndef __CVC4__BITVECTOR_H_ #define __CVC4__BITVECTOR_H_ @@ -25,8 +27,6 @@ #include "util/gmp_util.h" #include "util/integer.h" -using namespace std; - namespace CVC4 { class BitVector { -- cgit v1.2.3