diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-23 16:17:48 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-23 16:17:48 -0600 |
| commit | a04226ef3519c4fdce7bd6c3ff92f18bf6bee83c (patch) | |
| tree | 40ba3c986de4107e322adb19a5e3a247dcec0972 /src/theory/bv/bitblast | |
| parent | 42f51547174e2644a244464c170115ff3b2bc22f (diff) | |
Add option to track and notify from CNF stream (#5708)
This adds functionality to CNF stream to allow e.g. TheoryProxy to be notified when a formula is asserted (not just literals).
This will be required for SAT relevancy.
No behavior changes in this PR.
Diffstat (limited to 'src/theory/bv/bitblast')
| -rw-r--r-- | src/theory/bv/bitblast/eager_bitblaster.cpp | 3 | ||||
| -rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.cpp | 2 |
2 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index 046ad4b1b..44db8a3cd 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -18,6 +18,7 @@ #include "cvc4_private.h" #include "options/bv_options.h" +#include "options/smt_options.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" #include "smt/smt_engine.h" @@ -74,7 +75,7 @@ EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c) d_nullContext.get(), nullptr, rm, - false, + prop::FormulaLitPolicy::INTERNAL, "EagerBitblaster")); } diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index 95d78c69b..7f38c61a2 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -85,7 +85,7 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, d_nullContext.get(), nullptr, rm, - false, + prop::FormulaLitPolicy::INTERNAL, "LazyBitblaster")); d_satSolverNotify.reset( |