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.

1 files changed, 278 insertions, 122 deletions

diff --git a/src/expr/command.h b/src/expr/command.h
index b686025fe..cf8c1b615 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -41,9 +41,12 @@ namespace CVC4 {
 
 class SmtEngine;
 class Command;
+class CommandStatus;
 
-std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const Command&) throw() CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const CommandStatus*) throw() CVC4_PUBLIC;
 
 /** The status an SMT benchmark can have */
 enum BenchmarkStatus {
@@ -56,21 +59,156 @@ enum BenchmarkStatus {
 };
 
 std::ostream& operator<<(std::ostream& out,
-                         BenchmarkStatus status) CVC4_PUBLIC;
+                         BenchmarkStatus status) throw() CVC4_PUBLIC;
+
+/**
+ * IOStream manipulator to print success messages or not.
+ *
+ *   out << Command::printsuccess(false) << CommandSuccess();
+ *
+ * prints nothing, but
+ *
+ *   out << Command::printsuccess(true) << CommandSuccess();
+ *
+ * prints a success message (in a manner appropriate for the current
+ * output language).
+ */
+class CVC4_PUBLIC CommandPrintSuccess {
+  /**
+   * The allocated index in ios_base for our depth setting.
+   */
+  static const int s_iosIndex;
+
+  /**
+   * The default setting, for ostreams that haven't yet had a
+   * setdepth() applied to them.
+   */
+  static const int s_defaultPrintSuccess = false;
+
+  /**
+   * When this manipulator is used, the setting is stored here.
+   */
+  bool d_printSuccess;
+
+public:
+  /**
+   * Construct a CommandPrintSuccess with the given setting.
+   */
+  CommandPrintSuccess(bool printSuccess) throw() : d_printSuccess(printSuccess) {}
+
+  inline void applyPrintSuccess(std::ostream& out) throw() {
+    out.iword(s_iosIndex) = d_printSuccess;
+  }
+
+  static inline bool getPrintSuccess(std::ostream& out) throw() {
+    return out.iword(s_iosIndex);
+  }
+
+  static inline void setPrintSuccess(std::ostream& out, bool printSuccess) throw() {
+    out.iword(s_iosIndex) = printSuccess;
+  }
+
+  /**
+   * Set the print-success state on the output stream for the current
+   * stack scope.  This makes sure the old state is reset on the
+   * stream after normal OR exceptional exit from the scope, using the
+   * RAII C++ idiom.
+   */
+  class Scope {
+    std::ostream& d_out;
+    bool d_oldPrintSuccess;
+
+  public:
+
+    inline Scope(std::ostream& out, bool printSuccess) throw() :
+      d_out(out),
+      d_oldPrintSuccess(CommandPrintSuccess::getPrintSuccess(out)) {
+      CommandPrintSuccess::setPrintSuccess(out, printSuccess);
+    }
+
+    inline ~Scope() throw() {
+      CommandPrintSuccess::setPrintSuccess(d_out, d_oldPrintSuccess);
+    }
+
+  };/* class CommandPrintSuccess::Scope */
+
+};/* class CommandPrintSuccess */
+
+/**
+ * Sets the default print-success setting when pretty-printing an Expr
+ * to an ostream.  Use like this:
+ *
+ *   // let out be an ostream, e an Expr
+ *   out << Expr::setdepth(n) << e << endl;
+ *
+ * The depth stays permanently (until set again) with the stream.
+ */
+inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() {
+  cps.applyPrintSuccess(out);
+  return out;
+}
+
+class CVC4_PUBLIC CommandStatus {
+protected:
+  // shouldn't construct a CommandStatus (use a derived class)
+  CommandStatus() throw() {}
+public:
+  virtual ~CommandStatus() throw() {}
+  void toStream(std::ostream& out,
+                OutputLanguage language = language::output::LANG_AST) const throw();
+};/* class CommandStatus */
+
+class CVC4_PUBLIC CommandSuccess : public CommandStatus {
+  static const CommandSuccess* s_instance;
+public:
+  static const CommandSuccess* instance() throw() { return s_instance; }
+};/* class CommandSuccess */
+
+class CVC4_PUBLIC CommandUnsupported : public CommandStatus {
+};/* class CommandSuccess */
+
+class CVC4_PUBLIC CommandFailure : public CommandStatus {
+  std::string d_message;
+public:
+  CommandFailure(std::string message) throw() : d_message(message) {}
+  ~CommandFailure() throw() {}
+  std::string getMessage() const throw() { return d_message; }
+};/* class CommandFailure */
 
 class CVC4_PUBLIC Command {
+protected:
+  /**
+   * This field contains a command status if the command has been
+   * invoked, or NULL if it has not.  This field is either a
+   * dynamically-allocated pointer, or it's a pointer to the singleton
+   * CommandSuccess instance.  Doing so is somewhat asymmetric, but
+   * it avoids the need to dynamically allocate memory in the common
+   * case of a successful command.
+   */
+  const CommandStatus* d_commandStatus;
+
 public:
-  virtual ~Command() {}
+  typedef CommandPrintSuccess printsuccess;
+
+  Command() throw();
+  virtual ~Command() throw();
 
-  virtual void invoke(SmtEngine* smtEngine) = 0;
-  virtual void invoke(SmtEngine* smtEngine, std::ostream& out);
+  virtual void invoke(SmtEngine* smtEngine) throw() = 0;
+  virtual void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
 
   virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false,
-                        OutputLanguage language = language::output::LANG_AST) const;
+                        OutputLanguage language = language::output::LANG_AST) const throw();
+
+  std::string toString() const throw();
+
+  /** Either the command hasn't run yet, or it completed successfully. */
+  bool ok() const throw();
 
