diff options
| author | Tim King <taking@cs.nyu.edu> | 2016-03-22 20:45:14 -0700 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2016-03-22 20:45:14 -0700 |
| commit | d9afad0e10fade886a2b3e0076539740786bd6cb (patch) | |
| tree | 5272d864ca1e24da670b5059042d294e0884dd85 /src | |
| parent | 0ee7aa783c299eca1127005b590dd157b315f130 (diff) | |
Garbage collecting the MinisatEmptyNotify for the EagerBitblaster.
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/bv/bitblaster_template.h | 2 | ||||
| -rw-r--r-- | src/theory/bv/eager_bitblaster.cpp | 8 |
2 files changed, 8 insertions, 2 deletions
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 9c6c4af9b..10e30c5c7 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -266,6 +266,8 @@ class EagerBitblaster : public TBitblaster<Node> { TNodeSet d_bbAtoms; TNodeSet d_variables; + MinisatEmptyNotify d_notify; + Node getModelFromSatSolver(TNode a, bool fullModel); bool isSharedTerm(TNode node); diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index dd561667c..77e75091d 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -36,9 +36,14 @@ void BitblastingRegistrar::preRegister(Node n) { EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) : TBitblaster<Node>() + , d_satSolver(NULL) + , d_bitblastingRegistrar(NULL) + , d_nullContext(NULL) + , d_cnfStream(NULL) , d_bv(theory_bv) , d_bbAtoms() , d_variables() + , d_notify() { d_bitblastingRegistrar = new BitblastingRegistrar(this); d_nullContext = new context::Context(); @@ -50,8 +55,7 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) d_satSolver, d_bitblastingRegistrar, d_nullContext, options::proof(), "EagerBitblaster"); - MinisatEmptyNotify* notify = new MinisatEmptyNotify(); - d_satSolver->setNotify(notify); + d_satSolver->setNotify(&d_notify); d_bvp = NULL; } |