Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Mathias Preiner, Aina Niemetz, Abdalrhman Mohamed
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 : : * Bitblaster used to bitblast to Boolean Nodes.
14 : : */
15 : : #include "theory/bv/bitblast/node_bitblaster.h"
16 : :
17 : : #include "options/bv_options.h"
18 : : #include "theory/theory_model.h"
19 : : #include "theory/theory_state.h"
20 : :
21 : : namespace cvc5::internal {
22 : : namespace theory {
23 : : namespace bv {
24 : :
25 : 60927 : NodeBitblaster::NodeBitblaster(Env& env, TheoryState* s)
26 : 60927 : : TBitblaster<Node>(), EnvObj(env), d_state(s)
27 : : {
28 : 60927 : }
29 : :
30 : 8630220 : void NodeBitblaster::bbAtom(TNode node)
31 : : {
32 [ + + ]: 8630220 : node = node.getKind() == Kind::NOT ? node[0] : node;
33 : :
34 [ + + ]: 8630220 : if (hasBBAtom(node))
35 : : {
36 : 8537970 : return;
37 : : }
38 : :
39 : : /* Note: We rewrite here since it's not guaranteed (yet) that facts sent
40 : : * to theories are rewritten.
41 : : */
42 : 184506 : Node normalized = rewrite(node);
43 : : Node atom_bb =
44 : 184506 : normalized.getKind() != Kind::CONST_BOOLEAN
45 [ + - ]: 92253 : && normalized.getKind() != Kind::BITVECTOR_BIT
46 [ + - ]: 184506 : ? d_atomBBStrategies[static_cast<uint32_t>(normalized.getKind())](
47 : : normalized, this)
48 [ + - ][ - - ]: 276759 : : normalized;
49 : :
50 : 92253 : storeBBAtom(node, rewrite(atom_bb));
51 : : }
52 : :
53 : 92253 : void NodeBitblaster::storeBBAtom(TNode atom, Node atom_bb)
54 : : {
55 : 92253 : d_bbAtoms.emplace(atom, atom_bb);
56 : 92253 : }
57 : :
58 : 185104 : void NodeBitblaster::storeBBTerm(TNode node, const Bits& bits)
59 : : {
60 : 185104 : d_termCache.emplace(node, bits);
61 : 185104 : }
62 : :
63 : 19609200 : bool NodeBitblaster::hasBBAtom(TNode lit) const
64 : : {
65 [ - + ]: 19609200 : if (lit.getKind() == Kind::NOT)
66 : : {
67 : 0 : lit = lit[0];
68 : : }
69 : 19609200 : return d_bbAtoms.find(lit) != d_bbAtoms.end();
70 : : }
71 : :
72 : 64672 : void NodeBitblaster::makeVariable(TNode var, Bits& bits)
73 : : {
74 [ - + ][ - + ]: 64672 : Assert(bits.size() == 0);
[ - - ]
75 [ + + ]: 850792 : for (unsigned i = 0; i < utils::getSize(var); ++i)
76 : : {
77 : 786120 : bits.push_back(utils::mkBit(var, i));
78 : : }
79 : 64672 : d_variables.insert(var);
80 : 64672 : }
81 : :
82 : 0 : Node NodeBitblaster::getBBAtom(TNode node) const { return node; }
83 : :
84 : 702765 : void NodeBitblaster::bbTerm(TNode node, Bits& bits)
85 : : {
86 [ - + ][ - + ]: 702765 : Assert(node.getType().isBitVector());
[ - - ]
87 [ + + ]: 702765 : if (hasBBTerm(node))
88 : : {
89 : 517661 : getBBTerm(node, bits);
90 : 517661 : return;
91 : : }
92 : 185104 : d_termBBStrategies[static_cast<uint32_t>(node.getKind())](node, bits, this);
93 [ - + ][ - + ]: 185104 : Assert(bits.size() == utils::getSize(node));
[ - - ]
94 : 185104 : storeBBTerm(node, bits);
95 : : }
96 : :
97 : 9736880 : Node NodeBitblaster::getStoredBBAtom(TNode node)
98 : : {
99 : 9736880 : bool negated = false;
100 [ + + ]: 9736880 : if (node.getKind() == Kind::NOT)
101 : : {
102 : 4403570 : node = node[0];
103 : 4403570 : negated = true;
104 : : }
105 : :
106 [ - + ][ - + ]: 9736880 : Assert(hasBBAtom(node));
[ - - ]
107 : 19473800 : Node atom_bb = d_bbAtoms.at(node);
108 [ + + ]: 19473800 : return negated ? atom_bb.negate() : atom_bb;
109 : : }
110 : :
111 : 8066 : Node NodeBitblaster::getModelFromSatSolver(TNode a, bool fullModel)
112 : : {
113 : 8066 : NodeManager* nm = a.getNodeManager();
114 [ - + ]: 8066 : if (!hasBBTerm(a))
115 : : {
116 : 0 : return utils::mkConst(nm, utils::getSize(a), 0u);
117 : : }
118 : :
119 : : bool assignment;
120 : 16132 : Bits bits;
121 : 8066 : getBBTerm(a, bits);
122 : 16132 : Integer value(0);
123 : 16132 : Integer one(1), zero(0);
124 [ + + ]: 71113 : for (int i = bits.size() - 1; i >= 0; --i)
125 : : {
126 : 63047 : Integer bit;
127 [ + + ]: 63047 : if (d_state->hasSatValue(bits[i], assignment))
128 : : {
129 [ + + ]: 47757 : bit = assignment ? one : zero;
130 : : }
131 : : else
132 : : {
133 : 15290 : bit = zero;
134 : : }
135 : 63047 : value = value * 2 + bit;
136 : : }
137 : 8066 : return utils::mkConst(nm, bits.size(), value);
138 : : }
139 : :
140 : 9 : void NodeBitblaster::computeRelevantTerms(std::set<Node>& termSet)
141 : : {
142 [ - + ][ - + ]: 9 : Assert(options().bv.bitblastMode == options::BitblastMode::EAGER);
[ - - ]
143 [ + + ]: 32 : for (const auto& var : d_variables)
144 : : {
145 : 23 : termSet.insert(var);
146 : : }
147 : 9 : }
148 : :
149 : 4272 : bool NodeBitblaster::collectModelValues(TheoryModel* m,
150 : : const std::set<Node>& relevantTerms)
151 : : {
152 [ + + ]: 376332 : for (const auto& var : relevantTerms)
153 : : {
154 [ + + ]: 372060 : if (d_variables.find(var) == d_variables.end()) continue;
155 : :
156 : 8066 : Node const_value = getModelFromSatSolver(var, true);
157 [ + - ][ - + ]: 8066 : Assert(const_value.isNull() || const_value.isConst());
[ - + ][ - - ]
158 [ + - ]: 8066 : if (!const_value.isNull())
159 : : {
160 [ - + ]: 8066 : if (!m->assertEquality(var, const_value, true))
161 : : {
162 : 0 : return false;
163 : : }
164 : : }
165 : : }
166 : 4272 : return true;
167 : : }
168 : :
169 : 327528 : bool NodeBitblaster::isVariable(TNode node)
170 : : {
171 : 327528 : return d_variables.find(node) != d_variables.end();
172 : : }
173 : :
174 : 9574 : Node NodeBitblaster::applyAtomBBStrategy(TNode node)
175 : : {
176 [ - + ][ - + ]: 9574 : Assert(node.getKind() != Kind::CONST_BOOLEAN);
[ - - ]
177 [ - + ][ - + ]: 9574 : Assert(node.getKind() != Kind::BITVECTOR_BIT);
[ - - ]
178 : 9574 : return d_atomBBStrategies[static_cast<uint32_t>(node.getKind())](node, this);
179 : : }
180 : :
181 : : } // namespace bv
182 : : } // namespace theory
183 : : } // namespace cvc5::internal
|
