This is a merge from the "theoryfixes+cdattrhash" branch. The changes

are somewhat disparate but belonged on the same branch because they were
held back from trunk all for the same reason (to keep the trunk stable
for furious bitvector development).  Dejan has now given me the go-ahead
for a merge.

=========================================
THIS COMMIT CHANGES THE THEORY INTERFACE!
=========================================

Theory constructors are expected to take an additional "Valuation*"
parameter that each Theory should send along to the base class
constructor.  The base class Theory keeps the Valuation* in a
d_valuation field for use by it and by its derived classes.
Theory::getValue() no longer takes a Valuation* (it is expected
to use d_valuation instead).  This allows other theory functions
to take advantage of getValue() for debugging or heuristic
purposes.

TODO BEFORE MERGE TO TRUNK:
****implement BitIterator find() in CDAttrHash<bool>.

Specifically:

* Added QF_BV support for SMT-LIB v2.
* Two adjustments to the theory interface as requested by Tim King:
  1. As described above.
  2. Theories now have const access to the fact queue through base
     class functions facts_begin() and facts_end(); useful for
     debugging.
* Added an "Asserted" attribute so that theories can check if something
  has been asserted or not (and therefore not propagate it).  However, this
  has been disabled for now, pending more data on the overhead of it, and
  pending discussion at the 3/25/2011 meeting.
* Do not define NDEBUG in MiniSat in assertion-enabled builds (so
  that MiniSat asserts are evaluated).
* As a result of the new MiniSat assertions, some --incremental
  regressions had to be disabled; also, some bitvectors ?!!
* Bug 71 is resolved by adding a specialization for CDAttrHash<> in the
  attribute package.
* Fixes for some warnings flagged by clang.
* System tests have arrived!  So far mainly infrastructure for having
  system tests, but there is a system test aimed at improving code
  coverage of the printer package.
* Minor other adjustments to documentation and coding to be more
  conformant to CVC4 policy.

Tests have been performed to demonstrate that these changes have no or
negligible effect on performance.  In particular, changing the
CDAttrHash<> doesn't have any real effect on performance or memory right
now, since there is only one context-dependent boolean flag (as soon
as another is added, the effect is noticeable but probably still slight).

1 files changed, 34 insertions, 12 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 620c70710..72341869d 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -23,6 +23,7 @@
 
 #include "expr/node.h"
 #include "expr/attribute.h"
+#include "theory/valuation.h"
 #include "theory/output_channel.h"
 #include "context/context.h"
 #include "context/cdlist.h"
@@ -37,10 +38,11 @@ namespace CVC4 {
 class TheoryEngine;
 
 namespace theory {
-  class Valuation;
-}/* CVC4::theory namespace */
 
-namespace theory {
+/** Tag for the "newFact()-has-been-called-in-this-context" flag on Nodes */
+struct AssertedAttrTag {};
+/** The "newFact()-has-been-called-in-this-context" flag on Nodes */
+typedef CVC4::expr::CDAttribute<AssertedAttrTag, bool> Asserted;
 
 /**
  * Base class for T-solvers.  Abstract DPLL(T).
@@ -88,16 +90,15 @@ protected:
   /**
    * Construct a Theory.
    */
-  Theory(TheoryId id, context::Context* ctxt, OutputChannel& out) throw() :
+  Theory(TheoryId id, context::Context* ctxt, OutputChannel& out, Valuation valuation) throw() :
     d_id(id),
     d_context(ctxt),
     d_facts(ctxt),
     d_factsHead(ctxt, 0),
-    d_out(&out) {
+    d_out(&out),
+    d_valuation(valuation) {
   }
 
-
-
   /**
    * This is called at shutdown time by the TheoryEngine, just before
    * destruction.  It is important because there are destruction
@@ -114,10 +115,11 @@ protected:
    */
   OutputChannel* d_out;
 
-  /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */
-  struct PreRegistered {};
-  /** The "preRegisterTerm()-has-been-called" flag on Nodes */
-  typedef CVC4::expr::Attribute<PreRegistered, bool> PreRegisteredAttr;
+  /**
+   * The valuation proxy for the Theory to communicate back with the
+   * theory engine (and other theories).
+   */
+  Valuation d_valuation;
 
   /**
    * Returns the next atom in the assertFact() queue.  Guarantees that
@@ -135,6 +137,26 @@ protected:
     return fact;
   }
 
+  /**
+   * Provides access to the facts queue, primarily intended for theory
+   * debugging purposes.
+   *
+   * @return the iterator to the beginning of the fact queue
+   */
+  context::CDList<Node>::const_iterator facts_begin() const {
+    return d_facts.begin();
+  }
+
+  /**
+   * Provides access to the facts queue, primarily intended for theory
+   * debugging purposes.
+   *
+   * @return the iterator to the end of the fact queue
+   */
+  context::CDList<Node>::const_iterator facts_end() const {
+    return d_facts.end();
+  }
+
 public:
 
   static inline TheoryId theoryOf(TypeNode typeNode) {
@@ -345,7 +367,7 @@ public:
    * and suspect this situation is the case, return Node::null()
    * rather than throwing an exception.
    */
-  virtual Node getValue(TNode n, Valuation* valuation) {
+  virtual Node getValue(TNode n) {
     Unimplemented("Theory %s doesn't support Theory::getValue interface",
                   identify().c_str());
     return Node::null();