Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * A bit-blaster wrapper around BBSimple for proof logging.
11 : : */
12 : : #include "theory/bv/bitblast/proof_bitblaster.h"
13 : :
14 : : #include <unordered_set>
15 : :
16 : : #include "proof/conv_proof_generator.h"
17 : : #include "theory/bv/bitblast/bitblast_proof_generator.h"
18 : : #include "theory/theory_model.h"
19 : :
20 : : namespace cvc5::internal {
21 : : namespace theory {
22 : : namespace bv {
23 : :
24 : 18085 : BBProof::BBProof(Env& env, TheoryState* state, bool fineGrained)
25 : : : EnvObj(env),
26 : 18085 : d_bb(new NodeBitblaster(env, state)),
27 : 18085 : d_tcontext(new TheoryLeafTermContext(theory::THEORY_BV)),
28 : 36170 : d_tcpg(new TConvProofGenerator(
29 : : env,
30 : : nullptr,
31 : : /* ONCE to visit each term only once, post-order. FIXPOINT
32 : : * could lead to infinite loops due to terms being rewritten
33 : : * to terms that contain themselves */
34 : : TConvPolicy::ONCE,
35 : : /* STATIC to get the same ProofNode for a shared subterm. */
36 : : TConvCachePolicy::STATIC,
37 : : "BBProof::TConvProofGenerator",
38 : 18085 : d_tcontext.get(),
39 : 18085 : false)),
40 : 18085 : d_bbpg(new BitblastProofGenerator(env, d_tcpg.get())),
41 : 36170 : d_recordFineGrainedProofs(fineGrained)
42 : : {
43 : 18085 : }
44 : :
45 : 28428 : BBProof::~BBProof() {}
46 : :
47 : 31990 : void BBProof::bbAtom(TNode node)
48 : : {
49 [ + + ][ + + ]: 31990 : bool fineProofs = isProofsEnabled() && d_recordFineGrainedProofs;
50 : :
51 : : /* Bit-blasting bit-vector atoms consists of 3 steps:
52 : : * 1. rewrite the atom
53 : : * 2. bit-blast the rewritten atom
54 : : * 3. rewrite the resulting bit-blasted term
55 : : *
56 : : * This happens in a single call to d_bb->bbAtom(...). When we record
57 : : * fine-grained proofs, we explicitly record the above 3 steps.
58 : : *
59 : : * Note: The below post-order traversal corresponds to the recursive
60 : : * bit-blasting of bit-vector terms that happens implicitly when calling the
61 : : * corresponding bit-blasting strategy in d_bb->bbAtom(...).
62 : : */
63 [ + + ]: 31990 : if (fineProofs)
64 : : {
65 : 7726 : std::vector<TNode> visit;
66 : 7726 : std::unordered_set<TNode> visited;
67 : 7726 : NodeManager* nm = nodeManager();
68 : :
69 : : // post-rewrite atom
70 : 7726 : Node rwNode = rewrite(node);
71 : :
72 : : // Post-order traversal of `rwNode` to make sure that all subterms are
73 : : // bit-blasted and recorded.
74 : 7726 : visit.push_back(rwNode);
75 [ + + ]: 132974 : while (!visit.empty())
76 : : {
77 : 125248 : TNode n = visit.back();
78 : 125248 : if (hasBBAtom(n) || hasBBTerm(n))
79 : : {
80 : 5709 : visit.pop_back();
81 : 5709 : continue;
82 : : }
83 : :
84 [ + + ]: 119539 : if (visited.find(n) == visited.end())
85 : : {
86 : 59558 : visited.insert(n);
87 [ + + ]: 59558 : if (!Theory::isLeafOf(n, theory::THEORY_BV))
88 : : {
89 : 34198 : visit.insert(visit.end(), n.begin(), n.end());
90 : : }
91 : : }
92 : : else
93 : : {
94 : : /* Handle BV theory leafs as variables, i.e., apply the BITVECTOR_BIT
95 : : * operator to each bit of `n`. */
96 [ + + ][ + + ]: 59981 : if (Theory::isLeafOf(n, theory::THEORY_BV) && !n.isConst())
[ + - ][ + + ]
[ - - ]
97 : : {
98 : 17747 : Bits bits;
99 : 17747 : d_bb->makeVariable(n, bits);
100 : :
101 : 17747 : Node bbt = nm->mkNode(Kind::BITVECTOR_FROM_BOOLS, bits);
102 : 17747 : d_bbMap.emplace(n, bbt);
103 : 35494 : d_tcpg->addRewriteStep(
104 : : n, bbt, ProofRule::BV_BITBLAST_STEP, {}, {n.eqNode(bbt)});
105 : 17747 : }
106 [ + + ]: 42234 : else if (n.getType().isBitVector())
107 : : {
108 : 34508 : Bits bits;
109 : 34508 : d_bb->bbTerm(n, bits);
110 : :
111 : 34508 : Node bbt = nm->mkNode(Kind::BITVECTOR_FROM_BOOLS, bits);
112 : 34508 : Node rbbt;
113 [ + + ]: 34508 : if (n.isConst())
114 : : {
115 : 8036 : d_bbMap.emplace(n, bbt);
116 : 8036 : rbbt = n;
117 : : }
118 : : else
119 : : {
120 : 26472 : d_bbMap.emplace(n, bbt);
121 : 26472 : rbbt = reconstruct(n);
122 : : }
123 : 69016 : d_tcpg->addRewriteStep(
124 : : rbbt, bbt, ProofRule::BV_BITBLAST_STEP, {}, {rbbt.eqNode(bbt)});
125 : 34508 : }
126 : : else
127 : : {
128 [ - + ][ - + ]: 7726 : Assert(n == rwNode);
[ - - ]
129 : : }
130 : 59981 : visit.pop_back();
131 : : }
132 [ + + ]: 125248 : }
133 : :
134 : : /* Bit-blast given rewritten bit-vector atom `node`.
135 : : * Note: This will pre and post-rewrite and store it in the bit-blasting
136 : : * cache. */
137 : 7726 : d_bb->bbAtom(node);
138 : 7726 : Node result = d_bb->getStoredBBAtom(node);
139 : :
140 : : // Retrieve bit-blasted `rwNode` without post-rewrite.
141 : 15452 : Node bbt = rwNode.getKind() == Kind::CONST_BOOLEAN
142 [ - + ]: 7726 : || rwNode.getKind() == Kind::BITVECTOR_BIT
143 [ + - ]: 7726 : ? rwNode
144 [ + - ][ - - ]: 15452 : : d_bb->applyAtomBBStrategy(rwNode);
145 : :
146 : 7726 : Node rbbt = reconstruct(rwNode);
147 : :
148 : 15452 : d_tcpg->addRewriteStep(
149 : : rbbt, bbt, ProofRule::BV_BITBLAST_STEP, {}, {rbbt.eqNode(bbt)});
150 : :
151 : 7726 : d_bbpg->addBitblastStep(node, bbt, node.eqNode(result));
152 : 7726 : }
153 : : else
154 : : {
155 : 24264 : d_bb->bbAtom(node);
156 : :
157 : : /* Record coarse-grain bit-blast proof step. */
158 [ + + ][ + - ]: 24264 : if (isProofsEnabled() && !d_recordFineGrainedProofs)
[ + + ]
159 : : {
160 : 24106 : Node bbt = getStoredBBAtom(node);
161 : 24106 : d_bbpg->addBitblastStep(Node(), Node(), node.eqNode(bbt));
162 : 24106 : }
163 : : }
164 : 31990 : }
165 : :
166 : 34198 : Node BBProof::reconstruct(TNode t)
167 : : {
168 : 34198 : NodeManager* nm = nodeManager();
169 : :
170 : 34198 : std::vector<Node> children;
171 [ + + ]: 34198 : if (t.getMetaKind() == kind::metakind::PARAMETERIZED)
172 : : {
173 : 8879 : children.push_back(t.getOperator());
174 : : }
175 [ + + ]: 92162 : for (const auto& child : t)
176 : : {
177 : 57964 : children.push_back(d_bbMap.at(child));
178 : 57964 : }
179 : 68396 : return nm->mkNode(t.getKind(), children);
180 : 34198 : }
181 : :
182 : 1984149 : bool BBProof::hasBBAtom(TNode atom) const { return d_bb->hasBBAtom(atom); }
183 : :
184 : 125603 : bool BBProof::hasBBTerm(TNode atom) const { return d_bb->hasBBTerm(atom); }
185 : :
186 : 1890733 : Node BBProof::getStoredBBAtom(TNode node)
187 : : {
188 : 1890733 : return d_bb->getStoredBBAtom(node);
189 : : }
190 : :
191 : 105 : void BBProof::getBBTerm(TNode node, Bits& bits) const
192 : : {
193 : 105 : d_bb->getBBTerm(node, bits);
194 : 105 : }
195 : :
196 : 3738 : bool BBProof::collectModelValues(TheoryModel* m,
197 : : const std::set<Node>& relevantTerms)
198 : : {
199 : 3738 : return d_bb->collectModelValues(m, relevantTerms);
200 : : }
201 : :
202 : 1866379 : BitblastProofGenerator* BBProof::getProofGenerator() { return d_bbpg.get(); }
203 : :
204 : 56254 : bool BBProof::isProofsEnabled() const { return d_env.isTheoryProofProducing(); }
205 : :
206 : : } // namespace bv
207 : : } // namespace theory
208 : : } // namespace cvc5::internal
|
