Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Mathias Preiner, Aina Niemetz, Daniel Larraz
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 : 58138 : NodeBitblaster::NodeBitblaster(Env& env, TheoryState* s)
26 : 58138 : : TBitblaster<Node>(), EnvObj(env), d_state(s)
27 : : {
28 : 58138 : }
29 : :
30 : 9975140 : void NodeBitblaster::bbAtom(TNode node)
31 : : {
32 [ + + ]: 9975140 : node = node.getKind() == Kind::NOT ? node[0] : node;
33 : :
34 [ + + ]: 9975140 : if (hasBBAtom(node))
35 : : {
36 : 9897600 : return;
37 : : }
38 : :
39 : : /* Note: We rewrite here since it's not guaranteed (yet) that facts sent
40 : : * to theories are rewritten.
41 : : */
42 : 155088 : Node normalized = rewrite(node);
43 : : Node atom_bb =
44 : 155088 : normalized.getKind() != Kind::CONST_BOOLEAN
45 [ + - ]: 77544 : && normalized.getKind() != Kind::BITVECTOR_BIT
46 [ + - ]: 155088 : ? d_atomBBStrategies[static_cast<uint32_t>(normalized.getKind())](
47 : : normalized, this)
48 [ + - ][ - - ]: 232632 : : normalized;
49 : :
50 : 77544 : storeBBAtom(node, rewrite(atom_bb));
51 : : }
52 : :
53 : 77544 : void NodeBitblaster::storeBBAtom(TNode atom, Node atom_bb)
54 : : {
55 : 77544 : d_bbAtoms.emplace(atom, atom_bb);
56 : 77544 : }
57 : :
58 : 176130 : void NodeBitblaster::storeBBTerm(TNode node, const Bits& bits)
59 : : {
60 : 176130 : d_termCache.emplace(node, bits);
61 : 176130 : }
62 : :
63 : 24494700 : bool NodeBitblaster::hasBBAtom(TNode lit) const
64 : : {
65 [ - + ]: 24494700 : if (lit.getKind() == Kind::NOT)
66 : : {
67 : 0 : lit = lit[0];
68 : : }
69 : 24494700 : return d_bbAtoms.find(lit) != d_bbAtoms.end();
70 : : }
71 : :
72 : 58955 : void NodeBitblaster::makeVariable(TNode var, Bits& bits)
73 : : {
74 [ - + ][ - + ]: 58955 : Assert(bits.size() == 0);
[ - - ]
75 [ + + ]: 523858 : for (unsigned i = 0; i < utils::getSize(var); ++i)
76 : : {
77 : 464903 : bits.push_back(utils::mkBit(var, i));
78 : : }
79 : 58955 : d_variables.insert(var);
80 : 58955 : }
81 : :
82 : 0 : Node NodeBitblaster::getBBAtom(TNode node) const { return node; }
83 : :
84 : 635672 : void NodeBitblaster::bbTerm(TNode node, Bits& bits)
85 : : {
86 [ - + ][ - + ]: 635672 : Assert(node.getType().isBitVector());
[ - - ]
87 [ + + ]: 635672 : if (hasBBTerm(node))
88 : : {
89 : 459542 : getBBTerm(node, bits);
90 : 459542 : return;
91 : : }
92 : 176130 : d_termBBStrategies[static_cast<uint32_t>(node.getKind())](node, bits, this);
93 [ - + ][ - + ]: 176130 : Assert(bits.size() == utils::getSize(node));
[ - - ]
94 : 176130 : storeBBTerm(node, bits);
95 : : }
96 : :
97 : 12186500 : Node NodeBitblaster::getStoredBBAtom(TNode node)
98 : : {
99 : 12186500 : bool negated = false;
100 [ + + ]: 12186500 : if (node.getKind() == Kind::NOT)
101 : : {
102 : 5364760 : node = node[0];
103 : 5364760 : negated = true;
104 : : }
105 : :
106 [ - + ][ - + ]: 12186500 : Assert(hasBBAtom(node));
[ - - ]
107 : 24373000 : Node atom_bb = d_bbAtoms.at(node);
108 [ + + ]: 24373000 : return negated ? atom_bb.negate() : atom_bb;
109 : : }
110 : :
111 : 6135 : Node NodeBitblaster::getModelFromSatSolver(TNode a, bool fullModel)
112 : : {
113 : 6135 : NodeManager* nm = a.getNodeManager();
114 [ - + ]: 6135 : if (!hasBBTerm(a))
115 : : {
116 : 0 : return utils::mkConst(nm, utils::getSize(a), 0u);
117 : : }
118 : :
119 : : bool assignment;
120 : 12270 : Bits bits;
121 : 6135 : getBBTerm(a, bits);
122 : 12270 : Integer value(0);
123 : 12270 : Integer one(1), zero(0);
124 [ + + ]: 55607 : for (int i = bits.size() - 1; i >= 0; --i)
125 : : {
126 : 49472 : Integer bit;
127 [ + + ]: 49472 : if (d_state->hasSatValue(bits[i], assignment))
128 : : {
129 [ + + ]: 37304 : bit = assignment ? one : zero;
130 : : }
131 : : else
132 : : {
133 : 12168 : bit = zero;
134 : : }
135 : 49472 : value = value * 2 + bit;
136 : : }
137 : 6135 : 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 : 3666 : bool NodeBitblaster::collectModelValues(TheoryModel* m,
150 : : const std::set<Node>& relevantTerms)
151 : : {
152 [ + + ]: 282874 : for (const auto& var : relevantTerms)
153 : : {
154 [ + + ]: 279208 : if (d_variables.find(var) == d_variables.end()) continue;
155 : :
156 : 6135 : Node const_value = getModelFromSatSolver(var, true);
157 [ + - ][ - + ]: 6135 : Assert(const_value.isNull() || const_value.isConst());
[ - + ][ - - ]
158 [ + - ]: 6135 : if (!const_value.isNull())
159 : : {
160 [ - + ]: 6135 : if (!m->assertEquality(var, const_value, true))
161 : : {
162 : 0 : return false;
163 : : }
164 : : }
165 : : }
166 : 3666 : return true;
167 : : }
168 : :
169 : 327271 : bool NodeBitblaster::isVariable(TNode node)
170 : : {
171 : 327271 : return d_variables.find(node) != d_variables.end();
172 : : }
173 : :
174 : 7942 : Node NodeBitblaster::applyAtomBBStrategy(TNode node)
175 : : {
176 [ - + ][ - + ]: 7942 : Assert(node.getKind() != Kind::CONST_BOOLEAN);
[ - - ]
177 [ - + ][ - + ]: 7942 : Assert(node.getKind() != Kind::BITVECTOR_BIT);
[ - - ]
178 : 7942 : return d_atomBBStrategies[static_cast<uint32_t>(node.getKind())](node, this);
179 : : }
180 : :
181 : : } // namespace bv
182 : : } // namespace theory
183 : : } // namespace cvc5::internal
|
