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.

25 files changed, 596 insertions, 16 deletions

diff --git a/Makefile b/Makefile
index 0f04a94cb..4b731cb04 100644
--- a/Makefile
+++ b/Makefile
@@ -1,3 +1,10 @@
+# -*-makefile-*-
+#
+# This makefile is the _source_ directory's makefile, and is static,
+# not generated.  Makefile.am is the automake makefile for the build
+# top-level (its corresponding Makefile.in is here, too, but the
+# corresponding Makefile is under builds/$arch/$buildid.
+#
 builddir = builds
 
 .PHONY: _default_build_ all
diff --git a/Makefile.subdir b/Makefile.subdir
index 293b2771b..7b7c90561 100644
--- a/Makefile.subdir
+++ b/Makefile.subdir
@@ -1,4 +1,10 @@
 # -*-makefile-*-
+#
+# This makefile is included from source directories in order to
+# trigger a build in the corresponding build directory.
+#
+# See src/Makefile for an example.
+#
 include $(topdir)/builds/current
 builddir = $(topdir)/builds/$(CURRENT_BUILD)/$(srcdir)
 unittestdir = $(topdir)/builds/$(CURRENT_BUILD)/test/unit
diff --git a/README b/README
index d064c226d..aaa36ff67 100644
--- a/README
+++ b/README
@@ -27,9 +27,25 @@ given are minimum versions; more recent versions should be compatible.
 
 GNU C and C++ (gcc and g++), reasonably recent versions
 GNU Make
-GMP v4.2
-libantlr3c v3.2
-Optional: CLN v1.3
+GMP v4.2 (GNU Multi-Precision arithmetic library)
+libantlr3c v3.2 (ANTLR parser generator)
+Optional: CLN v1.3 (Class Library for Numbers)
+Optional: CUDD v2.4.2 (Colorado University Decision Diagram package)
+
+CUDD, if desired, must be installed in a special manner.  The default
+distribution from vlsi.colorado.edu doesn't build shared objects,
+and names things that make it difficult to compose software
+dependences (e.g. a "libutil" is distributed).  So we packaged our
+own version of cudd that changes only its build process, making it
+play nicely with libtool and packaging all the various cudd libraries
+into just a few.  This version must be used for cvc4, and is available
+from the CVC4 apt repository by dropping the following line into your
+/etc/apt/sources.list:
+
+  deb http://goedel.cims.nyu.edu/cvc4-builds/debian unstable/
+
+The debian source package "cudd", available from the same repository,
+includes a diff of all changes made to cudd makefiles.
 
 *** Build dependencies
 
diff --git a/configure.ac b/configure.ac
index 66e8acd7d..05e3bac8e 100644
--- a/configure.ac
+++ b/configure.ac
@@ -662,6 +662,49 @@ AC_SEARCH_LIBS([clock_gettime], [rt],
                           [Defined to 1 if clock_gettime() is supported by the platform.])],
                [AC_LIBOBJ([clock_gettime])])
 
+AC_ARG_WITH([cudd-dir],
+  [AS_HELP_STRING([--with-cudd-dir=DIR], [path to cudd installation])],
+  [CUDD_DIR="$withval"])
+if test -z "$CUDD_DIR"; then
+  CUDD_DIR=/usr
+fi
+AC_MSG_CHECKING([for cudd includes under $CUDD_DIR])
+CUDD_CPPFLAGS=
+CUDD_LDFLAGS=
+cvc4cudd=no
+result="not found"
+for cuddinc in "$CUDD_DIR/include" "$CUDD_DIR/include/cudd" "$CUDD_DIR"; do
+  if test -r "$cuddinc/cudd.h"; then
+    dnl TODO - should do a TRY_COMPILE instead
+    CUDD_CPPFLAGS="\"-I$cuddinc\""
+    result="$cuddinc"
+    cvc4cudd=yes
+    break
+  fi
+done
+AC_MSG_RESULT([$result])
+if test $cvc4cudd = yes; then
+  AC_MSG_CHECKING([for cudd libraries under $CUDD_DIR])
+  cvc4cudd=no
+  result="not found"
+  for cuddlib in "$CUDD_DIR/lib" "$CUDD_DIR/lib/cudd" "$CUDD_DIR"; do
+    if test -r "$cuddlib/libcuddxx.la"; then
+      dnl TODO - should do a TRY_LINK instead, that has the extra benefit
+      dnl of making sure both shared & static work
+      CUDD_LDFLAGS="\"-L$cuddlib\" -lcuddxx"
+      result="$cuddlib"
+      cvc4cudd=yes
+      break
+    fi
+  done
+  AC_MSG_RESULT([$result]);
+  if test $cvc4cudd = yes; then
+    AC_DEFINE_UNQUOTED(CVC4_CUDD, [], [Defined if using the CU Decision Diagram package (cudd).])
+  fi
+fi
+AC_SUBST([CUDD_CPPFLAGS])
+AC_SUBST([CUDD_LDFLAGS])
+
 # Check for antlr C++ runtime (defined in config/antlr.m4)
 AC_LIB_ANTLR
 
