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