diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-23 01:50:02 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-23 01:50:02 -0400 |
commit | 829b597108f64a97398c863d150905c6d203613f (patch) | |
tree | 71194e53b7536031cb6481320e0d109123deed37 /src/util/unsat_core.h | |
parent | ba9a2a34e37f856774662b50a09b3a1d3b9ae89f (diff) |
Unsat core printing.
Diffstat (limited to 'src/util/unsat_core.h')
-rw-r--r-- | src/util/unsat_core.h | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/src/util/unsat_core.h b/src/util/unsat_core.h index 51724b33b..c67a6e448 100644 --- a/src/util/unsat_core.h +++ b/src/util/unsat_core.h @@ -26,17 +26,30 @@ namespace CVC4 { +class SmtEngine; +class UnsatCore; + +std::ostream& operator<<(std::ostream& out, const UnsatCore& core) CVC4_PUBLIC; + class CVC4_PUBLIC UnsatCore { + friend std::ostream& operator<<(std::ostream&, const UnsatCore&); + + /** The SmtEngine we're associated with */ + SmtEngine* d_smt; + std::vector<Expr> d_core; public: - UnsatCore() {} + UnsatCore() : d_smt(NULL) {} template <class T> - UnsatCore(T begin, T end) : d_core(begin, end) {} + UnsatCore(SmtEngine* smt, T begin, T end) : d_smt(smt), d_core(begin, end) {} ~UnsatCore() {} + /** get the smt engine that this unsat core is hooked up to */ + SmtEngine* getSmtEngine() { return d_smt; } + typedef std::vector<Expr>::const_iterator iterator; typedef std::vector<Expr>::const_iterator const_iterator; @@ -47,8 +60,6 @@ public: };/* class UnsatCore */ -std::ostream& operator<<(std::ostream& out, const UnsatCore& core) CVC4_PUBLIC; - }/* CVC4 namespace */ #endif /* __CVC4__UNSAT_CORE_H */ |