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, 228 insertions, 0 deletions

diff --git a/src/util/propositional_query.cpp b/src/util/propositional_query.cpp
new file mode 100644
index 000000000..067896922
--- /dev/null
+++ b/src/util/propositional_query.cpp
@@ -0,0 +1,228 @@
+/*********************                                                        */
+/*! \file propositional_query.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A class for simple, quick, propositional
+ ** satisfiability/validity checking
+ **
+ ** PropositionalQuery is a way for parts of CVC4 to do quick purely
+ ** propositional satisfiability or validity checks on a Node.  These
+ ** checks do no theory reasoning, and handle atoms as propositional
+ ** variables, but can sometimes be useful for subqueries.
+ **/
+
+#include "util/propositional_query.h"
+
+#include <map>
+#include <algorithm>
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+
+#ifdef CVC4_CUDD
+
+#include <util.h>
+#include <cudd.h>
+#include <cuddObj.hh>
+
+namespace CVC4 {
+
+class BddInstance {
+private:
+  Cudd d_mgr;
+  typedef std::map<Node, BDD> AtomToIDMap;
+  AtomToIDMap d_atomToBddMap;
+
+  unsigned d_atomId;
+
+  BDD encodeNode(TNode t);
+  BDD encodeAtom(TNode t);
+  BDD encodeCombinator(TNode t);
+
+  bool isAnAtom(TNode t) {
+    switch(t.getKind()) {
+    case NOT:
+    case XOR:
+    case IFF:
+    case IMPLIES:
+    case OR:
+    case AND:
+      return false;
+    case ITE:
+      return t.getType().isBoolean();
+    default:
+      return true;
+    }
+  }
+
+  void setupAtoms(TNode t);
+
+  void clear() {
+    d_atomId = 0;
+    d_atomToBddMap.clear();
+  }
+
+  Result d_result;
+
+public:
+  static const unsigned MAX_VARIABLES = 20;
+
+  BddInstance(TNode t) : d_atomToBddMap(), d_atomId(0) {
+    setupAtoms(t);
+
+    Debug("bdd::sat") << t << endl;
+    Debug("bdd::sat") << d_atomToBddMap.size() << endl;
+
+
+    if(d_atomToBddMap.size() > MAX_VARIABLES) {
+      d_result = Result(Result::SAT_UNKNOWN, Result::TIMEOUT);
+    } else {
+      BDD res = encodeNode(t);
+      BDD falseBdd = d_mgr.bddZero();
+      bool isUnsat = (res == falseBdd);
+
+      clear();
+
+      if(isUnsat) {
+        d_result = Result::UNSAT;
+      } else {
+        d_result = Result::SAT;
+      }
+    }
+  }
+
+  Result getResult() const { return d_result; }
+
+};/* class BddInstance */
+
+}/* CVC4 namespace */
+
+BDD BddInstance::encodeNode(TNode t) {
+  if(isAnAtom(t)) {
+    return encodeAtom(t);
+  } else {
+    return encodeCombinator(t);
+  }
+}
+
+BDD BddInstance::encodeCombinator(TNode t) {
+  switch(t.getKind()) {
+  case XOR: {
+    Assert(t.getNumChildren() == 2);
+    return encodeNode(t[0]).Xor(encodeNode(t[1]));
+  }
+
+  case IFF: {
+    Assert(t.getNumChildren() == 2);
+    BDD left = encodeNode(t[0]);
+    BDD right = encodeNode(t[1]);
+    return (!left | right) & (left | !right);
+  }
+
+  case IMPLIES: {
+    Assert(t.getNumChildren() == 2);
+    BDD left = encodeNode(t[0]);
+    BDD right = encodeNode(t[1]);
+    return (!left | right);
+  }
+
+  case AND:
+  case OR: {
+    Assert(t.getNumChildren() >= 2);
+    TNode::iterator i = t.begin(), end = t.end();
+    BDD tmp = encodeNode(*i);
+    ++i;
+    for(; i != end; ++i) {
+      BDD curr = encodeNode(*i);
+      if(t.getKind() == AND) {
+        tmp = tmp & curr;
+      } else {
+        tmp = tmp | curr;
+      }
+    }
+    return tmp;
+  }
+
+  case ITE: {
+    Assert(t.getType().isBoolean());
+    BDD cnd = encodeNode(t[0]);
+    BDD thenBranch = encodeNode(t[1]);
+    BDD elseBranch = encodeNode(t[2]);
+    return cnd.Ite(thenBranch, elseBranch);
+  }
+
+  case NOT:
+    return ! encodeNode(t[0]);
+
+  default:
+    Unhandled(t.getKind());
+  }
+}
+
+BDD BddInstance::encodeAtom(TNode t) {
+  if(t.getKind() == kind::CONST_BOOLEAN) {
+    if(t.getConst<bool>()) {
+      return d_mgr.bddOne();
+    } else {
+      return d_mgr.bddZero();
+    }
+  }
+  Assert(t.getKind() != kind::CONST_BOOLEAN);
+
+  AtomToIDMap::iterator findT = d_atomToBddMap.find(t);
+
+  Assert(d_atomToBddMap.find(t) != d_atomToBddMap.end());
+  return findT->second;
+}
+
+void BddInstance::setupAtoms(TNode t) {
+  if(t.getKind() == kind::CONST_BOOLEAN) {
+    // do nothing
+  } else if(isAnAtom(t)) {
+    AtomToIDMap::iterator findT = d_atomToBddMap.find(t);
+    if(findT == d_atomToBddMap.end()) {
+      BDD var = d_mgr.bddVar();
+      d_atomToBddMap.insert(make_pair(t, var));
+      d_atomId++;
+    }
+  } else {
+    for(TNode::iterator i = t.begin(), end = t.end(); i != end; ++i) {
+      setupAtoms(*i);
+    }
+  }
+}
+
+Result PropositionalQuery::isSatisfiable(TNode q) {
+  BddInstance instance(q);
+  return instance.getResult();
+}
+
+Result PropositionalQuery::isTautology(TNode q) {
+  Node negQ = q.notNode();
+  Result satResult = isSatisfiable(negQ);
+  return satResult.asValidityResult();
+}
+
+#else /* CVC4_CUDD */
+
+// if CUDD wasn't available at build time, just return UNKNOWN everywhere.
+
+Result PropositionalQuery::isSatisfiable(TNode q) {
+  return Result(Result::SAT_UNKNOWN, Result::UNSUPPORTED);
+}
+
+Result PropositionalQuery::isTautology(TNode q) {
+  return Result(Result::VALIDITY_UNKNOWN, Result::UNSUPPORTED);
+}
+
+#endif /* CVC4_CUDD */