diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-06-22 18:12:15 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-23 01:12:15 +0000 |
commit | d469cd09002b47e1a7d51bc6a089456068135303 (patch) | |
tree | 3c5e68fb24113fca9e74c002614a388698d9a5f5 /src/main | |
parent | 21ee0f18c288d430d08c133f601173be25411187 (diff) |
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.
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/driver_unified.cpp | 183 |
1 files changed, 0 insertions, 183 deletions
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) |