Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Haniel Barbosa, Hans-Joerg Schurr, Aina Niemetz
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 : : * Implementation of a proof as produced by the equality engine.
14 : : */
15 : :
16 : : #include "theory/uf/eq_proof.h"
17 : :
18 : : #include "base/configuration.h"
19 : : #include "options/uf_options.h"
20 : : #include "proof/proof.h"
21 : : #include "proof/proof_checker.h"
22 : : #include "proof/proof_node_algorithm.h"
23 : : #include "proof/proof_node_manager.h"
24 : :
25 : : namespace cvc5::internal {
26 : : namespace theory {
27 : : namespace eq {
28 : :
29 : 0 : void EqProof::debug_print(const char* c, unsigned tb) const
30 : : {
31 : 0 : std::stringstream ss;
32 : 0 : debug_print(ss, tb);
33 : 0 : Trace(c) << ss.str();
34 : 0 : }
35 : :
36 : 0 : void EqProof::debug_print(std::ostream& os, unsigned tb) const
37 : : {
38 [ - - ]: 0 : for (unsigned i = 0; i < tb; i++)
39 : : {
40 : 0 : os << " ";
41 : : }
42 : 0 : os << d_id << "(";
43 [ - - ][ - - ]: 0 : if (d_children.empty() && d_node.isNull())
[ - - ]
44 : : {
45 : 0 : os << ")";
46 : 0 : return;
47 : : }
48 [ - - ]: 0 : if (!d_node.isNull())
49 : : {
50 : 0 : os << std::endl;
51 [ - - ]: 0 : for (unsigned i = 0; i < tb + 1; ++i)
52 : : {
53 : 0 : os << " ";
54 : : }
55 [ - - ]: 0 : os << d_node << (!d_children.empty() ? "," : "");
56 : : }
57 : 0 : unsigned size = d_children.size();
58 [ - - ]: 0 : for (unsigned i = 0; i < size; ++i)
59 : : {
60 : 0 : os << std::endl;
61 : 0 : d_children[i]->debug_print(os, tb + 1);
62 [ - - ]: 0 : if (i < size - 1)
63 : : {
64 [ - - ]: 0 : for (unsigned j = 0; j < tb + 1; ++j)
65 : : {
66 : 0 : os << " ";
67 : : }
68 : 0 : os << ",";
69 : : }
70 : : }
71 [ - - ]: 0 : if (size > 0)
72 : : {
73 [ - - ]: 0 : for (unsigned i = 0; i < tb; ++i)
74 : : {
75 : 0 : os << " ";
76 : : }
77 : : }
78 : 0 : os << ")" << std::endl;
79 : : }
80 : :
81 : 1456070 : void EqProof::cleanReflPremises(std::vector<Node>& premises) const
82 : : {
83 : 2912150 : std::vector<Node> newPremises;
84 : 1456070 : unsigned size = premises.size();
85 [ + + ]: 4591950 : for (unsigned i = 0; i < size; ++i)
86 : : {
87 [ + + ]: 3135880 : if (premises[i][0] == premises[i][1])
88 : : {
89 : 452768 : continue;
90 : : }
91 : 2683110 : newPremises.push_back(premises[i]);
92 : : }
93 [ + + ]: 1456070 : if (newPremises.size() != size)
94 : : {
95 [ + - ]: 429672 : Trace("eqproof-conv") << "EqProof::cleanReflPremises: removed "
96 : 0 : << (size >= newPremises.size()
97 [ - - ]: 214836 : ? size - newPremises.size()
98 : 0 : : 0)
99 : 214836 : << " refl premises from " << premises << "\n";
100 : 214836 : premises.clear();
101 : 214836 : premises.insert(premises.end(), newPremises.begin(), newPremises.end());
102 [ + - ]: 429672 : Trace("eqproof-conv") << "EqProof::cleanReflPremises: new premises "
103 : 214836 : << premises << "\n";
104 : : }
105 : 1456070 : }
106 : :
107 : 605208 : bool EqProof::expandTransitivityForDisequalities(
108 : : Node conclusion,
109 : : std::vector<Node>& premises,
110 : : CDProof* p,
111 : : std::unordered_set<Node>& assumptions) const
112 : : {
113 [ + - ]: 1210420 : Trace("eqproof-conv")
114 : : << "EqProof::expandTransitivityForDisequalities: check if need "
115 : 0 : "to expand transitivity step to conclude "
116 : 605208 : << conclusion << " from premises " << premises << "\n";
117 : : // Check premises to see if any of the form (= (= t1 t2) false), modulo
118 : : // symmetry
119 : 605208 : unsigned size = premises.size();
120 : : // termPos is, in (= (= t1 t2) false) or (= false (= t1 t2)), the position of
121 : : // the equality. When the i-th premise has that form, offending = i
122 : 605208 : unsigned termPos = 2, offending = size;
123 [ + + ]: 2381210 : for (unsigned i = 0; i < size; ++i)
124 : : {
125 [ - + ][ - + ]: 1776000 : Assert(premises[i].getKind() == Kind::EQUAL);
[ - - ]
126 [ + + ]: 5290960 : for (unsigned j = 0; j < 2; ++j)
127 : : {
128 [ + + ][ - - ]: 7074980 : if (premises[i][j].getKind() == Kind::CONST_BOOLEAN
129 [ + + ][ + - ]: 3575270 : && !premises[i][j].getConst<bool>()
[ - - ]
130 [ + + ][ + + ]: 7112760 : && premises[i][1 - j].getKind() == Kind::EQUAL)
[ + + ][ + + ]
[ - - ]
131 : : {
132 : : // there is only one offending equality
133 [ - + ][ - + ]: 22533 : Assert(offending == size);
[ - - ]
134 : 22533 : offending = i;
135 : 22533 : termPos = 1 - j;
136 : 22533 : break;
137 : : }
138 : : }
139 : : }
140 : : // if no equality of the searched form, nothing to do
141 [ + + ]: 605208 : if (offending == size)
142 : : {
143 [ + - ]: 1165350 : Trace("eqproof-conv")
144 : 582675 : << "EqProof::expandTransitivityForDisequalities: no need.\n";
145 : 582675 : return false;
146 : : }
147 : 22533 : NodeManager* nm = NodeManager::currentNM();
148 [ + + ][ - + ]: 22533 : Assert(termPos == 0 || termPos == 1);
[ - + ][ - - ]
149 [ + - ]: 45066 : Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: found "
150 : 0 : "offending equality at index "
151 : 22533 : << offending << " : " << premises[offending] << "\n";
152 : : // collect the premises to be used in the expansion, which are all but the
153 : : // offending one
154 : 45066 : std::vector<Node> expansionPremises;
155 [ + + ]: 86224 : for (unsigned i = 0; i < size; ++i)
156 : : {
157 [ + + ]: 63691 : if (i != offending)
158 : : {
159 : 41158 : expansionPremises.push_back(premises[i]);
160 : : }
161 : : }
162 : : // Eliminate spurious premises. Reasoning below assumes no refl steps.
163 : 22533 : cleanReflPremises(expansionPremises);
164 [ - + ][ - + ]: 22533 : Assert(!expansionPremises.empty());
[ - - ]
165 : : // Check if we are in the substitution case
166 : 45066 : Node expansionConclusion;
167 : 45066 : std::vector<Node> substPremises;
168 : 22533 : bool inSubstCase = false, substConclusionInReverseOrder = false;
169 [ + + ]: 45066 : if ((conclusion[0].getKind() == Kind::CONST_BOOLEAN)
170 : 22533 : != (conclusion[1].getKind() == Kind::CONST_BOOLEAN))
171 : : {
172 : 15109 : inSubstCase = true;
173 : : // reorder offending premise if constant is the first argument
174 [ + + ]: 15109 : if (termPos == 1)
175 : : {
176 : 13764 : premises[offending] =
177 : 27528 : premises[offending][1].eqNode(premises[offending][0]);
178 : : }
179 : : // reorder conclusion if constant is the first argument
180 : 15109 : conclusion = conclusion[1].getKind() == Kind::CONST_BOOLEAN
181 : 30218 : ? conclusion
182 : 15109 : : conclusion[1].eqNode(conclusion[0]);
183 : : // equality term in premise disequality
184 : 30218 : Node premiseTermEq = premises[offending][0];
185 : : // equality term in conclusion disequality
186 : 30218 : Node conclusionTermEq = conclusion[0];
187 [ + - ]: 30218 : Trace("eqproof-conv")
188 : : << "EqProof::expandTransitivityForDisequalities: Substitition "
189 : 0 : "case. Need to build subst from "
190 : 15109 : << premiseTermEq << " to " << conclusionTermEq << "\n";
191 : : // If only one argument in the premise is substituted, premiseTermEq and
192 : : // conclusionTermEq will share one argument and the other argument change
193 : : // defines the single substitution. Otherwise both arguments are replaced,
194 : : // so there are two substitutions.
195 [ + + ][ + + ]: 90654 : std::vector<Node> subs[2];
[ - - ]
196 : 15109 : subs[0].push_back(premiseTermEq[0]);
197 : 15109 : subs[1].push_back(premiseTermEq[1]);
198 : : // which of the arguments of premiseTermEq, if any, is equal to one argument
199 : : // of conclusionTermEq
200 : 15109 : int equalArg = -1;
201 [ + + ]: 45327 : for (unsigned i = 0; i < 2; ++i)
202 : : {
203 [ + + ]: 70493 : for (unsigned j = 0; j < 2; ++j)
204 : : {
205 [ + + ]: 53790 : if (premiseTermEq[i] == conclusionTermEq[j])
206 : : {
207 : 13515 : equalArg = i;
208 : : // identity sub
209 : 13515 : subs[i].push_back(conclusionTermEq[j]);
210 : : // sub that changes argument
211 : 13515 : subs[1 - i].push_back(conclusionTermEq[1 - j]);
212 : : // wither e.g. (= t1 t2), with sub t1->t3, becomes (= t2 t3)
213 : 13515 : substConclusionInReverseOrder = i != j;
214 : 13515 : break;
215 : : }
216 : : }
217 : : }
218 : : // simple case of single substitution
219 [ + + ]: 15109 : if (equalArg >= 0)
220 : : {
221 : : // case of
222 : : // (= (= t1 t2) false) (= t1 x1) ... (= xn t3)
223 : : // -------------------------------------------- EQP::TR
224 : : // (= (= t3 t2) false)
225 : : // where
226 : : //
227 : : // (= t1 x1) ... (= xn t3) - expansion premises
228 : : // ------------------------ TRANS
229 : : // (= t1 t3) - expansion conclusion
230 : : //
231 : : // will be the expansion made to justify the substitution for t1->t3.
232 : 13515 : expansionConclusion = subs[1 - equalArg][0].eqNode(subs[1 - equalArg][1]);
233 [ + - ]: 27030 : Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
234 : 0 : "Need to expand premises into "
235 : 13515 : << expansionConclusion << "\n";
236 : : // add refl step for the substitition t2->t2
237 : 27030 : p->addStep(subs[equalArg][0].eqNode(subs[equalArg][1]),
238 : : ProofRule::REFL,
239 : : {},
240 : 27030 : {subs[equalArg][0]});
241 : : }
242 : : else
243 : : {
244 : : // Hard case. We determine, and justify, the substitutions t1->t3/t4 and
245 : : // t2->t3/t4 based on the expansion premises.
246 [ + - ]: 3188 : Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
247 : 0 : "Need two substitutions. Look for "
248 : 1594 : << premiseTermEq[0] << " and " << premiseTermEq[1]
249 : 1594 : << " in premises " << expansionPremises << "\n";
250 [ - + ][ - - ]: 1594 : Assert(expansionPremises.size() >= 2)
251 : : << "Less than 2 expansion premises for substituting BOTH terms in "
252 : 0 : "disequality.\nDisequality: "
253 [ - + ][ - - ]: 1594 : << premises[offending]
254 : 0 : << "\nExpansion premises: " << expansionPremises
255 [ - + ][ - + ]: 1594 : << "\nConclusion: " << conclusion << "\n";
[ - - ]
256 : : // Easier case where we can determine the substitutions by directly
257 : : // looking at the premises, i.e. the two expansion premises are for
258 : : // example (= t1 t3) and (= t2 t4)
259 [ + + ]: 1594 : if (expansionPremises.size() == 2)
260 : : {
261 : : // iterate over args to be substituted
262 [ + + ]: 3747 : for (unsigned i = 0; i < 2; ++i)
263 : : {
264 : : // iterate over premises
265 [ + + ]: 7494 : for (unsigned j = 0; j < 2; ++j)
266 : : {
267 : : // iterate over args in premise
268 [ + + ]: 11160 : for (unsigned k = 0; k < 2; ++k)
269 : : {
270 [ + + ]: 8662 : if (premiseTermEq[i] == expansionPremises[j][k])
271 : : {
272 : 2498 : subs[i].push_back(expansionPremises[j][1 - k]);
273 : 2498 : break;
274 : : }
275 : : }
276 : : }
277 [ - + ][ - - ]: 2498 : Assert(subs[i].size() == 2)
278 [ - + ][ - + ]: 2498 : << " did not find term " << subs[i][0] << "\n";
[ - - ]
279 : : // check if argument to be substituted is in the same order in the
280 : : // conclusion
281 : : substConclusionInReverseOrder =
282 : 2498 : premiseTermEq[i] != conclusionTermEq[i];
283 : : }
284 : : }
285 : : else
286 : : {
287 [ + - ]: 690 : Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
288 : : "Build transitivity chains "
289 : 0 : "for two subs among more than 2 premises: "
290 : 345 : << expansionPremises << "\n";
291 : : // Hardest case. Try building a transitivity chain for (= t1 t3). If it
292 : : // can be built, use the remaining expansion premises to build a chain
293 : : // for (= t2 t4). Otherwise build it for (= t1 t4) and then build it for
294 : : // (= t2 t3). It should always succeed.
295 : 345 : subs[0].push_back(conclusionTermEq[0]);
296 : 345 : subs[1].push_back(conclusionTermEq[1]);
297 [ + + ]: 1035 : for (unsigned i = 0; i < 2; ++i)
298 : : {
299 : : // copy premises, since buildTransitivityChain is destructive
300 : : std::vector<Node> copy1ofExpPremises(expansionPremises.begin(),
301 : 690 : expansionPremises.end());
302 : 690 : Node transConclusion1 = subs[0][0].eqNode(subs[0][1]);
303 [ - + ]: 690 : if (!buildTransitivityChain(transConclusion1, copy1ofExpPremises))
304 : : {
305 : 0 : AlwaysAssert(i == 0)
306 : : << "Couldn't find sub at all for substituting BOTH terms in "
307 : 0 : "disequality.\nDisequality: "
308 : 0 : << premises[offending]
309 : 0 : << "\nExpansion premises: " << expansionPremises
310 : 0 : << "\nConclusion: " << conclusion << "\n";
311 : : // Failed. So flip sub and try again
312 : 0 : subs[0][1] = conclusionTermEq[1];
313 : 0 : subs[1][1] = conclusionTermEq[0];
314 : 0 : substConclusionInReverseOrder = false;
315 : 0 : continue;
316 : : }
317 : : // build next chain
318 : : std::vector<Node> copy2ofExpPremises(expansionPremises.begin(),
319 : 1380 : expansionPremises.end());
320 : 1380 : Node transConclusion2 = subs[1][0].eqNode(subs[1][1]);
321 [ - + ]: 690 : if (!buildTransitivityChain(transConclusion2, copy2ofExpPremises))
322 : : {
323 : 0 : Unreachable() << "Found sub " << transConclusion1
324 : 0 : << " but not other sub " << transConclusion2
325 : 0 : << ".\nDisequality: " << premises[offending]
326 : 0 : << "\nExpansion premises: " << expansionPremises
327 : 0 : << "\nConclusion: " << conclusion << "\n";
328 : : }
329 [ + - ]: 1380 : Trace("eqproof-conv")
330 : : << "EqProof::expandTransitivityForDisequalities: Built trans "
331 : : "chains: "
332 : 690 : "for two subs among more than 2 premises:\n";
333 [ + - ]: 1380 : Trace("eqproof-conv")
334 : 0 : << "EqProof::expandTransitivityForDisequalities: "
335 : 690 : << transConclusion1 << " <- " << copy1ofExpPremises << "\n";
336 [ + - ]: 1380 : Trace("eqproof-conv")
337 : 0 : << "EqProof::expandTransitivityForDisequalities: "
338 : 690 : << transConclusion2 << " <- " << copy2ofExpPremises << "\n";
339 : : // do transitivity steps if need be to justify each substitution
340 : 690 : if (copy1ofExpPremises.size() > 1
341 [ + + ][ + + ]: 690 : && !assumptions.count(transConclusion1))
[ + + ]
342 : : {
343 : 288 : p->addStep(transConclusion1,
344 : : ProofRule::TRANS,
345 : : copy1ofExpPremises,
346 : : {},
347 : : true);
348 : : }
349 : 690 : if (copy2ofExpPremises.size() > 1
350 [ + + ][ + + ]: 690 : && !assumptions.count(transConclusion2))
[ + + ]
351 : : {
352 : 308 : p->addStep(transConclusion2,
353 : : ProofRule::TRANS,
354 : : copy2ofExpPremises,
355 : : {},
356 : : true);
357 : : }
358 : : }
359 : : }
360 : : }
361 [ + - ]: 30218 : Trace("eqproof-conv")
362 : 0 : << "EqProof::expandTransitivityForDisequalities: Built substutitions "
363 : 0 : << subs[0] << " and " << subs[1] << " to map " << premiseTermEq
364 : 15109 : << " -> " << conclusionTermEq << "\n";
365 : 30218 : Assert(subs[0][1] == conclusion[0][0] || subs[0][1] == conclusion[0][1])
366 : 0 : << "EqProof::expandTransitivityForDisequalities: First substitution "
367 [ - + ][ - + ]: 15109 : << subs[0] << " doest not map to conclusion " << conclusion << "\n";
[ - - ]
368 : 30218 : Assert(subs[1][1] == conclusion[0][0] || subs[1][1] == conclusion[0][1])
369 : 0 : << "EqProof::expandTransitivityForDisequalities: Second substitution "
370 [ - + ][ - + ]: 15109 : << subs[1] << " doest not map to conclusion " << conclusion << "\n";
[ - - ]
371 : : // In the premises for the original conclusion, the substitution of
372 : : // premiseTermEq (= t1 t2) into conclusionTermEq (= t3 t4) is stored
373 : : // reversed, i.e. as (= (= t3 t4) (= t1 t2)), since the transitivity with
374 : : // the disequality is built as as
375 : : // (= (= t3 t4) (= t1 t2)) (= (= t1 t2) false)
376 : : // --------------------------------------------------------------------- TR
377 : : // (= (= t3 t4) false)
378 : 15109 : substPremises.push_back(subs[0][1].eqNode(subs[0][0]));
379 : 15109 : substPremises.push_back(subs[1][1].eqNode(subs[1][0]));
380 : : }
381 : : else
382 : : {
383 : : // In simple case the conclusion is always, modulo symmetry, false = true
384 : 14848 : Assert(conclusion[0].getKind() == Kind::CONST_BOOLEAN
385 : : && conclusion[1].getKind() == Kind::CONST_BOOLEAN);
386 : : // The expansion conclusion is the same as the equality term in the
387 : : // disequality, which is going to be justified by a transitivity step from
388 : : // the expansion premises
389 : 7424 : expansionConclusion = premises[offending][termPos];
390 : : }
391 : : // Unless we are in the double-substitution case, the proof has the shape
392 : : //
393 : : // ... ... ... ... - expansionPremises
394 : : // ------------------ TRANS
395 : : // (= (= (t t') false) (= t'' t''') - expansionConclusion
396 : : // ---------------------------------------------- TRANS or PRED_TRANSFORM
397 : : // conclusion
398 : : //
399 : : // although note that if it's a TRANS step, (= t'' t''') will be turned into a
400 : : // predicate equality and the premises are ordered.
401 : : //
402 : : // We build the transitivity step for the expansionConclusion here. It being
403 : : // non-null marks that we are not in the double-substitution case.
404 [ + + ]: 22533 : if (!expansionConclusion.isNull())
405 : : {
406 [ + - ]: 41878 : Trace("eqproof-conv")
407 : 0 : << "EqProof::expandTransitivityForDisequalities: need to derive "
408 : 0 : << expansionConclusion << " with premises " << expansionPremises
409 : 20939 : << "\n";
410 : 41878 : Assert(expansionPremises.size() > 1
411 : : || expansionConclusion == expansionPremises.back()
412 : : || (expansionConclusion[0] == expansionPremises.back()[1]
413 : : && expansionConclusion[1] == expansionPremises.back()[0]))
414 [ - + ][ - - ]: 20939 : << "single expansion premise " << expansionPremises.back()
415 [ - + ][ - + ]: 20939 : << " is not the same as expansionConclusion " << expansionConclusion
[ - - ]
416 : 0 : << " and not its symmetric\n";
417 : : // We track assumptions to avoid cyclic proofs, which can happen in EqProofs
418 : : // such as:
419 : : //
420 : : // (= l1 "") (= "" t)
421 : : // ----------------------- EQP::TR
422 : : // (= l1 "") (= l1 t) (= (= "" t) false)
423 : : // ----------------------------------------------------------------- EQP::TR
424 : : // (= false true)
425 : : //
426 : : // which would lead to the cyclic expansion proof:
427 : : //
428 : : // (= l1 "") (= l1 "") (= "" t)
429 : : // --------- SYMM ----------------------- TRANS
430 : : // (= "" l1) (= l1 t)
431 : : // ------------------------------------------ TRANS
432 : : // (= "" t)
433 [ + + ][ + + ]: 20939 : if (expansionPremises.size() > 1 && !assumptions.count(expansionConclusion))
[ + + ]
434 : : {
435 : : // create transitivity step to derive expected premise
436 : 6640 : buildTransitivityChain(expansionConclusion, expansionPremises);
437 [ + - ]: 13280 : Trace("eqproof-conv")
438 : : << "EqProof::expandTransitivityForDisequalities: add transitivity "
439 : 0 : "step for "
440 : 0 : << expansionConclusion << " with premises " << expansionPremises
441 : 6640 : << "\n";
442 : : // create expansion step
443 : 6640 : p->addStep(
444 : : expansionConclusion, ProofRule::TRANS, expansionPremises, {}, true);
445 : : }
446 : : }
447 [ + - ]: 45066 : Trace("eqproof-conv")
448 : 0 : << "EqProof::expandTransitivityForDisequalities: now derive conclusion "
449 : 22533 : << conclusion;
450 : 22533 : Node offendingNode = premises[offending];
451 : 22533 : premises.clear();
452 : 22533 : premises.push_back(offendingNode);
453 [ + + ]: 22533 : if (inSubstCase)
454 : : {
455 [ + - ][ - - ]: 30218 : Trace("eqproof-conv") << (substConclusionInReverseOrder ? " [inverted]"
456 : 0 : : "")
457 : 0 : << " via subsitution from " << premises[0]
458 : 15109 : << " and (inverted subst) " << substPremises << "\n";
459 : : // By this point, for premise disequality (= (= t1 t2) false), we have
460 : : // potentially already built
461 : : //
462 : : // (= t1 x1) ... (= xn t3) (= t2 y1) ... (= ym t4)
463 : : // ------------------------ TR ------------------------ TR
464 : : // (= t1 t3) (= t2 t4)
465 : : //
466 : : // to justify the substitutions t1->t3 and t2->t4 (where note that if t1=t3
467 : : // or t2=4, the step will actually be a REFL one). Not do
468 : : //
469 : : // ----------- SYMM ----------- SYMM
470 : : // (= t3 t1) (= t4 t2)
471 : : // ---------------------------------------- CONG
472 : : // (= (= t3 t4) (= t1 t2)) (= (= t1 t2) false)
473 : : // --------------------------------------------------------------------- TR
474 : : // (= (= t3 t4) false)
475 : : //
476 : : // where note that the SYMM steps are implicitly added by CDProof.
477 : : Node congConclusion = nm->mkNode(
478 : : Kind::EQUAL,
479 : 30218 : nm->mkNode(Kind::EQUAL, substPremises[0][0], substPremises[1][0]),
480 : 75545 : premises[0][0]);
481 : 30218 : p->addStep(congConclusion,
482 : : ProofRule::CONG,
483 : : substPremises,
484 : : {ProofRuleChecker::mkKindNode(Kind::EQUAL)},
485 : 15109 : true);
486 [ + - ]: 30218 : Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: via "
487 : 0 : "congruence derived "
488 : 15109 : << congConclusion << "\n";
489 : : // transitivity step between that and the original premise
490 : 15109 : premises.insert(premises.begin(), congConclusion);
491 : : Node transConclusion =
492 : 15109 : !substConclusionInReverseOrder
493 : : ? conclusion
494 : 37799 : : nm->mkNode(Kind::EQUAL, congConclusion[0], conclusion[1]);
495 : : // check to avoid cyclic proofs
496 [ + - ]: 15109 : if (!assumptions.count(transConclusion))
497 : : {
498 : 15109 : p->addStep(transConclusion, ProofRule::TRANS, premises, {}, true);
499 [ + - ]: 30218 : Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
500 : 0 : "via transitivity derived "
501 : 15109 : << transConclusion << "\n";
502 : : }
503 : : // if order is reversed, finish the proof of conclusion with
504 : : // (= (= t3 t4) false)
505 : : // --------------------- MACRO_SR_PRED_TRANSFORM
506 : : // (= (= t4 t3) false)
507 [ + + ]: 15109 : if (substConclusionInReverseOrder)
508 : : {
509 : 7581 : p->addStep(conclusion,
510 : : ProofRule::MACRO_SR_PRED_TRANSFORM,
511 : : {transConclusion},
512 : : {conclusion},
513 : 5054 : true);
514 [ + - ]: 5054 : Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
515 : 0 : "via macro transform derived "
516 : 2527 : << conclusion << "\n";
517 : : }
518 : : }
519 : : else
520 : : {
521 : : // create TRUE_INTRO step for expansionConclusion and add it to the premises
522 [ + - ]: 14848 : Trace("eqproof-conv")
523 : : << " via transitivity.\nEqProof::expandTransitivityForDisequalities: "
524 : 0 : "adding "
525 [ - + ][ - - ]: 7424 : << ProofRule::TRUE_INTRO << " step for " << expansionConclusion[0]
526 : 7424 : << "\n";
527 : : Node newExpansionConclusion =
528 : 7424 : expansionConclusion.eqNode(nm->mkConst<bool>(true));
529 : 14848 : p->addStep(newExpansionConclusion,
530 : : ProofRule::TRUE_INTRO,
531 : : {expansionConclusion},
532 : 7424 : {});
533 : 7424 : premises.push_back(newExpansionConclusion);
534 [ + - ]: 7424 : Trace("eqproof-conv") << ProofRule::TRANS << " from " << premises << "\n";
535 : 7424 : buildTransitivityChain(conclusion, premises);
536 : : // create final transitivity step
537 : 7424 : p->addStep(conclusion, ProofRule::TRANS, premises, {}, true);
538 : : }
539 : 22533 : return true;
540 : : }
541 : :
542 : : // TEMPORARY NOTE: This may not be enough. Worst case scenario I need to
543 : : // reproduce here a search for arbitrary chains between each of the variables in
544 : : // the conclusion and a constant
545 : 582675 : bool EqProof::expandTransitivityForTheoryDisequalities(
546 : : Node conclusion, std::vector<Node>& premises, CDProof* p) const
547 : : {
548 : : // whether conclusion is a disequality (= (= t1 t2) false), modulo symmetry
549 : 582675 : unsigned termPos = -1;
550 [ + + ]: 1748020 : for (unsigned i = 0; i < 2; ++i)
551 : : {
552 [ + + ][ - - ]: 1165350 : if (conclusion[i].getKind() == Kind::CONST_BOOLEAN
553 [ + + ][ + - ]: 1178940 : && !conclusion[i].getConst<bool>()
[ - - ]
554 [ + + ][ + + ]: 1178940 : && conclusion[1 - i].getKind() == Kind::EQUAL)
[ + + ][ + + ]
[ - - ]
555 : : {
556 : 10 : termPos = i - 1;
557 : 10 : break;
558 : : }
559 : : }
560 : : // no disequality
561 [ + + ]: 582675 : if (termPos == static_cast<unsigned>(-1))
562 : : {
563 : 582665 : return false;
564 : : }
565 [ + - ]: 20 : Trace("eqproof-conv")
566 : : << "EqProof::expandTransitivityForTheoryDisequalities: check if need "
567 : 0 : "to expand transitivity step to conclude disequality "
568 : 10 : << conclusion << " from premises " << premises << "\n";
569 : :
570 : : // Check if the premises are (= t1 c1) and (= t2 c2), modulo symmetry
571 : 20 : std::vector<Node> subChildren, constChildren;
572 [ + + ]: 30 : for (unsigned i = 0; i < 2; ++i)
573 : : {
574 : 40 : Node term = conclusion[termPos][i];
575 [ + + ]: 60 : for (const Node& premise : premises)
576 : : {
577 [ + + ]: 90 : for (unsigned j = 0; j < 2; ++j)
578 : : {
579 : 70 : if (premise[j] == term && premise[1 - j].isConst())
580 : : {
581 : 20 : subChildren.push_back(premise[j].eqNode(premise[1 - j]));
582 : 20 : constChildren.push_back(premise[1 - j]);
583 : 20 : break;
584 : : }
585 : : }
586 : : }
587 : : }
588 [ - + ]: 10 : if (subChildren.size() < 2)
589 : : {
590 : 0 : return false;
591 : : }
592 : : // Now build
593 : : // (= t1 c1) (= t2 c2)
594 : : // ------------------------- CONG ------------------- MACRO_SR_PRED_INTRO
595 : : // (= (= t1 t2) (= c1 c2)) (= (= c1 c2) false)
596 : : // --------------------------------------------------------------------- TR
597 : : // (= (= t1 t2) false)
598 : 20 : Node constApp = NodeManager::currentNM()->mkNode(Kind::EQUAL, constChildren);
599 : 20 : Node constEquality = constApp.eqNode(conclusion[1 - termPos]);
600 [ + - ]: 20 : Trace("eqproof-conv")
601 : 0 : << "EqProof::expandTransitivityForTheoryDisequalities: adding "
602 : 0 : << ProofRule::MACRO_SR_PRED_INTRO << " step for " << constApp << " = "
603 [ - + ][ - - ]: 10 : << conclusion[1 - termPos] << "\n";
604 : 20 : p->addStep(
605 : 10 : constEquality, ProofRule::MACRO_SR_PRED_INTRO, {}, {constEquality});
606 : : // build congruence conclusion (= (= t1 t2) (t c1 c2))
607 : 20 : Node congConclusion = conclusion[termPos].eqNode(constApp);
608 [ + - ]: 20 : Trace("eqproof-conv")
609 : 0 : << "EqProof::expandTransitivityForTheoryDisequalities: adding "
610 : 10 : << ProofRule::CONG << " step for " << congConclusion << " from "
611 : 10 : << subChildren << "\n";
612 : 20 : p->addStep(congConclusion,
613 : : ProofRule::CONG,
614 : : {subChildren},
615 : : {ProofRuleChecker::mkKindNode(Kind::EQUAL)},
616 : 10 : true);
617 [ + - ]: 20 : Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: via "
618 : 0 : "congruence derived "
619 : 10 : << congConclusion << "\n";
620 : 40 : std::vector<Node> transitivityChildren{congConclusion, constEquality};
621 : 10 : p->addStep(conclusion, ProofRule::TRANS, {transitivityChildren}, {});
622 : 10 : return true;
623 : : }
624 : :
625 : 1807090 : bool EqProof::buildTransitivityChain(Node conclusion,
626 : : std::vector<Node>& premises) const
627 : : {
628 [ + - ]: 3614180 : Trace("eqproof-conv") << push
629 : 0 : << "EqProof::buildTransitivityChain: Build chain for "
630 : 1807090 : << conclusion << " with premises " << premises << "\n";
631 [ + - ]: 4664330 : for (unsigned i = 0, size = premises.size(); i < size; ++i)
632 : : {
633 : 4664330 : bool occurs = false, correctlyOrdered = false;
634 [ + + ]: 4664330 : if (conclusion[0] == premises[i][0])
635 : : {
636 : 699827 : occurs = correctlyOrdered = true;
637 : : }
638 [ + + ]: 3964500 : else if (conclusion[0] == premises[i][1])
639 : : {
640 : 1107260 : occurs = true;
641 : : }
642 [ + + ]: 4664330 : if (occurs)
643 : : {
644 [ + - ]: 3614180 : Trace("eqproof-conv")
645 [ - - ]: 1807090 : << "EqProof::buildTransitivityChain: found " << conclusion[0] << " in"
646 [ - - ][ - + ]: 1807090 : << (correctlyOrdered ? "" : " non-") << " ordered premise "
647 : 1807090 : << premises[i] << "\n";
648 [ + + ][ + + ]: 1807090 : if (conclusion[1] == premises[i][correctlyOrdered ? 1 : 0])
649 : : {
650 [ + - ]: 1251290 : Trace("eqproof-conv")
651 [ - + ][ - - ]: 625646 : << "EqProof::buildTransitivityChain: found " << conclusion[1]
652 : 0 : << " in same premise. Closed chain.\n"
653 : 625646 : << pop;
654 : 625646 : premises.clear();
655 : 625646 : premises.push_back(conclusion);
656 : 1807090 : return true;
657 : : }
658 : : // Build chain with remaining equalities
659 : 1181440 : std::vector<Node> recursivePremises;
660 [ + + ]: 5242280 : for (unsigned j = 0; j < size; ++j)
661 : : {
662 [ + + ]: 4060840 : if (j != i)
663 : : {
664 : 2879390 : recursivePremises.push_back(premises[j]);
665 : : }
666 : : }
667 : : Node newTarget =
668 [ + + ]: 2362890 : premises[i][correctlyOrdered ? 1 : 0].eqNode(conclusion[1]);
669 [ + - ]: 2362890 : Trace("eqproof-conv")
670 : 0 : << "EqProof::buildTransitivityChain: search recursively for "
671 : 1181440 : << newTarget << "\n";
672 [ + - ]: 1181440 : if (buildTransitivityChain(newTarget, recursivePremises))
673 : : {
674 [ + - ]: 2362890 : Trace("eqproof-conv")
675 : 0 : << "EqProof::buildTransitivityChain: closed chain with "
676 : 0 : << 1 + recursivePremises.size() << " of the original "
677 : 1181440 : << premises.size() << " premises\n"
678 : 1181440 : << pop;
679 : : Node premiseNode = correctlyOrdered
680 : 446862 : ? premises[i]
681 : 2362890 : : premises[i][1].eqNode(premises[i][0]);
682 : 1181440 : premises.clear();
683 : 1181440 : premises.push_back(premiseNode);
684 : : premises.insert(
685 : 1181440 : premises.end(), recursivePremises.begin(), recursivePremises.end());
686 : 1181440 : return true;
687 : : }
688 : : }
689 : : }
690 [ - - ]: 0 : Trace("eqproof-conv")
691 : 0 : << "EqProof::buildTransitivityChain: Could not build chain for"
692 : 0 : << conclusion << " with premises " << premises << "\n";
693 [ - - ]: 0 : Trace("eqproof-conv") << pop;
694 : 0 : return false;
695 : : }
696 : :
697 : 2027980 : void EqProof::reduceNestedCongruence(
698 : : unsigned i,
699 : : Node conclusion,
700 : : std::vector<std::vector<Node>>& transitivityMatrix,
701 : : CDProof* p,
702 : : std::unordered_map<Node, Node>& visited,
703 : : std::unordered_set<Node>& assumptions,
704 : : bool isNary) const
705 : : {
706 [ + - ]: 4055970 : Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: building for " << i
707 : 2027980 : << "-th arg\n";
708 [ + + ]: 2027980 : if (d_id == MERGED_THROUGH_CONGRUENCE)
709 : : {
710 [ - + ][ - + ]: 1683070 : Assert(d_children.size() == 2);
[ - - ]
711 [ + - ]: 3366130 : Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: it's a "
712 : 0 : "congruence step. Reduce second child\n"
713 : 1683070 : << push;
714 : 3366130 : transitivityMatrix[i].push_back(
715 : 3366130 : d_children[1]->addToProof(p, visited, assumptions));
716 [ + - ]: 3366130 : Trace("eqproof-conv")
717 : 0 : << pop << "EqProof::reduceNestedCongruence: child conclusion "
718 : 1683070 : << transitivityMatrix[i].back() << "\n";
719 : : // if i == 0, first child must be REFL step, standing for (= f f), which can
720 : : // be ignored in a first-order calculus
721 : : // Notice if higher-order is disabled, the following holds:
722 : : // i > 0 || d_children[0]->d_id == MERGED_THROUGH_REFLEXIVITY
723 : : // We don't have access to whether we are higher-order in this context,
724 : : // so the above cannot be an assertion.
725 : : // recurse
726 [ + + ]: 1683070 : if (i > 1)
727 : : {
728 [ + - ]: 842430 : Trace("eqproof-conv")
729 : 0 : << "EqProof::reduceNestedCongruence: Reduce first child\n"
730 : 421215 : << push;
731 : 421215 : d_children[0]->reduceNestedCongruence(i - 1,
732 : : conclusion,
733 : : transitivityMatrix,
734 : : p,
735 : : visited,
736 : : assumptions,
737 : : isNary);
738 [ + - ]: 421215 : Trace("eqproof-conv") << pop;
739 : : }
740 : : // higher-order case
741 [ + + ]: 1261850 : else if (d_children[0]->d_id != MERGED_THROUGH_REFLEXIVITY)
742 : : {
743 [ + - ]: 508 : Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: HO case. "
744 : 254 : "Processing first child\n";
745 : : // we only handle these cases
746 [ + + ][ - + ]: 254 : Assert(d_children[0]->d_id == MERGED_THROUGH_EQUALITY
[ - + ][ - - ]
747 : : || d_children[0]->d_id == MERGED_THROUGH_TRANS);
748 : 508 : transitivityMatrix[0].push_back(
749 : 508 : d_children[0]->addToProof(p, visited, assumptions));
750 : : }
751 : 1683070 : return;
752 : : }
753 [ - + ][ - + ]: 344918 : Assert(d_id == MERGED_THROUGH_TRANS)
[ - - ]
754 : 0 : << "id is " << static_cast<MergeReasonType>(d_id) << "\n";
755 [ + - ]: 689836 : Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: it's a "
756 : 344918 : "transitivity step.\n";
757 : 344918 : Assert(d_node.isNull()
758 : : || d_node[0].getNumChildren() == d_node[1].getNumChildren() || isNary)
759 : : << "Non-null (internal cong) transitivity conclusion of different arity "
760 : 0 : "but not marked by isNary flag\n";
761 : : // If handling n-ary kinds and got a transitivity conclusion, we process it
762 : : // with addToProof, store the result into row i, and stop. This marks an
763 : : // "adjustment" of the arity, with empty rows 0..i-1 in the matrix determining
764 : : // the adjustment in addToProof processing the congruence of the original
765 : : // conclusion. See details there.
766 [ + + ][ + + ]: 344918 : if (isNary && !d_node.isNull())
[ + + ]
767 : : {
768 [ + - ]: 116 : Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: n-ary case, "
769 : 0 : "break recursion and indepedently process "
770 : 0 : << d_node << "\n"
771 : 58 : << push;
772 : 58 : transitivityMatrix[i].push_back(addToProof(p, visited, assumptions));
773 [ + - ]: 116 : Trace("eqproof-conv") << pop
774 : 0 : << "EqProof::reduceNestedCongruence: Got conclusion "
775 : 0 : << transitivityMatrix[i].back()
776 : 58 : << " from n-ary transitivity processing\n";
777 : 58 : return;
778 : : }
779 : : // Regular recursive processing of each transitivity premise
780 [ + + ]: 1298720 : for (unsigned j = 0, sizeTrans = d_children.size(); j < sizeTrans; ++j)
781 : : {
782 [ + - ]: 953855 : if (d_children[j]->d_id == MERGED_THROUGH_CONGRUENCE)
783 : : {
784 [ + - ]: 1907710 : Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: Reduce " << j
785 : 0 : << "-th transitivity congruence child\n"
786 : 953855 : << push;
787 : 953855 : d_children[j]->reduceNestedCongruence(
788 : : i, conclusion, transitivityMatrix, p, visited, assumptions, isNary);
789 [ + - ]: 953855 : Trace("eqproof-conv") << pop;
790 : : }
791 : : else
792 : : {
793 [ - - ]: 0 : Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: Add " << j
794 : 0 : << "-th transitivity child to proof\n"
795 : 0 : << push;
796 : 0 : transitivityMatrix[i].push_back(
797 : 0 : d_children[j]->addToProof(p, visited, assumptions));
798 [ - - ]: 0 : Trace("eqproof-conv") << pop;
799 : : }
800 : : }
801 : : }
802 : :
803 : 298059 : Node EqProof::addToProof(CDProof* p) const
804 : : {
805 : 596118 : std::unordered_map<Node, Node> cache;
806 : 596118 : std::unordered_set<Node> assumptions;
807 : 596118 : Node conclusion = addToProof(p, cache, assumptions);
808 [ + - ]: 596118 : Trace("eqproof-conv") << "EqProof::addToProof: root of proof: " << conclusion
809 : 298059 : << "\n";
810 [ + - ]: 596118 : Trace("eqproof-conv") << "EqProof::addToProof: tracked assumptions: "
811 : 298059 : << assumptions << "\n";
812 : : // If conclusion t1 = tn is, modulo symmetry, of the form (= t true/false), in
813 : : // which t is not true/false, it must be turned into t or (not t) with
814 : : // TRUE/FALSE_ELIM.
815 : 298059 : Node newConclusion = conclusion;
816 [ - + ][ - + ]: 298059 : Assert(conclusion.getKind() == Kind::EQUAL);
[ - - ]
817 [ + + ]: 596118 : if ((conclusion[0].getKind() == Kind::CONST_BOOLEAN)
818 : 298059 : != (conclusion[1].getKind() == Kind::CONST_BOOLEAN))
819 : : {
820 [ + - ]: 59014 : Trace("eqproof-conv")
821 : 29507 : << "EqProof::addToProof: process root for TRUE/FALSE_ELIM\n";
822 : : // Index of constant in equality
823 : : unsigned constIndex =
824 : 29507 : conclusion[0].getKind() == Kind::CONST_BOOLEAN ? 0 : 1;
825 : : // The premise for the elimination rule must have the constant as the second
826 : : // argument of the equality. If that's not the case, build it as such,
827 : : // relying on an implicit SYMM step to be added to the proof when justifying
828 : : // t / (not t).
829 : : Node elimPremise =
830 : 68334 : constIndex == 1 ? conclusion : conclusion[1].eqNode(conclusion[0]);
831 : : // Determine whether TRUE_ELIM or FALSE_ELIM, depending on the constant
832 : : // value. The new conclusion, whether t or (not t), is also determined
833 : : // accordingly.
834 : : ProofRule elimRule;
835 [ + + ]: 29507 : if (conclusion[constIndex].getConst<bool>())
836 : : {
837 : 8063 : elimRule = ProofRule::TRUE_ELIM;
838 : 8063 : newConclusion = conclusion[1 - constIndex];
839 : : }
840 : : else
841 : : {
842 : 21444 : elimRule = ProofRule::FALSE_ELIM;
843 : 21444 : newConclusion = conclusion[1 - constIndex].notNode();
844 : : }
845 : : // We also check if the final conclusion t / (not t) has already been
846 : : // justified, so that we can avoid a cyclic proof, which can be due to
847 : : // either t / (not t) being assumption in the original EqProof or it having
848 : : // a non-assumption proof step in the proof of (= t true/false).
849 [ + + ][ + - ]: 29507 : if (!assumptions.count(newConclusion) && !p->hasStep(newConclusion))
[ + + ][ + + ]
[ - - ]
850 : : {
851 [ + - ]: 38998 : Trace("eqproof-conv")
852 : 0 : << "EqProof::addToProof: conclude " << newConclusion << " via "
853 : 19499 : << elimRule << " step for " << elimPremise << "\n";
854 : 38998 : p->addStep(newConclusion, elimRule, {elimPremise}, {});
855 : : }
856 : : }
857 : 596118 : return newConclusion;
858 : : }
859 : :
860 : 3801140 : Node EqProof::addToProof(CDProof* p,
861 : : std::unordered_map<Node, Node>& visited,
862 : : std::unordered_set<Node>& assumptions) const
863 : : {
864 : 3801140 : std::unordered_map<Node, Node>::const_iterator it = visited.find(d_node);
865 [ + + ]: 3801140 : if (it != visited.end())
866 : : {
867 [ + - ]: 1744990 : Trace("eqproof-conv") << "EqProof::addToProof: already processed " << d_node
868 : 872495 : << ", returning " << it->second << "\n";
869 : 872495 : return it->second;
870 : : }
871 [ + - ]: 5857280 : Trace("eqproof-conv") << "EqProof::addToProof: adding step for " << d_id
872 : 2928640 : << " with conclusion " << d_node << "\n";
873 : : // Assumption
874 [ + + ]: 2928640 : if (d_id == MERGED_THROUGH_EQUALITY)
875 : : {
876 : : // Check that no (= true/false true/false) assumptions
877 [ + - ][ + - ]: 1373040 : if (Configuration::isDebugBuild() && d_node.getKind() == Kind::EQUAL)
[ + - ]
878 : : {
879 [ + + ]: 4119110 : for (unsigned i = 0; i < 2; ++i)
880 : : {
881 : 5492150 : Assert(d_node[i].getKind() != Kind::CONST_BOOLEAN
882 : : || d_node[1 - i].getKind() != Kind::CONST_BOOLEAN)
883 : 0 : << "EqProof::addToProof: fully boolean constant assumption "
884 [ - + ][ - + ]: 2746080 : << d_node << " is disallowed\n";
[ - - ]
885 : : }
886 : : }
887 : : // If conclusion is (= t true/false), we add a proof step
888 : : // t
889 : : // ---------------- TRUE/FALSE_INTRO
890 : : // (= t true/false)
891 : : // according to the value of the Boolean constant
892 : 4119110 : if (d_node.getKind() == Kind::EQUAL
893 [ + - ][ + + ]: 4119110 : && ((d_node[0].getKind() == Kind::CONST_BOOLEAN)
[ - - ]
894 [ + + ][ + - ]: 2746080 : != (d_node[1].getKind() == Kind::CONST_BOOLEAN)))
[ + - ][ - - ]
895 : : {
896 [ + - ]: 92244 : Trace("eqproof-conv")
897 : 46122 : << "EqProof::addToProof: add an intro step for " << d_node << "\n";
898 : : // Index of constant in equality
899 : 46122 : unsigned constIndex = d_node[0].getKind() == Kind::CONST_BOOLEAN ? 0 : 1;
900 : : // The premise for the intro rule is either t or (not t), according to the
901 : : // Boolean constant.
902 : 92244 : Node introPremise;
903 : : ProofRule introRule;
904 [ + + ]: 46122 : if (d_node[constIndex].getConst<bool>())
905 : : {
906 : 14084 : introRule = ProofRule::TRUE_INTRO;
907 : 14084 : introPremise = d_node[1 - constIndex];
908 : : // Track the new assumption. If it's an equality, also its symmetric
909 : 14084 : assumptions.insert(introPremise);
910 [ - + ]: 14084 : if (introPremise.getKind() == Kind::EQUAL)
911 : : {
912 : 0 : assumptions.insert(introPremise[1].eqNode(introPremise[0]));
913 : : }
914 : : }
915 : : else
916 : : {
917 : 32038 : introRule = ProofRule::FALSE_INTRO;
918 : 32038 : introPremise = d_node[1 - constIndex].notNode();
919 : : // Track the new assumption. If it's a disequality, also its symmetric
920 : 32038 : assumptions.insert(introPremise);
921 [ + + ]: 32038 : if (introPremise[0].getKind() == Kind::EQUAL)
922 : : {
923 : : assumptions.insert(
924 : 23544 : introPremise[0][1].eqNode(introPremise[0][0]).notNode());
925 : : }
926 : : }
927 : : // The original assumption can be e.g. (= false (= t1 t2)) in which case
928 : : // the necessary proof to be built is
929 : : // (not (= t1 t2))
930 : : // -------------------- FALSE_INTRO
931 : : // (= (= t1 t2) false)
932 : : // -------------------- SYMM
933 : : // (= false (= t1 t2))
934 : : //
935 : : // with the SYMM step happening automatically whenever the assumption is
936 : : // used in the proof p
937 : : Node introConclusion =
938 : 78935 : constIndex == 1 ? d_node : d_node[1].eqNode(d_node[0]);
939 : 92244 : p->addStep(introConclusion, introRule, {introPremise}, {});
940 : : }
941 : : else
942 : : {
943 : 2653830 : p->addStep(d_node, ProofRule::ASSUME, {}, {d_node});
944 : : }
945 : : // If non-equality predicate, turn into one via TRUE/FALSE intro
946 : 2746080 : Node conclusion = d_node;
947 [ - + ]: 1373040 : if (d_node.getKind() != Kind::EQUAL)
948 : : {
949 : : // Track original assumption
950 : 0 : assumptions.insert(d_node);
951 : : ProofRule intro;
952 [ - - ]: 0 : if (d_node.getKind() == Kind::NOT)
953 : : {
954 : 0 : intro = ProofRule::FALSE_INTRO;
955 : : conclusion =
956 : 0 : d_node[0].eqNode(NodeManager::currentNM()->mkConst<bool>(false));
957 : : }
958 : : else
959 : : {
960 : 0 : intro = ProofRule::TRUE_INTRO;
961 : : conclusion =
962 : 0 : d_node.eqNode(NodeManager::currentNM()->mkConst<bool>(true));
963 : : }
964 [ - - ]: 0 : Trace("eqproof-conv") << "EqProof::addToProof: adding " << intro
965 : 0 : << " step for " << d_node << "\n";
966 : 0 : p->addStep(conclusion, intro, {d_node}, {});
967 : : }
968 : : // Keep track of assumptions to avoid cyclic proofs. Both the assumption and
969 : : // its symmetric are added
970 : 1373040 : assumptions.insert(conclusion);
971 : 1373040 : assumptions.insert(conclusion[1].eqNode(conclusion[0]));
972 [ + - ]: 2746080 : Trace("eqproof-conv") << "EqProof::addToProof: tracking assumptions "
973 [ - - ]: 1373040 : << conclusion << ", (= " << conclusion[1] << " "
974 [ - + ][ - + ]: 1373040 : << conclusion[0] << ")\n";
[ - - ]
975 : 1373040 : visited[d_node] = conclusion;
976 : 1373040 : return conclusion;
977 : : }
978 : : // Refl and laborious congruence steps for (= (f t1 ... tn) (f t1 ... tn)),
979 : : // which can be safely turned into reflexivity steps. These laborious
980 : : // congruence steps are currently generated in the equality engine because of
981 : : // the suboptimal handling of n-ary operators.
982 : 3111200 : if (d_id == MERGED_THROUGH_REFLEXIVITY
983 : 1555600 : || (d_node.getKind() == Kind::EQUAL && d_node[0] == d_node[1]))
984 : : {
985 [ + - ]: 283830 : Trace("eqproof-conv") << "EqProof::addToProof: refl step\n";
986 : : Node conclusion =
987 [ + - ]: 567660 : d_node.getKind() == Kind::EQUAL ? d_node : d_node.eqNode(d_node);
988 : 567660 : p->addStep(conclusion, ProofRule::REFL, {}, {conclusion[0]});
989 : 283830 : visited[d_node] = conclusion;
990 : 283830 : return conclusion;
991 : : }
992 : : // Equalities due to theory reasoning
993 [ + + ]: 1271770 : if (d_id == MERGED_THROUGH_CONSTANTS)
994 : : {
995 : 27300 : Assert(!d_node.isNull()
996 : : && ((d_node.getKind() == Kind::EQUAL && d_node[1].isConst())
997 : : || (d_node.getKind() == Kind::NOT
998 : : && d_node[0].getKind() == Kind::EQUAL
999 : : && d_node[0][0].isConst() && d_node[0][1].isConst())))
1000 [ - + ][ - + ]: 13650 : << ". Conclusion " << d_node << " from " << d_id
[ - - ]
1001 : 0 : << " was expected to be (= (f t1 ... tn) c) or (not (= c1 c2))\n";
1002 [ - + ][ - - ]: 13650 : Assert(!assumptions.count(d_node))
1003 [ - + ][ - + ]: 13650 : << "Conclusion " << d_node << " from " << d_id << " is an assumption\n";
[ - - ]
1004 : : // The step has the form (not (= c1 c2)). We conclude it via
1005 : : // MACRO_SR_PRED_INTRO and turn it into an equality with false, so that the
1006 : : // rest of the reconstruction works
1007 [ + + ]: 13650 : if (d_children.empty())
1008 : : {
1009 : : Node conclusion =
1010 : 792 : d_node[0].eqNode(NodeManager::currentNM()->mkConst<bool>(false));
1011 : 528 : p->addStep(d_node, ProofRule::MACRO_SR_PRED_INTRO, {}, {d_node});
1012 : 528 : p->addStep(conclusion, ProofRule::FALSE_INTRO, {d_node}, {});
1013 : 264 : visited[d_node] = conclusion;
1014 : 264 : return conclusion;
1015 : : }
1016 : : // The step has the form
1017 : : // [(= t1 c1)] ... [(= tn cn)]
1018 : : // ------------------------
1019 : : // (= (f t1 ... tn) c)
1020 : : // where premises equating ti to constants are present when they are not
1021 : : // already constants. Note that the premises may be in any order, e.g. with
1022 : : // the equality for the second term being justified in the first premise.
1023 : : // Moreover, they may be of the form (= ci ti).
1024 : : //
1025 : : // First recursively process premises, if any
1026 : 26772 : std::vector<Node> premises;
1027 [ + + ]: 40467 : for (unsigned i = 0; i < d_children.size(); ++i)
1028 : : {
1029 [ + - ]: 54162 : Trace("eqproof-conv")
1030 : 0 : << "EqProof::addToProof: recurse on child " << i << "\n"
1031 : 27081 : << push;
1032 : 27081 : premises.push_back(d_children[i]->addToProof(p, visited, assumptions));
1033 [ + - ]: 27081 : Trace("eqproof-conv") << pop;
1034 : : }
1035 : : // After building the proper premises we could build a step like
1036 : : // [(= t1 c1)] ... [(= tn cn)]
1037 : : // ---------------------------- MACRO_SR_PRED_INTRO
1038 : : // (= (f t1 ... tn) c)
1039 : : // but note that since the substitution applied by MACRO_SR_PRED_INTRO is
1040 : : // *not* simultenous this could lead to issues if t_{i+1} occurred in some
1041 : : // t_{i}. So we build proofs as
1042 : : //
1043 : : // [(= t1 c1)] ... [(= tn cn)]
1044 : : // ------------------------------- CONG -------------- MACRO_SR_PRED_INTRO
1045 : : // (= (f t1 ... tn) (f c1 ... cn)) (= (f c1 ... cn) c)
1046 : : // ---------------------------------------------------------- TRANS
1047 : : // (= (f t1 ... tn) c)
1048 : 26772 : std::vector<Node> subChildren, constChildren;
1049 [ + + ]: 40467 : for (unsigned i = 0, size = d_node[0].getNumChildren(); i < size; ++i)
1050 : : {
1051 : 27081 : Node term = d_node[0][i];
1052 : : // term already is a constant, add a REFL step
1053 [ + + ]: 27081 : if (term.isConst())
1054 : : {
1055 : 10239 : subChildren.push_back(term.eqNode(term));
1056 : 20478 : p->addStep(subChildren.back(), ProofRule::REFL, {}, {term});
1057 : 10239 : constChildren.push_back(term);
1058 : 10239 : continue;
1059 : : }
1060 : : // Build the equality (= ti ci) as a premise, finding the respective ci is
1061 : : // the original premises
1062 : 33684 : Node constant;
1063 [ + - ]: 27954 : for (const Node& premise : premises)
1064 : : {
1065 [ - + ][ - + ]: 27954 : Assert(premise.getKind() == Kind::EQUAL);
[ - - ]
1066 [ + + ]: 27954 : if (premise[0] == term)
1067 : : {
1068 [ - + ][ - + ]: 3692 : Assert(premise[1].isConst());
[ - - ]
1069 : 3692 : constant = premise[1];
1070 : 3692 : break;
1071 : : }
1072 [ + + ]: 24262 : if (premise[1] == term)
1073 : : {
1074 [ - + ][ - + ]: 13150 : Assert(premise[0].isConst());
[ - - ]
1075 : 13150 : constant = premise[0];
1076 : 13150 : break;
1077 : : }
1078 : : }
1079 [ - + ][ - + ]: 16842 : Assert(!constant.isNull());
[ - - ]
1080 : 16842 : subChildren.push_back(term.eqNode(constant));
1081 : 16842 : constChildren.push_back(constant);
1082 : : }
1083 : : // build constant application (f c1 ... cn) and equality (= (f c1 ... cn) c)
1084 : 13386 : Kind k = d_node[0].getKind();
1085 : 26772 : std::vector<Node> cargs;
1086 : 13386 : ProofRule rule = expr::getCongRule(d_node[0], cargs);
1087 [ - + ]: 13386 : if (d_node[0].getMetaKind() == kind::metakind::PARAMETERIZED)
1088 : : {
1089 : 0 : constChildren.insert(constChildren.begin(), d_node[0].getOperator());
1090 : : }
1091 : 26772 : Node constApp = NodeManager::currentNM()->mkNode(k, constChildren);
1092 : 26772 : Node constEquality = constApp.eqNode(d_node[1]);
1093 [ + - ]: 26772 : Trace("eqproof-conv") << "EqProof::addToProof: adding "
1094 : 0 : << ProofRule::MACRO_SR_PRED_INTRO << " step for "
1095 [ - + ][ - - ]: 13386 : << constApp << " = " << d_node[1] << "\n";
1096 : 26772 : p->addStep(
1097 : 13386 : constEquality, ProofRule::MACRO_SR_PRED_INTRO, {}, {constEquality});
1098 : : // build congruence conclusion (= (f t1 ... tn) (f c1 ... cn))
1099 : 26772 : Node congConclusion = d_node[0].eqNode(constApp);
1100 [ + - ]: 26772 : Trace("eqproof-conv") << "EqProof::addToProof: adding " << rule
1101 : 0 : << " step for " << congConclusion << " from "
1102 : 13386 : << subChildren << "\n";
1103 : 13386 : p->addStep(congConclusion, rule, {subChildren}, cargs, true);
1104 [ + - ]: 26772 : Trace("eqproof-conv") << "EqProof::addToProof: adding " << ProofRule::TRANS
1105 : 13386 : << " step for original conclusion " << d_node << "\n";
1106 : 66930 : std::vector<Node> transitivityChildren{congConclusion, constEquality};
1107 : 13386 : p->addStep(d_node, ProofRule::TRANS, {transitivityChildren}, {});
1108 : 13386 : visited[d_node] = d_node;
1109 : 13386 : return d_node;
1110 : : }
1111 : : // Transtivity and disequality reasoning steps
1112 [ + + ]: 1258120 : if (d_id == MERGED_THROUGH_TRANS)
1113 : : {
1114 : 1210420 : Assert(d_node.getKind() == Kind::EQUAL
1115 : : || (d_node.getKind() == Kind::NOT
1116 : : && d_node[0].getKind() == Kind::EQUAL))
1117 [ - + ][ - + ]: 605208 : << "EqProof::addToProof: transitivity step conclusion " << d_node
[ - - ]
1118 : 0 : << " is not equality or negated equality\n";
1119 : : // If conclusion is (not (= t1 t2)) change it to (= (= t1 t2) false), which
1120 : : // is the correct conclusion of the equality reasoning step. A FALSE_ELIM
1121 : : // step to revert this is only necessary when this is the root. That step is
1122 : : // done in the non-recursive caller of this function.
1123 : : Node conclusion =
1124 : 605208 : d_node.getKind() != Kind::NOT
1125 : 600995 : ? d_node
1126 : 1214630 : : d_node[0].eqNode(NodeManager::currentNM()->mkConst<bool>(false));
1127 : : // If the conclusion is an assumption, its derivation was spurious, so it
1128 : : // can be discarded. Moreover, reconstructing the step may lead to cyclic
1129 : : // proofs, so we *must* cut here.
1130 [ - + ]: 605208 : if (assumptions.count(conclusion))
1131 : : {
1132 : 0 : visited[d_node] = conclusion;
1133 : 0 : return conclusion;
1134 : : }
1135 : : // Process premises recursively
1136 : 1210420 : std::vector<Node> children;
1137 [ + + ]: 2388540 : for (unsigned i = 0, size = d_children.size(); i < size; ++i)
1138 : : {
1139 : : // If one of the steps is a "fake congruence" one, marked by a null
1140 : : // conclusion, it must deleted. Its premises are moved down to premises of
1141 : : // the transitivity step.
1142 : 1783340 : EqProof* childProof = d_children[i].get();
1143 : 3566670 : if (childProof->d_id == MERGED_THROUGH_CONGRUENCE
1144 [ + + ][ + + ]: 1783340 : && childProof->d_node.isNull())
[ + + ]
1145 : : {
1146 [ + - ]: 18562 : Trace("eqproof-conv") << "EqProof::addToProof: child proof " << i
1147 : 9281 : << " is fake cong step. Fold it.\n";
1148 [ - + ][ - + ]: 9281 : Assert(childProof->d_children.size() == 2);
[ - - ]
1149 [ + - ]: 9281 : Trace("eqproof-conv") << push;
1150 [ + + ]: 27843 : for (unsigned j = 0, sizeJ = childProof->d_children.size(); j < sizeJ;
1151 : : ++j)
1152 : : {
1153 [ + - ]: 37124 : Trace("eqproof-conv")
1154 : 0 : << "EqProof::addToProof: recurse on child " << j << "\n"
1155 : 18562 : << push;
1156 : 18562 : children.push_back(
1157 : 37124 : childProof->d_children[j]->addToProof(p, visited, assumptions));
1158 [ + - ]: 18562 : Trace("eqproof-conv") << pop;
1159 : : }
1160 [ + - ]: 9281 : Trace("eqproof-conv") << pop;
1161 : 9281 : continue;
1162 : : }
1163 [ + - ]: 3548110 : Trace("eqproof-conv")
1164 : 0 : << "EqProof::addToProof: recurse on child " << i << "\n"
1165 : 1774060 : << push;
1166 : 1774060 : children.push_back(childProof->addToProof(p, visited, assumptions));
1167 [ + - ]: 1774060 : Trace("eqproof-conv") << pop;
1168 : : }
1169 : : // Eliminate spurious premises. Reasoning below assumes no refl steps.
1170 : 605208 : cleanReflPremises(children);
1171 : : // If any premise is of the form (= (t1 t2) false), then the transitivity
1172 : : // step may be coarse-grained and needs to be expanded. If the expansion
1173 : : // happens it also finalizes the proof of conclusion.
1174 [ + + ]: 605208 : if (!expandTransitivityForDisequalities(
1175 : : conclusion, children, p, assumptions))
1176 : : {
1177 [ - + ][ - + ]: 582675 : Assert(!children.empty());
[ - - ]
1178 : : // similarly, if a disequality is concluded because of theory reasoning,
1179 : : // the step is coarse-grained and needs to be expanded, in which case the
1180 : : // proof is finalized in the call
1181 [ + + ]: 582675 : if (!expandTransitivityForTheoryDisequalities(conclusion, children, p))
1182 : : {
1183 [ + - ]: 1165330 : Trace("eqproof-conv")
1184 : 0 : << "EqProof::addToProof: build chain for transitivity premises"
1185 : 582665 : << children << " to conclude " << conclusion << "\n";
1186 : : // Build ordered transitivity chain from children to derive the
1187 : : // conclusion
1188 : 582665 : buildTransitivityChain(conclusion, children);
1189 : 582708 : Assert(
1190 : : children.size() > 1
1191 : : || (!children.empty()
1192 : : && (children[0] == conclusion
1193 : : || children[0][1].eqNode(children[0][0]) == conclusion)));
1194 : : // Only add transitivity step if there is more than one premise in the
1195 : : // chain. Otherwise the premise will be the conclusion itself and it'll
1196 : : // already have had a step added to it when the premises were
1197 : : // recursively processed.
1198 [ + + ]: 582665 : if (children.size() > 1)
1199 : : {
1200 : 582622 : p->addStep(conclusion, ProofRule::TRANS, children, {}, true);
1201 : : }
1202 : : }
1203 : : }
1204 : 1210420 : Assert(p->hasStep(conclusion) || assumptions.count(conclusion))
1205 [ - + ][ - + ]: 605208 : << "Conclusion " << conclusion
[ - - ]
1206 : 0 : << " does not have a step in the proof neither it's an assumption.\n";
1207 : 605208 : visited[d_node] = conclusion;
1208 : 605208 : return conclusion;
1209 : : }
1210 [ - + ][ - + ]: 652914 : Assert(d_id == MERGED_THROUGH_CONGRUENCE);
[ - - ]
1211 : : // The processing below is mainly dedicated to flattening congruence steps
1212 : : // (since EqProof assumes currying) and to prossibly reconstructing the
1213 : : // conclusion in case it involves n-ary steps.
1214 [ - + ][ - - ]: 652914 : Assert(d_node.getKind() == Kind::EQUAL)
1215 [ - + ][ - + ]: 652914 : << "EqProof::addToProof: conclusion " << d_node << " is not equality\n";
[ - - ]
1216 : : // The given conclusion is taken as ground truth. If the premises do not
1217 : : // align, for example with (= (f t1) (f t2)) but a premise being (= t2 t1), we
1218 : : // use (= t1 t2) as a premise and rely on a symmetry step to justify it.
1219 : 652914 : unsigned arity = d_node[0].getNumChildren();
1220 : 652914 : Kind k = d_node[0].getKind();
1221 : 652914 : bool isNary = NodeManager::isNAryKind(k);
1222 : :
1223 : : // N-ary operators are fun. The following proof is a valid EqProof
1224 : : //
1225 : : // (= (f t1 t2 t3) (f t6 t5)) (= (f t6 t5) (f t5 t6))
1226 : : // -------------------------------------------------- TRANS
1227 : : // (= (f t1 t2 t3) (f t5 t6)) (= t4 t7)
1228 : : // ------------------------------------------------------------ CONG
1229 : : // (= (f t1 t2 t3 t4) (f t5 t6 t7))
1230 : : //
1231 : : // We modify the above proof to conclude
1232 : : //
1233 : : // (= (f (f t1 t2 t3) t4) (f (f t5 t6) t7))
1234 : : //
1235 : : // which is a valid congruence conclusion (applications of f with the same
1236 : : // arity). For the processing below to be// performed correctly we update
1237 : : // arity to be maximal one among the two applications (4 in the above
1238 : : // example).
1239 [ - + ]: 652914 : if (d_node[0].getNumChildren() != d_node[1].getNumChildren())
1240 : : {
1241 : 0 : Assert(isNary) << "We only handle congruences of apps with different "
1242 : 0 : "number of children for theory n-ary operators";
1243 : 0 : arity =
1244 : 0 : d_node[1].getNumChildren() < arity ? arity : d_node[1].getNumChildren();
1245 [ - - ]: 0 : Trace("eqproof-conv")
1246 : 0 : << "EqProof::addToProof: Mismatching arities in cong conclusion "
1247 : 0 : << d_node << ". Use tentative arity " << arity << "\n";
1248 : : }
1249 : : // For a congruence proof of (= (f a0 ... an-1) (g b0 ... bn-1)), build a
1250 : : // transitivity matrix of n rows where the first row contains a transitivity
1251 : : // chain justifying (= f g) and the next rows (= ai bi)
1252 : 1305830 : std::vector<std::vector<Node>> transitivityChildren;
1253 [ + + ]: 2379330 : for (unsigned i = 0; i < arity + 1; ++i)
1254 : : {
1255 : 1726420 : transitivityChildren.push_back(std::vector<Node>());
1256 : : }
1257 : 652914 : reduceNestedCongruence(
1258 : 652914 : arity, d_node, transitivityChildren, p, visited, assumptions, isNary);
1259 : : // Congruences over n-ary operators may require changing the conclusion (as in
1260 : : // the above example). This is handled in a general manner below according to
1261 : : // whether the transitivity matrix computed by reduceNestedCongruence contains
1262 : : // empty rows
1263 : 1305830 : Node conclusion = d_node;
1264 : 652914 : NodeManager* nm = NodeManager::currentNM();
1265 [ + + ]: 652914 : if (isNary)
1266 : : {
1267 : 577863 : unsigned emptyRows = 0;
1268 [ + + ]: 1551540 : for (unsigned i = 1; i <= arity; ++i)
1269 : : {
1270 [ + + ]: 973679 : if (transitivityChildren[i].empty())
1271 : : {
1272 : 58 : emptyRows++;
1273 : : }
1274 : : }
1275 : : // Given two n-ary applications f1:(f a0 ... an-1), f2:(f b0 ... bm-1), of
1276 : : // arities n and m, arity = max(n,m), the number emptyRows establishes the
1277 : : // sizes of the prefixes of f1 of f2 that have been equated via a
1278 : : // transitivity step. The prefixes necessarily have different sizes. The
1279 : : // suffixes have the same sizes. The new conclusion will be of the form
1280 : : // (= (f (f a0 ... ak1) ... an-1) (f (f b0 ... bk2) ... bm-1))
1281 : : // where
1282 : : // k1 = emptyRows + 1 - (arity - n)
1283 : : // k2 = emptyRows + 1 - (arity - m)
1284 : : // k1 != k2
1285 : : // n - k1 == m - k2
1286 : : // Note that by construction the equality between the first emptyRows + 1
1287 : : // arguments of each application is justified by the transitivity step in
1288 : : // the row emptyRows + 1 in the matrix.
1289 : : //
1290 : : // All of the above is with the very first row in the matrix, reserved for
1291 : : // justifying the equality between the functions, which is not necessary in
1292 : : // the n-ary case, notwithstanding.
1293 [ + + ]: 577863 : if (emptyRows > 0)
1294 : : {
1295 [ + - ]: 116 : Trace("eqproof-conv")
1296 : 0 : << "EqProof::addToProof: Found " << emptyRows
1297 : 58 : << " empty rows. Rebuild conclusion " << d_node << "\n";
1298 : : // New transitivity matrix is as before except that the empty rows in the
1299 : : // beginning are eliminated, as the new arity is the maximal arity among
1300 : : // the applications minus the number of empty rows.
1301 : : std::vector<std::vector<Node>> newTransitivityChildren{
1302 : 58 : transitivityChildren.begin() + 1 + emptyRows,
1303 : 174 : transitivityChildren.end()};
1304 : 58 : transitivityChildren.clear();
1305 : 58 : transitivityChildren.push_back(std::vector<Node>());
1306 : 58 : transitivityChildren.insert(transitivityChildren.end(),
1307 : : newTransitivityChildren.begin(),
1308 : 116 : newTransitivityChildren.end());
1309 : : unsigned arityPrefix1 =
1310 : 58 : emptyRows + 1 - (arity - d_node[0].getNumChildren());
1311 [ - + ][ - - ]: 116 : Assert(arityPrefix1 < d_node[0].getNumChildren())
1312 : 0 : << "arityPrefix1 " << arityPrefix1 << " not smaller than "
1313 : 58 : << d_node[0] << "'s arity " << d_node[0].getNumChildren() << "\n";
1314 : : unsigned arityPrefix2 =
1315 : 58 : emptyRows + 1 - (arity - d_node[1].getNumChildren());
1316 [ - + ][ - - ]: 116 : Assert(arityPrefix2 < d_node[1].getNumChildren())
1317 : 0 : << "arityPrefix2 " << arityPrefix2 << " not smaller than "
1318 : 58 : << d_node[1] << "'s arity " << d_node[1].getNumChildren() << "\n";
1319 [ + - ]: 116 : Trace("eqproof-conv") << "EqProof::addToProof: New internal "
1320 : 0 : "applications with arities "
1321 : 58 : << arityPrefix1 << ", " << arityPrefix2 << ":\n";
1322 : : std::vector<Node> childrenPrefix1{d_node[0].begin(),
1323 : 174 : d_node[0].begin() + arityPrefix1};
1324 : : std::vector<Node> childrenPrefix2{d_node[1].begin(),
1325 : 174 : d_node[1].begin() + arityPrefix2};
1326 : 116 : Node newFirstChild1 = nm->mkNode(k, childrenPrefix1);
1327 : 116 : Node newFirstChild2 = nm->mkNode(k, childrenPrefix2);
1328 [ + - ]: 116 : Trace("eqproof-conv")
1329 : 58 : << "EqProof::addToProof:\t " << newFirstChild1 << "\n";
1330 [ + - ]: 116 : Trace("eqproof-conv")
1331 : 58 : << "EqProof::addToProof:\t " << newFirstChild2 << "\n";
1332 : 232 : std::vector<Node> newChildren1{newFirstChild1};
1333 : 58 : newChildren1.insert(newChildren1.end(),
1334 : 58 : d_node[0].begin() + arityPrefix1,
1335 : 174 : d_node[0].end());
1336 : 174 : std::vector<Node> newChildren2{newFirstChild2};
1337 : 58 : newChildren2.insert(newChildren2.end(),
1338 : 58 : d_node[1].begin() + arityPrefix2,
1339 : 174 : d_node[1].end());
1340 : 174 : conclusion = nm->mkNode(Kind::EQUAL,
1341 : 116 : nm->mkNode(k, newChildren1),
1342 : 174 : nm->mkNode(k, newChildren2));
1343 : : // update arity
1344 [ - + ][ - + ]: 58 : Assert((arity - emptyRows) == conclusion[0].getNumChildren());
[ - - ]
1345 : 58 : arity = arity - emptyRows;
1346 [ + - ]: 116 : Trace("eqproof-conv")
1347 : 58 : << "EqProof::addToProof: New conclusion " << conclusion << "\n";
1348 : : }
1349 : : }
1350 [ - + ]: 652914 : if (TraceIsOn("eqproof-conv"))
1351 : : {
1352 [ - - ]: 0 : Trace("eqproof-conv")
1353 : 0 : << "EqProof::addToProof: premises from reduced cong of " << conclusion
1354 : 0 : << ":\n";
1355 [ - - ]: 0 : for (unsigned i = 0; i <= arity; ++i)
1356 : : {
1357 [ - - ]: 0 : Trace("eqproof-conv") << "EqProof::addToProof:\t" << i
1358 : 0 : << "-th arg: " << transitivityChildren[i] << "\n";
1359 : : }
1360 : : }
1361 : 1305830 : std::vector<Node> children(arity + 1);
1362 : : // Process transitivity matrix to (possibly) generate transitivity steps for
1363 : : // congruence premises (= ai bi)
1364 [ + + ]: 2379280 : for (unsigned i = 0; i <= arity; ++i)
1365 : : {
1366 : 1726360 : Node transConclusion;
1367 : : // We special case the operator case because there is only ever the need to
1368 : : // do something when in some HO case
1369 [ + + ]: 1726360 : if (i == 0)
1370 : : {
1371 : : // no justification for equality between functions, skip
1372 [ + + ]: 652914 : if (transitivityChildren[0].empty())
1373 : : {
1374 : 652660 : continue;
1375 : : }
1376 : : // HO case
1377 [ - + ][ - + ]: 254 : Assert(k == Kind::APPLY_UF) << "Congruence with different functions only "
[ - - ]
1378 : 0 : "allowed for uninterpreted functions.\n";
1379 : : transConclusion =
1380 : 254 : conclusion[0].getOperator().eqNode(conclusion[1].getOperator());
1381 : : }
1382 : : else
1383 : : {
1384 : 1073450 : transConclusion = conclusion[0][i - 1].eqNode(conclusion[1][i - 1]);
1385 : : }
1386 : 1073700 : children[i] = transConclusion;
1387 [ - + ][ - - ]: 1073700 : Assert(!transitivityChildren[i].empty())
1388 : 0 : << "EqProof::addToProof: did not add any justification for " << i
1389 [ - + ][ - + ]: 1073700 : << "-th arg of congruence " << conclusion << "\n";
[ - - ]
1390 : : // If the transitivity conclusion is a reflexivity step, just add it. Note
1391 : : // that this can happen even with the respective transitivityChildren row
1392 : : // containing several equalities in the case of (= ai bi) being the same
1393 : : // n-ary application that was justified by a congruence step, which can
1394 : : // happen in the current equality engine.
1395 [ + + ]: 1073700 : if (transConclusion[0] == transConclusion[1])
1396 : : {
1397 : 490738 : p->addStep(transConclusion, ProofRule::REFL, {}, {transConclusion[0]});
1398 : 245369 : continue;
1399 : : }
1400 : : // Remove spurious refl steps from the premises for (= ai bi)
1401 : 828333 : cleanReflPremises(transitivityChildren[i]);
1402 : 1656670 : Assert(transitivityChildren[i].size() > 1 || transitivityChildren[i].empty()
1403 : : || CDProof::isSame(transitivityChildren[i][0], transConclusion))
1404 : 0 : << "EqProof::addToProof: premises " << transitivityChildren[i] << "for "
1405 [ - + ][ - + ]: 828333 : << i << "-th cong premise " << transConclusion << " don't justify it\n";
[ - - ]
1406 : 828333 : unsigned sizeTrans = transitivityChildren[i].size();
1407 : : // If no transitivity premise left or if (= ai bi) is an assumption (which
1408 : : // might lead to a cycle with a transtivity step), nothing else to do.
1409 [ + - ][ + + ]: 828333 : if (sizeTrans == 0 || assumptions.count(transConclusion) > 0)
[ + + ]
1410 : : {
1411 : 411321 : continue;
1412 : : }
1413 : : // If the transitivity conclusion, or its symmetric, occurs in the
1414 : : // transitivity premises, nothing to do, as it is already justified and
1415 : : // doing so again would lead to a cycle.
1416 : 417012 : bool occurs = false;
1417 [ + + ][ + + ]: 865570 : for (unsigned j = 0; j < sizeTrans && !occurs; ++j)
1418 : : {
1419 [ + + ]: 448558 : if (CDProof::isSame(transitivityChildren[i][j], transConclusion))
1420 : : {
1421 : 389475 : occurs = true;
1422 : : }
1423 : : }
1424 [ + + ]: 417012 : if (!occurs)
1425 : : {
1426 : : // Build transitivity step
1427 : 27537 : buildTransitivityChain(transConclusion, transitivityChildren[i]);
1428 [ + - ]: 55074 : Trace("eqproof-conv")
1429 : 0 : << "EqProof::addToProof: adding trans step for cong premise "
1430 : 0 : << transConclusion << " with children " << transitivityChildren[i]
1431 : 27537 : << "\n";
1432 : 55074 : p->addStep(
1433 : 27537 : transConclusion, ProofRule::TRANS, transitivityChildren[i], {}, true);
1434 : : }
1435 : : }
1436 : : // first-order case
1437 [ + + ]: 652914 : if (children[0].isNull())
1438 : : {
1439 : : // remove placehold for function equality case
1440 : 652660 : children.erase(children.begin());
1441 : : // Get node of the function operator over which congruence is being
1442 : : // applied.
1443 : 652660 : std::vector<Node> args;
1444 : 652660 : ProofRule r = expr::getCongRule(d_node[0], args);
1445 : : // Add congruence step
1446 [ - + ]: 652660 : if (TraceIsOn("eqproof-conv"))
1447 : : {
1448 [ - - ]: 0 : Trace("eqproof-conv")
1449 : 0 : << "EqProof::addToProof: build cong step of " << conclusion;
1450 [ - - ]: 0 : if (!args.empty())
1451 : : {
1452 [ - - ]: 0 : Trace("eqproof-conv") << " with op " << args[0];
1453 : : }
1454 [ - - ]: 0 : Trace("eqproof-conv") << " and children " << children << "\n";
1455 : : }
1456 : 652660 : p->addStep(conclusion, r, children, args, true);
1457 : : }
1458 : : // higher-order case
1459 : : else
1460 : : {
1461 : : // Add congruence step
1462 [ + - ]: 508 : Trace("eqproof-conv") << "EqProof::addToProof: build HO-cong step of "
1463 : 0 : << conclusion << " with children " << children
1464 : 254 : << "\n";
1465 : 508 : p->addStep(conclusion,
1466 : : ProofRule::HO_CONG,
1467 : : children,
1468 : : {ProofRuleChecker::mkKindNode(Kind::APPLY_UF)},
1469 : 254 : true);
1470 : : }
1471 : : // If the conclusion of the congruence step changed due to the n-ary handling,
1472 : : // we obtained for example (= (f (f t1 t2 t3) t4) (f (f t5 t6) t7)), which is
1473 : : // flattened into the original conclusion (= (f t1 t2 t3 t4) (f t5 t6 t7)) via
1474 : : // rewriting
1475 [ + + ]: 652914 : if (!CDProof::isSame(conclusion, d_node))
1476 : : {
1477 [ + - ]: 116 : Trace("eqproof-conv") << "EqProof::addToProof: try to flatten via a"
1478 : 58 : << ProofRule::MACRO_SR_PRED_TRANSFORM
1479 : 0 : << " step the rebuilt conclusion " << conclusion
1480 : 58 : << " into " << d_node << "\n";
1481 : : Node res = p->getManager()->getChecker()->checkDebug(
1482 : : ProofRule::MACRO_SR_PRED_TRANSFORM,
1483 : : {conclusion},
1484 : 58 : {d_node},
1485 : 0 : Node::null(),
1486 : 406 : "eqproof-conv");
1487 : : // If rewriting was not able to flatten the rebuilt conclusion into the
1488 : : // original one, we give up and use a TRUST_FLATTENING_REWRITE step,
1489 : : // generating a proof for the original conclusion d_node such as
1490 : : //
1491 : : // Converted EqProof
1492 : : // ---------------------- ------------------- TRUST_FLATTENING_REWRITE
1493 : : // conclusion conclusion = d_node
1494 : : // ------------------------------------------------------- EQ_RESOLVE
1495 : : // d_node
1496 : : //
1497 : : //
1498 : : // If rewriting was able to do it, however, we just add the macro step.
1499 [ + + ]: 58 : if (res.isNull())
1500 : : {
1501 [ + - ]: 30 : Trace("eqproof-conv")
1502 : 15 : << "EqProof::addToProof: adding a trust flattening rewrite step\n";
1503 : 15 : Node bridgeEq = conclusion.eqNode(d_node);
1504 : 15 : p->addTrustedStep(bridgeEq, TrustId::FLATTENING_REWRITE, {}, {});
1505 [ + + ][ - - ]: 45 : p->addStep(d_node, ProofRule::EQ_RESOLVE, {conclusion, bridgeEq}, {});
1506 : : }
1507 : : else
1508 : : {
1509 : 129 : p->addStep(d_node,
1510 : : ProofRule::MACRO_SR_PRED_TRANSFORM,
1511 : : {conclusion},
1512 : 43 : {d_node},
1513 : 86 : true);
1514 : : }
1515 : : }
1516 : 652914 : visited[d_node] = d_node;
1517 : 652914 : return d_node;
1518 : : }
1519 : :
1520 : : } // namespace eq
1521 : : } // Namespace theory
1522 : : } // namespace cvc5::internal
|
