summaryrefslogtreecommitdiff
path: root/src/util/unsat_core.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/unsat_core.h')
-rw-r--r--src/util/unsat_core.h7
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback