diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-25 18:40:06 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-26 15:20:32 -0400 |
commit | 525e7328cad1ac8afbc60ed8103e06665cf5b163 (patch) | |
tree | 61d8f46addfa6e76b233b234025df9bf54f7aea1 /src/expr | |
parent | 34a27e2fef540ee3d90c43f771397e0e9ce3fef9 (diff) |
Improved SMT-LIBv2 language support for unsat cores.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 14 | ||||
-rw-r--r-- | src/expr/command.h | 3 |
2 files changed, 14 insertions, 3 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index a07076281..a3f5170fa 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -1121,6 +1121,9 @@ std::string GetInstantiationsCommand::getCommandName() const throw() { GetUnsatCoreCommand::GetUnsatCoreCommand() throw() { } +GetUnsatCoreCommand::GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw() : d_names(names) { +} + void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() { try { d_result = smtEngine->getUnsatCore(); @@ -1134,18 +1137,23 @@ void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) con if(! ok()) { this->Command::printResult(out, verbosity); } else { - d_result.toStream(out); + d_result.toStream(out, d_names); } } +const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const throw() { + // of course, this will be empty if the command hasn't been invoked yet + return d_result; +} + Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetUnsatCoreCommand* c = new GetUnsatCoreCommand(); + GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names); c->d_result = d_result; return c; } Command* GetUnsatCoreCommand::clone() const { - GetUnsatCoreCommand* c = new GetUnsatCoreCommand(); + GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names); c->d_result = d_result; return c; } diff --git a/src/expr/command.h b/src/expr/command.h index e84c53d09..4d2957b7c 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -602,11 +602,14 @@ public: class CVC4_PUBLIC GetUnsatCoreCommand : public Command { protected: UnsatCore d_result; + std::map<Expr, std::string> d_names; public: GetUnsatCoreCommand() throw(); + GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw(); ~GetUnsatCoreCommand() throw() {} void invoke(SmtEngine* smtEngine) throw(); void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + const UnsatCore& getUnsatCore() const throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; std::string getCommandName() const throw(); |