[BV] An option for SAT proof optimization (#2915)

* [BV] An option for SAT proof optimization

The option doesn't **do** anything yet, but exists.

* CopyPaste Fix: BvOptimizeSatProof documentation

It was the documentation for a different option. Now it has been
updated.

* Fix Typos per Mathias' review.

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>

5 files changed, 96 insertions, 0 deletions

diff --git a/src/options/bv_bitblast_mode.cpp b/src/options/bv_bitblast_mode.cpp
index 4bd7b9d77..d2425831a 100644
--- a/src/options/bv_bitblast_mode.cpp
+++ b/src/options/bv_bitblast_mode.cpp
@@ -81,4 +81,25 @@ std::ostream& operator<<(std::ostream& out, theory::bv::BvProofFormat format)
   return out;
 }
 
+std::ostream& operator<<(std::ostream& out,
+                         theory::bv::BvOptimizeSatProof level)
+{
+  switch (level)
+  {
+    case theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_NONE:
+      out << "BITVECTOR_OPTIMIZE_SAT_PROOF_NONE";
+      break;
+    case theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF:
+      out << "BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF";
+      break;
+    case theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA:
+      out << "BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA";
+      break;
+    default: out << "BvOptimizeSatProof:UNKNOWN![" << unsigned(level) << "]";
+  }
+
+  return out;
+}
+
 }/* CVC4 namespace */
+
diff --git a/src/options/bv_bitblast_mode.h b/src/options/bv_bitblast_mode.h
index 871333b35..270f2346d 100644
--- a/src/options/bv_bitblast_mode.h
+++ b/src/options/bv_bitblast_mode.h
@@ -88,6 +88,27 @@ enum BvProofFormat
   BITVECTOR_PROOF_LRAT,
 };
 
+/**
+ * When the BV solver does eager bit-blasting backed by DRAT-producing SAT solvers, proofs
+ * can be written in a variety of formats.
+ */
+enum BvOptimizeSatProof
+{
+  /**
+   * Do not optimize the SAT proof.
+   */
+  BITVECTOR_OPTIMIZE_SAT_PROOF_NONE = 0,
+  /**
+   * Optimize the SAT proof, but do not shrink the formula
+   */
+  BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF = 1,
+  /**
+   * Optimize the SAT proof and shrink the formula
+   */
+  BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA = 2,
+};
+
+
 }/* CVC4::theory::bv namespace */
 }/* CVC4::theory namespace */
 
@@ -95,6 +116,7 @@ std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode);
 std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode);
 std::ostream& operator<<(std::ostream& out, theory::bv::SatSolverMode mode);
 std::ostream& operator<<(std::ostream& out, theory::bv::BvProofFormat format);
+std::ostream& operator<<(std::ostream& out, theory::bv::BvOptimizeSatProof level);
 
 }/* CVC4 namespace */
 
diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index 6dd755625..9529b7500 100644
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -14,6 +14,17 @@ header = "options/bv_options.h"
   help       = "choose which UNSAT proof format to use, see --bv-sat-solver=help"
 
 [[option]]
+  name       = "bvOptimizeSatProof"
+  category   = "expert"
+  long       = "bv-optimize-sat-proof=MODE"
+  type       = "CVC4::theory::bv::BvOptimizeSatProof"
+  default    = "CVC4::theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA"
+  handler    = "stringToBvOptimizeSatProof"
+  predicates = ["satSolverEnabledBuild"]
+  includes   = ["options/bv_bitblast_mode.h"]
+  help       = "enable SAT proof optimizations, see --bv-optimize-sat-proof=help"
+
+[[option]]
   name       = "bvSatSolver"
   smt_name   = "bv-sat-solver"
   category   = "expert"
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index f171c907e..7a4967de5 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1245,6 +1245,45 @@ theory::bv::BvProofFormat OptionsHandler::stringToBvProofFormat(
   }
 }
 
+const std::string OptionsHandler::s_bvOptimizeSatProofHelp =
+    "\
+Optimization levels currently supported by the --bv-optimize-sat-proof option:\n\
+\n\
+  none    : Do not optimize the SAT proof\n\
+\n\
+  proof   : Use drat-trim to shrink the SAT proof\n\
+\n\
+  formula : Use drat-trim to shrink the SAT proof and formula (default)\
+";
+
+theory::bv::BvOptimizeSatProof OptionsHandler::stringToBvOptimizeSatProof(
+    std::string option, std::string optarg)
+{
+  if (optarg == "none")
+  {
+    return theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_NONE;
+  }
+  else if (optarg == "proof")
+  {
+    return theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF;
+  }
+  else if (optarg == "formula")
+  {
+    return theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA;
+  }
+  else if (optarg == "help")
+  {
+    puts(s_bvOptimizeSatProofHelp.c_str());
+    exit(1);
+  }
+  else
+  {
+    throw OptionException(std::string("unknown option for --bv-optimize-sat-proof: `")
+                          + optarg + "'.  Try --bv-optimize-sat-proof=help.");
+  }
+}
+
+
 const std::string OptionsHandler::s_bitblastingModeHelp = "\
 Bit-blasting modes currently supported by the --bitblast option:\n\
 \n\
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 16ddbce4d..5c354be57 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -148,6 +148,8 @@ public:
 
   theory::bv::BvProofFormat stringToBvProofFormat(std::string option,
                                                   std::string optarg);
+  theory::bv::BvOptimizeSatProof stringToBvOptimizeSatProof(std::string option,
+                                                            std::string optarg);
 
   theory::strings::ProcessLoopMode stringToStringsProcessLoopMode(
       std::string option, std::string optarg);
@@ -238,6 +240,7 @@ public:
   static const std::string s_bitblastingModeHelp;
   static const std::string s_bvSatSolverHelp;
   static const std::string s_bvProofFormatHelp;
+  static const std::string s_bvOptimizeSatProofHelp;
   static const std::string s_booleanTermConversionModeHelp;
   static const std::string s_bvSlicerModeHelp;
   static const std::string s_stringToStringsProcessLoopModeHelp;