Split lazy bit-vector solver from TheoryBV (#5009)

This commit separates the lazy bit-vector solver from TheoryBV, which is now a thin wrapper around a bit-vector solver d_internal . This will allow us to easily swap out the bit-vector solver in the future.

1 files changed, 11 insertions, 0 deletions

diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index 92116648e..7fecacf82 100644
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -329,6 +329,17 @@ class TheoryInferenceManager
    * decided with polarity pol, for details see OutputChannel::requirePhase.
    */
   void requirePhase(TNode n, bool pol);
+
+  /**
+   * Forward to OutputChannel::spendResource() to spend resources.
+   */
+  void spendResource(ResourceManager::Resource r);
+
+  /**
+   * Forward to OutputChannel::safePoint() to spend resources.
+   */
+  void safePoint(ResourceManager::Resource r);
+
  protected:
   /**
    * Process internal fact. This is a common helper method for the