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 : : * Bitblaster used to bitblast to Boolean Nodes.
11 : : */
12 : : #include "theory/bv/bitblast/node_bitblaster.h"
13 : :
14 : : #include "options/bv_options.h"
15 : : #include "theory/theory_model.h"
16 : : #include "theory/theory_state.h"
17 : :
18 : : namespace cvc5::internal {
19 : : namespace theory {
20 : : namespace bv {
21 : :
22 : 58621 : NodeBitblaster::NodeBitblaster(Env& env, TheoryState* s)
23 : 58621 : : TBitblaster<Node>(), EnvObj(env), d_state(s)
24 : : {
25 : 58621 : }
26 : :
27 : 7780402 : void NodeBitblaster::bbAtom(TNode node)
28 : : {
29 [ + + ]: 7780402 : node = node.getKind() == Kind::NOT ? node[0] : node;
30 : :
31 [ + + ]: 7780402 : if (hasBBAtom(node))
32 : : {
33 : 7699402 : return;
34 : : }
35 : :
36 : : /* Note: We rewrite here since it's not guaranteed (yet) that facts sent
37 : : * to theories are rewritten.
38 : : */
39 : 81000 : Node normalized = rewrite(node);
40 : : Node atom_bb =
41 : 162000 : normalized.getKind() != Kind::CONST_BOOLEAN
42 [ + - ]: 81000 : && normalized.getKind() != Kind::BITVECTOR_BIT
43 [ + - ]: 162000 : ? d_atomBBStrategies[static_cast<uint32_t>(normalized.getKind())](
44 : : normalized, this)
45 [ + - ][ - - ]: 243000 : : normalized;
46 : :
47 : 81000 : storeBBAtom(node, rewrite(atom_bb));
48 : 81000 : }
49 : :
50 : 81000 : void NodeBitblaster::storeBBAtom(TNode atom, Node atom_bb)
51 : : {
52 : 81000 : d_bbAtoms.emplace(atom, atom_bb);
53 : 81000 : }
54 : :
55 : 177105 : void NodeBitblaster::storeBBTerm(TNode node, const Bits& bits)
56 : : {
57 : 177105 : d_termCache.emplace(node, bits);
58 : 177105 : }
59 : :
60 : 19411914 : bool NodeBitblaster::hasBBAtom(TNode lit) const
61 : : {
62 [ - + ]: 19411914 : if (lit.getKind() == Kind::NOT)
63 : : {
64 : 0 : lit = lit[0];
65 : : }
66 : 19411914 : return d_bbAtoms.find(lit) != d_bbAtoms.end();
67 : : }
68 : :
69 : 57935 : void NodeBitblaster::makeVariable(TNode var, Bits& bits)
70 : : {
71 [ - + ][ - + ]: 57935 : Assert(bits.size() == 0);
[ - - ]
72 [ + + ]: 510819 : for (unsigned i = 0; i < utils::getSize(var); ++i)
73 : : {
74 : 452884 : bits.push_back(utils::mkBit(var, i));
75 : : }
76 : 57935 : d_variables.insert(var);
77 : 57935 : }
78 : :
79 : 0 : Node NodeBitblaster::getBBAtom(TNode node) const { return node; }
80 : :
81 : 416535 : void NodeBitblaster::bbTerm(TNode node, Bits& bits)
82 : : {
83 [ - + ][ - + ]: 416535 : Assert(node.getType().isBitVector());
[ - - ]
84 [ + + ]: 416535 : if (hasBBTerm(node))
85 : : {
86 : 239430 : getBBTerm(node, bits);
87 : 239430 : return;
88 : : }
89 : 177105 : d_termBBStrategies[static_cast<uint32_t>(node.getKind())](node, bits, this);
90 [ - + ][ - + ]: 177105 : Assert(bits.size() == utils::getSize(node));
[ - - ]
91 : 177105 : storeBBTerm(node, bits);
92 : : }
93 : :
94 : 9647137 : Node NodeBitblaster::getStoredBBAtom(TNode node)
95 : : {
96 : 9647137 : bool negated = false;
97 [ + + ]: 9647137 : if (node.getKind() == Kind::NOT)
98 : : {
99 : 4092998 : node = node[0];
100 : 4092998 : negated = true;
101 : : }
102 : :
103 [ - + ][ - + ]: 9647137 : Assert(hasBBAtom(node));
[ - - ]
104 : 9647137 : Node atom_bb = d_bbAtoms.at(node);
105 [ + + ]: 19294274 : return negated ? atom_bb.negate() : atom_bb;
106 : 9647137 : }
107 : :
108 : 6175 : Node NodeBitblaster::getModelFromSatSolver(TNode a, CVC5_UNUSED bool fullModel)
109 : : {
110 : 6175 : NodeManager* nm = a.getNodeManager();
111 [ - + ]: 6175 : if (!hasBBTerm(a))
112 : : {
113 : 0 : return utils::mkConst(nm, utils::getSize(a), 0u);
114 : : }
115 : :
116 : : bool assignment;
117 : 6175 : Bits bits;
118 : 6175 : getBBTerm(a, bits);
119 : 6175 : Integer value(0);
120 : 6175 : Integer one(1), zero(0);
121 [ + + ]: 55875 : for (int i = bits.size() - 1; i >= 0; --i)
122 : : {
123 : 49700 : Integer bit;
124 [ + + ]: 49700 : if (d_state->hasSatValue(bits[i], assignment))
125 : : {
126 [ + + ]: 37556 : bit = assignment ? one : zero;
127 : : }
128 : : else
129 : : {
130 : 12144 : bit = zero;
131 : : }
132 : 49700 : value = value * 2 + bit;
133 : 49700 : }
134 : 6175 : return utils::mkConst(nm, bits.size(), value);
135 : 6175 : }
136 : :
137 : 9 : void NodeBitblaster::computeRelevantTerms(std::set<Node>& termSet)
138 : : {
139 [ - + ][ - + ]: 9 : Assert(options().bv.bitblastMode == options::BitblastMode::EAGER);
[ - - ]
140 [ + + ]: 32 : for (const auto& var : d_variables)
141 : : {
142 : 23 : termSet.insert(var);
143 : : }
144 : 9 : }
145 : :
146 : 4322 : bool NodeBitblaster::collectModelValues(TheoryModel* m,
147 : : const std::set<Node>& relevantTerms)
148 : : {
149 [ + + ]: 286964 : for (const auto& var : relevantTerms)
150 : : {
151 [ + + ]: 282642 : if (d_variables.find(var) == d_variables.end()) continue;
152 : :
153 : 6175 : Node const_value = getModelFromSatSolver(var, true);
154 [ + - ][ + - ]: 6175 : Assert(const_value.isNull() || const_value.isConst());
[ - + ][ - + ]
[ - - ]
155 [ + - ]: 6175 : if (!const_value.isNull())
156 : : {
157 [ - + ]: 6175 : if (!m->assertEquality(var, const_value, true))
158 : : {
159 : 0 : return false;
160 : : }
161 : : }
162 [ + - ]: 6175 : }
163 : 4322 : return true;
164 : : }
165 : :
166 : 337104 : bool NodeBitblaster::isVariable(TNode node)
167 : : {
168 : 337104 : return d_variables.find(node) != d_variables.end();
169 : : }
170 : :
171 : 7714 : Node NodeBitblaster::applyAtomBBStrategy(TNode node)
172 : : {
173 [ - + ][ - + ]: 7714 : Assert(node.getKind() != Kind::CONST_BOOLEAN);
[ - - ]
174 [ - + ][ - + ]: 7714 : Assert(node.getKind() != Kind::BITVECTOR_BIT);
[ - - ]
175 : 7714 : return d_atomBBStrategies[static_cast<uint32_t>(node.getKind())](node, this);
176 : : }
177 : :
178 : : } // namespace bv
179 : : } // namespace theory
180 : : } // namespace cvc5::internal
|
