From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 16 Jun 2014 23:59:24 +0000 (-0400)
Subject: Some fixes for tear-down-incremental and "success" output.
X-Git-Tag: cvc5-1.0.0~6758^2~31
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b8e28a7116d3410589bfdef8bb3ecccf98ac80b9;p=cvc5.git

Some fixes for tear-down-incremental and "success" output.
---

diff --git a/contrib/run-script-smtcomp2014-application b/contrib/run-script-smtcomp2014-application
index b04b33775..2decdb98a 100755
--- a/contrib/run-script-smtcomp2014-application
+++ b/contrib/run-script-smtcomp2014-application
@@ -9,7 +9,7 @@ function runcvc4 {
   # we run in this way for line-buffered input, otherwise memory's a
   # concern (plus it mimics what we'll end up getting from an
   # application-track trace runner?)
-  cat "$bench" | $cvc4 -L smt2 --print-success --no-checking --no-interactive --tear-down-incremental "$@"
+  cat "$bench" | $cvc4 -L smt2 --print-success --no-checking --no-interactive --no-incremental --tear-down-incremental "$@"
 }
 
 case "$logic" in
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index e6e3d3411..d28f711af 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -52,6 +52,17 @@ public:
    */
   bool doCommand(CVC4::Command* cmd);
 
+  /**
+   * Allow one to set an option on the underlying SmtEngine.
+   * This could be done with a Command object, but then it's
+   * interpreted as a user command (and might result in "success"
+   * or "error" output, for example.  This function can throw
+   * exceptions.
+   */
+  void setOption(const std::string& key, const CVC4::SExpr& value) {
+    d_smtEngine->setOption(key, value);
+  }
+
   Result getResult() const { return d_result; }
   void reset();
 
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 9215c6073..c39627550 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -269,18 +269,14 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     if(opts[options::interactive] && inputFromStdin) {
       if(opts[options::tearDownIncremental] && opts[options::incrementalSolving]) {
         if(opts.wasSetByUser(options::incrementalSolving)) {
-          throw OptionException("--tear-down-incremental incompatible with --interactive");
+          throw OptionException("--tear-down-incremental incompatible with --incremental");
         }
 
-        cmd = new SetOptionCommand("incremental", false);
-        pExecutor->doCommand(cmd);
-        delete cmd;
+        pExecutor->setOption("incremental", false);
       }
 #ifndef PORTFOLIO_BUILD
       if(!opts.wasSetByUser(options::incrementalSolving)) {
-        cmd = new SetOptionCommand("incremental", true);
-        pExecutor->doCommand(cmd);
-        delete cmd;
+        pExecutor->setOption("incremental", true);
       }
 #endif /* PORTFOLIO_BUILD */
       InteractiveShell shell(*exprMgr, opts);
@@ -308,12 +304,10 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     } else if(opts[options::tearDownIncremental]) {
       if(opts[options::incrementalSolving]) {
         if(opts.wasSetByUser(options::incrementalSolving)) {
-          throw OptionException("--tear-down-incremental incompatible with --interactive");
+          throw OptionException("--tear-down-incremental incompatible with --incremental");
         }
 
-        cmd = new SetOptionCommand("incremental", false);
-        pExecutor->doCommand(cmd);
-        delete cmd;
+        pExecutor->setOption("incremental", false);
       }
 
       ParserBuilder parserBuilder(exprMgr, filename, opts);
@@ -338,7 +332,8 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         if(dynamic_cast<PushCommand*>(cmd) != NULL) {
           if(needReset) {
             pExecutor->reset();
-            bool succ = opts[options::printSuccess];
+            bool succ = Command::printsuccess::getPrintSuccess(*opts[options::out]);
+            Command::printsuccess::setPrintSuccess(*opts[options::out], false);
             opts.set(options::printSuccess, false);
             for(size_t i = 0; i < allCommands.size(); ++i) {
               for(size_t j = 0; j < allCommands[i].size(); ++j) {
@@ -347,15 +342,16 @@ int runCvc4(int argc, char* argv[], Options& opts) {
                 delete cmd;
               }
             }
-            opts.set(options::printSuccess, succ);
+            Command::printsuccess::setPrintSuccess(*opts[options::out], succ);
             needReset = false;
           }
+          *opts[options::out] << CommandSuccess();
           allCommands.push_back(vector<Command*>());
         } else if(dynamic_cast<PopCommand*>(cmd) != NULL) {
           allCommands.pop_back(); // fixme leaks cmds here
           pExecutor->reset();
-          bool succ = opts[options::printSuccess];
-          opts.set(options::printSuccess, false);
+          bool succ = Command::printsuccess::getPrintSuccess(*opts[options::out]);
+          Command::printsuccess::setPrintSuccess(*opts[options::out], false);
           for(size_t i = 0; i < allCommands.size(); ++i) {
             for(size_t j = 0; j < allCommands[i].size(); ++j) {
               Command* cmd = allCommands[i][j]->clone();
@@ -363,13 +359,14 @@ int runCvc4(int argc, char* argv[], Options& opts) {
               delete cmd;
             }
           }
-          opts.set(options::printSuccess, succ);
+          Command::printsuccess::setPrintSuccess(*opts[options::out], succ);
+          *opts[options::out] << CommandSuccess();
         } else if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
                   dynamic_cast<QueryCommand*>(cmd) != NULL) {
           if(needReset) {
             pExecutor->reset();
-            bool succ = opts[options::printSuccess];
-            opts.set(options::printSuccess, false);
+            bool succ = Command::printsuccess::getPrintSuccess(*opts[options::out]);
+            Command::printsuccess::setPrintSuccess(*opts[options::out], false);
             for(size_t i = 0; i < allCommands.size(); ++i) {
               for(size_t j = 0; j < allCommands[i].size(); ++j) {
                 Command* cmd = allCommands[i][j]->clone();
@@ -377,7 +374,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
                 delete cmd;
               }
             }
-            opts.set(options::printSuccess, succ);
+            Command::printsuccess::setPrintSuccess(*opts[options::out], succ);
           }
           status = pExecutor->doCommand(cmd);
           needReset = true;
@@ -395,9 +392,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       delete parser;
     } else {
       if(!opts.wasSetByUser(options::incrementalSolving)) {
-        cmd = new SetOptionCommand("incremental", false);
-        pExecutor->doCommand(cmd);
-        delete cmd;
+        pExecutor->setOption("incremental", false);
       }
 
       ParserBuilder parserBuilder(exprMgr, filename, opts);