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.

13 files changed, 101 insertions, 19 deletions

diff --git a/src/theory/bv/cd_set_collection.h b/src/theory/bv/cd_set_collection.h
index 30e4e47ec..ba9d104a1 100644
--- a/src/theory/bv/cd_set_collection.h
+++ b/src/theory/bv/cd_set_collection.h
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file cd_set_collection.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
+ ** 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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
 /*
  * set_collection.h
  *
diff --git a/src/theory/bv/equality_engine.cpp b/src/theory/bv/equality_engine.cpp
index fa0650506..ee4e9903c 100644
--- a/src/theory/bv/equality_engine.cpp
+++ b/src/theory/bv/equality_engine.cpp
@@ -2,10 +2,10 @@
 /*! \file equality_engine.cpp
  ** \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  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
diff --git a/src/theory/bv/equality_engine.h b/src/theory/bv/equality_engine.h
index 31a4bfd27..558fd2b7b 100644
--- a/src/theory/bv/equality_engine.h
+++ b/src/theory/bv/equality_engine.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** 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
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index d10e32ee0..d502c5ecb 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -5,6 +5,7 @@
 #
 
 theory THEORY_BV ::CVC4::theory::bv::TheoryBV "theory/bv/theory_bv.h"
+typechecker "theory/bv/theory_bv_type_rules.h"
 
 properties finite
 properties check propagate
@@ -99,4 +100,47 @@ parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-
 parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left"
 parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right"
 
+typerule CONST_BITVECTOR ::CVC4::theory::bv::BitVectorConstantTypeRule
+
+typerule BITVECTOR_AND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_OR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_XOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_NOT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_NAND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_NOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_XNOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+
+typerule BITVECTOR_COMP ::CVC4::theory::bv::BitVectorCompRule
+
+typerule BITVECTOR_MULT ::CVC4::theory::bv::BitVectorArithRule
+typerule BITVECTOR_PLUS ::CVC4::theory::bv::BitVectorArithRule
+typerule BITVECTOR_SUB ::CVC4::theory::bv::BitVectorArithRule
+typerule BITVECTOR_NEG ::CVC4::theory::bv::BitVectorArithRule
+
+typerule BITVECTOR_UDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_UREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_SDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_SREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_SMOD ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_SHL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_LSHR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_ASHR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_ROTATE_LEFT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_ROTATE_RIGHT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+
+typerule BITVECTOR_ULT ::CVC4::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_ULE ::CVC4::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_UGT ::CVC4::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_UGE ::CVC4::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_SLT ::CVC4::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_SLE ::CVC4::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_SGT ::CVC4::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule
+
+typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule
+typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatRule
+typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule
+typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
+typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
+
 endtheory
diff --git a/src/theory/bv/slice_manager.h b/src/theory/bv/slice_manager.h
index 4fb11f105..9e0b09f2f 100644
--- a/src/theory/bv/slice_manager.h
+++ b/src/theory/bv/slice_manager.h
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file slice_manager.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** 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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
 /*
  * slice_manager.h
  *
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 593274281..c1fa692b9 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -2,10 +2,10 @@
 /*! \file theory_bv.cpp
  ** \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  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
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 27fadce0b..5c6797e76 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: dejan
- ** Minor contributors (to current version): barrett
+ ** 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
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index b66fef0a9..68f75847f 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** 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
diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index e94388754..b1541fa4a 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** 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
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 5bcbdf746..a232ad33b 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -2,7 +2,7 @@
 /*! \file theory_bv_rewriter.cpp
  ** \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/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 7af5b4496..20da74ce8 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -2,7 +2,7 @@
 /*! \file theory_bv_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/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 613df47f3..926ceb767 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -2,10 +2,10 @@
 /*! \file theory_bv_type_rules.h
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: cconway
- ** Minor contributors (to current version): mdeters
+ ** 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
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index a3135f077..fc4fbf834 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -2,10 +2,10 @@
 /*! \file theory_bv_utils.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  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