diff options
author | Liana Hadarean <lianah@cs.nyu.edu> | 2014-11-17 15:26:42 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-17 15:26:42 -0500 |
commit | 3ba7ed6b1b09739385ae2ffb77a5c7ccd18b40a5 (patch) | |
tree | 845ae47600ffff9c68fa654c0f78d3474e406beb /src/theory/bv/bitblaster_template.h | |
parent | d8da3b13bc9df7750723cf3da38edc8cb6f67d3d (diff) |
Resource-limiting work.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Diffstat (limited to 'src/theory/bv/bitblaster_template.h')
-rw-r--r-- | src/theory/bv/bitblaster_template.h | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 0ff12da95..e13587323 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -28,6 +28,7 @@ #include "prop/sat_solver.h" #include "theory/valuation.h" #include "theory/theory_registrar.h" +#include "util/resource_manager.h" class Abc_Obj_t_; typedef Abc_Obj_t_ Abc_Obj_t; @@ -134,6 +135,7 @@ class TLazyBitblaster : public TBitblaster<Node> { {} bool notify(prop::SatLiteral lit); void notify(prop::SatClause& clause); + void spendResource(); void safePoint(); }; @@ -228,7 +230,8 @@ private: Statistics(const std::string& name); ~Statistics(); }; - std::string d_name; + std::string d_name; +public: Statistics d_statistics; }; @@ -237,6 +240,9 @@ public: MinisatEmptyNotify() {} bool notify(prop::SatLiteral lit) { return true; } void notify(prop::SatClause& clause) { } + void spendResource() { + NodeManager::currentResourceManager()->spendResource(); + } void safePoint() {} }; |