Merge from my post-smtcomp branch. Includes:

Dumping infrastructure.  Can dump preprocessed queries and clauses.  Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc.  For a
full list of options see --dump=help.

CUDD building much cleaner.

Documentation and assertion fixes.

Printer improvements, printing of commands in language-defined way, etc.

Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.

CVC3 compatibility layer (builds as libcompat).

SWIG detection and language binding support (infrastructure).

Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).

Copyright and file headers regenerated.

8 files changed, 84 insertions, 27 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 9797e4c67..5b8e4c3f3 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -2,8 +2,8 @@
 /*! \file cnf_stream.cpp
  ** \verbatim
  ** Original author: taking
- ** Major contributors: dejan
- ** Minor contributors (to current version): cconway, mdeters
+ ** Major contributors: mdeters, dejan
+ ** Minor contributors (to current version): cconway
  ** 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
@@ -18,13 +18,15 @@
  ** of given an equisatisfiable stream of assertions to PropEngine.
  **/
 
-#include "sat.h"
+#include "prop/sat.h"
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
 #include "theory/theory_engine.h"
 #include "expr/node.h"
 #include "util/Assert.h"
 #include "util/output.h"
+#include "expr/command.h"
+#include "expr/expr.h"
 
 #include <queue>
 
@@ -57,6 +59,21 @@ TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver, theory::Registr
 
 void CnfStream::assertClause(TNode node, SatClause& c) {
   Debug("cnf") << "Inserting into stream " << c << endl;
+  if(Dump.isOn("clauses")) {
+    if(Message.isOn()) {
+      if(c.size() == 1) {
+        Message() << AssertCommand(BoolExpr(getNode(c[0]).toExpr())) << endl;
+      } else {
+        Assert(c.size() > 1);
+        NodeBuilder<> b(kind::OR);
+        for(int i = 0; i < c.size(); ++i) {
+          b << getNode(c[i]);
+        }
+        Node n = b;
+        Message() << AssertCommand(BoolExpr(n.toExpr())) << endl;
+      }
+    }
+  }
   d_satSolver->addClause(c, d_removable);
 }
 
@@ -114,7 +131,8 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
 
   // If it's a theory literal, need to store it for back queries
   if ( theoryLiteral ||
-       ( CVC4_USE_REPLAY && Options::current()->replayLog != NULL ) ) {
+       ( CVC4_USE_REPLAY && Options::current()->replayLog != NULL ) ||
+       Dump.isOn("clauses") ) {
     d_nodeCache[lit] = node;
     d_nodeCache[~lit] = node.notNode();
   }
@@ -580,6 +598,15 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated
 
 void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
   Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
