diff options
author | Clark Barrett <clarkbarrett@google.com> | 2015-04-27 18:23:54 -0700 |
---|---|---|
committer | Clark Barrett <clarkbarrett@google.com> | 2015-04-27 18:23:54 -0700 |
commit | 1261597c32e3c8a98225a91fdd7b420867f89329 (patch) | |
tree | 9d8be67f09a2f998b54ee8689020c7d288882e18 /src | |
parent | 91cd90ae485a159799d82f7341438a4e9a12a72d (diff) | |
parent | 721cbfad7ebe3668e87679f65e7ce80251878dc6 (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4
Diffstat (limited to 'src')
-rw-r--r-- | src/util/unsat_core.cpp | 4 | ||||
-rw-r--r-- | src/util/unsat_core.h | 5 |
2 files changed, 7 insertions, 2 deletions
diff --git a/src/util/unsat_core.cpp b/src/util/unsat_core.cpp index 929d5e909..95d066c6d 100644 --- a/src/util/unsat_core.cpp +++ b/src/util/unsat_core.cpp @@ -21,6 +21,10 @@ namespace CVC4 { +void UnsatCore::initMessage() const { + Debug("core") << "UnsatCore size " << d_core.size() << std::endl; +} + UnsatCore::const_iterator UnsatCore::begin() const { return d_core.begin(); } diff --git a/src/util/unsat_core.h b/src/util/unsat_core.h index 8f497688a..644f56509 100644 --- a/src/util/unsat_core.h +++ b/src/util/unsat_core.h @@ -23,7 +23,6 @@ #include <iostream> #include <vector> #include "expr/expr.h" -#include "util/output.h" namespace CVC4 { @@ -40,12 +39,14 @@ class CVC4_PUBLIC UnsatCore { std::vector<Expr> d_core; + void initMessage() const; + public: UnsatCore() : d_smt(NULL) {} template <class T> UnsatCore(SmtEngine* smt, T begin, T end) : d_smt(smt), d_core(begin, end) { - Debug("core") << "UnsatCore size " << d_core.size() << std::endl; + initMessage(); } ~UnsatCore() {} |