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.

9 files changed, 326 insertions, 2 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 4f853b9e3..c94d208d2 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -3,7 +3,12 @@ AM_CPPFLAGS = \
 	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
-noinst_LTLIBRARIES = libutil.la
+noinst_LTLIBRARIES = libutil.la libutilcudd.la
+
+# libutilcudd.la is a separate library so that we can pass separate
+# compiler flags
+libutilcudd_la_CPPFLAGS = $(CPPFLAGS) $(AM_CPPFLAGS) @CUDD_CPPFLAGS@
+libutilcudd_la_LIBADD = @CUDD_LDFLAGS@
 
 libutil_la_SOURCES = \
 	Assert.h \
@@ -34,6 +39,11 @@ libutil_la_SOURCES = \
 	dynamic_array.h \
 	language.h \
 	triple.h
+libutil_la_LIBADD = \
+	@builddir@/libutilcudd.la
+libutilcudd_la_SOURCES = \
+	propositional_query.h \
+	propositional_query.cpp
 
 BUILT_SOURCES = \
 	rational.h \
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index 8cd824b0c..94ade5a52 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -96,6 +96,10 @@ bool Configuration::isBuiltWithCln() {
   return IS_CLN_BUILD;
 }
 
+bool Configuration::isBuiltWithCudd() {
+  return IS_CUDD_BUILD;
+}
+
 bool Configuration::isBuiltWithTlsSupport() {
   return USING_TLS;
 }
diff --git a/src/util/configuration.h b/src/util/configuration.h
index a9d59a7fe..150354c29 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -71,6 +71,8 @@ public:
 
   static bool isBuiltWithCln();
 
+  static bool isBuiltWithCudd();
+
   static bool isBuiltWithTlsSupport();
 };
 
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index 56423e7d5..c0ce86c97 100644
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -70,6 +70,12 @@ namespace CVC4 {
 #  define IS_COMPETITION_BUILD false
 #endif /* CVC4_COMPETITION_MODE */
 
+#ifdef CVC4_CUDD
+#  define IS_CUDD_BUILD true
+#else /* CVC4_CUDD */
+#  define IS_CUDD_BUILD false
+#endif /* CVC4_CUDD */
+
 #ifdef CVC4_GMP_IMP
 #  define IS_GMP_BUILD true
 #else /* CVC4_GMP_IMP */
@@ -90,7 +96,7 @@ namespace CVC4 {
 
 #define CVC4_ABOUT_STRING string("\
 This is CVC4 version " CVC4_RELEASE_STRING "\n\n\
-Copyright (C) 2009, 2010\n\
+Copyright (C) 2009, 2010, 2011\n\
   The ACSys Group\n\
   Courant Institute of Mathematical Sciences\n\
   New York University\n\
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 0c3915d1d..6fc71bae3 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -416,6 +416,11 @@ throw(OptionException) {
       printf("coverage   : %s\n", Configuration::isCoverageBuild() ? "yes" : "no");
       printf("profiling  : %s\n", Configuration::isProfilingBuild() ? "yes" : "no");
       printf("competition: %s\n", Configuration::isCompetitionBuild() ? "yes" : "no");
+      printf("\n");
+      printf("cudd       : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no");
+      printf("cln        : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no");
+      printf("gmp        : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no");
+      printf("tls        : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no");
       exit(0);
 
     case '?':
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 */
diff --git a/src/util/propositional_query.h b/src/util/propositional_query.h
new file mode 100644
index 000000000..f520f142d
--- /dev/null
+++ b/src/util/propositional_query.h
@@ -0,0 +1,66 @@
+/*********************                                                        */
+/*! \file propositional_query.h
+ ** \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 "cvc4_private.h"
+
+#ifndef __CVC4__PROPOSITIONAL_QUERY_H
+#define __CVC4__PROPOSITIONAL_QUERY_H
+
+#include "expr/node.h"
+#include "util/result.h"
+
+namespace CVC4 {
+
+/**
+ * PropositionalQuery is a way for parts of CVC4 to do quick purely
+ * propositional satisfiability or validity checks on a Node.
+ */
+class PropositionalQuery {
+public:
+
+  /**
+   * Returns whether a node q is propositionally satisfiable.
+   *
+   * @params q Node to be checked for satisfiability.
+   * @params e A number representing the effort to use between 0 (minimum effort),
+   *  and 1 (maximum effort).
+   * @precondition q is a ground formula.
+   * @precondition effort is between 0 and 1.
+   */
+  static Result isSatisfiable(TNode q);
+
+  /**
+   * Returns whether a node q is a propositional tautology.
+   *
+   * @params q Node to be checked for satisfiability.
+   * @params e A number representing the effort to use between 0 (minimum effort),
+   *  and 1 (maximum effort).
+   * @precondition q is a ground formula.
+   * @precondition effort is between 0 and 1.
+   */
+  static Result isTautology(TNode q);
+
+};/* class PropositionalQuery */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PROPOSITIONAL_QUERY_H */
diff --git a/src/util/result.h b/src/util/result.h
index 1e0729332..7da1dc0b7 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -61,6 +61,7 @@ public:
     TIMEOUT,
     MEMOUT,
     NO_STATUS,
+    UNSUPPORTED,
     OTHER,
     UNKNOWN_REASON
   };
diff --git a/src/util/stats.h b/src/util/stats.h
index 4dbf31120..a78070de4 100644
--- a/src/util/stats.h
+++ b/src/util/stats.h
@@ -43,6 +43,8 @@ namespace CVC4 {
 
 class CVC4_PUBLIC Stat;
 
+inline std::ostream& operator<<(std::ostream& os, const ::timespec& t);
+
 /**
  * The main statistics registry.  This registry maintains the list of
  * currently active statistics and is able to "flush" them all.