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.)

5 files changed, 24 insertions, 9 deletions

diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 6e10c9a8a..610902270 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -63,7 +63,7 @@ CommandExecutorPortfolio::CommandExecutorPortfolio
   d_stats.registerStat_(&d_statLastWinner);
   d_stats.registerStat_(&d_statWaitTime);
 
-  /* Duplication, Individualisation */
+  /* Duplication, individualization */
   d_exprMgrs.push_back(&d_exprMgr);
   for(unsigned i = 1; i < d_numThreads; ++i) {
     d_exprMgrs.push_back(new ExprManager(d_threadOptions[i]));
@@ -202,6 +202,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
             dynamic_cast<GetAssignmentCommand*>(cmd) != NULL ||
             dynamic_cast<GetModelCommand*>(cmd) != NULL ||
             dynamic_cast<GetProofCommand*>(cmd) != NULL ||
+            dynamic_cast<GetInstantiationsCommand*>(cmd) != NULL ||
             dynamic_cast<GetUnsatCoreCommand*>(cmd) != NULL ||
             dynamic_cast<GetAssertionsCommand*>(cmd) != NULL ||
             dynamic_cast<GetInfoCommand*>(cmd) != NULL ||
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 5fbd5aff5..f9b222b2b 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -35,9 +35,11 @@
 #include "util/configuration.h"
 #include "options/options.h"
 #include "main/command_executor.h"
-# ifdef PORTFOLIO_BUILD
-#    include "main/command_executor_portfolio.h"
-# endif
+
+#ifdef PORTFOLIO_BUILD
+#  include "main/command_executor_portfolio.h"
+#endif
+
 #include "main/options.h"
 #include "smt/options.h"
 #include "util/output.h"
@@ -185,7 +187,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     } else {
       unsigned len = strlen(filename);
       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
-        opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2);
+        opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2_5);
       } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
         opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V1);
       } else if(len >= 5 && !strcmp(".smt1", filename + len - 5)) {
@@ -373,6 +375,10 @@ int runCvc4(int argc, char* argv[], Options& opts) {
           }
           status = pExecutor->doCommand(cmd);
           needReset = true;
+        } else if(dynamic_cast<ResetCommand*>(cmd) != NULL) {
+          pExecutor->doCommand(cmd);
+          allCommands.clear();
+          allCommands.push_back(vector<Command*>());
         } else {
           // We shouldn't copy certain commands, because they can cause
           // an error on replay since there's no associated sat/unsat check
@@ -382,7 +388,10 @@ int runCvc4(int argc, char* argv[], Options& opts) {
              dynamic_cast<GetValueCommand*>(cmd) == NULL &&
              dynamic_cast<GetModelCommand*>(cmd) == NULL &&
              dynamic_cast<GetAssignmentCommand*>(cmd) == NULL &&
-             dynamic_cast<GetInstantiationsCommand*>(cmd) == NULL) {
+             dynamic_cast<GetInstantiationsCommand*>(cmd) == NULL &&
+             dynamic_cast<GetAssertionsCommand*>(cmd) == NULL &&
+             dynamic_cast<GetInfoCommand*>(cmd) == NULL &&
+             dynamic_cast<GetOptionCommand*>(cmd) == NULL) {
             Command* copy = cmd->clone();
             allCommands.back().push_back(copy);
           }
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index bdc956535..0aee195e4 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -123,7 +123,8 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
       commandsBegin = smt1_commands;
       commandsEnd = smt1_commands + sizeof(smt1_commands) / sizeof(*smt1_commands);
       break;
-    case output::LANG_SMTLIB_V2:
+    case output::LANG_SMTLIB_V2_0:
+    case output::LANG_SMTLIB_V2_5:
       d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2";
       commandsBegin = smt2_commands;
       commandsEnd = smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands);
@@ -323,7 +324,8 @@ restart:
     line += "\n";
     goto restart;
   } catch(ParserException& pe) {
-    if(d_options[options::outputLanguage] == output::LANG_SMTLIB_V2) {
+    if(d_options[options::outputLanguage] == output::LANG_SMTLIB_V2_0 ||
+       d_options[options::outputLanguage] == output::LANG_SMTLIB_V2_5) {
       d_out << "(error \"" << pe << "\")" << endl;
     } else {
       d_out << pe << endl;
diff --git a/src/main/main.cpp b/src/main/main.cpp
index ca7266b59..a70c3c7c3 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -65,7 +65,8 @@ int main(int argc, char* argv[]) {
 #ifdef CVC4_COMPETITION_MODE
     *opts[options::out] << "unknown" << endl;
 #endif
-    if(opts[options::outputLanguage] == output::LANG_SMTLIB_V2) {
+    if(opts[options::outputLanguage] == output::LANG_SMTLIB_V2_0 ||
+       opts[options::outputLanguage] == output::LANG_SMTLIB_V2_5) {
       *opts[options::err] << "(error \"" << e << "\")" << endl;
     } else {
       *opts[options::err] << "CVC4 Error:" << endl << e << endl;
diff --git a/src/main/options b/src/main/options
index 6cc6a0ca0..18cc08ed7 100644
--- a/src/main/options
+++ b/src/main/options
@@ -41,6 +41,8 @@ option fallbackSequential  --fallback-sequential bool :default false
 option incrementalParallel --incremental-parallel bool :default false :link --incremental
  Use parallel solver even in incremental mode (may print 'unknown's at times)
 
+option interactive : --interactive bool :read-write
+ force interactive/non-interactive mode
 undocumented-option interactivePrompt /--no-interactive-prompt bool :default true
  turn off interactive prompting while in interactive mode