diff --git a/contrib/addsourcedir b/contrib/addsourcedir
index ef6aedd15..00357cadf 100755
--- a/contrib/addsourcedir
+++ b/contrib/addsourcedir
@@ -2,7 +2,7 @@
 #
 # addsourcedir
 # Morgan Deters <mdeters@cs.nyu.edu> for the CVC4 project
-# Copyright (c) 2010  The CVC4 Project
+# Copyright (c) 2010, 2011  The CVC4 Project
 #
 # usage: addsourcedir paths...
 #
diff --git a/contrib/configure-in-place b/contrib/configure-in-place
index 09771676e..9da584d36 100755
--- a/contrib/configure-in-place
+++ b/contrib/configure-in-place
@@ -2,7 +2,7 @@
 #
 # configure-in-place
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010  The CVC4 Project
+# Copyright (c) 2010, 2011  The CVC4 Project
 #
 # usage: configure-in-place [ arguments... ]
 #
diff --git a/contrib/debug-keys b/contrib/debug-keys
new file mode 100755
index 000000000..6d2804974
--- /dev/null
+++ b/contrib/debug-keys
@@ -0,0 +1,33 @@
+#!/bin/bash
+#
+# Lists the Trace() and Debug() keys used in sources.
+#
+# e.g. if Debug("uf") occurs in the sources, then "uf" is printed by this script.
+
+if [ "$1" = "-h" -o "$1" = "-help" -o "$1" = "-?" -o "$1" = "--help" ]; then
+  echo "usage: `basename $0` [dirs...]" >&2
+  echo "This utility will print all Debug("foo") and Trace("foo") keys."
+  echo "With optional dirs..., use dirs instead of top-level \"src\"." >&2
+  exit 1
+fi
+
+if [ $# -eq 0 ]; then
+  cd `dirname "$0"`/..
+
+  if ! [ -d src ]; then
+    echo "`basename $0`: not in CVC4 directory tree?!" >&2
+    exit 1
+  fi
+
+  set src
+fi
+
+echo "Trace and debug flags used in $*:"
+
+while [ $# -gt 0 ]; do
+  dir="$1"
+  shift
+
+  test -r "$dir" && grep -r --exclude-dir=.svn '\(Debug\|Trace\)\(\.isOn\)\?("[^"]\+")' "$dir" | sed 's,.*\(Debug\|Trace\)\(\.isOn\)\?("\([^"]\+\)").*,\3,' | sort -u
+done | sort -u
+
diff --git a/contrib/dimacs_to_smt.pl b/contrib/dimacs_to_smt.pl
index 6c1e0eeea..701768119 100755
--- a/contrib/dimacs_to_smt.pl
+++ b/contrib/dimacs_to_smt.pl
@@ -1,7 +1,7 @@
 #!/usr/bin/perl -w
 # DIMACS to SMT
 # Morgan Deters
-# Copyright (c) 2009, 2010  The CVC4 Project
+# Copyright (c) 2009, 2010, 2011  The CVC4 Project
 
 use strict;
 
diff --git a/contrib/get-authors b/contrib/get-authors
index dbe878d6b..ef6abff8e 100755
--- a/contrib/get-authors
+++ b/contrib/get-authors
@@ -2,7 +2,7 @@
 #
 # get-authors
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2009, 2010  The CVC4 Project
+# Copyright (c) 2009, 2010, 2011  The CVC4 Project
 #
 # usage: get-authors [ files... ]
 #
diff --git a/src/expr/type.h b/src/expr/type.h
index 453eaf5c4..d357c869e 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -34,6 +34,8 @@ class NodeManager;
 class ExprManager;
 class TypeNode;
 
+class SmtEngine;
+
 template <bool ref_count>
 class NodeTemplate;
 
@@ -69,7 +71,6 @@ std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC;
 class CVC4_PUBLIC Type {
 
   friend class SmtEngine;
-  friend class SmtEnginePrivate;
   friend class ExprManager;
   friend class TypeNode;
   friend class TypeHashStrategy;
diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am
index 2cdba2d27..30be07d7c 100644
--- a/src/prop/Makefile.am
+++ b/src/prop/Makefile.am
@@ -11,7 +11,7 @@ libprop_la_SOURCES = \
 	prop_engine.cpp \
 	prop_engine.h \
 	sat.h \
-        sat.cpp \
+	sat.cpp \
 	cnf_stream.h \
 	cnf_stream.cpp
 
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);
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 456fdb746..b75140bc7 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -27,6 +27,8 @@
 #include "util/rational.h"
 #include "util/integer.h"
 
+#include "theory/rewriter.h"
+
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/partial_model.h"
@@ -79,6 +81,8 @@ TheoryArith::Statistics::Statistics():
   d_staticLearningTimer("theory::arith::staticLearningTimer"),
   d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0),
   d_presolveTime("theory::arith::presolveTime"),
+  d_miplibtrickApplications("theory::arith::miplibtrickApplications", 0),
+  d_avgNumMiplibtrickValues("theory::arith::avgNumMiplibtrickValues"),
   d_initialTableauDensity("theory::arith::initialTableauDensity", 0.0),
   d_avgTableauDensityAtRestart("theory::arith::avgTableauDensityAtRestarts"),
   d_tableauResets("theory::arith::tableauResets", 0),
@@ -93,6 +97,9 @@ TheoryArith::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_permanentlyRemovedVariables);
   StatisticsRegistry::registerStat(&d_presolveTime);
 
