Partial merge from kind-backend branch, including Minisat and CNF work to

support incrementality.

Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.

Expected performance change negligible; slightly better on memory:
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!

11 files changed, 325 insertions, 24 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index e24184ad2..e8d33fbd4 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -57,6 +57,8 @@ libutil_la_SOURCES = \
 	ntuple.h \
 	recursion_breaker.h \
 	subrange_bound.h \
+	predicate.h \
+	predicate.cpp \
 	cardinality.h \
 	cardinality.cpp \
 	cache.h \
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index 211a1127b..8942c049b 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -190,7 +190,7 @@ string Configuration::getSubversionId() {
   return ss.str();
 }
 
-string Configuration::getCompiler() {
+std::string Configuration::getCompiler() {
   stringstream ss;
 #ifdef __GNUC__
   ss << "GCC";
@@ -205,4 +205,8 @@ string Configuration::getCompiler() {
   return ss.str();
 }
 
+std::string Configuration::getCompiledDateTime() {
+  return __DATE__ " " __TIME__;
+}
+
 }/* CVC4 namespace */
diff --git a/src/util/configuration.h b/src/util/configuration.h
index 1a57af62b..1bd48999e 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -102,6 +102,7 @@ public:
   static std::string getSubversionId();
 
   static std::string getCompiler();
+  static std::string getCompiledDateTime();
 
 };/* class Configuration */
 
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index fc0915f28..b93a6dd5e 100644
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -121,7 +121,8 @@ This is CVC4 version " CVC4_RELEASE_STRING ) + \
         ? ( ::std::string(" [") + ::CVC4::Configuration::getSubversionId() + "]" ) \
         : ::std::string("") \
     ) + "\n\
-compiled with " + ::CVC4::Configuration::getCompiler() + "\n\n\
+compiled with " + ::CVC4::Configuration::getCompiler() + "\n\
+on " + ::CVC4::Configuration::getCompiledDateTime() + "\n\n\
 Copyright (C) 2009, 2010, 2011, 2012\n\
   The ACSys Group\n\
   Courant Institute of Mathematical Sciences\n\
diff --git a/src/util/datatype.i b/src/util/datatype.i
index 056c15004..2b2a96030 100644
--- a/src/util/datatype.i
+++ b/src/util/datatype.i
@@ -11,6 +11,8 @@
   %ignore to_array();// ocaml
   %ignore vector(size_type);// java/python
   %ignore resize(size_type);// java/python
+  %ignore set(int i, const CVC4::Datatype& x);
+  %ignore to_array();
 };
 %template(vectorDatatype) std::vector< CVC4::Datatype >;
 
@@ -23,6 +25,8 @@
   %ignore to_array();// ocaml
   %ignore vector(size_type);// java/python
   %ignore resize(size_type);// java/python
+  %ignore set(int i, const CVC4::Datatype::Constructor& x);
+  %ignore to_array();
 };
 %template(vectorDatatypeConstructor) std::vector< CVC4::DatatypeConstructor >;
 
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 161666df5..a02f5d2c1 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -268,14 +268,14 @@ public:
     long si = d_value.get_si();
     // ensure there wasn't overflow
     AlwaysAssert(mpz_cmp_si(d_value.get_mpz_t(), si) == 0,
-                 "Overflow detected in Integer::getLong()");
+                 "Overflow when extracting long from multiprecision integer");
     return si;
   }
   unsigned long getUnsignedLong() const {
     unsigned long ui = d_value.get_ui();
     // ensure there wasn't overflow
     AlwaysAssert(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0,
-                 "Overflow detected in Integer::getUnsignedLong()");
+                 "Overflow when extracting unsigned long from multiprecision integer");
     return ui;
   }
 
diff --git a/src/util/options.cpp b/src/util/options.cpp
index e33fbc263..d21df27ac 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -23,6 +23,7 @@
 #include <string.h>
 #include <stdint.h>
 #include <time.h>
