diff options
Diffstat (limited to 'src/smt/command.h')
| -rw-r--r-- | src/smt/command.h | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/src/smt/command.h b/src/smt/command.h index b81b55b91..7088c09ed 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -31,8 +31,6 @@ #include "api/cvc4cpp.h" #include "expr/expr.h" #include "expr/type.h" -#include "expr/variable_type_map.h" -#include "proof/unsat_core.h" #include "util/result.h" #include "util/sexpr.h" @@ -43,6 +41,7 @@ class Solver; class Term; } // namespace api +class UnsatCore; class SmtEngine; class Command; class CommandStatus; @@ -1224,7 +1223,7 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command { public: GetUnsatCoreCommand(); - const UnsatCore& getUnsatCore() const; + const std::vector<api::Term>& getUnsatCore() const; void invoke(api::Solver* solver) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; @@ -1239,8 +1238,10 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; protected: - // the result of the unsat core call - UnsatCore d_result; + /** The solver we were invoked with */ + api::Solver* d_solver; + /** the result of the unsat core call */ + std::vector<api::Term> d_result; }; /* class GetUnsatCoreCommand */ class CVC4_PUBLIC GetAssertionsCommand : public Command |