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.

14 files changed, 471 insertions, 8 deletions

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.