+  StatisticsRegistry::registerStat(&d_miplibtrickApplications);
+  StatisticsRegistry::registerStat(&d_avgNumMiplibtrickValues);
+
   StatisticsRegistry::registerStat(&d_initialTableauDensity);
   StatisticsRegistry::registerStat(&d_avgTableauDensityAtRestart);
   StatisticsRegistry::registerStat(&d_tableauResets);
@@ -109,19 +116,43 @@ TheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_permanentlyRemovedVariables);
   StatisticsRegistry::unregisterStat(&d_presolveTime);
 
+  StatisticsRegistry::unregisterStat(&d_miplibtrickApplications);
+  StatisticsRegistry::unregisterStat(&d_avgNumMiplibtrickValues);
+
   StatisticsRegistry::unregisterStat(&d_initialTableauDensity);
   StatisticsRegistry::unregisterStat(&d_avgTableauDensityAtRestart);
   StatisticsRegistry::unregisterStat(&d_tableauResets);
   StatisticsRegistry::unregisterStat(&d_restartTimer);
 }
 
+#include "util/propositional_query.h"
 void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
   TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer);
 
+  /*
+  if(Debug.isOn("prop::static")){
+    Debug("prop::static") << n << "is "
+                          << prop::PropositionalQuery::isSatisfiable(n)
+                          << endl;
+  }
+  */
+
   vector<TNode> workList;
   workList.push_back(n);
   __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed;
 
+  //Contains an underapproximation of nodes that must hold.
+  __gnu_cxx::hash_set<TNode, TNodeHashFunction> defTrue;
+
+  /* Maps a variable, x, to the set of defTrue nodes of the form
+   *  (=> _ (= x c))
+   * where c is a constant.
+   */
+  typedef __gnu_cxx::hash_map<TNode, set<TNode>, TNodeHashFunction> VarToNodeSetMap;
+  VarToNodeSetMap miplibTrick;
+
+  defTrue.insert(n);
+
   while(!workList.empty()) {
     n = workList.back();
 
@@ -133,6 +164,11 @@ void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
         unprocessedChildren = true;
       }
     }
+    if(n.getKind() == AND && defTrue.find(n) != defTrue.end() ){
+      for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
+        defTrue.insert(*i);
+      }
+    }
 
     if(unprocessedChildren) {
       continue;
@@ -202,6 +238,105 @@ void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
       Debug("arith::mins") << n << " is a constant sandwich"  << nGeqMin << nLeqMax << endl;
       learned << nGeqMin << nLeqMax;
     }
