bv: Assert input facts on user-level 0. (#6515)

The bitblast solver currently uses solving under assumptions for all facts that are sent to the bit-vector solver. For input facts on user-level 0 we can however assert the fact to the SAT solver, which allows the SAT solver to do more preprocessing. This PR adds the option to assert user-level 0 input facts, which is disabled by default.

1 files changed, 16 insertions, 0 deletions

diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index a1a3db706..7438279b1 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -185,6 +185,22 @@ public:
   bool isDecision(Node lit) const;
 
   /**
+   * Return the current decision level of `lit`.
+   *
+   * @param lit: The node in question, must have an associated SAT literal.
+   * @return Decision level of the SAT variable of `lit` (phase is disregarded),
+   *         or -1 if `lit` has not been assigned yet.
+   */
+  int32_t getDecisionLevel(Node lit) const;
+
+  /**
+   * Return the user-context level when `lit` was introduced..
+   *
+   * @return User-context level or -1 if not yet introduced.
+   */
+  int32_t getIntroLevel(Node lit) const;
+
+  /**
    * Get the assertion level of the SAT solver.
    */
   unsigned getAssertionLevel() const;