[BV Proofs] Option for proof format (#2777)

We're building out a system whereby (eager) BV proofs can be emitted in
one of three formats. Let's add an option for specifying which!

My testing mechanism was not very thorough: I verified that I could specify each of the following option values:
* `er`
* `lrat`
* `drat`
* `help`

and that I could not provide random other option values.

diff --git a/src/options/bv_bitblast_mode.cpp b/src/options/bv_bitblast_mode.cpp
index 9cfa2d6d36fdbcb7b884518ab82cde82852c96e9..59a97c5a2b06bda289318881381a68f7f4a28a08 100644 (file)
--- a/src/options/bv_bitblast_mode.cpp
+++ b/src/options/bv_bitblast_mode.cpp
@@ -68,4 +68,17 @@ std::ostream& operator<<(std::ostream& out, theory::bv::SatSolverMode solver) {
   return out;
 }
 
+std::ostream& operator<<(std::ostream& out, theory::bv::BvProofFormat format)
+{
+  switch (format)
+  {
+    case theory::bv::BITVECTOR_PROOF_ER: out << "BITVECTOR_PROOF_ER"; break;
+    case theory::bv::BITVECTOR_PROOF_DRAT: out << "BITVECTOR_PROOF_DRAT"; break;
+    case theory::bv::BITVECTOR_PROOF_LRAT: out << "BITVECTOR_PROOF_LRAT"; break;
+    default: out << "BvProofFormat:UNKNOWN![" << unsigned(format) << "]";
+  }
+
+  return out;
+}
+
 }/* CVC4 namespace */

diff --git a/src/options/bv_bitblast_mode.h b/src/options/bv_bitblast_mode.h
index 5306326741f02a3c234f2fb93b17c322c00a992e..fa5791ac922c4934b7f7602b566529b432ab4163 100644 (file)
--- a/src/options/bv_bitblast_mode.h
+++ b/src/options/bv_bitblast_mode.h
@@ -68,12 +68,33 @@ enum SatSolverMode
   SAT_SOLVER_CADICAL,
 }; /* enum SatSolver */
 
+/**
+ * When the BV solver does eager bitblasting backed by CryptoMiniSat, proofs
+ * can be written in a variety of formats.
+ */
+enum BvProofFormat
+{
+  /**
+   * Write extended resolution proofs.
+   */
+  BITVECTOR_PROOF_ER,
+  /**
+   * Write DRAT proofs.
+   */
+  BITVECTOR_PROOF_DRAT,
+  /**
+   * Write LRAT proofs.
+   */
+  BITVECTOR_PROOF_LRAT,
+};
+
 }/* CVC4::theory::bv namespace */
 }/* CVC4::theory namespace */
 
 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);
 
 }/* CVC4 namespace */
 

diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index 00290da7d5fe8e242d38946c8b360a122cac763d..0422ae06f912e1630629d12c1109c4b989cdbcc0 100644 (file)
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -2,6 +2,17 @@ id     = "BV"
 name   = "Bitvector theory"
 header = "options/bv_options.h"
 
+[[option]]
+  name       = "bvProofFormat"
+  category   = "expert"
+  long       = "bv-proof-format=MODE"
+  type       = "CVC4::theory::bv::BvProofFormat"
+  default    = "CVC4::theory::bv::BITVECTOR_PROOF_LRAT"
+  handler    = "stringToBvProofFormat"
+  predicates = ["satSolverEnabledBuild"]
+  includes   = ["options/bv_bitblast_mode.h"]
+  help       = "choose which UNSAT proof format to use, see --bv-sat-solver=help"
+
 [[option]]
   name       = "bvSatSolver"
   smt_name   = "bv-sat-solver"

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 36144e70ec0e29ef42ee3f28417fde7888a83b5e..c08c59d89ef6a55cbba6375f925fc3aca9705a4b 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1203,6 +1203,48 @@ theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option,
   }
 }
 
+const std::string OptionsHandler::s_bvProofFormatHelp =
+    "\
+Proof formats currently supported by the --bv-proof-format option:\n\
+\n\
+  lrat : DRAT with unit propagation hints to accelerate checking (default)\n\
+\n\
+  drat : Deletion and Resolution Asymmetric Tautology Additions \n\
+\n\
+  er : Extended Resolution, i.e. resolution with new variable definitions\n\
+\n\
+This option controls which underlying UNSAT proof format is used in BV proofs.\n\
+\n\
+Note: Currently this option does nothing. BV proofs are a work in progress!\
+";
+
+theory::bv::BvProofFormat OptionsHandler::stringToBvProofFormat(
+    std::string option, std::string optarg)
+{
+  if (optarg == "er")
+  {
+    return theory::bv::BITVECTOR_PROOF_ER;
+  }
+  else if (optarg == "lrat")
+  {
+    return theory::bv::BITVECTOR_PROOF_LRAT;
+  }
+  else if (optarg == "drat")
+  {
+    return theory::bv::BITVECTOR_PROOF_DRAT;
+  }
+  else if (optarg == "help")
+  {
+    puts(s_bvProofFormatHelp.c_str());
+    exit(1);
+  }
+  else
+  {
+    throw OptionException(std::string("unknown option for --bv-proof-format: `")
+                          + optarg + "'.  Try --bv-proof-format=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 f9663269671e0f2bb5e3cf8c380070de1dc0b6eb..126538436daa6994e5d718fc9b54db207ba18ef1 100644 (file)
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -145,6 +145,9 @@ public:
   theory::bv::SatSolverMode stringToSatSolver(std::string option,
                                               std::string optarg);
 
+  theory::bv::BvProofFormat stringToBvProofFormat(std::string option,
+                                                  std::string optarg);
+
   // theory/uf/options_handlers.h
   theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg);
 
@@ -230,6 +233,7 @@ public:
   /* Help strings */
   static const std::string s_bitblastingModeHelp;
   static const std::string s_bvSatSolverHelp;
+  static const std::string s_bvProofFormatHelp;
   static const std::string s_booleanTermConversionModeHelp;
   static const std::string s_bvSlicerModeHelp;
   static const std::string s_boolToBVModeHelp;