From a04226ef3519c4fdce7bd6c3ff92f18bf6bee83c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 23 Dec 2020 16:17:48 -0600 Subject: 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. --- src/theory/bv/bitblast/eager_bitblaster.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/theory/bv/bitblast/eager_bitblaster.cpp') 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")); } -- cgit v1.2.3