Add BV solver bitblast. (#5851)

This PR adds a new bit-blasting BV solver, which can be enabled via --bv-solver=bitblast. The new bit-blast solver can be used instead of the lazy BV solver and currently supports CaDiCaL and CryptoMiniSat as SAT back end.

1 files changed, 18 insertions, 0 deletions

diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index 1072003d2..d375388ef 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -39,6 +39,15 @@ CMSat::Lit toInternalLit(SatLiteral lit)
   return CMSat::Lit(lit.getSatVariable(), lit.isNegated());
 }
 
+SatLiteral toSatLiteral(CMSat::Lit lit)
+{
+  if (lit == CMSat::lit_Undef)
+  {
+    return undefSatLiteral;
+  }
+  return SatLiteral(lit.var(), lit.sign());
+}
+
 SatValue toSatLiteralValue(CMSat::lbool res)
 {
   if (res == CMSat::l_True) return SAT_VALUE_TRUE;
@@ -181,6 +190,15 @@ SatValue CryptoMinisatSolver::solve(const std::vector<SatLiteral>& assumptions)
   return toSatLiteralValue(d_solver->solve(&assumpts));
 }
 
+void CryptoMinisatSolver::getUnsatAssumptions(
+    std::vector<SatLiteral>& assumptions)
+{
+  for (const CMSat::Lit& lit : d_solver->get_conflict())
+  {
+    assumptions.push_back(toSatLiteral(~lit));
+  }
+}
+
 SatValue CryptoMinisatSolver::value(SatLiteral l){
   const std::vector<CMSat::lbool> model = d_solver->get_model();
   CMSatVar var = l.getSatVariable();