diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-06-02 11:18:36 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-02 11:18:36 -0700 |
commit | d440c5f3bea930c4f30d62858b878ab36c676312 (patch) | |
tree | b2a0b76a76c99902814b0a2c6ae4dd3b98d37f57 /src/theory/bv/bitblast | |
parent | 806f4071423ee1bf8f02f1836843de73faabb952 (diff) |
Fix BV-abstraction check to consider SKOLEM. (#2042)
Further, fix a bug in the AIG bitblaster that was also uncovered with the
minimized file.
Diffstat (limited to 'src/theory/bv/bitblast')
-rw-r--r-- | src/theory/bv/bitblast/aig_bitblaster.cpp | 7 | ||||
-rw-r--r-- | src/theory/bv/bitblast/aig_bitblaster.h | 2 |
2 files changed, 6 insertions, 3 deletions
diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp index 7e666bcbf..80930866f 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.cpp +++ b/src/theory/bv/bitblast/aig_bitblaster.cpp @@ -139,7 +139,8 @@ AigBitblaster::AigBitblaster() d_nullContext(new context::Context()), d_aigCache(), d_bbAtoms(), - d_aigOutputNode(NULL) + d_aigOutputNode(NULL), + d_notify() { prop::SatSolver* solver = nullptr; switch (options::bvSatSolver()) @@ -149,8 +150,8 @@ AigBitblaster::AigBitblaster() prop::BVSatSolverInterface* minisat = prop::SatSolverFactory::createMinisat( d_nullContext.get(), smtStatisticsRegistry(), "AigBitblaster"); - MinisatEmptyNotify notify; - minisat->setNotify(¬ify); + d_notify.reset(new MinisatEmptyNotify()); + minisat->setNotify(d_notify.get()); solver = minisat; break; } diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h index 30f1dd00b..dea2d0429 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.h +++ b/src/theory/bv/bitblast/aig_bitblaster.h @@ -67,6 +67,8 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*> // the thing we are checking for sat Abc_Obj_t* d_aigOutputNode; + std::unique_ptr<MinisatEmptyNotify> d_notify; + void addAtom(TNode atom); void simplifyAig(); void storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) override; |