+#include <sstream>
 
 #include <getopt.h>
 
@@ -274,10 +275,10 @@ Dump modes can be combined with multiple uses of --dump.  Generally you want\n\
 one from the assertions category (either asertions, learned, or clauses), and\n\
 perhaps one or more stateful or non-stateful modes for checking correctness\n\
 and completeness of decision procedure implementations.  Stateful modes dump\n\
-the contextual assertions made by the core solver (all decisions and propagations\n\
-as assertions; that affects the validity of the resulting correctness and\n\
-completeness queries, so of course stateful and non-stateful modes cannot\n\
-be mixed in the same run.\n\
+the contextual assertions made by the core solver (all decisions and\n\
+propagations as assertions; that affects the validity of the resulting\n\
+correctness and completeness queries, so of course stateful and non-stateful\n\
+modes cannot be mixed in the same run.\n\
 \n\
 The --output-language option controls the language used for dumping, and\n\
 this allows you to connect CVC4 to another solver implementation via a UNIX\n\
@@ -983,7 +984,12 @@ throw(OptionException) {
       break; 
 
     case ':':
-      throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument");
+      // This can be a long or short option, and the way to get at the name of it is different.
+      if(optopt == 0) { // was a long option
+        throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument");
+      } else { // was a short option
+        throw OptionException(string("option `-") + char(optopt) + "' missing its required argument");
+      }
 
     case '?':
     default:
@@ -1004,7 +1010,13 @@ throw(OptionException) {
         }
         break;
       }
-      throw OptionException(string("can't understand option `") + argv[optind - 1] + "'");
+
+      // This can be a long or short option, and the way to get at the name of it is different.
+      if(optopt == 0) { // was a long option
+        throw OptionException(string("can't understand option `") + argv[optind - 1] + "'");
+      } else { // was a short option
+        throw OptionException(string("can't understand option `-") + char(optopt) + "'");
+      }
     }
   }
 
diff --git a/src/util/output.h b/src/util/output.h
index 8a90ef136..8afb4e05a 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -28,6 +28,7 @@
 #include <cstdio>
 #include <cstdarg>
 #include <set>
+#include <utility>
 
 namespace CVC4 {
 
@@ -167,6 +168,20 @@ CVC4ostream& CVC4ostream::operator<<(T const& t) {
   return *this;
 }
 
+/**
+ * Does nothing; designed for compilation of non-debug/non-trace
+ * builds.  None of these should ever be called in such builds, but we
+ * offer this to the compiler so it doesn't complain.
+ */
+class CVC4_PUBLIC NullC {
+public:
+  operator bool() { return false; }
+  operator CVC4ostream() { return CVC4ostream(); }
+  operator std::ostream&() { return null_os; }
+};/* class NullC */
+
+extern NullC nullCvc4Stream CVC4_PUBLIC;
+
 /** The debug output class */
 class CVC4_PUBLIC DebugC {
   std::set<std::string> d_tags;
@@ -208,6 +223,7 @@ public:
 
 /** The warning output class */
 class CVC4_PUBLIC WarningC {
+  std::set< std::pair<const char*, size_t> > d_alreadyWarned;
   std::ostream* d_os;
 
 public:
@@ -221,6 +237,22 @@ public:
   std::ostream& getStream() { return *d_os; }
 
   bool isOn() const { return d_os != &null_os; }
+
+  // This function supports the WarningOnce() macro, which allows you
+  // to easily indicate that a warning should be emitted, but only
+  // once for a given run of CVC4.
+  bool warnOnce(const char* file, size_t line) {
+    std::pair<const char*, size_t> pr = std::make_pair(file, line);
+    if(d_alreadyWarned.find(pr) != d_alreadyWarned.end()) {
+      // signal caller not to warn again
+      return false;
+    }
+
+    // okay warn this time, but don't do it again
+    d_alreadyWarned.insert(pr);
+    return true;
+  }
+
 };/* class WarningC */
 
 /** The message output class */
@@ -378,6 +410,7 @@ extern DumpC DumpChannel CVC4_PUBLIC;
 
 #  define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel
 #  define Warning ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
+#  define WarningOnce ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
 #  define Message ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel
 #  define Notice ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel
 #  define Chat ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel
@@ -405,6 +438,7 @@ inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; }
 inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; }
 #  endif /* CVC4_DEBUG */
 #  define Warning (! ::CVC4::WarningChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
