From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Wed, 9 Jan 2019 18:19:22 +0000 (+0100)
Subject: [BV Proofs] Option for proof format (#2777)
X-Git-Tag: cvc5-1.0.0~4296
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1df477011ed5d35f222340580cba916af3ba73b5;p=cvc5.git

[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 9cfa2d6d3..59a97c5a2 100644
--- 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 530632674..fa5791ac9 100644
--- 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 00290da7d..0422ae06f 100644
--- 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 36144e70e..c08c59d89 100644
--- 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 f96632696..126538436 100644
--- 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;