From 829b597108f64a97398c863d150905c6d203613f Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 23 Aug 2014 01:50:02 -0400 Subject: Unsat core printing. --- src/util/unsat_core.h | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) (limited to 'src/util/unsat_core.h') 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 d_core; public: - UnsatCore() {} + UnsatCore() : d_smt(NULL) {} template - 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::const_iterator iterator; typedef std::vector::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 */ -- cgit v1.2.3