+#  define WarningOnce (! ::CVC4::WarningChannel.isOn() || ! ::CVC4::WarningChannel.warnOnce(__FILE__,__LINE__)) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
 #  define Message (! ::CVC4::MessageChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel
 #  define Notice (! ::CVC4::NoticeChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel
 #  define Chat (! ::CVC4::ChatChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel
@@ -533,20 +567,6 @@ public:
 #endif /* CVC4_TRACING */
 
 /**
- * Does nothing; designed for compilation of non-debug/non-trace
- * builds.  None of these should ever be called in such builds, but we
- * offer this to the compiler so it doesn't complain.
- */
-class CVC4_PUBLIC NullC {
-public:
-  operator bool() { return false; }
-  operator CVC4ostream() { return CVC4ostream(); }
-  operator std::ostream&() { return null_os; }
-};/* class NullC */
-
-extern NullC nullCvc4Stream CVC4_PUBLIC;
-
-/**
  * Pushes an indentation level on construction, pop on destruction.
  * Useful for tracing recursive functions especially, but also can be
  * used for clearly separating different phases of an algorithm,
diff --git a/src/util/predicate.cpp b/src/util/predicate.cpp
new file mode 100644
index 000000000..1868f557d
--- /dev/null
+++ b/src/util/predicate.cpp
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file predicate.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** 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 Representation of predicates for predicate subtyping
+ **
+ ** Simple class to represent predicates for predicate subtyping.
+ ** Instances of this class are carried as the payload of
+ ** the CONSTANT-metakinded SUBTYPE_TYPE types.
+ **/
+
+#include "expr/expr.h"
+#include "util/predicate.h"
+#include "util/Assert.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+Predicate::Predicate(Expr e, Expr w) throw(IllegalArgumentException) : d_predicate(e), d_witness(w) {
+  CheckArgument(! e.isNull(), e, "Predicate cannot be null");
+  CheckArgument(e.getType().isPredicate(), e, "Expression given is not predicate");
+  CheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e, "Expression given is not predicate of a single argument");
+}
+
+Predicate::operator Expr() const {
+  return d_predicate;
+}
+
+bool Predicate::operator==(const Predicate& p) const {
+  return d_predicate == p.d_predicate && d_witness == p.d_witness;
+}
+
+std::ostream&
+operator<<(std::ostream& out, const Predicate& p) {
+  out << p.d_predicate;
+  if(! p.d_witness.isNull()) {
+    out << " : " << p.d_witness;
+  }
+  return out;
+}
+
+size_t PredicateHashStrategy::hash(const Predicate& p) {
+  ExprHashFunction h;
+  return h(p.d_witness) * 5039 + h(p.d_predicate);
+}
+
+}/* CVC4 namespace */
diff --git a/src/util/predicate.h b/src/util/predicate.h
new file mode 100644
index 000000000..94a685177
--- /dev/null
+++ b/src/util/predicate.h
@@ -0,0 +1,64 @@
+/*********************                                                        */
+/*! \file predicate.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** 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 Representation of predicates for predicate subtyping
+ **
+ ** Simple class to represent predicates for predicate subtyping.
+ ** Instances of this class are carried as the payload of
+ ** the CONSTANT-metakinded SUBTYPE_TYPE types.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__PREDICATE_H
+#define __CVC4__PREDICATE_H
+
+#include "util/Assert.h"
+
+namespace CVC4 {
+
+class Predicate;
+
+std::ostream& operator<<(std::ostream& out, const Predicate& p) CVC4_PUBLIC;
+
+struct CVC4_PUBLIC PredicateHashStrategy {
+  static size_t hash(const Predicate& p);
+};/* class PredicateHashStrategy */
+
+}/* CVC4 namespace */
+
+#include "expr/expr.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC Predicate {
+
+  Expr d_predicate;
+  Expr d_witness;
+
+public:
+
+  Predicate(Expr e, Expr w = Expr()) throw(IllegalArgumentException);
+
+  operator Expr() const;
+
+  bool operator==(const Predicate& p) const;
+
+  friend std::ostream& operator<<(std::ostream& out, const Predicate& p);
+  friend size_t PredicateHashStrategy::hash(const Predicate& p);
+
+};/* class Predicate */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PREDICATE_H */
diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h
index 0c84b214e..9d4d446bd 100644
--- a/src/util/subrange_bound.h
+++ b/src/util/subrange_bound.h
@@ -25,6 +25,8 @@
 #include "util/integer.h"
 #include "util/Assert.h"
 
