Merge from cudd branch. This mostly just adds support for linking

against cudd libraries, the propositional_query class (in util/),
which uses cudd if it's available (and otherwise answers UNKNOWN for
all queries), and the arith theory support for it (currently disabled
per Tim's request, so he can clean it up).

Other changes include:

* contrib/debug-keys - script to print all used keys under Debug(), Trace()
* test/regress/run_regression - minor fix (don't export a variable)
* configure.ac - replace a comment removed by dejan's google perf commit
* some minor copyright/documentation updates, and minor changes to source
  text to make 'clang --analyze' happy.

1 files changed, 4 insertions, 4 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 273b2322a..fe5e55ae6 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -530,7 +530,7 @@ Result SmtEngine::query(const BoolExpr& e) {
   d_queryMade = true;
   ensureBoolean(e);// ensure expr is type-checked at this point
   internalPush();
-  SmtEnginePrivate::addFormula(*this, e.getNode().notNode());
+  smt::SmtEnginePrivate::addFormula(*this, e.getNode().notNode());
   Result r = check().asValidityResult();
   internalPop();
   d_status = r;
@@ -547,7 +547,7 @@ Result SmtEngine::assertFormula(const BoolExpr& e) {
   if(d_assertionList != NULL) {
     d_assertionList->push_back(e);
   }
-  SmtEnginePrivate::addFormula(*this, e.getNode());
+  smt::SmtEnginePrivate::addFormula(*this, e.getNode());
   return quickCheck().asValidityResult();
 }
 
@@ -589,7 +589,7 @@ Expr SmtEngine::getValue(const Expr& e)
 
   NodeManagerScope nms(d_nodeManager);
   Node eNode = e.getNode();
-  Node n = SmtEnginePrivate::preprocess(*this, eNode);
+  Node n = smt::SmtEnginePrivate::preprocess(*this, eNode);
 
   Debug("smt") << "--- getting value of " << n << endl;
   Node resultNode = d_theoryEngine->getValue(n);
@@ -655,7 +655,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
       ++i) {
     Assert((*i).getType() == boolType);
 
-    Node n = SmtEnginePrivate::preprocess(*this, *i);
+    Node n = smt::SmtEnginePrivate::preprocess(*this, *i);
 
     Debug("smt") << "--- getting value of " << n << endl;
     Node resultNode = d_theoryEngine->getValue(n);