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