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, 10 insertions, 0 deletions

diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index b09ffd685..293e7175b 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -259,6 +259,16 @@ bool MinisatSatSolver::isDecision(SatVariable decn) const {
   return d_minisat->isDecision( decn );
 }
 
+int32_t MinisatSatSolver::getDecisionLevel(SatVariable v) const
+{
+  return d_minisat->level(v);
+}
+
+int32_t MinisatSatSolver::getIntroLevel(SatVariable v) const
+{
+  return d_minisat->intro_level(v);
+}
+
 SatProofManager* MinisatSatSolver::getProofManager()
 {
   return d_minisat->getProofManager();