diff options
Diffstat (limited to 'src/smt/command.cpp')
-rw-r--r-- | src/smt/command.cpp | 39 |
1 files changed, 2 insertions, 37 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 88f04f885..cb95cf348 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -2275,57 +2275,22 @@ void BlockModelValuesCommand::toStream(std::ostream& out, /* class GetProofCommand */ /* -------------------------------------------------------------------------- */ -GetProofCommand::GetProofCommand() : d_smtEngine(nullptr), d_result(nullptr) {} +GetProofCommand::GetProofCommand() {} void GetProofCommand::invoke(SmtEngine* smtEngine) { - try - { - d_smtEngine = smtEngine; - d_result = &smtEngine->getProof(); - d_commandStatus = CommandSuccess::instance(); - } - catch (RecoverableModalException& e) - { - d_commandStatus = new CommandRecoverableFailure(e.what()); - } - catch (UnsafeInterruptException& e) - { - d_commandStatus = new CommandInterrupted(); - } - catch (exception& e) - { - d_commandStatus = new CommandFailure(e.what()); - } -} - -const Proof& GetProofCommand::getResult() const { return *d_result; } -void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const -{ - if (!ok()) - { - this->Command::printResult(out, verbosity); - } - else - { - smt::SmtScope scope(d_smtEngine); - d_result->toStream(out); - } + Unimplemented() << "Unimplemented get-proof\n"; } Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { GetProofCommand* c = new GetProofCommand(); - c->d_result = d_result; - c->d_smtEngine = d_smtEngine; return c; } Command* GetProofCommand::clone() const { GetProofCommand* c = new GetProofCommand(); - c->d_result = d_result; - c->d_smtEngine = d_smtEngine; return c; } |