+    // == 3-FINITE VALUE SET : Collect information ==
+    if(n.getKind() == IMPLIES &&
+       n[1].getKind() == EQUAL &&
+       n[1][0].getMetaKind() == metakind::VARIABLE &&
+       defTrue.find(n) != defTrue.end()){
+      Node eqTo = n[1][1];
+      Node rewriteEqTo = Rewriter::rewrite(eqTo);
+      if(rewriteEqTo.getKind() == CONST_RATIONAL){
+
+        TNode var = n[1][0];
+        if(miplibTrick.find(var)  == miplibTrick.end()){
+          //[MGD] commented out following line as per TAK's instructions
+          //miplibTrick.insert(make_pair(var, set<TNode>()));
+        }
+        //[MGD] commented out following line as per TAK's instructions
+        //miplibTrick[var].insert(n);
+        Debug("arith::miplib") << "insert " << var  << " const " << n << endl;
+      }
+    }
+  }
+
+  // == 3-FINITE VALUE SET ==
+  VarToNodeSetMap::iterator i = miplibTrick.begin(), endMipLibTrick = miplibTrick.end();
+  for(; i != endMipLibTrick; ++i){
+    TNode var = i->first;
+    const set<TNode>& imps = i->second;
+
+    Assert(!imps.empty());
+    vector<Node> conditions;
+    vector<Rational> valueCollection;
+    set<TNode>::const_iterator j=imps.begin(), impsEnd=imps.end();
+    for(; j != impsEnd; ++j){
+      TNode imp = *j;
+      Assert(imp.getKind() == IMPLIES);
+      Assert(defTrue.find(imp) != defTrue.end());
+      Assert(imp[1].getKind() == EQUAL);
+
+
+      Node eqTo = imp[1][1];
+      Node rewriteEqTo = Rewriter::rewrite(eqTo);
+      Assert(rewriteEqTo.getKind() == CONST_RATIONAL);
+
+      conditions.push_back(imp[0]);
+      valueCollection.push_back(rewriteEqTo.getConst<Rational>());
+    }
+
+    Node possibleTaut = Node::null();
+    if(conditions.size() == 1){
+      possibleTaut = conditions.front();
+    }else{
+      NodeBuilder<> orBuilder(OR);
+      orBuilder.append(conditions);
+      possibleTaut = orBuilder;
+    }
+
+
+    Debug("arith::miplib") << "var: " << var << endl;
+    Debug("arith::miplib") << "possibleTaut: " << possibleTaut << endl;
+
+    Result isTaut = PropositionalQuery::isTautology(possibleTaut);
+    if(isTaut == Result(Result::VALID)){
+      Debug("arith::miplib") << var << " found a tautology!"<< endl;
+
+      set<Rational> values(valueCollection.begin(), valueCollection.end());
+      const Rational& min = *(values.begin());
+      const Rational& max = *(values.rbegin());
+
+      Debug("arith::miplib") << "min: " << min << endl;
+      Debug("arith::miplib") << "max: " << max << endl;
+
+      Assert(min <= max);
+
+      ++(d_statistics.d_miplibtrickApplications);
+      (d_statistics.d_avgNumMiplibtrickValues).addEntry(values.size());
+
+      Node nGeqMin = NodeBuilder<2>(GEQ) << var << mkRationalNode(min);
+      Node nLeqMax = NodeBuilder<2>(LEQ) << var << mkRationalNode(max);
+      Debug("arith::miplib") << nGeqMin << nLeqMax << endl;
+      learned << nGeqMin << nLeqMax;
+      set<Rational>::iterator valuesIter = values.begin();
+      set<Rational>::iterator valuesEnd = values.end();
+      set<Rational>::iterator valuesPrev = valuesIter;
+      ++valuesIter;
+      for(; valuesIter != valuesEnd; valuesPrev = valuesIter, ++valuesIter){
+        const Rational& prev = *valuesPrev;
+        const Rational& curr = *valuesIter;
+        Assert(prev < curr);
+
+        //The interval (last,curr) can be excluded:
+        //(not (and (> var prev) (< var curr))
+        //<=> (or (not (> var prev)) (not (< var curr)))
+        //<=> (or (<= var prev) (>= var curr))
+        Node leqPrev = NodeBuilder<2>(LEQ) << var << mkRationalNode(prev);
+        Node geqCurr = NodeBuilder<2>(GEQ) << var << mkRationalNode(curr);
+        Node excludedMiddle =  NodeBuilder<2>(OR) << leqPrev << geqCurr;
+        Debug("arith::miplib") << excludedMiddle << endl;
+        learned << excludedMiddle;
+      }
+    }
   }
 }
 
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 3ff83abdf..1dcdceab0 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -237,6 +237,9 @@ private:
     IntStat d_permanentlyRemovedVariables;
     TimerStat d_presolveTime;
 
+    IntStat d_miplibtrickApplications;
+    AverageStat d_avgNumMiplibtrickValues;
+
     BackedStat<double> d_initialTableauDensity;
     AverageStat d_avgTableauDensityAtRestart;
     IntStat d_tableauResets;
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.
diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index 91b1d41c7..aca076d9f 100644
--- a/test/regress/regress0/arith/Makefile.am
+++ b/test/regress/regress0/arith/Makefile.am
@@ -8,7 +8,8 @@ TESTS =	\
 	arith.02.cvc \
 	arith.03.cvc \
 	delta-minimized-row-vector-bug.smt \
-	leq.01.smt
+	leq.01.smt \
+	miplibtrick.smt
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/arith/miplibtrick.smt b/test/regress/regress0/arith/miplibtrick.smt
new file mode 100644
index 000000000..93cd6d219
--- /dev/null
+++ b/test/regress/regress0/arith/miplibtrick.smt
@@ -0,0 +1,11 @@
+(benchmark miplibtrick
+  :status sat
+  :logic QF_LRA
+  :extrafuns ((tmp1 Real))
+  :extrapreds ((x177))
+
+  :formula( and
+    ( implies ( and ( not x177 ) true ) ( = tmp1 0 ) )
+    ( implies ( and x177 true ) ( = tmp1 (~ 350) ) )
+  )
+)