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

diff --git a/contrib/run-script-smtcomp2014-application b/contrib/run-script-smtcomp2014-application
index b04b3377546d9fb773ccade0c3a8474b32a92937..2decdb98a6a13a0235de1b00e06c176fa12fb73d 100755 (executable)
--- 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 e6e3d3411786d42bbfb59d96d76c9ccd86c1b69c..d28f711af258dc167d633fb50e014ca4447954da 100644 (file)
--- 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 9215c607376df74514b1a1b39caa43185957c125..c39627550ffb3a280107758e8bde6ed6a7e99b13 100644 (file)
--- 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);