+#include <limits>
+
 namespace CVC4 {
 
 /**
@@ -76,8 +78,132 @@ public:
     return !(*this == b);
   }
 
+  /**
+   * Is this SubrangeBound "less than" another?  For two
+   * SubrangeBounds that "have bounds," this is defined as expected.
+   * For a finite SubrangeBound b1 and a SubrangeBounds b2 without a
+   * bound, b1 < b2 (but note also that b1 > b2).  This strange
+   * behavior is due to the fact that a SubrangeBound without a bound
+   * is the representation for both +infinity and -infinity.
+   */
+  bool operator<(const SubrangeBound& b) const throw() {
+    return (!hasBound() && b.hasBound()) || (hasBound() && !b.hasBound()) ||
+      ( hasBound() && b.hasBound() && getBound() < b.getBound() );
+  }
+
+  /**
+   * Is this SubrangeBound "less than or equal to" another?  For two
+   * SubrangeBounds that "have bounds," this is defined as expected.
+   * For a finite SubrangeBound b1 and a SubrangeBounds b2 without a
+   * bound, b1 < b2 (but note also that b1 > b2).  This strange
+   * behavior is due to the fact that a SubrangeBound without a bound
+   * is the representation for both +infinity and -infinity.
+   */
+  bool operator<=(const SubrangeBound& b) const throw() {
+    return !hasBound() || !b.hasBound() ||
+      ( hasBound() && b.hasBound() && getBound() <= b.getBound() );
+  }
+
+  /**
+   * Is this SubrangeBound "greater than" another?  For two
+   * SubrangeBounds that "have bounds," this is defined as expected.
+   * For a finite SubrangeBound b1 and a SubrangeBounds b2 without a
+   * bound, b1 > b2 (but note also that b1 < b2).  This strange
+   * behavior is due to the fact that a SubrangeBound without a bound
+   * is the representation for both +infinity and -infinity.
+   */
+  bool operator>(const SubrangeBound& b) const throw() {
+    return (!hasBound() && b.hasBound()) || (hasBound() && !b.hasBound()) ||
+      ( hasBound() && b.hasBound() && getBound() < b.getBound() );
+  }
+
+  /**
+   * Is this SubrangeBound "greater than or equal to" another?  For
+   * two SubrangeBounds that "have bounds," this is defined as
+   * expected.  For a finite SubrangeBound b1 and a SubrangeBounds b2
+   * without a bound, b1 > b2 (but note also that b1 < b2).  This
+   * strange behavior is due to the fact that a SubrangeBound without
+   * a bound is the representation for both +infinity and -infinity.
+   */
+  bool operator>=(const SubrangeBound& b) const throw() {
+    return !hasBound() || !b.hasBound() ||
+      ( hasBound() && b.hasBound() && getBound() <= b.getBound() );
+  }
+
 };/* class SubrangeBound */
 
