More language bindings work:

* with a patched SWIG, the ocaml bindings build correctly.
** I will provide my patch to the SWIG dev team.
* fixed some class interfaces to play more nicely with SWIG.
* php, perl, tcl now work; examples added.
* improved binding module building and installation.

Also:

Stop #defining NULL ((void*) 0).  This has been in cvc4_public.h for
a long, long time, I forget why I added it in the first place, and
it's a very, very bad idea.  In C++, certain things are permitted
for NULL that aren't permitted for ((void*) 0), like for instance
implicit conversion to any pointer type.  We didn't see an issue
here (until now, when interfacing with SWIG), because GCC is usually
pretty smart at working around such a broken #definition of NULL.
But that's fragile.

New exception-free Command architecture.  Previously, some command
invocations were wrapped in a try {} catch() {} and printed out an
error.  This is much more consistent now.  Each Command invocation
results in a CommandStatus.  The status can be "unsupported",
"error", or "success" (these are each derived classes, though, not
strings, so that they can be easily printed in a language-specific
way... e.g., in SMT-LIBv2, they are printed in a manner consistent
with the spec, and "success" is not printed if the print-success
option is off.)  All Command functionality are now no-throw
functions, which @cconway reports is a Good Thing for Google
(where all C++ exceptions are suspect), and also I think is much
cleaner than the old way in this instance.

Added an --smtlib2 option that enables an "SMT-LIBv2 compliance
mode"---really it just sets a few other options like strictParsing,
inputLanguage, and printSuccess.  In the future we might put other
options into a compliance mode, or we might choose to make it the
default.

8 files changed, 100 insertions, 91 deletions

diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp
index b8a79cd9e..8aba4ad41 100644
--- a/src/util/cardinality.cpp
+++ b/src/util/cardinality.cpp
@@ -24,9 +24,9 @@ const Integer Cardinality::s_unknownCard(0);
 const Integer Cardinality::s_intCard(-1);
 const Integer Cardinality::s_realCard(-2);
 
