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 : : * Utilities for resolution proofs.
11 : : */
12 : :
13 : : #include "proof/resolution_proofs_util.h"
14 : :
15 : : #include "proof/proof.h"
16 : : #include "proof/proof_checker.h"
17 : : #include "proof/proof_node_manager.h"
18 : :
19 : : namespace cvc5::internal {
20 : : namespace proof {
21 : :
22 : : /** The information relevant for converting CHAIN_M_RESOLUTION steps into
23 : : * CHAIN_RESOLUTION+FACTORING steps when "crowding literals" are present. See
24 : : * `ProofPostprocessCallback::eliminateCrowdingLits` for more information. */
25 : : struct CrowdingLitInfo
26 : : {
27 : 417160 : CrowdingLitInfo(size_t lastInclusion = static_cast<size_t>(-1),
28 : : size_t eliminator = static_cast<size_t>(-1),
29 : : bool onlyCrowdAndConcLitsInElim = false,
30 : : size_t maxSafeMovePosition = static_cast<size_t>(-1))
31 : 417160 : : d_lastInclusion(lastInclusion),
32 : 417160 : d_eliminator(eliminator),
33 : 417160 : d_onlyCrowdAndConcLitsInElim(onlyCrowdAndConcLitsInElim),
34 : 417160 : d_maxSafeMovePosition(maxSafeMovePosition)
35 : : {
36 : 417160 : }
37 : : /* Index of last (left-to-right) premise to introduce this crowding literal */
38 : : size_t d_lastInclusion;
39 : : /* Index of last premise to eliminate this crowding literal */
40 : : size_t d_eliminator;
41 : : /* Whether there are only crowding/conclusion literals in the eliminator. */
42 : : bool d_onlyCrowdAndConcLitsInElim;
43 : : /* Maximum position to which the eliminator premise can be moved without
44 : : * changing the behavior of the resolution chain. Note this only applies when
45 : : * d_onlyCrowdAndConcLitsInElim is true. */
46 : : size_t d_maxSafeMovePosition;
47 : : };
48 : :
49 : 0 : std::ostream& operator<<(std::ostream& out, CrowdingLitInfo info)
50 : : {
51 : 0 : out << "{" << info.d_lastInclusion << ", " << info.d_eliminator << ", ";
52 [ - - ]: 0 : if (info.d_onlyCrowdAndConcLitsInElim)
53 : : {
54 : 0 : out << "true, " << info.d_maxSafeMovePosition;
55 : : }
56 : : else
57 : : {
58 : 0 : out << "false";
59 : : }
60 : 0 : out << "}";
61 : 0 : return out;
62 : : }
63 : :
64 : 20549 : Node eliminateCrowdingLits(NodeManager* nm,
65 : : bool reorderPremises,
66 : : const std::vector<Node>& clauseLits,
67 : : const std::vector<Node>& targetClauseLits,
68 : : const std::vector<Node>& children,
69 : : const std::vector<Node>& args,
70 : : CDProof* cdp,
71 : : ProofNodeManager* pnm)
72 : : {
73 [ + - ]: 20549 : Trace("crowding-lits") << push;
74 [ + - ]: 20549 : Trace("crowding-lits") << "Clause lits: " << clauseLits << "\n";
75 [ + - ]: 20549 : Trace("crowding-lits") << "Target lits: " << targetClauseLits << "\n\n";
76 : 20549 : std::vector<Node> newChildren{children}, newArgs{args};
77 : 20549 : Node trueNode = nm->mkConst(true);
78 : : // get crowding lits and the position of the last clause that includes
79 : : // them. The factoring step must be added after the last inclusion and before
80 : : // its elimination.
81 : 20549 : std::unordered_set<TNode> crowding;
82 : 20549 : size_t childrenSize = children.size(), numCrowding = 0;
83 : 20549 : std::vector<std::pair<Node, size_t>> lastInclusion;
84 : : // for each crowding lit, the information that is used to eliminate it
85 : 20549 : std::map<Node, CrowdingLitInfo> crowdLitsInfo;
86 : : // positions of eliminators of crowding literals, which are the positions of
87 : : // the clauses that eliminate crowding literals *after* their last inclusion
88 : 20549 : std::vector<size_t> eliminators;
89 [ + + ]: 1754691 : for (size_t i = 0, size = clauseLits.size(); i < size; ++i)
90 : : {
91 : : // repeated crowding literal or conclusion literal
92 [ + + ][ - - ]: 3468284 : if (crowding.count(clauseLits[i])
93 [ + + ][ + + ]: 6472534 : || std::find(
94 : 1502125 : targetClauseLits.begin(), targetClauseLits.end(), clauseLits[i])
95 [ + - ]: 4738392 : != targetClauseLits.end())
96 : : {
97 : 1525562 : continue;
98 : : }
99 : 208580 : Node crowdLit = clauseLits[i];
100 : 208580 : crowding.insert(crowdLit);
101 [ + - ]: 208580 : Trace("crowding-lits3") << "crowding lit " << crowdLit << "\n";
102 : : // found crowding lit, now get its last inclusion position, which is the
103 : : // position of the last resolution link that introduces the crowding
104 : : // literal. Note that this position has to be *before* the last link, as a
105 : : // link *after* the last inclusion must eliminate the crowding literal.
106 : : size_t j;
107 [ + - ]: 3452649 : for (j = childrenSize - 1; j > 0; --j)
108 : : {
109 : : // notice that only non-singleton clauses may be introducing the
110 : : // crowding literal, so we only care about non-singleton OR nodes. We
111 : : // check then against the kind and whether the whole OR node occurs as a
112 : : // pivot of the respective resolution
113 [ + + ]: 3452649 : if (newChildren[j - 1].getKind() != Kind::OR)
114 : : {
115 : 303570 : continue;
116 : : }
117 : 3149079 : uint64_t pivotIndex = 2 * (j - 1);
118 : 3149079 : if (newArgs[pivotIndex] == newChildren[j - 1]
119 [ + + ][ - + ]: 6298158 : || newArgs[pivotIndex].notNode() == newChildren[j - 1])
[ + + ][ + + ]
[ - - ]
120 : : {
121 : 2374 : continue;
122 : : }
123 : 6293410 : if (std::find(
124 : 6293410 : newChildren[j - 1].begin(), newChildren[j - 1].end(), crowdLit)
125 [ + + ]: 6293410 : != newChildren[j - 1].end())
126 : : {
127 : 208580 : break;
128 : : }
129 : : }
130 [ - + ][ - + ]: 208580 : Assert(j > 0);
[ - - ]
131 : 208580 : lastInclusion.emplace_back(crowdLit, j - 1);
132 : 208580 : CrowdingLitInfo info;
133 : 208580 : info.d_lastInclusion = j - 1;
134 : :
135 [ + - ]: 208580 : Trace("crowding-lits3") << "last inc " << j - 1 << "\n";
136 : : // get elimination position, starting from the following link as the last
137 : : // inclusion one. The result is the last (in the chain, but first from
138 : : // this point on) resolution link that eliminates the crowding literal. A
139 : : // literal l is eliminated by a link if it contains a literal l' with
140 : : // opposite polarity to l.
141 [ + - ]: 601739 : for (; j < childrenSize; ++j)
142 : : {
143 : 601739 : bool posFirst = newArgs[(2 * j) - 1] == trueNode;
144 : 601739 : Node pivot = newArgs[(2 * j)];
145 [ + - ]: 1203478 : Trace("crowding-lits3")
146 : 601739 : << "\tcheck w/ args " << posFirst << " / " << pivot << "\n";
147 : : // To eliminate the crowding literal (crowdLit), the clause must contain
148 : : // it with opposite polarity. There are three successful cases,
149 : : // according to the pivot and its sign
150 : : //
151 : : // - crowdLit is the same as the pivot and posFirst is true, which means
152 : : // that the clause contains its negation and eliminates it
153 : : //
154 : : // - crowdLit is the negation of the pivot and posFirst is false, so the
155 : : // clause contains the node whose negation is crowdLit. Note that this
156 : : // case may either be crowdLit.notNode() == pivot or crowdLit ==
157 : : // pivot.notNode().
158 [ - + ]: 126610 : if ((crowdLit == pivot && posFirst)
159 [ - + ][ - - ]: 1076868 : || (crowdLit.notNode() == pivot && !posFirst)
[ + + ][ - - ]
160 [ + + ][ + + ]: 1203478 : || (pivot.notNode() == crowdLit && !posFirst))
[ + - ][ + + ]
[ + + ][ - - ]
161 : : {
162 [ + - ]: 208580 : Trace("crowding-lits3") << "\t\tfound it!\n";
163 : 208580 : eliminators.push_back(j);
164 : 208580 : break;
165 : : }
166 [ + + ]: 601739 : }
167 : 208580 : info.d_eliminator = eliminators.back();
168 : 208580 : crowdLitsInfo[crowdLit] = info;
169 [ + - ]: 417160 : Trace("crowding-lits3") << "last inc " << info.d_lastInclusion << ", elim "
170 : 208580 : << info.d_eliminator << "\n";
171 [ - + ][ - + ]: 208580 : AlwaysAssert(j < childrenSize);
[ - - ]
172 : 208580 : }
173 [ - + ][ - + ]: 20549 : Assert(!lastInclusion.empty());
[ - - ]
174 [ + - ]: 41098 : Trace("crowding-lits") << "..total of " << lastInclusion.size()
175 : 20549 : << " crowding literals\n";
176 : 20549 : numCrowding = lastInclusion.size();
177 : : // order map so that we process crowding literals in the order of the clauses
178 : : // that last introduce them
179 : 832700 : auto cmp = [](std::pair<Node, size_t>& a, std::pair<Node, size_t>& b) {
180 : 832700 : return a.second < b.second;
181 : : };
182 : 20549 : std::sort(lastInclusion.begin(), lastInclusion.end(), cmp);
183 : : // order eliminators
184 : 20549 : std::sort(eliminators.begin(), eliminators.end());
185 [ + - ]: 20549 : if (reorderPremises)
186 : : {
187 : : // compute extra information. We are trying to determine if we can move
188 : : // crowding literal eliminators further to the right in the resolution
189 : : // chain. This will reduce the number of divisions to the chain to be made
190 : : // in the expansion below. Currently we determine this moving worthwhile
191 : : // when the eliminator has no non-crowding, non-conclusion, non-pivot
192 : : // literals, since they would necessarily be eliminated somewhere down the
193 : : // road, and moving the premise beyond that point would break the resolution
194 : : // chain. While this may also happen for conclusion and other crowding
195 : : // literals, we can compute the safe point to move relatively cheaply.
196 [ + + ]: 229129 : for (size_t i = 0; i < numCrowding; ++i)
197 : : {
198 : 208580 : Node crowdingLit = lastInclusion[i].first;
199 : 208580 : size_t elim = crowdLitsInfo[crowdingLit].d_eliminator;
200 : : // Since this primise is an eliminator, if it's an OR it can only be a
201 : : // singleton if the crowding literal is its negation.
202 : 208580 : size_t maxSafeMove = childrenSize,
203 : 208580 : numLits = (newChildren[elim].getKind() != Kind::OR
204 [ + + ]: 202230 : || (crowdingLit.getKind() == Kind::NOT
205 [ + + ][ - - ]: 153630 : && crowdingLit[0] == newChildren[elim]))
206 [ + + ]: 417162 : ? 1
207 [ + + ]: 208580 : : newChildren[elim].getNumChildren();
208 : : // unit eliminators can be moved to the end
209 [ + + ]: 208580 : if (numLits == 1)
210 : : {
211 [ + - ]: 12704 : Trace("crowding-lits2") << "....elim " << elim << " is unit (of " << i
212 : 6352 : << "-th crowding lit)\n";
213 : 6352 : crowdLitsInfo[lastInclusion[i].first].d_onlyCrowdAndConcLitsInElim =
214 : : true;
215 : 6352 : crowdLitsInfo[lastInclusion[i].first].d_maxSafeMovePosition =
216 : : maxSafeMove;
217 : 6352 : continue;
218 : : }
219 : : // how many non-crowding non-conclusion lits
220 : 202228 : uint32_t regularLits = 0;
221 : : // only search while it's possible (no non-crowding, non-conclusion,
222 : : // non-pivot literals) or worthwhile (would move at least one
223 : : // position). Note that there will always be at least one "regular"
224 : : // literal, i.e., the pivot that eliminates the crowding literal.
225 : 888309 : for (size_t j = 0;
226 [ + + ][ + + ]: 888309 : j < numLits && regularLits <= 1 && (maxSafeMove - elim) > 1;
[ + + ]
227 : : ++j)
228 : : {
229 : 686081 : bool isCrowdingLit = crowding.count(newChildren[elim][j]);
230 : : // if not crowding and not in conclusion it's a regular literal
231 : 1571338 : if (!isCrowdingLit
232 [ + + ][ + + ]: 1716279 : && std::find(targetClauseLits.begin(),
[ + + ][ - - ]
233 : : targetClauseLits.end(),
234 : 515099 : newChildren[elim][j])
235 [ + + ]: 1716279 : == targetClauseLits.end())
236 : : {
237 : 199176 : regularLits++;
238 : 199176 : continue;
239 : : }
240 : : // If it's a crowding literal we know it's unsafe to move this premise
241 : : // beyond its last inclusion
242 [ + + ]: 486905 : if (isCrowdingLit)
243 : : {
244 [ - + ][ - + ]: 170982 : Assert(crowdLitsInfo.find(newChildren[elim][j])
[ - - ]
245 : : != crowdLitsInfo.end());
246 : 170982 : size_t lastInc = crowdLitsInfo[newChildren[elim][j]].d_lastInclusion;
247 [ + + ]: 170982 : maxSafeMove = lastInc < maxSafeMove ? lastInc : maxSafeMove;
248 : : }
249 : : // We check the pivots of the steps until the current limit
250 : : // (maxSafeMove). If this literal is a pivot in any such step then it is
251 : : // unsafe to move the eliminator beyond it. That then becomes the new
252 : : // limit. The literal is such a pivot if it matches a lhs pivot, i.e.,
253 : : // the same as a (pivot, +pol) or the negation of a (pivot, -pol).
254 : 486905 : for (size_t k = 2 * (elim + 1) - 1, checkLim = (2 * maxSafeMove) - 1;
255 [ + + ]: 3516853 : k < checkLim;
256 : 3029948 : k = k + 2)
257 : : {
258 : 3030153 : bool posPivot = newArgs[k] == trueNode;
259 [ - + ][ + + ]: 6060458 : if ((newChildren[elim][j] == newArgs[k + 1] && posPivot)
[ - - ]
260 : 6060511 : || (newChildren[elim][j] == newArgs[k + 1].notNode()
261 [ + - ]: 53 : && !posPivot))
262 : : {
263 : 205 : maxSafeMove = (k + 1) / 2;
264 : 205 : break;
265 : : }
266 : : }
267 : : }
268 : : // If there is a single regular literal, all other are either crowiding or
269 : : // conclusion literals.
270 [ + + ][ + + ]: 202228 : if (regularLits == 1 && maxSafeMove > elim && maxSafeMove - elim > 1)
[ + + ]
271 : : {
272 [ + - ]: 139948 : Trace("crowding-lits2")
273 : 0 : << "....elim " << elim << " has only crowd/conc lits (of " << i
274 : 69974 : << "-th crowding lit). MaxSafeMove: " << maxSafeMove << "\n";
275 : 69974 : crowdLitsInfo[lastInclusion[i].first].d_onlyCrowdAndConcLitsInElim =
276 : : true;
277 : 69974 : crowdLitsInfo[lastInclusion[i].first].d_maxSafeMovePosition =
278 : : maxSafeMove;
279 : : }
280 [ + + ]: 208580 : }
281 [ - + ]: 20549 : if (TraceIsOn("crowding-lits"))
282 : : {
283 [ - - ]: 0 : Trace("crowding-lits") << "crowding lits last inclusion:\n";
284 [ - - ]: 0 : for (size_t i = 0, size = lastInclusion.size(); i < size; ++i)
285 : : {
286 : 0 : Node crowdingLit = lastInclusion[i].first;
287 [ - - ]: 0 : Trace("crowding-lits")
288 : 0 : << "\t- [" << crowdLitsInfo[crowdingLit].d_lastInclusion << "] : {"
289 : 0 : << crowdLitsInfo[crowdingLit].d_eliminator << "} " << crowdingLit
290 : 0 : << "\n";
291 [ - - ]: 0 : if (crowdLitsInfo[crowdingLit].d_onlyCrowdAndConcLitsInElim)
292 : : {
293 [ - - ]: 0 : Trace("crowding-lits")
294 : 0 : << "\t\t- onlyCrowdAndConcLitsInElim; maxSafeMove: "
295 : 0 : << crowdLitsInfo[crowdingLit].d_maxSafeMovePosition << "\n";
296 : : }
297 : 0 : }
298 : : }
299 : : // Every eliminator can be moved, without loss of generality, up to the
300 : : // immediate position before a clause that eliminates one its non-pivot
301 : : // literals. We also add restrict the move to be up to the minimal last
302 : : // inclusion of a crowding literal, as moving beyond that would require
303 : : // recomputing the information of that crowding literal. So for example, an
304 : : // eliminator in position i, which has only crowding/conclusion literals
305 : : // that are not eliminated before a minimun last inclusion position i+1000,
306 : : // can be moved anywhere in the premises between i and i+999. This is the
307 : : // case since all the literals that are introduced by the eliminator are
308 : : // going to be killed (or preserved for conclusion) only starting at i+1000.
309 : : //
310 : : // Given the above we proceed, based on the crowding lits information, to
311 : : // move up to maximum all eliminators.
312 : : //
313 : : // We will use std::rotate to do the moving of the premises, which moves to
314 : : // target position (first argument) an interval [l, u), where l and u are
315 : : // the second and third arguments. For each eliminator in position i that
316 : : // has a minimum crowding last inclusion k bigger than i + 1, we do the
317 : : // moving with arguments (i, i+1, k). As a consequence newChildren[i] will
318 : : // move to position k-1. Since we are moving premises we also need to move
319 : : // arguments. The polarity/pivot of the eliminator in position i are (2*i)
320 : : // -1 and 2*i. So the rotation in the arguments is with (2*i-1, 2*i+1,
321 : : // 2*k-1).
322 [ + - ]: 20549 : Trace("smt-proof-pp-debug") << "Moving eliminators\n" << push;
323 : : // This guys will be used to search for the position of the eliminator
324 : : // within newChildren after the moves below. This is necessary because an
325 : : // eliminator originally moved to position k can end up in some position
326 : : // before k if any other eliminator is moved ahead of k
327 : 20549 : uint32_t counterMoved = 0;
328 [ + + ]: 229129 : for (size_t i = 0; i < numCrowding; ++i)
329 : : {
330 : 208580 : Node crowdingLit = lastInclusion[i].first;
331 : 208580 : size_t elim = crowdLitsInfo[crowdingLit].d_eliminator;
332 : 208580 : size_t maxSafeMove = crowdLitsInfo[crowdingLit].d_maxSafeMovePosition;
333 : 208580 : Assert(maxSafeMove >= elim) << i << "-th crowding lit " << crowdingLit
334 : 0 : << " has info " << crowdLitsInfo[crowdingLit];
335 : 208580 : if (!crowdLitsInfo[crowdingLit].d_onlyCrowdAndConcLitsInElim
336 [ + + ][ + + ]: 208580 : || maxSafeMove - elim <= 1)
[ + + ]
337 : : {
338 : 132470 : continue;
339 : : }
340 : 76110 : ++counterMoved;
341 [ + - ]: 152220 : Trace("crowding-lits")
342 : 76110 : << "..move elim " << elim << " to " << maxSafeMove - 1 << "\n";
343 : 152220 : std::rotate(newChildren.begin() + elim,
344 : 76110 : newChildren.begin() + elim + 1,
345 : 76110 : newChildren.begin() + maxSafeMove);
346 : 152220 : std::rotate(newArgs.begin() + (2 * elim) - 1,
347 : 76110 : newArgs.begin() + (2 * elim) + 1,
348 : 76110 : newArgs.begin() + (2 * maxSafeMove) - 1);
349 : : // Being pedantic here we should assert that the rotated
350 : : // newChildren/newArgs still yield the same conclusion with a
351 : : // CHAIN_M_RESOLUTION step. However this can be very expensive to check,
352 : : // so we don't do this. Only if one is debugging this code this test
353 : : // should be added.
354 : :
355 : : // Now we need to update the indices, since we have changed newChildren.
356 : : // For every crowding literal whose information indices are in the
357 : : // interval [elim+1, maxSafeMove), these indices should be decremented
358 : : // by 1.
359 [ + + ]: 1522704 : for (std::pair<const Node, CrowdingLitInfo>& p : crowdLitsInfo)
360 : : {
361 : 1446594 : bool updated = false;
362 : : // guarantee we update who we just moved...
363 [ + + ]: 1446594 : if (p.first == crowdingLit)
364 : : {
365 : 76110 : p.second.d_eliminator = maxSafeMove - 1;
366 : 76110 : continue;
367 : : }
368 : : // can update lastInclusion, eliminator and maxSafeMovePosition
369 [ + + ]: 1370484 : if (p.second.d_lastInclusion >= elim + 1
370 [ + + ]: 549424 : && p.second.d_lastInclusion < maxSafeMove)
371 : : {
372 : 28544 : --p.second.d_lastInclusion;
373 : 28544 : updated = true;
374 : : }
375 [ + + ]: 1370484 : if (p.second.d_eliminator >= elim + 1
376 [ + + ]: 738434 : && p.second.d_eliminator < maxSafeMove)
377 : : {
378 : 198361 : --p.second.d_eliminator;
379 : 198361 : updated = true;
380 : : }
381 [ + + ]: 1370484 : if (p.second.d_onlyCrowdAndConcLitsInElim
382 [ + + ]: 607926 : && p.second.d_maxSafeMovePosition >= elim + 1
383 [ + + ]: 375846 : && p.second.d_maxSafeMovePosition < maxSafeMove)
384 : : {
385 : 2314 : --p.second.d_maxSafeMovePosition;
386 : 2314 : updated = true;
387 : : }
388 [ + + ]: 1370484 : if (updated)
389 : : {
390 [ + - ]: 398414 : Trace("crowding-lits")
391 : 0 : << "\tUpdated other crowding lit " << p.first << " info to "
392 : 199207 : << crowdLitsInfo[p.first] << "\n";
393 : : }
394 : : }
395 [ + + ]: 208580 : }
396 [ + - ]: 20549 : Trace("smt-proof-pp-debug") << pop;
397 [ + + ]: 20549 : if (counterMoved)
398 : : {
399 [ + - ]: 30888 : Trace("crowding-lits")
400 : 15444 : << "..moved up " << counterMoved << " eliminators\n";
401 [ + - ]: 30888 : Trace("smt-proof-pp-debug")
402 : 15444 : << "Updating bookkeeping of lastInclusion/eliminators vectors\n";
403 [ + - ]: 15444 : Trace("crowding-lits") << "New premises " << newChildren << "\n";
404 [ + - ]: 15444 : Trace("crowding-lits") << "New args " << newArgs << "\n";
405 : : // lastInclusion order will not have changed, so we just traverse in the
406 : : // same way and update
407 [ + + ]: 210109 : for (auto& p : lastInclusion)
408 : : {
409 : 194665 : p.second = crowdLitsInfo[p.first].d_lastInclusion;
410 : : }
411 : : // since eliminators may have changed drastically, we fully recompute
412 : 15444 : eliminators.clear();
413 [ + + ]: 210109 : for (const std::pair<const Node, CrowdingLitInfo>& p : crowdLitsInfo)
414 : : {
415 : 194665 : eliminators.push_back(p.second.d_eliminator);
416 : : }
417 : 15444 : std::sort(eliminators.begin(), eliminators.end());
418 : : }
419 : : }
420 [ - + ]: 20549 : if (TraceIsOn("crowding-lits"))
421 : : {
422 [ - - ]: 0 : Trace("crowding-lits") << "crowding lits last inclusion:\n";
423 [ - - ]: 0 : for (size_t i = 0, size = lastInclusion.size(); i < size; ++i)
424 : : {
425 : 0 : Node crowdingLit = lastInclusion[i].first;
426 [ - - ]: 0 : Trace("crowding-lits")
427 : 0 : << "\t- [" << crowdLitsInfo[crowdingLit].d_lastInclusion << "] : {"
428 : 0 : << crowdLitsInfo[crowdingLit].d_eliminator << "} " << crowdingLit
429 : 0 : << "\n";
430 [ - - ]: 0 : if (crowdLitsInfo[crowdingLit].d_onlyCrowdAndConcLitsInElim)
431 : : {
432 [ - - ]: 0 : Trace("crowding-lits")
433 : 0 : << "\t\t- onlyCrowdingInElim; maxSafeMove: "
434 : 0 : << crowdLitsInfo[lastInclusion[i].first].d_maxSafeMovePosition
435 : 0 : << "\n";
436 : : }
437 : 0 : }
438 : : }
439 : : // TODO (cvc4-wishues/issues/77): implement also simpler version and compare
440 : : //
441 : : // We now start to break the chain, one step at a time. Naively this breaking
442 : : // down would be one resolution/factoring to each crowding literal, but we can
443 : : // merge some of the cases. We do the following:
444 : : //
445 : : //
446 : : // lastClause children[start] ... children[end]
447 : : // ---------------------------------------------- CHAIN_RES
448 : : // C
449 : : // ----------- FACTORING
450 : : // lastClause' children[start'] ... children[end']
451 : : // -------------------------------------------------------------- CHAIN_RES
452 : : // ...
453 : : //
454 : : // where
455 : : // lastClause_0 = children[0]
456 : : // start_0 = 1
457 : : // end_0 = eliminators[0] - 1
458 : : // start_i+1 = nextGuardedElimPos - 1
459 : : //
460 : : // The important point is how end_i+1 is computed. It is based on what we call
461 : : // the "nextGuardedElimPos", i.e., the next elimination position that requires
462 : : // removal of duplicates. The intuition is that a factoring step may eliminate
463 : : // the duplicates of crowding literals l1 and l2. If the last inclusion of l2
464 : : // is before the elimination of l1, then we can go ahead and also perform the
465 : : // elimination of l2 without another factoring. However if another literal l3
466 : : // has its last inclusion after the elimination of l2, then the elimination of
467 : : // l3 is the next guarded elimination.
468 : : //
469 : : // To do the above computation then we determine, after a resolution/factoring
470 : : // step, the first crowded literal to have its last inclusion after "end". The
471 : : // first elimination position to be bigger than the position of that crowded
472 : : // literal is the next guarded elimination position.
473 : 20549 : size_t lastElim = 0;
474 : 20549 : Node lastClause = newChildren[0];
475 : 20549 : std::vector<Node> childrenRes;
476 : 20549 : std::vector<Node> childrenResArgs;
477 : 20549 : Node resPlaceHolder;
478 : 20549 : size_t nextGuardedElimPos = eliminators[0];
479 : : do
480 : : {
481 : 138585 : size_t start = lastElim + 1;
482 : 138585 : size_t end = nextGuardedElimPos - 1;
483 [ + - ]: 277170 : Trace("crowding-lits") << "res with:\n\t\tlastClause: " << lastClause
484 : 0 : << "\n\t\tstart: " << start << "\n\t\tend: " << end
485 : 138585 : << "\n";
486 : 138585 : childrenRes.push_back(lastClause);
487 : : // note that the interval of insert is exclusive in the end, so we add 1
488 : 277170 : childrenRes.insert(childrenRes.end(),
489 : 138585 : newChildren.begin() + start,
490 : 138585 : newChildren.begin() + end + 1);
491 : 277170 : childrenResArgs.insert(childrenResArgs.end(),
492 : 138585 : newArgs.begin() + (2 * start) - 1,
493 : 138585 : newArgs.begin() + (2 * end) + 1);
494 : 138585 : std::vector<Node> cpols;
495 : 138585 : std::vector<Node> clits;
496 [ + + ]: 650985 : for (size_t i = 0, ncargs = childrenResArgs.size(); i < ncargs; i = i + 2)
497 : : {
498 : 512400 : cpols.push_back(childrenResArgs[i]);
499 : 512400 : clits.push_back(childrenResArgs[i + 1]);
500 : : }
501 : 138585 : std::vector<Node> cargs;
502 : 138585 : cargs.push_back(nm->mkNode(Kind::SEXPR, cpols));
503 : 138585 : cargs.push_back(nm->mkNode(Kind::SEXPR, clits));
504 [ + - ]: 138585 : Trace("crowding-lits") << "\tres children: " << childrenRes << "\n";
505 [ + - ]: 138585 : Trace("crowding-lits") << "\tres args: " << childrenResArgs << "\n";
506 : 415755 : resPlaceHolder = pnm->getChecker()->checkDebug(
507 : 415755 : ProofRule::CHAIN_RESOLUTION, childrenRes, cargs, Node::null(), "");
508 [ + - ]: 138585 : Trace("crowding-lits") << "resPlaceHorder: " << resPlaceHolder << "\n";
509 [ + - ]: 138585 : Trace("crowding-lits") << "-------\n";
510 : 138585 : cdp->addStep(
511 : : resPlaceHolder, ProofRule::CHAIN_RESOLUTION, childrenRes, cargs);
512 : : // I need to add factoring if end < children.size(). Otherwise, this is
513 : : // to be handled by the caller
514 [ + + ]: 138585 : if (end < childrenSize - 1)
515 : : {
516 : 472144 : lastClause = pnm->getChecker()->checkDebug(
517 : 354108 : ProofRule::FACTORING, {resPlaceHolder}, {}, Node::null(), "");
518 [ + - ]: 118036 : if (!lastClause.isNull())
519 : : {
520 : 236072 : cdp->addStep(lastClause, ProofRule::FACTORING, {resPlaceHolder}, {});
521 [ + - ]: 118036 : Trace("crowding-lits") << "Apply factoring.\n";
522 : : }
523 : : else
524 : : {
525 : 0 : lastClause = resPlaceHolder;
526 : : }
527 [ + - ]: 118036 : Trace("crowding-lits") << "lastClause: " << lastClause << "\n";
528 : : }
529 : : else
530 : : {
531 : 20549 : lastClause = resPlaceHolder;
532 : 20549 : break;
533 : : }
534 : : // update for next round
535 : 118036 : childrenRes.clear();
536 : 118036 : childrenResArgs.clear();
537 : 118036 : lastElim = end;
538 : :
539 : : // find the position of the last inclusion of the next crowded literal
540 : 118036 : size_t nextCrowdedInclusionPos = numCrowding;
541 [ + + ]: 1113463 : for (size_t i = 0; i < numCrowding; ++i)
542 : : {
543 [ + + ]: 1092914 : if (lastInclusion[i].second > lastElim)
544 : : {
545 : 97487 : nextCrowdedInclusionPos = i;
546 : 97487 : break;
547 : : }
548 : : }
549 [ + - ]: 236072 : Trace("crowding-lits") << "nextCrowdedInclusion/Pos: "
550 : 0 : << lastInclusion[nextCrowdedInclusionPos].second
551 : 118036 : << "/" << nextCrowdedInclusionPos << "\n";
552 : : // if there is none, then the remaining literals will be used in the next
553 : : // round
554 : 118036 : nextGuardedElimPos = childrenSize;
555 [ + + ]: 118036 : if (nextCrowdedInclusionPos != numCrowding)
556 : : {
557 : 97487 : nextGuardedElimPos = newChildren.size();
558 [ + - ]: 844867 : for (size_t i = 0; i < numCrowding; ++i)
559 : : {
560 : : // nextGuardedElimPos is the largest element of
561 : : // eliminators bigger the next crowded literal's last inclusion
562 [ + + ]: 844867 : if (eliminators[i] > lastInclusion[nextCrowdedInclusionPos].second)
563 : : {
564 : 97487 : nextGuardedElimPos = eliminators[i];
565 : 97487 : break;
566 : : }
567 : : }
568 [ - + ][ - + ]: 97487 : Assert(nextGuardedElimPos < childrenSize);
[ - - ]
569 : : }
570 [ + - ]: 236072 : Trace("crowding-lits") << "nextGuardedElimPos: " << nextGuardedElimPos
571 : 118036 : << "\n";
572 [ + + ][ + + ]: 297719 : } while (true);
[ + + ]
573 [ + - ]: 20549 : Trace("crowding-lits") << pop;
574 : 41098 : return lastClause;
575 : 20549 : }
576 : :
577 : 83761 : bool isSingletonClause(TNode res,
578 : : const std::vector<Node>& children,
579 : : const std::vector<Node>& args)
580 : : {
581 [ + + ]: 83761 : if (res.getKind() != Kind::OR)
582 : : {
583 : 16714 : return true;
584 : : }
585 : : size_t i;
586 : 67047 : Node trueNode = res.getNodeManager()->mkConst(true);
587 : : // Find out the last child to introduced res, if any. We only need to
588 : : // look at the last one because any previous introduction would have
589 : : // been eliminated.
590 : : //
591 : : // After the loop finishes i is the index of the child C_i that
592 : : // introduced res. If i=0 none of the children introduced res as a
593 : : // subterm and therefore it cannot be a singleton clause.
594 [ + + ]: 2256738 : for (i = children.size(); i > 0; --i)
595 : : {
596 : : // only non-singleton clauses may be introducing
597 : : // res, so we only care about non-singleton or nodes. We check then
598 : : // against the kind and whether the whole or node occurs as a pivot of
599 : : // the respective resolution
600 [ + + ]: 2190371 : if (children[i - 1].getKind() != Kind::OR)
601 : : {
602 : 216319 : continue;
603 : : }
604 [ + + ]: 1974052 : size_t pivotIndex = (i != 1) ? 2 * (i - 1) - 1 : 1;
605 : 1974052 : if (args[pivotIndex] == children[i - 1]
606 [ + + ][ - + ]: 3948104 : || args[pivotIndex].notNode() == children[i - 1])
[ + + ][ + + ]
[ - - ]
607 : : {
608 : 2018 : continue;
609 : : }
610 : : // if res occurs as a subterm of a non-singleton premise
611 : 1972034 : if (std::find(children[i - 1].begin(), children[i - 1].end(), res)
612 [ + + ]: 3944068 : != children[i - 1].end())
613 : : {
614 : 680 : break;
615 : : }
616 : : }
617 : :
618 : : // If res is a subterm of one of the children we still need to check if
619 : : // that subterm is eliminated
620 [ + + ]: 67047 : if (i > 0)
621 : : {
622 [ + + ]: 680 : bool posFirst = (i == 1) ? (args[0] == trueNode)
623 : 90 : : (args[(2 * (i - 1)) - 2] == trueNode);
624 [ + + ]: 680 : Node pivot = (i == 1) ? args[1] : args[(2 * (i - 1)) - 1];
625 : :
626 : : // Check if it is eliminated by the previous resolution step
627 [ - - ][ - + ]: 1360 : if ((res == pivot && !posFirst) || (res.notNode() == pivot && posFirst)
[ - - ][ - + ]
[ - - ]
628 [ - + ][ - + ]: 1360 : || (pivot.notNode() == res && posFirst))
[ - - ][ + - ]
[ + - ][ - - ]
629 : : {
630 : : // We decrease i by one, since it could have been the case that i
631 : : // was equal to children.size(), so that we return false in the end
632 : 0 : --i;
633 : : }
634 : : else
635 : : {
636 : : // Otherwise check if any subsequent premise eliminates it
637 [ + + ]: 1327 : for (; i < children.size(); ++i)
638 : : {
639 : 653 : posFirst = args[(2 * i) - 2] == trueNode;
640 : 653 : pivot = args[(2 * i) - 1];
641 : : // To eliminate res, the clause must contain it with opposite
642 : : // polarity. There are three successful cases, according to the
643 : : // pivot and its sign
644 : : //
645 : : // - res is the same as the pivot and posFirst is true, which
646 : : // means that the clause contains its negation and eliminates it
647 : : //
648 : : // - res is the negation of the pivot and posFirst is false, so
649 : : // the clause contains the node whose negation is res. Note that
650 : : // this case may either be res.notNode() == pivot or res ==
651 : : // pivot.notNode().
652 [ - + ][ - + ]: 1306 : if ((res == pivot && posFirst) || (res.notNode() == pivot && !posFirst)
[ - - ][ + + ]
[ - - ]
653 [ + + ][ - + ]: 1306 : || (pivot.notNode() == res && !posFirst))
[ - - ][ + + ]
[ + + ][ - - ]
654 : : {
655 : 6 : break;
656 : : }
657 : : }
658 : : }
659 : 680 : }
660 : : // if not eliminated (loop went to the end), then it's a singleton
661 : : // clause
662 : 67047 : return i == children.size();
663 : 67047 : }
664 : :
665 : : } // namespace proof
666 : : } // namespace cvc5::internal
|
