summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/main/driver_unified.cpp183
-rw-r--r--src/options/main_options.toml10
2 files changed, 1 insertions, 192 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)
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
@@ -89,14 +89,6 @@ public = true
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"
long = "dump-models"
@@ -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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback