diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-07-02 15:13:17 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-02 22:13:17 +0000 |
| commit | de0401e53e4baab30a5e78d5bd51048348b1e1ce (patch) | |
| tree | 0f1697a82a4c839b5fd7a365ce3c5777c741c70f /src/theory/bv/bv_solver_bitblast.h | |
| parent | f83a753ad62a005085c47a7c0f4ba2e406d9acd7 (diff) | |
Fix bv assert input reset assertions (#6820)
If reset-assertions was called it will now reset the SAT solver and the
CNF stream if clauses were permanently added to the SAT solver via
option --bv-assert-input.
Diffstat (limited to 'src/theory/bv/bv_solver_bitblast.h')
| -rw-r--r-- | src/theory/bv/bv_solver_bitblast.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h index c5134c6fc..1fb721deb 100644 --- a/src/theory/bv/bv_solver_bitblast.h +++ b/src/theory/bv/bv_solver_bitblast.h @@ -33,6 +33,7 @@ namespace cvc5 { namespace theory { namespace bv { +class NotifyResetAssertions; class BBRegistrar; /** @@ -70,6 +71,9 @@ class BVSolverBitblast : public BVSolver const std::set<Node>& termSet) override; private: + /** Initialize SAT solver and CNF stream. */ + void initSatSolver(); + /** * Get value of `node` from SAT solver. * @@ -153,6 +157,9 @@ class BVSolverBitblast : public BVSolver /** Option to enable/disable bit-level propagation. */ bool d_propagate; + + /** Notifies when reset-assertion was called. */ + std::unique_ptr<NotifyResetAssertions> d_resetNotify; }; } // namespace bv |