From 1df477011ed5d35f222340580cba916af3ba73b5 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Wed, 9 Jan 2019 19:19:22 +0100 Subject: [PATCH] [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. --- src/options/bv_bitblast_mode.cpp | 13 ++++++++++ src/options/bv_bitblast_mode.h | 21 ++++++++++++++++ src/options/bv_options.toml | 11 +++++++++ src/options/options_handler.cpp | 42 ++++++++++++++++++++++++++++++++ src/options/options_handler.h | 4 +++ 5 files changed, 91 insertions(+) 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; -- 2.30.2