diff options
author | Clark Barrett <clarkbarrett@google.com> | 2015-04-23 10:45:04 -0700 |
---|---|---|
committer | Clark Barrett <clarkbarrett@google.com> | 2015-04-23 10:45:04 -0700 |
commit | 9f2ff7173d434162d49814ba3f24a9f9db21d476 (patch) | |
tree | f56f01b17d1233b2820fea26d259984c0b6d1c83 /src/util | |
parent | d4afd65c3dcc26bab066507356ad187cbcb23d9e (diff) | |
parent | 0daf670d46ec2e781c2060b41449f2787b6e8f66 (diff) |
Merge branch 'master' into google
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/unsat_core.h | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/util/unsat_core.h b/src/util/unsat_core.h index 27cf86488..8f497688a 100644 --- a/src/util/unsat_core.h +++ b/src/util/unsat_core.h @@ -23,6 +23,7 @@ #include <iostream> #include <vector> #include "expr/expr.h" +#include "util/output.h" namespace CVC4 { @@ -43,13 +44,17 @@ public: UnsatCore() : d_smt(NULL) {} template <class T> - UnsatCore(SmtEngine* smt, T begin, T end) : d_smt(smt), d_core(begin, end) {} + UnsatCore(SmtEngine* smt, T begin, T end) : d_smt(smt), d_core(begin, end) { + Debug("core") << "UnsatCore size " << d_core.size() << std::endl; + } ~UnsatCore() {} /** get the smt engine that this unsat core is hooked up to */ SmtEngine* getSmtEngine() { return d_smt; } + size_t size() const { return d_core.size(); } + typedef std::vector<Expr>::const_iterator iterator; typedef std::vector<Expr>::const_iterator const_iterator; |