Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.

* support for new commands meta-info, declare-const, echo, get-model,
  reset, and reset-assertions
* support for set-option :global-declarations
* support for set-option :produce-assertions
* support for set-option :reproducible-resource-limit
* support for get-info :assertion-stack-levels
* support for set-info :smt-lib-version 2.5
* ascribe types for abstract values (the new 2.5 standard clarifies that
  this is required)
* SMT-LIB v2.5 string literals (we still support 2.0 string literals when
  in 2.0 mode)

What's still to do:
* check-sat-assumptions/get-unsat-assumptions (still being hotly debated).
  Also set-option :produce-unsat-assumptions.
* define-fun-rec doesn't allow mutual recursion
* All options should be restored to defaults with (reset) command.
  (Currently :incremental and maybe others get "stuck" due to late driver
  integration.)

3 files changed, 34 insertions, 1 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index c976588d4..be1b06cb8 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -385,6 +385,29 @@ std::string ResetCommand::getCommandName() const throw() {
   return "reset";
 }
 
+/* class ResetAssertionsCommand */
+
+void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    smtEngine->resetAssertions();
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+Command* ResetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  return new ResetAssertionsCommand();
+}
+
+Command* ResetAssertionsCommand::clone() const {
+  return new ResetAssertionsCommand();
+}
+
+std::string ResetAssertionsCommand::getCommandName() const throw() {
+  return "reset-assertions";
+}
+
 /* class QuitCommand */
 
 void QuitCommand::invoke(SmtEngine* smtEngine) throw() {
diff --git a/src/expr/command.h b/src/expr/command.h
index 75cf80aae..c4f2fc1bc 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -807,6 +807,16 @@ public:
   std::string getCommandName() const throw();
 };/* class ResetCommand */
 
+class CVC4_PUBLIC ResetAssertionsCommand : public Command {
+public:
+  ResetAssertionsCommand() throw() {}
+  ~ResetAssertionsCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
+  std::string getCommandName() const throw();
+};/* class ResetAssertionsCommand */
+
 class CVC4_PUBLIC QuitCommand : public Command {
 public:
   QuitCommand() throw() {}
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index c5e8e77de..d769ed109 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -985,7 +985,7 @@ inline std::ostream& operator<<(std::ostream& out, ExprDag d) {
  * Use like this:
  *
  *   // let out be an ostream, e an Expr
- *   out << Expr::setlanguage(LANG_SMTLIB_V2) << e << endl;
+ *   out << Expr::setlanguage(LANG_SMTLIB_V2_5) << e << endl;
  *
  * The setting stays permanently (until set again) with the stream.
  */