Add Valuation::getSatValue() so that theories can access the current
authorMorgan Deters <mdeters@gmail.com>
Wed, 30 Mar 2011 03:59:05 +0000 (03:59 +0000)
committerMorgan Deters <mdeters@gmail.com>
Wed, 30 Mar 2011 03:59:05 +0000 (03:59 +0000)
commit10cabf82a20258da80be53eb6d23b1a536e82eb5
treed8262298ed5fba5a3c51681cc5739551747f7a90
parentd35d086268fa2a3d9b3c387157e4c54f1b967e0e
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())
16 files changed:
contrib/update-copyright.pl
src/expr/attribute_internals.h
src/lib/clock_gettime.h
src/main/interactive_shell.cpp
src/prop/minisat/core/Solver.cc
src/prop/prop_engine.cpp
src/theory/theory_engine.h
src/theory/theory_traits_template.h
src/theory/valuation.cpp
src/theory/valuation.h
src/util/output.cpp
src/util/output.h
test/regress/regress0/Makefile.am
test/regress/regress0/uf20-03.tim.cvc [new file with mode: 0644]
test/unit/expr/attribute_white.h
test/unit/util/output_black.h