From 55c2f669abe354ffb258a0da89358f8c5366e2c4 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 22 Apr 2021 18:19:05 -0700 Subject: BV: Add proof logging for bit-blasting. (#6373) --- src/expr/proof_rule.cpp | 41 ++++++++++++++++++ src/expr/proof_rule.h | 62 ++++++++++++++++++++++++++++ src/expr/term_conversion_proof_generator.cpp | 3 ++ 3 files changed, 106 insertions(+) (limited to 'src/expr') diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 92944a7f4..fbeaea729 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -119,6 +119,47 @@ const char* toString(PfRule id) case PfRule::ARRAYS_TRUST: return "ARRAYS_TRUST"; //================================================= Bit-Vector rules case PfRule::BV_BITBLAST: return "BV_BITBLAST"; + case PfRule::BV_BITBLAST_CONST: return "BV_BITBLAST_CONST"; + case PfRule::BV_BITBLAST_VAR: return "BV_BITBLAST_VAR"; + case PfRule::BV_BITBLAST_EQUAL: return "BV_BITBLAST_EQUAL"; + case PfRule::BV_BITBLAST_ULT: return "BV_BITBLAST_ULT"; + case PfRule::BV_BITBLAST_ULE: return "BV_BITBLAST_ULE"; + case PfRule::BV_BITBLAST_UGT: return "BV_BITBLAST_UGT"; + case PfRule::BV_BITBLAST_UGE: return "BV_BITBLAST_UGE"; + case PfRule::BV_BITBLAST_SLT: return "BV_BITBLAST_SLT"; + case PfRule::BV_BITBLAST_SLE: return "BV_BITBLAST_SLE"; + case PfRule::BV_BITBLAST_SGT: return "BV_BITBLAST_SGT"; + case PfRule::BV_BITBLAST_SGE: return "BV_BITBLAST_SGE"; + case PfRule::BV_BITBLAST_NOT: return "BV_BITBLAST_NOT"; + case PfRule::BV_BITBLAST_CONCAT: return "BV_BITBLAST_CONCAT"; + case PfRule::BV_BITBLAST_AND: return "BV_BITBLAST_AND"; + case PfRule::BV_BITBLAST_OR: return "BV_BITBLAST_OR"; + case PfRule::BV_BITBLAST_XOR: return "BV_BITBLAST_XOR"; + case PfRule::BV_BITBLAST_XNOR: return "BV_BITBLAST_XNOR"; + case PfRule::BV_BITBLAST_NAND: return "BV_BITBLAST_NAND"; + case PfRule::BV_BITBLAST_NOR: return "BV_BITBLAST_NOR"; + case PfRule::BV_BITBLAST_COMP: return "BV_BITBLAST_COMP"; + case PfRule::BV_BITBLAST_MULT: return "BV_BITBLAST_MULT"; + case PfRule::BV_BITBLAST_PLUS: return "BV_BITBLAST_PLUS"; + case PfRule::BV_BITBLAST_SUB: return "BV_BITBLAST_SUB"; + case PfRule::BV_BITBLAST_NEG: return "BV_BITBLAST_NEG"; + case PfRule::BV_BITBLAST_UDIV: return "BV_BITBLAST_UDIV"; + case PfRule::BV_BITBLAST_UREM: return "BV_BITBLAST_UREM"; + case PfRule::BV_BITBLAST_SDIV: return "BV_BITBLAST_SDIV"; + case PfRule::BV_BITBLAST_SREM: return "BV_BITBLAST_SREM"; + case PfRule::BV_BITBLAST_SMOD: return "BV_BITBLAST_SMOD"; + case PfRule::BV_BITBLAST_SHL: return "BV_BITBLAST_SHL"; + case PfRule::BV_BITBLAST_LSHR: return "BV_BITBLAST_LSHR"; + case PfRule::BV_BITBLAST_ASHR: return "BV_BITBLAST_ASHR"; + case PfRule::BV_BITBLAST_ULTBV: return "BV_BITBLAST_ULTBV"; + case PfRule::BV_BITBLAST_SLTBV: return "BV_BITBLAST_SLTBV"; + case PfRule::BV_BITBLAST_ITE: return "BV_BITBLAST_ITE"; + case PfRule::BV_BITBLAST_EXTRACT: return "BV_BITBLAST_EXTRACT"; + case PfRule::BV_BITBLAST_REPEAT: return "BV_BITBLAST_REPEAT"; + case PfRule::BV_BITBLAST_ZERO_EXTEND: return "BV_BITBLAST_ZERO_EXTEND"; + case PfRule::BV_BITBLAST_SIGN_EXTEND: return "BV_BITBLAST_SIGN_EXTEND"; + case PfRule::BV_BITBLAST_ROTATE_RIGHT: return "BV_BITBLAST_ROTATE_RIGHT"; + case PfRule::BV_BITBLAST_ROTATE_LEFT: return "BV_BITBLAST_ROTATE_LEFT"; case PfRule::BV_EAGER_ATOM: return "BV_EAGER_ATOM"; //================================================= Datatype rules case PfRule::DT_UNIF: return "DT_UNIF"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index d2aa75d8c..88e344b8a 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -701,12 +701,74 @@ enum class PfRule : uint32_t ARRAYS_TRUST, //================================================= Bit-Vector rules + // Note: bitblast() represents the result of the bit-blasted term as a + // bit-vector consisting of the output bits of the bit-blasted circuit + // representation of the term. Terms are bit-blasted according to the + // strategies defined in + // theory/bv/bitblast/bitblast_strategies_template.h. // ======== Bitblast // Children: none // Arguments: (t) // --------------------- // Conclusion: (= t bitblast(t)) BV_BITBLAST, + // ======== Bitblast Bit-Vector Constant + // Children: none + // Arguments: (= t bitblast(t)) + // --------------------- + // Conclusion: (= t bitblast(t)) + BV_BITBLAST_CONST, + // ======== Bitblast Bit-Vector Variable + // Children: none + // Arguments: (= t bitblast(t)) + // --------------------- + // Conclusion: (= t bitblast(t)) + BV_BITBLAST_VAR, + // ======== Bitblast Bit-Vector Terms + // TODO cvc4-projects issue #275 + // Children: none + // Arguments: (= (KIND bitblast(child_1) ... bitblast(child_n)) bitblast(t)) + // --------------------- + // Conclusion: (= (KIND bitblast(child_1) ... bitblast(child_n)) bitblast(t)) + BV_BITBLAST_EQUAL, + BV_BITBLAST_ULT, + BV_BITBLAST_ULE, + BV_BITBLAST_UGT, + BV_BITBLAST_UGE, + BV_BITBLAST_SLT, + BV_BITBLAST_SLE, + BV_BITBLAST_SGT, + BV_BITBLAST_SGE, + BV_BITBLAST_NOT, + BV_BITBLAST_CONCAT, + BV_BITBLAST_AND, + BV_BITBLAST_OR, + BV_BITBLAST_XOR, + BV_BITBLAST_XNOR, + BV_BITBLAST_NAND, + BV_BITBLAST_NOR, + BV_BITBLAST_COMP, + BV_BITBLAST_MULT, + BV_BITBLAST_PLUS, + BV_BITBLAST_SUB, + BV_BITBLAST_NEG, + BV_BITBLAST_UDIV, + BV_BITBLAST_UREM, + BV_BITBLAST_SDIV, + BV_BITBLAST_SREM, + BV_BITBLAST_SMOD, + BV_BITBLAST_SHL, + BV_BITBLAST_LSHR, + BV_BITBLAST_ASHR, + BV_BITBLAST_ULTBV, + BV_BITBLAST_SLTBV, + BV_BITBLAST_ITE, + BV_BITBLAST_EXTRACT, + BV_BITBLAST_REPEAT, + BV_BITBLAST_ZERO_EXTEND, + BV_BITBLAST_SIGN_EXTEND, + BV_BITBLAST_ROTATE_RIGHT, + BV_BITBLAST_ROTATE_LEFT, // ======== Eager Atom // Children: none // Arguments: (F) diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp index 2233dcc7b..18057e149 100644 --- a/src/expr/term_conversion_proof_generator.cpp +++ b/src/expr/term_conversion_proof_generator.cpp @@ -133,6 +133,9 @@ Node TConvProofGenerator::registerRewriteStep(Node t, uint32_t tctx, bool isPre) { + Assert(!t.isNull()); + Assert(!s.isNull()); + if (t == s) { return Node::null(); -- cgit v1.2.3