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 : : * Definition of ProofRule::ACI_NORM and ProofRule::ABSORB.
11 : : */
12 : :
13 : : #include "expr/aci_norm.h"
14 : :
15 : : #include "expr/attribute.h"
16 : : #include "expr/skolem_manager.h"
17 : : #include "theory/bv/theory_bv_utils.h"
18 : : #include "theory/strings/word.h"
19 : : #include "util/bitvector.h"
20 : : #include "util/finite_field_value.h"
21 : : #include "util/rational.h"
22 : : #include "util/regexp.h"
23 : : #include "util/string.h"
24 : :
25 : : using namespace cvc5::internal::kind;
26 : :
27 : : namespace cvc5::internal {
28 : : namespace expr {
29 : :
30 : 1089629 : Node getNullTerminator(NodeManager* nm, Kind k, TypeNode tn)
31 : : {
32 : 1089629 : Node nullTerm;
33 [ + + ][ + + ]: 1089629 : switch (k)
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + ]
34 : : {
35 : 480695 : case Kind::OR: nullTerm = nm->mkConst(false); break;
36 : 365762 : case Kind::AND:
37 : 365762 : case Kind::SEP_STAR: nullTerm = nm->mkConst(true); break;
38 : 10 : case Kind::ADD:
39 [ + - ][ - - ]: 30 : nullTerm = tn.isInteger() ? nm->mkConstInt(Rational(0))
40 [ - + ][ + - ]: 20 : : nm->mkConstReal(Rational(0));
[ - - ]
41 : 10 : break;
42 : 2 : case Kind::MULT:
43 : : case Kind::NONLINEAR_MULT:
44 [ + - ][ - - ]: 6 : nullTerm = tn.isInteger() ? nm->mkConstInt(Rational(1))
45 [ - + ][ + - ]: 4 : : nm->mkConstReal(Rational(1));
[ - - ]
46 : 2 : break;
47 : 34169 : case Kind::STRING_CONCAT:
48 : : // handles strings and sequences
49 [ + - ]: 34169 : if (tn.isStringLike())
50 : : {
51 : 34169 : nullTerm = theory::strings::Word::mkEmptyWord(tn);
52 : : }
53 : 34169 : break;
54 : 386 : case Kind::REGEXP_CONCAT:
55 : : // the language containing only the empty string
56 : 386 : nullTerm = nm->mkNode(Kind::STRING_TO_REGEXP, nm->mkConst(String("")));
57 : 386 : break;
58 : 243 : case Kind::REGEXP_UNION:
59 : : // empty language
60 : 243 : nullTerm = nm->mkNode(Kind::REGEXP_NONE);
61 : 243 : break;
62 : 290 : case Kind::REGEXP_INTER:
63 : : // universal language
64 : 290 : nullTerm = nm->mkNode(Kind::REGEXP_ALL);
65 : 290 : break;
66 : 4621 : case Kind::BITVECTOR_AND:
67 : : // it may be the case that we are an abstract type, which we guard here
68 : : // and return the null node.
69 [ + - ]: 4621 : if (tn.isBitVector())
70 : : {
71 : 4621 : nullTerm = theory::bv::utils::mkOnes(nm, tn.getBitVectorSize());
72 : : }
73 : 4621 : break;
74 : 8132 : case Kind::BITVECTOR_OR:
75 : : case Kind::BITVECTOR_ADD:
76 : : case Kind::BITVECTOR_XOR:
77 [ + + ]: 8132 : if (tn.isBitVector())
78 : : {
79 : 7866 : nullTerm = theory::bv::utils::mkZero(nm, tn.getBitVectorSize());
80 : : }
81 : 8132 : break;
82 : 596 : case Kind::BITVECTOR_MULT:
83 [ + - ]: 596 : if (tn.isBitVector())
84 : : {
85 : 596 : nullTerm = theory::bv::utils::mkOne(nm, tn.getBitVectorSize());
86 : : }
87 : 596 : break;
88 : 12785 : case Kind::BITVECTOR_CONCAT:
89 : : {
90 : 12785 : nullTerm = nm->getSkolemManager()->mkSkolemFunction(SkolemId::BV_EMPTY);
91 : : }
92 : 12785 : break;
93 : 689 : case Kind::FINITE_FIELD_ADD:
94 [ + - ]: 689 : if (tn.isFiniteField())
95 : : {
96 : 689 : nullTerm = nm->mkConst(FiniteFieldValue(Integer(0), tn.getFfSize()));
97 : : }
98 : 689 : break;
99 : 758 : case Kind::FINITE_FIELD_MULT:
100 [ + - ]: 758 : if (tn.isFiniteField())
101 : : {
102 : 758 : nullTerm = nm->mkConst(FiniteFieldValue(Integer(1), tn.getFfSize()));
103 : : }
104 : 758 : break;
105 : 180491 : default:
106 : : // not handled as null-terminated
107 : 180491 : break;
108 : : }
109 : 1089629 : return nullTerm;
110 : 0 : }
111 : :
112 : 4966792 : bool isAssocCommIdem(Kind k)
113 : : {
114 [ + + ]: 4966792 : switch (k)
115 : : {
116 : 262087 : case Kind::OR:
117 : : case Kind::AND:
118 : : case Kind::SEP_STAR:
119 : : case Kind::REGEXP_UNION:
120 : : case Kind::REGEXP_INTER:
121 : : case Kind::BITVECTOR_AND:
122 : : case Kind::BITVECTOR_OR:
123 : : case Kind::FINITE_FIELD_ADD:
124 : 262087 : case Kind::FINITE_FIELD_MULT: return true;
125 : 4704705 : default: break;
126 : : }
127 : 4704705 : return false;
128 : : }
129 : :
130 : 1302582 : bool isAssocComm(Kind k) { return (k == Kind::BITVECTOR_XOR); }
131 : :
132 : 2387232 : bool isAssoc(Kind k)
133 : : {
134 [ + + ]: 2387232 : switch (k)
135 : : {
136 : 72441 : case Kind::BITVECTOR_CONCAT:
137 : : case Kind::STRING_CONCAT:
138 : 72441 : case Kind::REGEXP_CONCAT: return true;
139 : 2314791 : default: break;
140 : : }
141 : : // also return true for the operators listed above
142 : 2314791 : return isAssocCommIdem(k);
143 : : }
144 : :
145 : : struct NormalFormTag
146 : : {
147 : : };
148 : : using NormalFormAttr = expr::Attribute<NormalFormTag, Node>;
149 : :
150 : 3401779 : Node getACINormalForm(Node a)
151 : : {
152 : : NormalFormAttr nfa;
153 : 3401779 : Node an = a.getAttribute(nfa);
154 [ + + ]: 3401779 : if (!an.isNull())
155 : : {
156 : : // already computed
157 : 2099197 : return an;
158 : : }
159 : 1302582 : Kind k = a.getKind();
160 : 1302582 : bool aci = isAssocCommIdem(k);
161 [ + + ][ + + ]: 1302582 : bool ac = isAssocComm(k) || aci;
162 [ + + ][ + + ]: 1302582 : if (!ac && !isAssoc(k))
[ + + ]
163 : : {
164 : : // not associative, return self
165 : 1088671 : a.setAttribute(nfa, a);
166 : 1088671 : return a;
167 : : }
168 : 213911 : TypeNode atn = a.getType();
169 : 213911 : Node nt = getNullTerminator(a.getNodeManager(), k, atn);
170 [ - + ]: 213911 : if (nt.isNull())
171 : : {
172 : : // no null terminator, likely abstract type, return self
173 : 0 : a.setAttribute(nfa, a);
174 : 0 : return a;
175 : : }
176 : 213911 : std::vector<Node> toProcess;
177 : 213911 : toProcess.insert(toProcess.end(), a.rbegin(), a.rend());
178 : 213911 : std::vector<Node> children;
179 : 213911 : Node cur;
180 : : do
181 : : {
182 : 1138848 : cur = toProcess.back();
183 : 1138848 : toProcess.pop_back();
184 [ + + ]: 1138848 : if (cur == nt)
185 : : {
186 : : // ignore null terminator (which is the neutral element)
187 : 37638 : continue;
188 : : }
189 [ + + ]: 1101210 : else if (cur.getKind() == k)
190 : : {
191 : : // flatten
192 : 126278 : toProcess.insert(toProcess.end(), cur.rbegin(), cur.rend());
193 : : }
194 : 1949864 : else if (!aci
195 [ + + ][ + + ]: 2717644 : || std::find(children.begin(), children.end(), cur)
196 [ + + ]: 2717644 : == children.end())
197 : : {
198 : : // add to final children if not idempotent or if not a duplicate
199 : 967670 : children.push_back(cur);
200 : : }
201 [ + + ]: 1138848 : } while (!toProcess.empty());
202 [ + + ]: 213911 : if (ac)
203 : : {
204 : : // sort if commutative
205 : 183789 : std::sort(children.begin(), children.end());
206 : : }
207 : 213911 : an = children.empty()
208 [ + + ][ + + ]: 662256 : ? nt
209 : 234434 : : (children.size() == 1 ? children[0]
210 : 213911 : : a.getNodeManager()->mkNode(k, children));
211 : 213911 : a.setAttribute(nfa, an);
212 : 213911 : return an;
213 : 3401779 : }
214 : :
215 : 1609067 : bool isACINorm(Node a, Node b)
216 : : {
217 : 1609067 : Node an = getACINormalForm(a);
218 : 1609067 : Node bn = getACINormalForm(b);
219 [ + + ]: 1609067 : if (a.getKind() == b.getKind())
220 : : {
221 : : // if the kinds are equal, we compare their normal forms only, as the checks
222 : : // below are spurious.
223 : 404442 : return (an == bn);
224 : : }
225 : : // note we compare three possibilities, to handle cases like
226 : : // (or (and A B) false) == (and A B).
227 : : //
228 : : // Note that we do *not* succeed if an==bn here, since this depends on the
229 : : // chosen ordering. For example, if (or (and A B) false) == (and B A),
230 : : // we get a normal form of (and A B) for the LHS. The normal form of the
231 : : // RHS is either (and A B) or (and B A). If we succeeded when an==bn,
232 : : // then this would only be the case if the former was chosen as a normal
233 : : // form. Instead, both fail.
234 [ + + ][ + + ]: 1204625 : return (a == bn) || (an == b);
235 : 1609067 : }
236 : :
237 : 1600199 : Node getZeroElement(NodeManager* nm, Kind k, TypeNode tn)
238 : : {
239 : 1600199 : Node zeroTerm;
240 [ + + ][ + + ]: 1600199 : switch (k)
[ + + ][ + + ]
241 : : {
242 : 38889 : case Kind::OR: zeroTerm = nm->mkConst(true); break;
243 : 128458 : case Kind::AND:
244 : 128458 : case Kind::SEP_STAR: zeroTerm = nm->mkConst(false); break;
245 : 20185 : case Kind::MULT:
246 : : case Kind::NONLINEAR_MULT:
247 : : // Note that we ignore the type. This is safe since multiplication is
248 : : // permissive for subtypes.
249 : 20185 : zeroTerm = nm->mkConstInt(Rational(0));
250 : 20185 : break;
251 : 63 : case Kind::REGEXP_UNION:
252 : : // universal language
253 : 63 : zeroTerm = nm->mkNode(Kind::REGEXP_ALL);
254 : 63 : break;
255 : 339 : case Kind::REGEXP_INTER:
256 : : case Kind::REGEXP_CONCAT:
257 : : // empty language
258 : 339 : zeroTerm = nm->mkNode(Kind::REGEXP_NONE);
259 : 339 : break;
260 : 3285 : case Kind::BITVECTOR_OR:
261 [ + - ]: 3285 : if (tn.isBitVector())
262 : : {
263 : 3285 : zeroTerm = theory::bv::utils::mkOnes(nm, tn.getBitVectorSize());
264 : : }
265 : 3285 : break;
266 : 5780 : case Kind::BITVECTOR_AND:
267 : : case Kind::BITVECTOR_MULT:
268 : : // it may be the case that we are an abstract type, which we guard here
269 : : // and return the null node.
270 [ + - ]: 5780 : if (tn.isBitVector())
271 : : {
272 : 5780 : zeroTerm = theory::bv::utils::mkZero(nm, tn.getBitVectorSize());
273 : : }
274 : 5780 : break;
275 : 1403200 : default:
276 : : // no zero
277 : 1403200 : break;
278 : : }
279 : 1600199 : return zeroTerm;
280 : 0 : }
281 : :
282 : : struct AbsorbTag
283 : : {
284 : : };
285 : : struct AbsorbComputedTag
286 : : {
287 : : };
288 : : /**
289 : : * Attribute true for terms that can be absorbd. Note the same attribute
290 : : * is stored for all kinds.
291 : : */
292 : : typedef expr::Attribute<AbsorbTag, bool> AbsorbAttr;
293 : : typedef expr::Attribute<AbsorbComputedTag, bool> AbsorbComputedAttr;
294 : :
295 : 48739 : bool isAbsorb(Kind k)
296 : : {
297 [ + + ]: 48739 : switch (k)
298 : : {
299 : 43776 : case Kind::OR:
300 : : case Kind::AND:
301 : : case Kind::REGEXP_UNION:
302 : : case Kind::REGEXP_INTER:
303 : : case Kind::REGEXP_CONCAT:
304 : : case Kind::BITVECTOR_AND:
305 : 43776 : case Kind::BITVECTOR_OR: return true;
306 : 4963 : default: break;
307 : : }
308 : 4963 : return false;
309 : : }
310 : :
311 : 48739 : bool isAbsorb(Node a, const Node& zero)
312 : : {
313 : 48739 : Kind k = a.getKind();
314 [ + + ]: 48739 : if (!isAbsorb(k))
315 : : {
316 : 4963 : return false;
317 : : }
318 : : AbsorbAttr aa;
319 : : AbsorbComputedAttr aca;
320 : 43776 : std::unordered_set<TNode> visited;
321 : 43776 : std::unordered_set<TNode>::iterator it;
322 : 43776 : std::vector<TNode> visit;
323 : 43776 : TNode cur;
324 : 43776 : visit.push_back(a);
325 : : do
326 : : {
327 : 93783 : cur = visit.back();
328 [ - + ][ - + ]: 93783 : Assert(cur.getKind() == k);
[ - - ]
329 [ + + ]: 93783 : if (cur.getAttribute(aca))
330 : : {
331 : 21489 : visit.pop_back();
332 : 57636 : continue;
333 : : }
334 : 72294 : it = visited.find(cur);
335 [ + + ]: 72294 : if (it == visited.end())
336 : : {
337 : 36147 : visited.insert(cur);
338 [ + + ]: 145589 : for (const Node& cc : cur)
339 : : {
340 [ + + ]: 109442 : if (cc.getKind() == k)
341 : : {
342 : 13860 : visit.push_back(cc);
343 : : }
344 : 109442 : }
345 : 36147 : continue;
346 : 36147 : }
347 : 36147 : visit.pop_back();
348 : 36147 : bool isAnnil = false;
349 [ + + ]: 121658 : for (const Node& cc : cur)
350 : : {
351 : : // only absorbs if the child is zero or has the same kind and
352 : : // absorbs
353 [ + + ][ + + ]: 101394 : if (cc == zero || (cc.getKind() == k && cc.getAttribute(aa)))
[ + + ][ + + ]
354 : : {
355 : 15883 : isAnnil = true;
356 : 15883 : break;
357 : : }
358 [ + + ]: 101394 : }
359 : 36147 : cur.setAttribute(aa, isAnnil);
360 : 36147 : cur.setAttribute(aca, true);
361 [ + + ]: 93783 : } while (!visit.empty());
362 : 43776 : return a.getAttribute(aa);
363 : 43776 : }
364 : :
365 : : } // namespace expr
366 : : } // namespace cvc5::internal
|
