From 7a2312eb876ddd632bd5cdcda34ca6a550f55df7 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Mon, 1 Nov 2021 18:00:12 -0700 Subject: [PATCH] bv: Remove remaining Rewriter::rewrite calls. (#7545) --- .../bv/bitblast/bitblast_proof_generator.cpp | 9 ++-- .../bv/bitblast/bitblast_proof_generator.h | 7 ++- src/theory/bv/bitblast/bitblaster.h | 52 ------------------- src/theory/bv/bitblast/proof_bitblaster.cpp | 5 +- .../theory_bv_rewrite_rules_normalization.h | 6 --- 5 files changed, 13 insertions(+), 66 deletions(-) diff --git a/src/theory/bv/bitblast/bitblast_proof_generator.cpp b/src/theory/bv/bitblast/bitblast_proof_generator.cpp index 57435f651..c05243e8c 100644 --- a/src/theory/bv/bitblast/bitblast_proof_generator.cpp +++ b/src/theory/bv/bitblast/bitblast_proof_generator.cpp @@ -21,9 +21,10 @@ namespace cvc5 { namespace theory { namespace bv { -BitblastProofGenerator::BitblastProofGenerator(ProofNodeManager* pnm, +BitblastProofGenerator::BitblastProofGenerator(Env& env, + ProofNodeManager* pnm, TConvProofGenerator* tcpg) - : d_pnm(pnm), d_tcpg(tcpg) + : EnvObj(env), d_pnm(pnm), d_tcpg(tcpg) { } @@ -78,7 +79,7 @@ std::shared_ptr BitblastProofGenerator::getProofFor(Node eq) * sub-terms and recording these bit-blast steps in the conversion proof. */ - Node rwt = Rewriter::rewrite(t); + Node rwt = rewrite(t); std::vector transSteps; @@ -94,7 +95,7 @@ std::shared_ptr BitblastProofGenerator::getProofFor(Node eq) transSteps.push_back(rwt.eqNode(bbt)); // Record post-rewrite of bit-blasted term. - Node rwbbt = Rewriter::rewrite(bbt); + Node rwbbt = rewrite(bbt); if (bbt != rwbbt) { cdp.addStep(bbt.eqNode(rwbbt), PfRule::REWRITE, {}, {bbt}); diff --git a/src/theory/bv/bitblast/bitblast_proof_generator.h b/src/theory/bv/bitblast/bitblast_proof_generator.h index 114bf4749..a0627010a 100644 --- a/src/theory/bv/bitblast/bitblast_proof_generator.h +++ b/src/theory/bv/bitblast/bitblast_proof_generator.h @@ -19,6 +19,7 @@ #include "proof/proof_generator.h" #include "proof/proof_node_manager.h" +#include "smt/env_obj.h" namespace cvc5 { @@ -28,10 +29,12 @@ namespace theory { namespace bv { /** Proof generator fot bit-blast proofs. */ -class BitblastProofGenerator : public ProofGenerator +class BitblastProofGenerator : public ProofGenerator, protected EnvObj { public: - BitblastProofGenerator(ProofNodeManager* pnm, TConvProofGenerator* tcpg); + BitblastProofGenerator(Env& env, + ProofNodeManager* pnm, + TConvProofGenerator* tcpg); ~BitblastProofGenerator(){}; /** diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index ef75bd5f8..fddf6c51e 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -199,58 +199,6 @@ void TBitblaster::invalidateModelCache() d_modelCache.clear(); } -template -Node TBitblaster::getTermModel(TNode node, bool fullModel) -{ - if (d_modelCache.find(node) != d_modelCache.end()) return d_modelCache[node]; - - if (node.isConst()) return node; - - Node value = getModelFromSatSolver(node, false); - if (!value.isNull()) - { - Debug("bv-equality-status") - << "TLazyBitblaster::getTermModel from SatSolver" << node << " => " - << value << "\n"; - d_modelCache[node] = value; - Assert(value.isConst()); - return value; - } - - if (Theory::isLeafOf(node, theory::THEORY_BV)) - { - // if it is a leaf may ask for fullModel - value = getModelFromSatSolver(node, true); - Debug("bv-equality-status") << "TLazyBitblaster::getTermModel from VarValue" - << node << " => " << value << "\n"; - Assert((fullModel && !value.isNull() && value.isConst()) || !fullModel); - if (!value.isNull()) - { - d_modelCache[node] = value; - } - return value; - } - Assert(node.getType().isBitVector()); - - NodeBuilder nb(node.getKind()); - if (node.getMetaKind() == kind::metakind::PARAMETERIZED) - { - nb << node.getOperator(); - } - - for (unsigned i = 0; i < node.getNumChildren(); ++i) - { - nb << getTermModel(node[i], fullModel); - } - value = nb; - value = Rewriter::rewrite(value); - Assert(value.isConst()); - d_modelCache[node] = value; - Debug("bv-term-model") << "TLazyBitblaster::getTermModel Building Value" - << node << " => " << value << "\n"; - return value; -} - } // namespace bv } // namespace theory } // namespace cvc5 diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp index 6119e9d7c..d8f327b29 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.cpp +++ b/src/theory/bv/bitblast/proof_bitblaster.cpp @@ -45,7 +45,8 @@ BBProof::BBProof(Env& env, d_tcontext.get(), false) : nullptr), - d_bbpg(pnm ? new BitblastProofGenerator(pnm, d_tcpg.get()) : nullptr), + d_bbpg(pnm ? new BitblastProofGenerator(env, pnm, d_tcpg.get()) + : nullptr), d_recordFineGrainedProofs(fineGrained) { } @@ -75,7 +76,7 @@ void BBProof::bbAtom(TNode node) NodeManager* nm = NodeManager::currentNM(); // post-rewrite atom - Node rwNode = Rewriter::rewrite(node); + Node rwNode = rewrite(node); // Post-order traversal of `rwNode` to make sure that all subterms are // bit-blasted and recorded. diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 5ead8a215..d73497adf 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -844,15 +844,9 @@ inline Node RewriteRule::apply(TNode node) if (newLeft < newRight) { - Assert((newRight == left && newLeft == right) - || Rewriter::rewrite(newRight) != left - || Rewriter::rewrite(newLeft) != right); return newRight.eqNode(newLeft); } - Assert((newLeft == left && newRight == right) - || Rewriter::rewrite(newLeft) != left - || Rewriter::rewrite(newRight) != right); return newLeft.eqNode(newRight); } -- 2.30.2