GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/uf/eq_proof.cpp Lines: 560 717 78.1 %
Date: 2021-03-23 Branches: 1345 3784 35.5 %

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