Add bit-level propagation support to BV bitblast solver. (#5906)

This commit adds support for bit-level propagation for the BV bitblast solver to quickly detect conflicts on effort levels != FULL. Bit-level propagation for the bitblast solver is by default disabled for now. Further, bit-blasting of facts is now handled more lazily with a bit-blast queue.

1 files changed, 7 insertions, 0 deletions

diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 896233f41..d421155ae 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -81,6 +81,13 @@ public:
     return SAT_VALUE_UNKNOWN;
   };
 
+  /**
+   * Tell SAT solver to only do propagation on next solve().
+   *
+   * @return true if feature is supported, otherwise false.
+   */
+  virtual bool setPropagateOnly() { return false; }
+
   /** Interrupt the solver */
   virtual void interrupt() = 0;