Add Valuation::getSatValue() so that theories can access the current

(propositional) assignment for theory atoms.

Fixed Debug/Trace as discussed in bug ticket #252 and on the mailing list.
This implementation leads to some compiler warnings in production builds,
but these will be corrected in coming days.  There appears to be a small
speedup in the parser as a result of this fix:

  http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=1902&reference_id=1886&p=5

Cleaned up a few CD Boolean attribute things.

Various small fixes to coding guidelines / test coverage.

This commit:
* Resolves bug 252 (tracing not disabled in production builds)
* Resolves bug 254 (implement CDAttrHash<>::BitIterator::find())

2 files changed, 118 insertions, 0 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index c732ffbb2..83291eb5a 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -52,6 +52,7 @@ CVC_TESTS = \
 	test9.cvc \
 	test11.cvc \
 	uf20-03.cvc \
+	uf20-03.tim.cvc \
 	wiki.01.cvc \
 	wiki.02.cvc \
 	wiki.03.cvc \
diff --git a/test/regress/regress0/uf20-03.tim.cvc b/test/regress/regress0/uf20-03.tim.cvc
new file mode 100644
index 000000000..f13bdcce5
--- /dev/null
+++ b/test/regress/regress0/uf20-03.tim.cvc
@@ -0,0 +1,117 @@
+% COMMAND-LINE: --uf=tim
+% EXPECT: invalid
+x_1 : BOOLEAN;
+x_2 : BOOLEAN;
+x_3 : BOOLEAN;
+x_4 : BOOLEAN;
+x_5 : BOOLEAN;
+x_6 : BOOLEAN;
+x_7 : BOOLEAN;
+x_8 : BOOLEAN;
+x_9 : BOOLEAN;
+x_10 : BOOLEAN;
+x_11 : BOOLEAN;
+x_12 : BOOLEAN;
+x_13 : BOOLEAN;
+x_14 : BOOLEAN;
+x_15 : BOOLEAN;
+x_16 : BOOLEAN;
+x_17 : BOOLEAN;
+x_18 : BOOLEAN;
+x_19 : BOOLEAN;
+x_20 : BOOLEAN;
+ASSERT NOT x_9 OR x_3 OR NOT x_15;
+ASSERT NOT x_12 OR NOT x_4 OR NOT x_15;
+ASSERT x_6 OR x_14 OR NOT x_17;
+ASSERT x_10 OR x_16 OR x_11;
+ASSERT NOT x_15 OR x_20 OR NOT x_7;
+ASSERT NOT x_1 OR x_10 OR x_16;
+ASSERT x_13 OR x_17 OR NOT x_7;
+ASSERT NOT x_2 OR NOT x_14 OR NOT x_13;
+ASSERT x_13 OR NOT x_6 OR x_15;
+ASSERT NOT x_9 OR x_3 OR x_16;
+ASSERT NOT x_20 OR NOT x_13 OR x_4;
+ASSERT NOT x_7 OR x_15 OR NOT x_14;
+ASSERT NOT x_15 OR NOT x_16 OR x_6;
+ASSERT x_5 OR NOT x_18 OR x_20;
+ASSERT NOT x_16 OR NOT x_19 OR x_7;
+ASSERT x_20 OR NOT x_18 OR NOT x_2;
+ASSERT x_10 OR NOT x_19 OR NOT x_14;
+ASSERT x_16 OR NOT x_7 OR x_12;
+ASSERT x_6 OR NOT x_5 OR NOT x_1;
+ASSERT NOT x_9 OR x_11 OR x_15;
+ASSERT x_19 OR NOT x_6 OR x_7;
+ASSERT NOT x_11 OR x_17 OR NOT x_19;
+ASSERT x_9 OR NOT x_16 OR x_6;
+ASSERT x_15 OR NOT x_20 OR x_10;
+ASSERT x_9 OR NOT x_1 OR NOT x_11;
+ASSERT NOT x_8 OR NOT x_19 OR x_5;
+ASSERT NOT x_19 OR x_11 OR x_20;
+ASSERT NOT x_12 OR x_13 OR NOT x_3;
+ASSERT NOT x_7 OR NOT x_17 OR NOT x_19;
+ASSERT x_17 OR x_6 OR NOT x_11;
+ASSERT NOT x_7 OR NOT x_17 OR x_10;
+ASSERT NOT x_14 OR x_9 OR x_20;
+ASSERT x_1 OR NOT x_18 OR NOT x_16;
+ASSERT NOT x_2 OR NOT x_15 OR x_20;
+ASSERT x_14 OR x_18 OR NOT x_1;
+ASSERT NOT x_8 OR NOT x_4 OR x_1;
+ASSERT x_13 OR x_3 OR NOT x_9;
+ASSERT x_5 OR x_7 OR x_8;
+ASSERT x_9 OR x_4 OR NOT x_20;
+ASSERT NOT x_18 OR NOT x_15 OR NOT x_10;
+ASSERT x_10 OR x_3 OR NOT x_20;
+ASSERT x_20 OR NOT x_14 OR x_16;
+ASSERT x_20 OR NOT x_3 OR NOT x_11;
+ASSERT NOT x_12 OR x_19 OR NOT x_16;
+ASSERT NOT x_3 OR x_5 OR x_10;
+ASSERT x_8 OR x_13 OR NOT x_7;
+ASSERT NOT x_2 OR NOT x_15 OR x_10;
+ASSERT NOT x_3 OR x_9 OR x_16;
+ASSERT NOT x_12 OR NOT x_16 OR NOT x_18;
+ASSERT x_3 OR x_1 OR NOT x_12;
+ASSERT NOT x_18 OR x_13 OR x_5;
+ASSERT x_1 OR x_3 OR NOT x_19;
+ASSERT NOT x_19 OR NOT x_5 OR x_6;
+ASSERT NOT x_20 OR x_8 OR NOT x_2;
+ASSERT x_17 OR NOT x_8 OR NOT x_13;
+ASSERT x_7 OR NOT x_11 OR NOT x_12;
+ASSERT NOT x_10 OR NOT x_14 OR NOT x_20;
+ASSERT NOT x_1 OR x_16 OR NOT x_12;
+ASSERT x_5 OR NOT x_3 OR x_9;
+ASSERT NOT x_18 OR x_8 OR x_14;
+ASSERT x_1 OR x_16 OR x_12;
+ASSERT x_20 OR NOT x_1 OR NOT x_16;
+ASSERT x_5 OR x_10 OR NOT x_13;
+ASSERT x_9 OR NOT x_10 OR x_6;
+ASSERT NOT x_12 OR x_10 OR NOT x_14;
+ASSERT NOT x_13 OR x_1 OR x_4;
+ASSERT NOT x_20 OR NOT x_7 OR x_3;
+ASSERT x_12 OR x_1 OR NOT x_10;
+ASSERT NOT x_1 OR NOT x_16 OR x_7;
+ASSERT x_11 OR NOT x_6 OR NOT x_4;
+ASSERT x_1 OR x_16 OR NOT x_20;
+ASSERT x_9 OR x_7 OR x_15;
+ASSERT NOT x_6 OR x_17 OR x_10;
+ASSERT x_8 OR x_9 OR x_17;
+ASSERT x_18 OR x_11 OR x_10;
+ASSERT x_7 OR x_1 OR NOT x_8;
+ASSERT NOT x_5 OR NOT x_12 OR x_18;
+ASSERT NOT x_6 OR x_2 OR x_15;
+ASSERT x_2 OR x_18 OR x_1;
+ASSERT NOT x_7 OR NOT x_13 OR x_16;
+ASSERT x_18 OR x_19 OR x_9;
+ASSERT x_9 OR NOT x_14 OR x_18;
+ASSERT x_14 OR x_12 OR NOT x_5;
+ASSERT NOT x_13 OR NOT x_7 OR NOT x_14;
+ASSERT NOT x_1 OR x_8 OR NOT x_16;
+ASSERT NOT x_11 OR x_4 OR x_7;
+ASSERT NOT x_4 OR x_20 OR x_5;
+ASSERT NOT x_5 OR x_2 OR x_12;
+ASSERT NOT x_5 OR x_13 OR NOT x_18;
+ASSERT NOT x_18 OR x_9 OR x_1;
+ASSERT x_10 OR NOT x_11 OR x_16;
+
+
+QUERY FALSE;
+% EXIT: 10