-  std::string toString() const;
+  /** Get the command status (it's NULL if we haven't run yet). */
+  const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; }
 
-  virtual void printResult(std::ostream& out) const;
+  virtual void printResult(std::ostream& out) const throw();
 
 };/* class Command */
 
@@ -82,45 +220,51 @@ class CVC4_PUBLIC EmptyCommand : public Command {
 protected:
   std::string d_name;
 public:
-  EmptyCommand(std::string name = "");
-  std::string getName() const;
-  void invoke(SmtEngine* smtEngine);
+  EmptyCommand(std::string name = "") throw();
+  ~EmptyCommand() throw() {}
+  std::string getName() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class EmptyCommand */
 
 class CVC4_PUBLIC AssertCommand : public Command {
 protected:
   BoolExpr d_expr;
 public:
-  AssertCommand(const BoolExpr& e);
-  BoolExpr getExpr() const;
-  void invoke(SmtEngine* smtEngine);
+  AssertCommand(const BoolExpr& e) throw();
+  ~AssertCommand() throw() {}
+  BoolExpr getExpr() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class AssertCommand */
 
 class CVC4_PUBLIC PushCommand : public Command {
 public:
-  void invoke(SmtEngine* smtEngine);
+  ~PushCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class PushCommand */
 
 class CVC4_PUBLIC PopCommand : public Command {
 public:
-  void invoke(SmtEngine* smtEngine);
+  ~PopCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class PopCommand */
 
 class CVC4_PUBLIC DeclarationDefinitionCommand : public Command {
 protected:
   std::string d_symbol;
 public:
-  DeclarationDefinitionCommand(const std::string& id);
-  std::string getSymbol() const;
+  DeclarationDefinitionCommand(const std::string& id) throw();
+  ~DeclarationDefinitionCommand() throw() {}
+  std::string getSymbol() const throw();
 };/* class DeclarationDefinitionCommand */
 
 class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand {
 protected:
   Type d_type;
 public:
-  DeclareFunctionCommand(const std::string& id, Type type);
-  Type getType() const;
-  void invoke(SmtEngine* smtEngine);
+  DeclareFunctionCommand(const std::string& id, Type type) throw();
+  ~DeclareFunctionCommand() throw() {}
+  Type getType() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class DeclareFunctionCommand */
 
 class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand {
@@ -128,10 +272,11 @@ protected:
   size_t d_arity;
   Type d_type;
 public:
-  DeclareTypeCommand(const std::string& id, size_t arity, Type t);
-  size_t getArity() const;
-  Type getType() const;
-  void invoke(SmtEngine* smtEngine);
+  DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw();
+  ~DeclareTypeCommand() throw() {}
+  size_t getArity() const throw();
+  Type getType() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class DeclareTypeCommand */
 
 class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand {
@@ -139,11 +284,12 @@ protected:
   std::vector<Type> d_params;
   Type d_type;
 public:
-  DefineTypeCommand(const std::string& id, Type t);
-  DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t);
-  const std::vector<Type>& getParameters() const;
-  Type getType() const;
-  void invoke(SmtEngine* smtEngine);
+  DefineTypeCommand(const std::string& id, Type t) throw();
+  DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t) throw();
+  ~DefineTypeCommand() throw() {}
+  const std::vector<Type>& getParameters() const throw();
+  Type getType() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class DefineTypeCommand */
 
 class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand {
@@ -152,13 +298,14 @@ protected:
   std::vector<Expr> d_formals;
   Expr d_formula;
 public:
-  DefineFunctionCommand(const std::string& id, Expr func, Expr formula);
+  DefineFunctionCommand(const std::string& id, Expr func, Expr formula) throw();
   DefineFunctionCommand(const std::string& id, Expr func,
-                        const std::vector<Expr>& formals, Expr formula);
-  Expr getFunction() const;
-  const std::vector<Expr>& getFormals() const;
-  Expr getFormula() const;
-  void invoke(SmtEngine* smtEngine);
+                        const std::vector<Expr>& formals, Expr formula) throw();
+  ~DefineFunctionCommand() throw() {}
+  Expr getFunction() const throw();
+  const std::vector<Expr>& getFormals() const throw();
+  Expr getFormula() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class DefineFunctionCommand */
 
 /**
@@ -169,8 +316,8 @@ public:
 class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand {
 public:
   DefineNamedFunctionCommand(const std::string& id, Expr func,
-                             const std::vector<Expr>& formals, Expr formula);
-  void invoke(SmtEngine* smtEngine);
+                             const std::vector<Expr>& formals, Expr formula) throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class DefineNamedFunctionCommand */
 
 class CVC4_PUBLIC CheckSatCommand : public Command {
@@ -178,12 +325,13 @@ protected:
   BoolExpr d_expr;
   Result d_result;
 public:
-  CheckSatCommand();
-  CheckSatCommand(const BoolExpr& expr);
-  BoolExpr getExpr() const;
-  void invoke(SmtEngine* smtEngine);
-  Result getResult() const;
-  void printResult(std::ostream& out) const;
+  CheckSatCommand() throw();
+  CheckSatCommand(const BoolExpr& expr) throw();
+  ~CheckSatCommand() throw() {}
+  BoolExpr getExpr() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  Result getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class CheckSatCommand */
 
 class CVC4_PUBLIC QueryCommand : public Command {
@@ -191,11 +339,12 @@ protected:
   BoolExpr d_expr;
   Result d_result;
 public:
-  QueryCommand(const BoolExpr& e);
-  BoolExpr getExpr() const;
-  void invoke(SmtEngine* smtEngine);
-  Result getResult() const;
-  void printResult(std::ostream& out) const;
+  QueryCommand(const BoolExpr& e) throw();
+  ~QueryCommand() throw() {}
+  BoolExpr getExpr() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  Result getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class QueryCommand */
 
 // this is TRANSFORM in the CVC presentation language
@@ -204,11 +353,12 @@ protected:
   Expr d_term;
   Expr d_result;
 public:
-  SimplifyCommand(Expr term);
-  Expr getTerm() const;
-  void invoke(SmtEngine* smtEngine);
-  Expr getResult() const;
-  void printResult(std::ostream& out) const;
+  SimplifyCommand(Expr term) throw();
+  ~SimplifyCommand() throw() {}
+  Expr getTerm() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  Expr getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class SimplifyCommand */
 
 class CVC4_PUBLIC GetValueCommand : public Command {
@@ -216,75 +366,77 @@ protected:
   Expr d_term;
   Expr d_result;
 public:
-  GetValueCommand(Expr term);
-  Expr getTerm() const;
-  void invoke(SmtEngine* smtEngine);
-  Expr getResult() const;
-  void printResult(std::ostream& out) const;
+  GetValueCommand(Expr term) throw();
+  ~GetValueCommand() throw() {}
+  Expr getTerm() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  Expr getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class GetValueCommand */
 
 class CVC4_PUBLIC GetAssignmentCommand : public Command {
 protected:
   SExpr d_result;
 public:
-  GetAssignmentCommand();
-  void invoke(SmtEngine* smtEngine);
-  SExpr getResult() const;
-  void printResult(std::ostream& out) const;
+  GetAssignmentCommand() throw();
+  ~GetAssignmentCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
+  SExpr getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class GetAssignmentCommand */
 
 class CVC4_PUBLIC GetProofCommand : public Command {
 protected:
   Proof* d_result;
 public:
-  GetProofCommand();
-  void invoke(SmtEngine* smtEngine);
-  Proof* getResult() const;
-  void printResult(std::ostream& out) const;
+  GetProofCommand() throw();
+  ~GetProofCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
+  Proof* getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class GetProofCommand */
 
 class CVC4_PUBLIC GetAssertionsCommand : public Command {
 protected:
   std::string d_result;
 public:
-  GetAssertionsCommand();
-  void invoke(SmtEngine* smtEngine);
-  std::string getResult() const;
-  void printResult(std::ostream& out) const;
+  GetAssertionsCommand() throw();
+  ~GetAssertionsCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
+  std::string getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class GetAssertionsCommand */
 
 class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
 protected:
-  std::string d_result;
   BenchmarkStatus d_status;
 public:
-  SetBenchmarkStatusCommand(BenchmarkStatus status);
-  BenchmarkStatus getStatus() const;
-  void invoke(SmtEngine* smtEngine);
+  SetBenchmarkStatusCommand(BenchmarkStatus status) throw();
+  ~SetBenchmarkStatusCommand() throw() {}
+  BenchmarkStatus getStatus() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class SetBenchmarkStatusCommand */
 
 class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
 protected:
-  std::string d_result;
   std::string d_logic;
 public:
-  SetBenchmarkLogicCommand(std::string logic);
-  std::string getLogic() const;
-  void invoke(SmtEngine* smtEngine);
+  SetBenchmarkLogicCommand(std::string logic) throw();
+  ~SetBenchmarkLogicCommand() throw() {}
+  std::string getLogic() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class SetBenchmarkLogicCommand */
 
 class CVC4_PUBLIC SetInfoCommand : public Command {
 protected:
   std::string d_flag;
   SExpr d_sexpr;
-  std::string d_result;
 public:
-  SetInfoCommand(std::string flag, const SExpr& sexpr);
-  std::string getFlag() const;
-  SExpr getSExpr() const;
-  void invoke(SmtEngine* smtEngine);
-  std::string getResult() const;
-  void printResult(std::ostream& out) const;
+  SetInfoCommand(std::string flag, const SExpr& sexpr) throw();
+  ~SetInfoCommand() throw() {}
+  std::string getFlag() const throw();
+  SExpr getSExpr() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class SetInfoCommand */
 
 class CVC4_PUBLIC GetInfoCommand : public Command {
@@ -292,25 +444,24 @@ protected:
   std::string d_flag;
   std::string d_result;
 public:
-  GetInfoCommand(std::string flag);
-  std::string getFlag() const;
-  void invoke(SmtEngine* smtEngine);
-  std::string getResult() const;
-  void printResult(std::ostream& out) const;
+  GetInfoCommand(std::string flag) throw();
+  ~GetInfoCommand() throw() {}
+  std::string getFlag() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  std::string getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class GetInfoCommand */
 
 class CVC4_PUBLIC SetOptionCommand : public Command {
 protected:
   std::string d_flag;
   SExpr d_sexpr;
-  std::string d_result;
 public:
-  SetOptionCommand(std::string flag, const SExpr& sexpr);
-  std::string getFlag() const;
-  SExpr getSExpr() const;
-  void invoke(SmtEngine* smtEngine);
-  std::string getResult() const;
-  void printResult(std::ostream& out) const;
+  SetOptionCommand(std::string flag, const SExpr& sexpr) throw();
+  ~SetOptionCommand() throw() {}
+  std::string getFlag() const throw();
+  SExpr getSExpr() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class SetOptionCommand */
 
 class CVC4_PUBLIC GetOptionCommand : public Command {
@@ -318,35 +469,39 @@ protected:
   std::string d_flag;
   std::string d_result;
 public:
-  GetOptionCommand(std::string flag);
-  std::string getFlag() const;
-  void invoke(SmtEngine* smtEngine);
-  std::string getResult() const;
-  void printResult(std::ostream& out) const;
+  GetOptionCommand(std::string flag) throw();
+  ~GetOptionCommand() throw() {}
+  std::string getFlag() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  std::string getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class GetOptionCommand */
 
 class CVC4_PUBLIC DatatypeDeclarationCommand : public Command {
 private:
   std::vector<DatatypeType> d_datatypes;
 public:
-  DatatypeDeclarationCommand(const DatatypeType& datatype);
-  DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes);
-  const std::vector<DatatypeType>& getDatatypes() const;
-  void invoke(SmtEngine* smtEngine);
+  DatatypeDeclarationCommand(const DatatypeType& datatype) throw();
+  ~DatatypeDeclarationCommand() throw() {}
+  DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw();
+  const std::vector<DatatypeType>& getDatatypes() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class DatatypeDeclarationCommand */
 
 class CVC4_PUBLIC QuitCommand : public Command {
 public:
-  QuitCommand();
-  void invoke(SmtEngine* smtEngine);
+  QuitCommand() throw();
+  ~QuitCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class QuitCommand */
 
 class CVC4_PUBLIC CommentCommand : public Command {
   std::string d_comment;
 public:
-  CommentCommand(std::string comment);
-  std::string getComment() const;
-  void invoke(SmtEngine* smtEngine);
+  CommentCommand(std::string comment) throw();
+  ~CommentCommand() throw() {}
+  std::string getComment() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class CommentCommand */
 
 class CVC4_PUBLIC CommandSequence : public Command {
@@ -356,27 +511,28 @@ private:
   /** Next command to be executed */
   unsigned int d_index;
 public:
-  CommandSequence();
-  ~CommandSequence();
+  CommandSequence() throw();
+  ~CommandSequence() throw();
 
-  void addCommand(Command* cmd);
+  void addCommand(Command* cmd) throw();
 
-  void invoke(SmtEngine* smtEngine);
-  void invoke(SmtEngine* smtEngine, std::ostream& out);
+  void invoke(SmtEngine* smtEngine) throw();
+  void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
 
   typedef std::vector<Command*>::iterator iterator;
   typedef std::vector<Command*>::const_iterator const_iterator;
 
-  const_iterator begin() const;
-  const_iterator end() const;
+  const_iterator begin() const throw();
+  const_iterator end() const throw();
 
-  iterator begin();
-  iterator end();
+  iterator begin() throw();
+  iterator end() throw();
 
 };/* class CommandSequence */
 
 class CVC4_PUBLIC DeclarationSequence : public CommandSequence {
 public:
+  ~DeclarationSequence() throw() {}
 };/* class DeclarationSequence */
 
 }/* CVC4 namespace */