-const Cardinality Cardinality::INTEGERS(Cardinality::Beth(0));
-const Cardinality Cardinality::REALS(Cardinality::Beth(1));
-const Cardinality Cardinality::UNKNOWN((Cardinality::Unknown()));
+const Cardinality Cardinality::INTEGERS(CardinalityBeth(0));
+const Cardinality Cardinality::REALS(CardinalityBeth(1));
+const Cardinality Cardinality::UNKNOWN((CardinalityUnknown()));
 
 Cardinality& Cardinality::operator+=(const Cardinality& c) throw() {
   if(isUnknown()) {
@@ -127,7 +127,7 @@ std::string Cardinality::toString() const throw() {
 }
 
 
-std::ostream& operator<<(std::ostream& out, Cardinality::Beth b) throw() {
+std::ostream& operator<<(std::ostream& out, CardinalityBeth b) throw() {
   out << "beth[" << b.getNumber() << ']';
 
   return out;
@@ -140,7 +140,7 @@ std::ostream& operator<<(std::ostream& out, const Cardinality& c) throw() {
   } else if(c.isFinite()) {
     out << c.getFiniteCardinality();
   } else {
-    out << Cardinality::Beth(c.getBethNumber());
+    out << CardinalityBeth(c.getBethNumber());
   }
 
   return out;
diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index e08f09bb6..057bb0b0c 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -31,6 +31,35 @@
 namespace CVC4 {
 
 /**
+ * Representation for a Beth number, used only to construct
+ * Cardinality objects.
+ */
+class CVC4_PUBLIC CardinalityBeth {
+  Integer d_index;
+
+public:
+  CardinalityBeth(const Integer& beth) : d_index(beth) {
+    CheckArgument(beth >= 0, beth,
+                  "Beth index must be a nonnegative integer, not %s.",
+                  beth.toString().c_str());
+  }
+
+  const Integer& getNumber() const throw() {
+    return d_index;
+  }
+
+};/* class CardinalityBeth */
+
+/**
+ * Representation for an unknown cardinality.
+ */
+class CVC4_PUBLIC CardinalityUnknown {
+public:
+  CardinalityUnknown() throw() {}
+  ~CardinalityUnknown() throw() {}
+};/* class CardinalityUnknown */
+
+/**
  * A simple representation of a cardinality.  We store an
  * arbitrary-precision integer for finite cardinalities, and we
  * distinguish infinite cardinalities represented as Beth numbers.
@@ -65,34 +94,6 @@ public:
   static const Cardinality UNKNOWN;
 
   /**
-   * Representation for a Beth number, used only to construct
-   * Cardinality objects.
-   */
-  class CVC4_PUBLIC Beth {
-    Integer d_index;
-
-  public:
-    Beth(const Integer& beth) : d_index(beth) {
-      CheckArgument(beth >= 0, beth,
-                    "Beth index must be a nonnegative integer, not %s.",
-                    beth.toString().c_str());
-    }
-
-    const Integer& getNumber() const throw() {
-      return d_index;
-    }
-  };/* class Cardinality::Beth */
-
-  /**
-   * Representation for an unknown cardinality.
-   */
-  class CVC4_PUBLIC Unknown {
-  public:
-    Unknown() throw() {}
-    ~Unknown() throw() {}
-  };/* class Cardinality::Unknown */
-
-  /**
    * Construct a finite cardinality equal to the integer argument.
    * The argument must be nonnegative.  If we change this to an
    * "unsigned" argument to enforce the restriction, we mask some
@@ -120,14 +121,14 @@ public:
   /**
    * Construct an infinite cardinality equal to the given Beth number.
    */
-  Cardinality(Beth beth) : d_card(-beth.getNumber() - 1) {
+  Cardinality(CardinalityBeth beth) : d_card(-beth.getNumber() - 1) {
     Assert(!isFinite());
   }
 
   /**
    * Construct an unknown cardinality.
    */
-  Cardinality(Unknown) : d_card(0) {
+  Cardinality(CardinalityUnknown) : d_card(0) {
   }
 
   /** Returns true iff this cardinality is unknown. */
@@ -256,7 +257,7 @@ public:
 
 
 /** Print an element of the InfiniteCardinality enumeration. */
-std::ostream& operator<<(std::ostream& out, Cardinality::Beth b)
+std::ostream& operator<<(std::ostream& out, CardinalityBeth b)
   throw() CVC4_PUBLIC;
 
 
diff --git a/src/util/cardinality.i b/src/util/cardinality.i
index 4e1382f87..c88037cfe 100644
--- a/src/util/cardinality.i
+++ b/src/util/cardinality.i
@@ -2,7 +2,7 @@
 #include "util/cardinality.h"
 %}
 
-%feature("valuewrapper") CVC4::Cardinality::Beth;
+%feature("valuewrapper") CVC4::CardinalityBeth;
 
 %rename(plusAssign) CVC4::Cardinality::operator+=(const Cardinality&);
 %rename(timesAssign) CVC4::Cardinality::operator*=(const Cardinality&);
@@ -18,36 +18,6 @@
 %rename(greaterEqual) CVC4::Cardinality::operator>=(const Cardinality&) const;
 
 %ignore CVC4::operator<<(std::ostream&, const Cardinality&);
-%ignore CVC4::operator<<(std::ostream&, Cardinality::Beth);
-
-namespace CVC4 {
-  class Beth {
-    Integer d_index;
-
-  public:
-    Beth(const Integer& beth) : d_index(beth) {
-      CheckArgument(beth >= 0, beth,
-                    "Beth index must be a nonnegative integer, not %s.",
-                    beth.toString().c_str());
-    }
-
-    const Integer& getNumber() const throw() {
-      return d_index;
-    }
-  };/* class Cardinality::Beth */
-
-  class Unknown {
-  public:
-    Unknown() throw() {}
-    ~Unknown() throw() {}
-  };/* class Cardinality::Unknown */
-}
+%ignore CVC4::operator<<(std::ostream&, CardinalityBeth);
 
 %include "util/cardinality.h"
-
-%{
-namespace CVC4 {
-  typedef CVC4::Cardinality::Beth Beth;
-  typedef CVC4::Cardinality::Unknown Unknown;
-}
-%}
diff --git a/src/util/exception.h b/src/util/exception.h
index 43a0354ca..fe01eba36 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -24,25 +24,29 @@
 #include <iostream>
 #include <string>
 #include <sstream>
+#include <exception>
 
 namespace CVC4 {
 
-class CVC4_PUBLIC Exception {
+class CVC4_PUBLIC Exception : public std::exception {
 protected:
   std::string d_msg;
 
 public:
   // Constructors
-  Exception() : d_msg("Unknown exception") {}
-  Exception(const std::string& msg) : d_msg(msg) {}
-  Exception(const char* msg) : d_msg(msg) {}
+  Exception() throw() : d_msg("Unknown exception") {}
+  Exception(const std::string& msg) throw() : d_msg(msg) {}
+  Exception(const char* msg) throw() : d_msg(msg) {}
 
   // Destructor
   virtual ~Exception() throw() {}
 
   // NON-VIRTUAL METHOD for setting and printing the error message
-  void setMessage(const std::string& msg) { d_msg = msg; }
-  std::string getMessage() const { return d_msg; }
+  void setMessage(const std::string& msg) throw() { d_msg = msg; }
+  std::string getMessage() const throw() { return d_msg; }
+
+  // overridden from base class std::exception
+  virtual const char* what() const throw() { return d_msg.c_str(); }
 
   /**
    * Get this exception as a string.  Note that
@@ -56,7 +60,7 @@ public:
    * toString(), there is no stream, so the parameters are default
    * and you'll get exprs and types printed using the AST language.
    */
-  std::string toString() const {
+  std::string toString() const throw() {
     std::stringstream ss;
     toStream(ss);
     return ss.str();
@@ -67,12 +71,12 @@ public:
    * a derived class, it's recommended that this method print the
    * type of exception before the actual message.
    */
-  virtual void toStream(std::ostream& os) const { os << d_msg; }
+  virtual void toStream(std::ostream& os) const throw() { os << d_msg; }
 
 };/* class Exception */
 
-inline std::ostream& operator<<(std::ostream& os, const Exception& e) CVC4_PUBLIC;
-inline std::ostream& operator<<(std::ostream& os, const Exception& e) {
+inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() {
   e.toStream(os);
   return os;
 }
diff --git a/src/util/exception.i b/src/util/exception.i
index 52ff28922..ab6284633 100644
--- a/src/util/exception.i
+++ b/src/util/exception.i
@@ -2,7 +2,7 @@
 #include "util/exception.h"
 %}
 
-%ignore CVC4::operator<<(std::ostream&, const Exception&);
-%ignore CVC4::Exception::Exception(const char*);
+%ignore CVC4::operator<<(std::ostream&, const Exception&) throw();
+%ignore CVC4::Exception::Exception(const char*) throw();
 
 %include "util/exception.h"
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 94ddf082f..842bd84b2 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -27,6 +27,7 @@
 #include <getopt.h>
 
 #include "expr/expr.h"
+#include "expr/command.h"
 #include "util/configuration.h"
 #include "util/exception.h"
 #include "util/language.h"
@@ -118,6 +119,8 @@ Most commonly-used CVC4 options:\n\
    --no-interactive       force non-interactive mode\n\
    --produce-models | -m  support the get-value command\n\
    --produce-assignments  support the get-assignment command\n\
+   --print-success        print the \"success\" output required of SMT-LIBv2\n\
+   --smtlib2              SMT-LIBv2 conformance mode (implies other options)\n\
    --proof                turn on proof generation\n\
    --incremental | -i     enable incremental solving\n\
    --tlimit=MS            enable time limiting (give milliseconds)\n\
@@ -306,6 +309,8 @@ enum OptionValue {
   INTERACTIVE,
   NO_INTERACTIVE,
   PRODUCE_ASSIGNMENTS,
+  PRINT_SUCCESS,
+  SMTLIB2,
   PROOF,
   NO_TYPE_CHECKING,
   LAZY_TYPE_CHECKING,
@@ -384,6 +389,8 @@ static struct option cmdlineOptions[] = {
   { "no-interactive", no_argument   , NULL, NO_INTERACTIVE },
   { "produce-models", no_argument   , NULL, 'm' },
   { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS },
+  { "print-success", no_argument, NULL, PRINT_SUCCESS },
+  { "smtlib2", no_argument, NULL, SMTLIB2 },
   { "proof", no_argument, NULL, PROOF },
   { "no-type-checking", no_argument , NULL, NO_TYPE_CHECKING },
   { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING },
@@ -597,14 +604,12 @@ throw(OptionException) {
       break;
 
     case PRINT_EXPR_TYPES:
-      {
-        Debug.getStream() << Expr::printtypes(true);
-        Trace.getStream() << Expr::printtypes(true);
-        Notice.getStream() << Expr::printtypes(true);
-        Chat.getStream() << Expr::printtypes(true);
-        Message.getStream() << Expr::printtypes(true);
-        Warning.getStream() << Expr::printtypes(true);
-      }
+      Debug.getStream() << Expr::printtypes(true);
+      Trace.getStream() << Expr::printtypes(true);
+      Notice.getStream() << Expr::printtypes(true);
+      Chat.getStream() << Expr::printtypes(true);
+      Message.getStream() << Expr::printtypes(true);
+      Warning.getStream() << Expr::printtypes(true);
       break;
 
     case LAZY_DEFINITION_EXPANSION:
@@ -648,7 +653,27 @@ throw(OptionException) {
     case PRODUCE_ASSIGNMENTS:
       produceAssignments = true;
       break;
-      
+
+    case SMTLIB2: // smtlib v2 compliance mode
+      inputLanguage = language::input::LANG_SMTLIB_V2;
+      outputLanguage = language::output::LANG_SMTLIB_V2;
+      strictParsing = true;
+      // make sure entire expressions are printed on all the non-debug, non-trace streams
+      Notice.getStream() << Expr::setdepth(-1);
+      Chat.getStream() << Expr::setdepth(-1);
+      Message.getStream() << Expr::setdepth(-1);
+      Warning.getStream() << Expr::setdepth(-1);
+      /* intentionally fall through */
+
+    case PRINT_SUCCESS:
+      Debug.getStream() << Command::printsuccess(true);
+      Trace.getStream() << Command::printsuccess(true);
+      Notice.getStream() << Command::printsuccess(true);
+      Chat.getStream() << Command::printsuccess(true);
+      Message.getStream() << Command::printsuccess(true);
+      Warning.getStream() << Command::printsuccess(true);
+      break;
+
     case PROOF:
 #ifdef CVC4_PROOF
       proof = true;
diff --git a/src/util/stats.h b/src/util/stats.h
index e955a7d28..719bbaab6 100644
--- a/src/util/stats.h
+++ b/src/util/stats.h
@@ -30,6 +30,7 @@
 #include <set>
 #include <ctime>
 #include <vector>
+#include <stdint.h>
 
 #include "util/Assert.h"
 
@@ -390,7 +391,6 @@ public:
 
 };/* class WrappedStat<T> */
 
-
 /**
  * A backed integer-valued (64-bit signed) statistic.
  * This doesn't functionally differ from its base class BackedStat<int64_t>,
@@ -655,7 +655,7 @@ class CVC4_PUBLIC CodeTimer;
  * arbitrarily, like a stopwatch; the value of the statistic at the
  * end is the accumulated time over all (start,stop) pairs.
  */
-class CVC4_PUBLIC TimerStat : public BackedStat< timespec > {
+class CVC4_PUBLIC TimerStat : public BackedStat<timespec> {
 
   // strange: timespec isn't placed in 'std' namespace ?!
   /** The last start time of this timer */
diff --git a/src/util/stats.i b/src/util/stats.i
index 5d3b81d4d..6f1ef5367 100644
--- a/src/util/stats.i
+++ b/src/util/stats.i
@@ -2,6 +2,14 @@
 #include "util/stats.h"
 %}
 
+namespace CVC4 {
+  template <class T> class CVC4_PUBLIC BackedStat;
+
+  %template(int64_t_BackedStat) BackedStat<int64_t>;
+  %template(double_BackedStat) BackedStat<double>;
+  %template(timespec_BackedStat) BackedStat<timespec>;
+}/* CVC4 namespace */
+
 %ignore CVC4::operator<<(std::ostream&, const timespec&);
 
 %rename(increment) CVC4::IntStat::operator++();
@@ -19,3 +27,4 @@
 %rename(greaterEqual) CVC4::operator>=(const timespec&, const timespec&);
 
 %include "util/stats.h"
+