From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 17 Jun 2014 02:35:14 +0000 (-0400)
Subject: More application-track fixes for use with trace executor.
X-Git-Tag: cvc5-1.0.0~6758^2~29
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=180d7f3e5a339a68b396cf9fa2820a8b5a1e11a1;p=cvc5.git

More application-track fixes for use with trace executor.
---

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index c39627550..54f6383ac 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -332,17 +332,14 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         if(dynamic_cast<PushCommand*>(cmd) != NULL) {
           if(needReset) {
             pExecutor->reset();
-            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) {
                 Command* cmd = allCommands[i][j]->clone();
+                cmd->setMuted(true);
                 pExecutor->doCommand(cmd);
                 delete cmd;
               }
             }
-            Command::printsuccess::setPrintSuccess(*opts[options::out], succ);
             needReset = false;
           }
           *opts[options::out] << CommandSuccess();
@@ -350,36 +347,33 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         } else if(dynamic_cast<PopCommand*>(cmd) != NULL) {
           allCommands.pop_back(); // fixme leaks cmds here
           pExecutor->reset();
-          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();
+              cmd->setMuted(true);
               pExecutor->doCommand(cmd);
               delete cmd;
             }
           }
-          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 = 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();
+                cmd->setMuted(true);
                 pExecutor->doCommand(cmd);
                 delete cmd;
               }
             }
-            Command::printsuccess::setPrintSuccess(*opts[options::out], succ);
           }
           status = pExecutor->doCommand(cmd);
           needReset = true;
         } else {
-          allCommands.back().push_back(cmd->clone());
+          Command* copy = cmd->clone();
+          allCommands.back().push_back(copy);
           if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
             delete cmd;
             break;
diff --git a/src/options/base_options b/src/options/base_options
index ee15238c8..ed94e68f6 100644
--- a/src/options/base_options
+++ b/src/options/base_options
@@ -128,7 +128,7 @@ option - trace -t --trace=TAG argument :handler CVC4::options::addTraceTag
 option - debug -d --debug=TAG argument :handler CVC4::options::addDebugTag
  debug something (e.g. -d arith), can repeat
 
-option printSuccess print-success --print-success bool :predicate CVC4::options::setPrintSuccess :predicate-include "options/base_options_handlers.h" :read-write
+option printSuccess print-success --print-success bool :predicate CVC4::options::setPrintSuccess :predicate-include "options/base_options_handlers.h"
  print the "success" output required of SMT-LIBv2
 
 alias --smtlib-strict = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental --abstract-values