diff options
Diffstat (limited to 'src/smt/command.cpp')
-rw-r--r-- | src/smt/command.cpp | 61 |
1 files changed, 61 insertions, 0 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index e61ea868f..c77c4ed02 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1841,6 +1841,67 @@ std::string GetQuantifierEliminationCommand::getCommandName() const } /* -------------------------------------------------------------------------- */ +/* class GetUnsatAssumptionsCommand */ +/* -------------------------------------------------------------------------- */ + +GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() {} + +void GetUnsatAssumptionsCommand::invoke(SmtEngine* smtEngine) +{ + try + { + d_result = smtEngine->getUnsatAssumptions(); + d_commandStatus = CommandSuccess::instance(); + } + catch (RecoverableModalException& e) + { + d_commandStatus = new CommandRecoverableFailure(e.what()); + } + catch (exception& e) + { + d_commandStatus = new CommandFailure(e.what()); + } +} + +std::vector<Expr> GetUnsatAssumptionsCommand::getResult() const +{ + return d_result; +} + +void GetUnsatAssumptionsCommand::printResult(std::ostream& out, + uint32_t verbosity) const +{ + if (!ok()) + { + this->Command::printResult(out, verbosity); + } + else + { + out << d_result << endl; + } +} + +Command* GetUnsatAssumptionsCommand::exportTo( + ExprManager* exprManager, ExprManagerMapCollection& variableMap) +{ + GetUnsatAssumptionsCommand* c = new GetUnsatAssumptionsCommand; + c->d_result = d_result; + return c; +} + +Command* GetUnsatAssumptionsCommand::clone() const +{ + GetUnsatAssumptionsCommand* c = new GetUnsatAssumptionsCommand; + c->d_result = d_result; + return c; +} + +std::string GetUnsatAssumptionsCommand::getCommandName() const +{ + return "get-unsat-assumptions"; +} + +/* -------------------------------------------------------------------------- */ /* class GetUnsatCoreCommand */ /* -------------------------------------------------------------------------- */ |