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.

1 files changed, 10 insertions, 0 deletions

diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index e7f86c80e..6985ae38e 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -22,6 +22,11 @@
 #ifndef __CVC4__CARDINALITY_H
 #define __CVC4__CARDINALITY_H
 
+#if SWIG
+%include "util/integer.h"
+%include "util/Assert.h"
+#endif /* SWIG */
+
 #include <iostream>
 #include <utility>
 
@@ -140,6 +145,11 @@ public:
     return d_card > 0;
   }
 
+  /** Returns true iff this cardinality is infinite. */
+  bool isInfinite() const throw() {
+    return d_card < 0;
+  }
+
   /**
    * Returns true iff this cardinality is finite or countably
    * infinite.