+class CVC4_PUBLIC SubrangeBounds {
+public:
+
+  SubrangeBound lower;
+  SubrangeBound upper;
+
+  SubrangeBounds(const SubrangeBound& l, const SubrangeBound& u) :
+    lower(l),
+    upper(u) {
+    CheckArgument(!l.hasBound() || !u.hasBound() ||
+                  l.getBound() <= u.getBound(),
+                  l, "Bad subrange bounds specified");
+  }
+
+  bool operator==(const SubrangeBounds& bounds) const {
+    return lower == bounds.lower && upper == bounds.upper;
+  }
+
+  bool operator!=(const SubrangeBounds& bounds) const {
+    return !(*this == bounds);
+  }
+
+  /**
+   * Is this pair of SubrangeBounds "less than" (contained inside) the
+   * given pair of SubrangeBounds?  Think of this as a subtype
+   * relation, e.g., [0,2] < [0,3]
+   */
+  bool operator<(const SubrangeBounds& bounds) const {
+    return (lower > bounds.lower && upper <= bounds.upper) ||
+      (lower >= bounds.lower && upper < bounds.upper);
+  }
+
+  /**
+   * Is this pair of SubrangeBounds "less than or equal" (contained
+   * inside) the given pair of SubrangeBounds?  Think of this as a
+   * subtype relation, e.g., [0,2] < [0,3]
+   */
+  bool operator<=(const SubrangeBounds& bounds) const {
+    return lower >= bounds.lower && upper <= bounds.upper;
+  }
+
+  /**
+   * Is this pair of SubrangeBounds "greater than" (does it contain)
+   * the given pair of SubrangeBounds?  Think of this as a supertype
+   * relation, e.g., [0,3] > [0,2]
+   */
+  bool operator>(const SubrangeBounds& bounds) const {
+    return (lower < bounds.lower && upper >= bounds.upper) ||
+      (lower <= bounds.lower && upper > bounds.upper);
+  }
+
+  /**
+   * Is this pair of SubrangeBounds "greater than" (does it contain)
+   * the given pair of SubrangeBounds?  Think of this as a supertype
+   * relation, e.g., [0,3] > [0,2]
+   */
+  bool operator>=(const SubrangeBounds& bounds) const {
+    return lower <= bounds.lower && upper >= bounds.upper;
+  }
+
+};/* class SubrangeBounds */
+
+struct CVC4_PUBLIC SubrangeBoundsHashStrategy {
+  static inline size_t hash(const SubrangeBounds& bounds) {
+    // We use Integer::hash() rather than Integer::getUnsignedLong()
+    // because the latter might overflow and throw an exception
+    size_t l = bounds.lower.hasBound() ? bounds.lower.getBound().hash() : std::numeric_limits<size_t>::max();
+    size_t u = bounds.upper.hasBound() ? bounds.upper.getBound().hash() : std::numeric_limits<size_t>::max();
+    return l + 0x9e3779b9 + (u << 6) + (u >> 2);
+  }
+};/* struct SubrangeBoundsHashStrategy */
+
 inline std::ostream&
 operator<<(std::ostream& out, const SubrangeBound& bound) throw() CVC4_PUBLIC;
 
@@ -92,6 +218,16 @@ operator<<(std::ostream& out, const SubrangeBound& bound) throw() {
   return out;
 }
 
+inline std::ostream&
+operator<<(std::ostream& out, const SubrangeBounds& bounds) throw() CVC4_PUBLIC;
+
+inline std::ostream&
+operator<<(std::ostream& out, const SubrangeBounds& bounds) throw() {
+  out << bounds.lower << ".." << bounds.upper;
+
+  return out;
+}
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__SUBRANGE_BOUND_H */