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.

10 files changed, 60 insertions, 26 deletions

diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index 5a836fdc2..1e06621b4 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: lianah
  ** 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/arrays/array_info.h b/src/theory/arrays/array_info.h
index ce3f015b5..fcc45bbd5 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file array_info.h
+ ** \verbatim
+ ** Original author: lianah
+ ** 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
+ **/
+
 /*! \file array_info.h
  ** \verbatim
  ** Original author: lianah
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 30242db30..2f4bc7313 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -5,6 +5,7 @@
 #
 
 theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h"
+typechecker "theory/arrays/theory_arrays_type_rules.h"
 
 properties polite stable-infinite
 properties check propagate presolve
@@ -23,4 +24,7 @@ operator SELECT 2 "array select"
 # store a i e  is  a[i] <= e
 operator STORE 3 "array store"
 
+typerule SELECT ::CVC4::theory::arrays::ArraySelectTypeRule
+typerule STORE ::CVC4::theory::arrays::ArrayStoreTypeRule
+
 endtheory
diff --git a/src/theory/arrays/static_fact_manager.cpp b/src/theory/arrays/static_fact_manager.cpp
index 1e135514a..dfa32418f 100644
--- a/src/theory/arrays/static_fact_manager.cpp
+++ b/src/theory/arrays/static_fact_manager.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file static_fact_manager.cpp
  ** \verbatim
- ** Original author: mdeters
+ ** Original author: barrett
  ** Major contributors: none
  ** 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/arrays/static_fact_manager.h b/src/theory/arrays/static_fact_manager.h
index de487f97c..5e1ba27a3 100644
--- a/src/theory/arrays/static_fact_manager.h
+++ b/src/theory/arrays/static_fact_manager.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file static_fact_manager.h
  ** \verbatim
- ** Original author: mdeters
+ ** Original author: barrett
  ** 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/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 888a98a45..6985aaea8 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -2,8 +2,8 @@
 /*! \file theory_arrays.cpp
  ** \verbatim
  ** Original author: barrett
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** 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
@@ -22,6 +22,7 @@
 #include "expr/kind.h"
 #include <map>
 #include "theory/rewriter.h"
+#include "expr/command.h"
 
 using namespace std;
 using namespace CVC4;
@@ -689,7 +690,7 @@ void TheoryArrays::appendToDiseqList(TNode of, TNode eq) {
  * Iterates through the indices of a and stores of b and checks if any new
  * Row lemmas need to be instantiated.
  */
-bool TheoryArrays::isRedundandRowLemma(TNode a, TNode b, TNode i, TNode j) {
+bool TheoryArrays::isRedundantRowLemma(TNode a, TNode b, TNode i, TNode j) {
   Assert(a.getType().isArray());
   Assert(b.getType().isArray());
 
@@ -984,7 +985,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) {
       TNode j = store[1];
       TNode c = store[0];
 
-      if(  !isRedundandRowLemma(store, c, j, i)){
+      if(  !isRedundantRowLemma(store, c, j, i)){
          //&&!propagateFromRow(store, c, j, i)) {
         queueRowLemma(store, c, j, i);
       }
@@ -1004,7 +1005,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) {
       TNode c = store[0];
 
       if (   isNonLinear(c)
-          &&!isRedundandRowLemma(store, c, j, i)){
+          &&!isRedundantRowLemma(store, c, j, i)){
           //&&!propagateFromRow(store, c, j, i)) {
         queueRowLemma(store, c, j, i);
       }
@@ -1066,7 +1067,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) {
     Assert(store.getKind()==kind::STORE);
     TNode j = store[1];
     //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
-    if(!isRedundandRowLemma(store, store[0], j, i)) {
+    if(!isRedundantRowLemma(store, store[0], j, i)) {
       //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
       queueRowLemma(store, store[0], j, i);
     }
@@ -1078,7 +1079,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) {
     Assert(instore.getKind()==kind::STORE);
     TNode j = instore[1];
     //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
-    if(!isRedundandRowLemma(instore, instore[0], j, i)) {
+    if(!isRedundantRowLemma(instore, instore[0], j, i)) {
       //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
       queueRowLemma(instore, instore[0], j, i);
     }
@@ -1104,7 +1105,7 @@ void TheoryArrays::checkStore(TNode a) {
   for(; it!= js->end(); it++) {
     TNode j = *it;
 
-    if(!isRedundandRowLemma(a, b, i, j)) {
+    if(!isRedundantRowLemma(a, b, i, j)) {
       //Trace("arrays-lem")<<"Arrays::checkRowStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n";
       queueRowLemma(a,b,i,j);
     }
@@ -1141,7 +1142,17 @@ inline void TheoryArrays::addExtLemma(TNode a, TNode b) {
     && d_extAlreadyAdded.count(make_pair(b, a)) == 0) {
 
    NodeManager* nm = NodeManager::currentNM();
-   Node k = nm->mkVar(a.getType()[0]);
+   TypeNode ixType = a.getType()[0];
+   Node k = nm->mkVar(ixType);
+   if(Dump.isOn("declarations")) {
+     stringstream kss;
+     kss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump("declarations"))) << k;
+     string ks = kss.str();
+     Dump("declarations")
+       << CommentCommand(ks + " is an extensional lemma index variable "
+                         "from the theory of arrays") << endl
+       << DeclareFunctionCommand(ks, ixType.toType()) << endl;
+   }
    Node eq = nm->mkNode(kind::EQUAL, a, b);
    Node ak = nm->mkNode(kind::SELECT, a, k);
    Node bk = nm->mkNode(kind::SELECT, b, k);
@@ -1154,7 +1165,7 @@ inline void TheoryArrays::addExtLemma(TNode a, TNode b) {
    ++d_numExt;
    return;
  }
- Trace("arrays-cle")<<"Arrays::checkExtLemmas lemma already generated. \n";
 
+ Trace("arrays-cle")<<"Arrays::checkExtLemmas lemma already generated. \n";
 }
 
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index cf822cb65..37fffd2ec 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -2,10 +2,10 @@
 /*! \file theory_arrays.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: barrett
- ** Minor contributors (to current version): none
+ ** Major contributors: none
+ ** Minor contributors (to current version): 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
@@ -254,7 +254,7 @@ private:
   bool isAxiom(TNode lhs, TNode rhs);
 
 
-  bool isRedundandRowLemma(TNode a, TNode b, TNode i, TNode j);
+  bool isRedundantRowLemma(TNode a, TNode b, TNode i, TNode j);
   bool isRedundantInContext(TNode a, TNode b, TNode i, TNode j);
 
 
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index d7b37d8ba..8c1c16de2 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -2,7 +2,7 @@
 /*! \file theory_arrays_rewriter.h
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: none
+ ** Major contributors: barrett, 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/arrays/union_find.cpp b/src/theory/arrays/union_find.cpp
index b0f06b78e..57fd412e4 100644
--- a/src/theory/arrays/union_find.cpp
+++ b/src/theory/arrays/union_find.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file union_find.cpp
  ** \verbatim
- ** Original author: mdeters
+ ** Original author: lianah
  ** Major contributors: none
  ** 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/arrays/union_find.h b/src/theory/arrays/union_find.h
index 4a882806c..7ae85424d 100644
--- a/src/theory/arrays/union_find.h
+++ b/src/theory/arrays/union_find.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file union_find.h
  ** \verbatim
- ** Original author: mdeters
+ ** Original author: lianah
  ** Major contributors: none
  ** 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