From bfc4e276709166bfde990357f048cf9ab2c65c6f Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Tue, 13 Jul 2021 12:02:37 -0700 Subject: [PATCH] bv: Simplify BV_BITBLAST_* proof rules. (#6871) Introduces BV_BITBLAST_STEP rule, which replaces BV_BITBLAST_X rules. --- src/proof/proof_rule.cpp | 42 +------------ src/proof/proof_rule.h | 51 +-------------- src/theory/bv/bitblast/proof_bitblaster.cpp | 50 +-------------- src/theory/bv/bitblast/proof_bitblaster.h | 4 -- src/theory/bv/proof_checker.cpp | 69 ++------------------- 5 files changed, 12 insertions(+), 204 deletions(-) diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp index 676fa6a63..def57532d 100644 --- a/src/proof/proof_rule.cpp +++ b/src/proof/proof_rule.cpp @@ -121,47 +121,7 @@ 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_ADD: return "BV_BITBLAST_ADD"; - 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_BITBLAST_STEP: return "BV_BITBLAST_STEP"; case PfRule::BV_EAGER_ATOM: return "BV_EAGER_ATOM"; //================================================= Datatype rules case PfRule::DT_UNIF: return "DT_UNIF"; diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index c1cf0338a..d20c3ecc0 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -730,63 +730,18 @@ enum class PfRule : uint32_t // --------------------- // Conclusion: (= t bitblast(t)) BV_BITBLAST, - // ======== Bitblast Bit-Vector Constant + // ======== Bitblast Bit-Vector Constant, Variable // 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_ADD, - 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, + BV_BITBLAST_STEP, + // ======== Eager Atom // Children: none // Arguments: (F) diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp index a1b856d88..9d4de1387 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.cpp +++ b/src/theory/bv/bitblast/proof_bitblaster.cpp @@ -23,50 +23,6 @@ namespace cvc5 { namespace theory { namespace bv { -std::unordered_map - BBProof::s_kindToPfRule = { - {kind::CONST_BITVECTOR, PfRule::BV_BITBLAST_CONST}, - {kind::EQUAL, PfRule::BV_BITBLAST_EQUAL}, - {kind::BITVECTOR_ULT, PfRule::BV_BITBLAST_ULT}, - {kind::BITVECTOR_ULE, PfRule::BV_BITBLAST_ULE}, - {kind::BITVECTOR_UGT, PfRule::BV_BITBLAST_UGT}, - {kind::BITVECTOR_UGE, PfRule::BV_BITBLAST_UGE}, - {kind::BITVECTOR_SLT, PfRule::BV_BITBLAST_SLT}, - {kind::BITVECTOR_SLE, PfRule::BV_BITBLAST_SLE}, - {kind::BITVECTOR_SGT, PfRule::BV_BITBLAST_SGT}, - {kind::BITVECTOR_SGE, PfRule::BV_BITBLAST_SGE}, - {kind::BITVECTOR_NOT, PfRule::BV_BITBLAST_NOT}, - {kind::BITVECTOR_CONCAT, PfRule::BV_BITBLAST_CONCAT}, - {kind::BITVECTOR_AND, PfRule::BV_BITBLAST_AND}, - {kind::BITVECTOR_OR, PfRule::BV_BITBLAST_OR}, - {kind::BITVECTOR_XOR, PfRule::BV_BITBLAST_XOR}, - {kind::BITVECTOR_XNOR, PfRule::BV_BITBLAST_XNOR}, - {kind::BITVECTOR_NAND, PfRule::BV_BITBLAST_NAND}, - {kind::BITVECTOR_NOR, PfRule::BV_BITBLAST_NOR}, - {kind::BITVECTOR_COMP, PfRule::BV_BITBLAST_COMP}, - {kind::BITVECTOR_MULT, PfRule::BV_BITBLAST_MULT}, - {kind::BITVECTOR_ADD, PfRule::BV_BITBLAST_ADD}, - {kind::BITVECTOR_SUB, PfRule::BV_BITBLAST_SUB}, - {kind::BITVECTOR_NEG, PfRule::BV_BITBLAST_NEG}, - {kind::BITVECTOR_UDIV, PfRule::BV_BITBLAST_UDIV}, - {kind::BITVECTOR_UREM, PfRule::BV_BITBLAST_UREM}, - {kind::BITVECTOR_SDIV, PfRule::BV_BITBLAST_SDIV}, - {kind::BITVECTOR_SREM, PfRule::BV_BITBLAST_SREM}, - {kind::BITVECTOR_SMOD, PfRule::BV_BITBLAST_SMOD}, - {kind::BITVECTOR_SHL, PfRule::BV_BITBLAST_SHL}, - {kind::BITVECTOR_LSHR, PfRule::BV_BITBLAST_LSHR}, - {kind::BITVECTOR_ASHR, PfRule::BV_BITBLAST_ASHR}, - {kind::BITVECTOR_ULTBV, PfRule::BV_BITBLAST_ULTBV}, - {kind::BITVECTOR_SLTBV, PfRule::BV_BITBLAST_SLTBV}, - {kind::BITVECTOR_ITE, PfRule::BV_BITBLAST_ITE}, - {kind::BITVECTOR_EXTRACT, PfRule::BV_BITBLAST_EXTRACT}, - {kind::BITVECTOR_REPEAT, PfRule::BV_BITBLAST_REPEAT}, - {kind::BITVECTOR_ZERO_EXTEND, PfRule::BV_BITBLAST_ZERO_EXTEND}, - {kind::BITVECTOR_SIGN_EXTEND, PfRule::BV_BITBLAST_SIGN_EXTEND}, - {kind::BITVECTOR_ROTATE_RIGHT, PfRule::BV_BITBLAST_ROTATE_RIGHT}, - {kind::BITVECTOR_ROTATE_LEFT, PfRule::BV_BITBLAST_ROTATE_LEFT}, -}; - BBProof::BBProof(TheoryState* state, ProofNodeManager* pnm, bool fineGrained) : d_bb(new BBSimple(state)), d_pnm(pnm), @@ -129,7 +85,7 @@ void BBProof::bbAtom(TNode node) d_bbMap.emplace(n, n_tobv); d_tcpg->addRewriteStep(n, n_tobv, - PfRule::BV_BITBLAST_VAR, + PfRule::BV_BITBLAST_STEP, {}, {n.eqNode(n_tobv)}, false); @@ -165,7 +121,7 @@ void BBProof::bbAtom(TNode node) } d_tcpg->addRewriteStep(c_tobv, n_tobv, - s_kindToPfRule.at(kind), + PfRule::BV_BITBLAST_STEP, {}, {c_tobv.eqNode(n_tobv)}, false); @@ -185,7 +141,7 @@ void BBProof::bbAtom(TNode node) Node c_tobv = nm->mkNode(n.getKind(), children_tobv); d_tcpg->addRewriteStep(c_tobv, n_tobv, - s_kindToPfRule.at(n.getKind()), + PfRule::BV_BITBLAST_STEP, {}, {c_tobv.eqNode(n_tobv)}, false); diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h index 428581fe0..17be4204c 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.h +++ b/src/theory/bv/bitblast/proof_bitblaster.h @@ -49,10 +49,6 @@ class BBProof TConvProofGenerator* getProofGenerator(); private: - /** Map node kinds to proof rules. */ - static std::unordered_map - s_kindToPfRule; - /** Return true if proofs are enabled. */ bool isProofsEnabled() const; diff --git a/src/theory/bv/proof_checker.cpp b/src/theory/bv/proof_checker.cpp index 711e9798c..cbaec7ca6 100644 --- a/src/theory/bv/proof_checker.cpp +++ b/src/theory/bv/proof_checker.cpp @@ -22,47 +22,7 @@ namespace bv { void BVProofRuleChecker::registerTo(ProofChecker* pc) { pc->registerChecker(PfRule::BV_BITBLAST, this); - pc->registerChecker(PfRule::BV_BITBLAST_CONST, this); - pc->registerChecker(PfRule::BV_BITBLAST_VAR, this); - pc->registerChecker(PfRule::BV_BITBLAST_EQUAL, this); - pc->registerChecker(PfRule::BV_BITBLAST_ULT, this); - pc->registerChecker(PfRule::BV_BITBLAST_ULE, this); - pc->registerChecker(PfRule::BV_BITBLAST_UGT, this); - pc->registerChecker(PfRule::BV_BITBLAST_UGE, this); - pc->registerChecker(PfRule::BV_BITBLAST_SLT, this); - pc->registerChecker(PfRule::BV_BITBLAST_SLE, this); - pc->registerChecker(PfRule::BV_BITBLAST_SGT, this); - pc->registerChecker(PfRule::BV_BITBLAST_SGE, this); - pc->registerChecker(PfRule::BV_BITBLAST_NOT, this); - pc->registerChecker(PfRule::BV_BITBLAST_CONCAT, this); - pc->registerChecker(PfRule::BV_BITBLAST_AND, this); - pc->registerChecker(PfRule::BV_BITBLAST_OR, this); - pc->registerChecker(PfRule::BV_BITBLAST_XOR, this); - pc->registerChecker(PfRule::BV_BITBLAST_XNOR, this); - pc->registerChecker(PfRule::BV_BITBLAST_NAND, this); - pc->registerChecker(PfRule::BV_BITBLAST_NOR, this); - pc->registerChecker(PfRule::BV_BITBLAST_COMP, this); - pc->registerChecker(PfRule::BV_BITBLAST_MULT, this); - pc->registerChecker(PfRule::BV_BITBLAST_ADD, this); - pc->registerChecker(PfRule::BV_BITBLAST_SUB, this); - pc->registerChecker(PfRule::BV_BITBLAST_NEG, this); - pc->registerChecker(PfRule::BV_BITBLAST_UDIV, this); - pc->registerChecker(PfRule::BV_BITBLAST_UREM, this); - pc->registerChecker(PfRule::BV_BITBLAST_SDIV, this); - pc->registerChecker(PfRule::BV_BITBLAST_SREM, this); - pc->registerChecker(PfRule::BV_BITBLAST_SMOD, this); - pc->registerChecker(PfRule::BV_BITBLAST_SHL, this); - pc->registerChecker(PfRule::BV_BITBLAST_LSHR, this); - pc->registerChecker(PfRule::BV_BITBLAST_ASHR, this); - pc->registerChecker(PfRule::BV_BITBLAST_ULTBV, this); - pc->registerChecker(PfRule::BV_BITBLAST_SLTBV, this); - pc->registerChecker(PfRule::BV_BITBLAST_ITE, this); - pc->registerChecker(PfRule::BV_BITBLAST_EXTRACT, this); - pc->registerChecker(PfRule::BV_BITBLAST_REPEAT, this); - pc->registerChecker(PfRule::BV_BITBLAST_ZERO_EXTEND, this); - pc->registerChecker(PfRule::BV_BITBLAST_SIGN_EXTEND, this); - pc->registerChecker(PfRule::BV_BITBLAST_ROTATE_RIGHT, this); - pc->registerChecker(PfRule::BV_BITBLAST_ROTATE_LEFT, this); + pc->registerChecker(PfRule::BV_BITBLAST_STEP, this); pc->registerChecker(PfRule::BV_EAGER_ATOM, this); } @@ -77,30 +37,11 @@ Node BVProofRuleChecker::checkInternal(PfRule id, Assert(args[0].getKind() == kind::EQUAL); return args[0]; } - else if (id == PfRule::BV_BITBLAST_CONST || id == PfRule::BV_BITBLAST_VAR - || id == PfRule::BV_BITBLAST_EQUAL || id == PfRule::BV_BITBLAST_ULT - || id == PfRule::BV_BITBLAST_ULE || id == PfRule::BV_BITBLAST_UGT - || id == PfRule::BV_BITBLAST_UGE || id == PfRule::BV_BITBLAST_SLT - || id == PfRule::BV_BITBLAST_SLE || id == PfRule::BV_BITBLAST_SGT - || id == PfRule::BV_BITBLAST_SGE || id == PfRule::BV_BITBLAST_NOT - || id == PfRule::BV_BITBLAST_CONCAT || id == PfRule::BV_BITBLAST_AND - || id == PfRule::BV_BITBLAST_OR || id == PfRule::BV_BITBLAST_XOR - || id == PfRule::BV_BITBLAST_XNOR || id == PfRule::BV_BITBLAST_NAND - || id == PfRule::BV_BITBLAST_NOR || id == PfRule::BV_BITBLAST_COMP - || id == PfRule::BV_BITBLAST_MULT || id == PfRule::BV_BITBLAST_ADD - || id == PfRule::BV_BITBLAST_SUB || id == PfRule::BV_BITBLAST_NEG - || id == PfRule::BV_BITBLAST_UDIV || id == PfRule::BV_BITBLAST_UREM - || id == PfRule::BV_BITBLAST_SDIV || id == PfRule::BV_BITBLAST_SREM - || id == PfRule::BV_BITBLAST_SMOD || id == PfRule::BV_BITBLAST_SHL - || id == PfRule::BV_BITBLAST_LSHR || id == PfRule::BV_BITBLAST_ASHR - || id == PfRule::BV_BITBLAST_ULTBV || id == PfRule::BV_BITBLAST_SLTBV - || id == PfRule::BV_BITBLAST_ITE || id == PfRule::BV_BITBLAST_EXTRACT - || id == PfRule::BV_BITBLAST_REPEAT - || id == PfRule::BV_BITBLAST_ZERO_EXTEND - || id == PfRule::BV_BITBLAST_SIGN_EXTEND - || id == PfRule::BV_BITBLAST_ROTATE_RIGHT - || id == PfRule::BV_BITBLAST_ROTATE_LEFT) + else if (id == PfRule::BV_BITBLAST_STEP) { + Assert(children.empty()); + Assert(args.size() == 1); + Assert(args[0].getKind() == kind::EQUAL); return args[0]; } else if (id == PfRule::BV_EAGER_ATOM) -- 2.30.2