From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 23 Jun 2021 01:12:15 +0000 (-0700)
Subject: Remove `--tear-down-incremental` (#6745)
X-Git-Tag: cvc5-1.0.0~1567
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d469cd09002b47e1a7d51bc6a089456068135303;p=cvc5.git

Remove `--tear-down-incremental` (#6745)

Recent experiments have shown that `--tear-down-incremental` is actually
not really helping anymore and it has always been a bit of a workaround.
It is also broken on current master. This commit removes the option.
---

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index ed1825711..2bc5c59f3 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -213,11 +213,6 @@ int runCvc5(int argc, char* argv[], Options& opts)
     bool status = true;
     if (opts.driver.interactive && inputFromStdin)
     {
-      if (opts.driver.tearDownIncremental > 0)
-      {
-        throw Exception(
-            "--tear-down-incremental doesn't work in interactive mode");
-      }
       if (!opts.base.incrementalSolvingWasSetByUser)
       {
         cmd.reset(new SetOptionCommand("incremental", "true"));
@@ -256,184 +251,6 @@ int runCvc5(int argc, char* argv[], Options& opts)
         }
       }
     }
-    else if (opts.driver.tearDownIncremental > 0)
-    {
-      if (!opts.base.incrementalSolving
-          && opts.driver.tearDownIncremental > 1)
-      {
-        // For tear-down-incremental values greater than 1, need incremental
-        // on too.
-        cmd.reset(new SetOptionCommand("incremental", "true"));
-        cmd->setMuted(true);
-        pExecutor->doCommand(cmd);
-        // if(opts.base.incrementalWasSetByUser) {
-        //   throw OptionException(
-        //     "--tear-down-incremental incompatible with --incremental");
-        // }
-
-        // cmd.reset(new SetOptionCommand("incremental", "false"));
-        // cmd->setMuted(true);
-        // pExecutor->doCommand(cmd);
-      }
-
-      ParserBuilder parserBuilder(pExecutor->getSolver(),
-                                  pExecutor->getSymbolManager(),
-                                  opts);
-      std::unique_ptr<Parser> parser(parserBuilder.build());
-      if( inputFromStdin ) {
-        parser->setInput(Input::newStreamInput(
-            opts.base.inputLanguage, cin, filename));
-      }
-      else
-      {
-        parser->setInput(Input::newFileInput(opts.base.inputLanguage,
-                                             filename,
-                                             opts.parser.memoryMap));
-      }
-
-      vector< vector<Command*> > allCommands;
-      allCommands.push_back(vector<Command*>());
-      int needReset = 0;
-      // true if one of the commands was interrupted
-      bool interrupted = false;
-      while (status)
-      {
-        if (interrupted) {
-          *opts.base.out << CommandInterrupted();
-          break;
-        }
-
-        try {
-          cmd.reset(parser->nextCommand());
-          if (cmd == nullptr) break;
-        } catch (UnsafeInterruptException& e) {
-          interrupted = true;
-          continue;
-        }
-
-        if(dynamic_cast<PushCommand*>(cmd.get()) != nullptr) {
-          if (needReset >= opts.driver.tearDownIncremental)
-          {
-            pExecutor->reset();
-            for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
-              if (interrupted) break;
-              for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
-              {
-                Command* ccmd = allCommands[i][j]->clone();
-                ccmd->setMuted(true);
-                pExecutor->doCommand(ccmd);
-                if (ccmd->interrupted())
-                {
-                  interrupted = true;
-                }
-                delete ccmd;
-              }
-            }
-            needReset = 0;
-          }
-          allCommands.push_back(vector<Command*>());
-          Command* copy = cmd->clone();
-          allCommands.back().push_back(copy);
-          status = pExecutor->doCommand(cmd);
-          if(cmd->interrupted()) {
-            interrupted = true;
-            continue;
-          }
-        } else if(dynamic_cast<PopCommand*>(cmd.get()) != nullptr) {
-          allCommands.pop_back(); // fixme leaks cmds here
-          if (needReset >= opts.driver.tearDownIncremental)
-          {
-            pExecutor->reset();
-            for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
-              for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
-              {
-                std::unique_ptr<Command> ccmd(allCommands[i][j]->clone());
-                ccmd->setMuted(true);
-                pExecutor->doCommand(ccmd);
-                if (ccmd->interrupted())
-                {
-                  interrupted = true;
-                }
-              }
-            }
-            if (interrupted) continue;
-            *opts.base.out << CommandSuccess();
-            needReset = 0;
-          }
-          else
-          {
-            status = pExecutor->doCommand(cmd);
-            if(cmd->interrupted()) {
-              interrupted = true;
-              continue;
-            }
-          }
-        } else if(dynamic_cast<CheckSatCommand*>(cmd.get()) != nullptr ||
-                  dynamic_cast<QueryCommand*>(cmd.get()) != nullptr) {
-          if (needReset >= opts.driver.tearDownIncremental)
-          {
-            pExecutor->reset();
-            for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
-              for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
-              {
-                Command* ccmd = allCommands[i][j]->clone();
-                ccmd->setMuted(true);
-                pExecutor->doCommand(ccmd);
-                if (ccmd->interrupted())
-                {
-                  interrupted = true;
-                }
-                delete ccmd;
-              }
-            }
-            needReset = 0;
-          }
-          else
-          {
-            ++needReset;
-          }
-          if (interrupted) {
-            continue;
-          }
-
-          status = pExecutor->doCommand(cmd);
-          if(cmd->interrupted()) {
-            interrupted = true;
-            continue;
-          }
-        } else if(dynamic_cast<ResetCommand*>(cmd.get()) != nullptr) {
-          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
-          // preceding them.
-          if(dynamic_cast<GetUnsatCoreCommand*>(cmd.get()) == nullptr &&
-             dynamic_cast<GetProofCommand*>(cmd.get()) == nullptr &&
-             dynamic_cast<GetValueCommand*>(cmd.get()) == nullptr &&
-             dynamic_cast<GetModelCommand*>(cmd.get()) == nullptr &&
-             dynamic_cast<GetAssignmentCommand*>(cmd.get()) == nullptr &&
-             dynamic_cast<GetInstantiationsCommand*>(cmd.get()) == nullptr &&
-             dynamic_cast<GetAssertionsCommand*>(cmd.get()) == nullptr &&
-             dynamic_cast<GetInfoCommand*>(cmd.get()) == nullptr &&
-             dynamic_cast<GetOptionCommand*>(cmd.get()) == nullptr &&
-             dynamic_cast<EchoCommand*>(cmd.get()) == nullptr) {
-            Command* copy = cmd->clone();
-            allCommands.back().push_back(copy);
-          }
-          status = pExecutor->doCommand(cmd);
-          if(cmd->interrupted()) {
-            interrupted = true;
-            continue;
-          }
-
-          if(dynamic_cast<QuitCommand*>(cmd.get()) != nullptr) {
-            break;
-          }
-        }
-      }
-    }
     else
     {
       if (!opts.base.incrementalSolvingWasSetByUser)
diff --git a/src/options/main_options.toml b/src/options/main_options.toml
index fdaebbd6d..19bb97f34 100644
--- a/src/options/main_options.toml
+++ b/src/options/main_options.toml
@@ -88,14 +88,6 @@ public = true
   default    = "false"
   help       = "spin on segfault/other crash waiting for gdb"
 
-[[option]]
-  name       = "tearDownIncremental"
-  category   = "expert"
-  long       = "tear-down-incremental=N"
-  type       = "int"
-  default    = "0"
-  help       = "implement PUSH/POP/multi-query by destroying and recreating SmtEngine every N queries"
-
 [[option]]
   name       = "dumpModels"
   category   = "regular"
@@ -142,4 +134,4 @@ public = true
   long       = "force-no-limit-cpu-while-dump"
   type       = "bool"
   default    = "false"
-  help       = "Force no CPU limit when dumping models and proofs"
+  help       = "Force no CPU limit when dumping models and proofs"
\ No newline at end of file