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