+
+  if(hasLiteral(node)) {
+    Debug("cnf") << "==> fortunate literal detected!" << endl;
+    ++d_fortunateLiterals;
+    SatLiteral lit = getLiteral(node);
+    //d_satSolver->renewVar(lit);
+    assertClause(node, negated ? ~lit : lit);
+  }
+
   switch(node.getKind()) {
   case AND:
     convertAndAssertAnd(node, negated);
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index fd0ab6291..ecb0fd2fb 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: taking
  ** Major contributors: mdeters, dejan
- ** Minor contributors (to current version): cconway
+ ** Minor contributors (to current version): barrett, cconway
  ** 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
@@ -77,6 +77,24 @@ protected:
   /** Top level nodes that we translated */
   std::vector<TNode> d_translationTrail;
 
+  /**
+   * How many literals were already mapped at the top-level when we
+   * tried to convertAndAssert() something.  This
+   * achieves early detection of units and leads to fewer
+   * clauses.  It's motivated by the following pattern:
+   *
+   *   ASSERT  BIG FORMULA => x
+   *   (and then later...)
+   *   ASSERT  BIG FORMULA
+   *
+   * With the first assert, BIG FORMULA is clausified, and a literal
+   * is assigned for the top level so that the final clause for the
+   * implication is "lit => x".  But without "fortunate literal
+   * detection," when BIG FORMULA is later asserted, it is clausified
+   * separately, and "lit" is never asserted as a unit clause.
+   */
+  KEEP_STATISTIC(IntStat, d_fortunateLiterals, "prop::CnfStream::fortunateLiterals", 0);
+
   /** Remove nots from the node */
   TNode stripNot(TNode node) {
     while (node.getKind() == kind::NOT) {
diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am
index 3e844ef79..6e003c248 100644
--- a/src/prop/minisat/Makefile.am
+++ b/src/prop/minisat/Makefile.am
@@ -1,7 +1,7 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
 	-D __STDC_LIMIT_MACROS \
-	-D __STDC_FORMAT_MACROS \               	
+	-D __STDC_FORMAT_MACROS \
 	-I@srcdir@/ -I@srcdir@/../.. -I@builddir@/../.. -I@srcdir@/../../include
 AM_CXXFLAGS = -Wall -Wno-parentheses -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 711379519..e160e1ef5 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -20,9 +20,14 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include <math.h>
 
+#include <iostream>
+
 #include "mtl/Sort.h"
 #include "core/Solver.h"
+
 #include "prop/sat.h"
+#include "util/output.h"
+#include "expr/command.h"
 
 using namespace Minisat;
 using namespace CVC4;
@@ -287,10 +292,16 @@ bool Solver::satisfied(const Clause& c) const {
 // Revert to the state at given level (keeping all assignment at 'level' but not beyond).
 //
 void Solver::cancelUntil(int level) {
+    Debug("minisat") << "minisat::cancelUntil(" << level << std::endl;
+
     if (decisionLevel() > level){
         // Pop the SMT context
-        for (int l = trail_lim.size() - level; l > 0; --l)
+        for (int l = trail_lim.size() - level; l > 0; --l) {
           context->pop();
+          if(Dump.isOn("state")) {
+            Dump("state") << PopCommand() << std::endl;
+          }
+        }
         for (int c = trail.size()-1; c >= trail_lim[level]; c--){
             Var      x  = var(trail[c]);
             assigns [x] = l_Undef;
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 4c6e98a2e..8e5e05b1c 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -23,6 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "cvc4_private.h"
 
+#include <iostream>
+
 #include "mtl/Vec.h"
 #include "mtl/Heap.h"
 #include "mtl/Alg.h"
@@ -31,12 +33,14 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "context/context.h"
 #include "theory/theory.h"
+#include "util/output.h"
+#include "expr/command.h"
 
 namespace CVC4 {
 namespace prop {
   class SatSolver;
-}
-}
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
 
 namespace Minisat {
 
@@ -441,7 +445,7 @@ inline bool     Solver::addClause       (Lit p, bool removable)
 inline bool     Solver::addClause       (Lit p, Lit q, bool removable)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); }
 inline bool     Solver::addClause       (Lit p, Lit q, Lit r, bool removable)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); }
 inline bool     Solver::locked          (const Clause& c) const { return value(c[0]) == l_True && isPropagatedBy(var(c[0]), c); }
-inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); context->push(); }
+inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); context->push(); if(Dump.isOn("state")) { Dump("state") << CVC4::PushCommand() << std::endl; } }
 
 inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }
 inline uint32_t Solver::abstractLevel (Var x) const   { return 1 << (level(x) & 31); }
@@ -495,6 +499,6 @@ inline void     Solver::toDimacs     (const char* file, Lit p, Lit q, Lit r){ ve
 
 
 //=================================================================================================
-}
+}/* Minisat namespace */
 
 #endif
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 046e4ef7e..c8e4083b1 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -2,8 +2,8 @@
 /*! \file prop_engine.cpp
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: taking, cconway, dejan
- ** Minor contributors (to current version): none
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): barrett, taking, cconway
  ** 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
@@ -90,14 +90,10 @@ void PropEngine::assertLemma(TNode node, bool negated, bool removable) {
   //Assert(d_inCheckSat, "Sat solver should be in solve()!");
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
 
-  if(Options::current()->preprocessOnly) {
-    if(Message.isOn()) {
-      // If "preprocess only" mode is in effect, the lemmas we get
-      // here are due to theory reasoning during preprocessing.  So
-      // push the lemma to the Message() stream.
-      expr::ExprSetDepth::Scope sdScope(Message.getStream(), -1);
-      Message() << AssertCommand(BoolExpr(node.toExpr())) << endl;
-    }
+  if(!d_inCheckSat && Dump.isOn("learned")) {
+    Dump("learned") << AssertCommand(BoolExpr(node.toExpr())) << endl;
+  } else if(Dump.isOn("lemmas")) {
+    Dump("lemmas") << AssertCommand(BoolExpr(node.toExpr())) << endl;
   }
 
   //TODO This comment is now false
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 599439987..af7067130 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -3,18 +3,18 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: taking, dejan
- ** Minor contributors (to current version): cconway
+ ** Minor contributors (to current version): cconway, barrett
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** 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 The PropEngine (proposiitonal engine); main interface point
- ** between CVC4's SMT infrastructure and the SAT solver.
+ ** \brief The PropEngine (propositional engine); main interface point
+ ** between CVC4's SMT infrastructure and the SAT solver
  **
- ** The PropEngine (proposiitonal engine); main interface point
+ ** The PropEngine (propositional engine); main interface point
  ** between CVC4's SMT infrastructure and the SAT solver.
  **/
 
@@ -118,6 +118,7 @@ public:
    * Return true if node has an associated SAT literal
    */
   bool isSatLiteral(TNode node);
+
   /**
    * Check if the node has a value and return it if yes.
    */
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index a7eced6f2..8bda0fd1e 100644
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -2,7 +2,7 @@
 /*! \file sat.cpp
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: dejan, mdeters, taking
+ ** Major contributors: dejan, taking, 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)