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, 23 insertions, 16 deletions

diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index fd44ec13b..318fdecce 100644
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -2,7 +2,7 @@
 /*! \file circuit_propagator.cpp
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
+ ** Major contributors: dejan
  ** 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)
@@ -29,11 +29,11 @@ namespace CVC4 {
 namespace theory {
 namespace booleans {
 
-void CircuitPropagator::assert(TNode assertion) 
+void CircuitPropagator::assert(TNode assertion)
 {
   if (assertion.getKind() == kind::AND) {
     for (unsigned i = 0; i < assertion.getNumChildren(); ++ i) {
-      assert(assertion[i]);  
+      assert(assertion[i]);
     }
   } else {
     // Analyze the assertion for back-edges and all that
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index 73a5be0f8..9593f7735 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -2,7 +2,7 @@
 /*! \file circuit_propagator.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
+ ** Major contributors: dejan
  ** 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)
@@ -189,20 +189,16 @@ private:
   bool d_forwardPropagation;
   /** Whether to perform backward propagation */
   bool d_backwardPropagation;
-  /** Whether to perform expensive propagations */
-  bool d_expensivePropagation;
 
 public:
   /**
    * Construct a new CircuitPropagator with the given atoms and backEdges.
    */
-  CircuitPropagator(std::vector<Node>& outLearnedLiterals, bool enableForward = true, bool enableBackward = true, bool enableExpensive = true) :
+  CircuitPropagator(std::vector<Node>& outLearnedLiterals, bool enableForward = true, bool enableBackward = true) :
     d_conflict(false),
     d_learnedLiterals(outLearnedLiterals),
     d_forwardPropagation(enableForward),
-    d_backwardPropagation(enableBackward),
-    d_expensivePropagation(enableExpensive)
-  {
+    d_backwardPropagation(enableBackward) {
   }
 
   /** Assert for propagation */
diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds
index d540d57f5..5580418e5 100644
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -5,6 +5,7 @@
 #
 
 theory THEORY_BOOL ::CVC4::theory::booleans::TheoryBool "theory/booleans/theory_bool.h"
+typechecker "theory/booleans/theory_bool_type_rules.h"
 
 properties finite
 
@@ -31,4 +32,14 @@ operator OR 2: "logical or"
 operator XOR 2 "exclusive or"
 operator ITE 3 "if-then-else"
 
+typerule CONST_BOOLEAN ::CVC4::theory::boolean::BooleanTypeRule
+
+typerule NOT ::CVC4::theory::boolean::BooleanTypeRule
+typerule AND ::CVC4::theory::boolean::BooleanTypeRule
+typerule IFF ::CVC4::theory::boolean::BooleanTypeRule
+typerule IMPLIES ::CVC4::theory::boolean::BooleanTypeRule
+typerule OR ::CVC4::theory::boolean::BooleanTypeRule
+typerule XOR ::CVC4::theory::boolean::BooleanTypeRule
+typerule ITE ::CVC4::theory::boolean::IteTypeRule
+
 endtheory
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 01185281a..2be1dac55 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -2,7 +2,7 @@
 /*! \file theory_bool.cpp
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
+ ** Major contributors: dejan
  ** 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)
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index ce9938b10..d53337fa7 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -2,8 +2,8 @@
 /*! \file theory_bool.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: taking
- ** Minor contributors (to current version): barrett
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** 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
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index d2693268f..4f41d2fa5 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -2,7 +2,7 @@
 /*! \file theory_bool_rewriter.cpp
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: none
+ ** Major contributors: mdeters, barrett
  ** 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)
diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h
index 4a23249d4..6771f775c 100644
--- a/src/theory/booleans/theory_bool_rewriter.h
+++ b/src/theory/booleans/theory_bool_rewriter.h
@@ -2,7 +2,7 @@
 /*! \file theory_bool_rewriter.h
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: none
+ ** 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)
diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h
index 09030d331..e6c3e0f54 100644
--- a/src/theory/booleans/theory_bool_type_rules.h
+++ b/src/theory/booleans/theory_bool_type_rules.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters, cconway
  ** Minor contributors (to current version): none
  ** 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