GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/uf/proof_equality_engine.cpp Lines: 182 262 69.5 %
Date: 2021-03-23 Branches: 411 1314 31.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_equality_engine.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Gereon Kremer
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 the proof-producing equality engine
13
 **/
14
15
#include "theory/uf/proof_equality_engine.h"
16
17
#include "expr/lazy_proof_chain.h"
18
#include "expr/proof_node.h"
19
#include "expr/proof_node_manager.h"
20
#include "theory/rewriter.h"
21
#include "theory/uf/eq_proof.h"
22
#include "theory/uf/equality_engine.h"
23
#include "theory/uf/proof_checker.h"
24
25
using namespace CVC4::kind;
26
27
namespace CVC4 {
28
namespace theory {
29
namespace eq {
30
31
7165
ProofEqEngine::ProofEqEngine(context::Context* c,
32
                             context::UserContext* u,
33
                             EqualityEngine& ee,
34
7165
                             ProofNodeManager* pnm)
35
14330
    : EagerProofGenerator(pnm, u, "pfee::" + ee.identify()),
36
      d_ee(ee),
37
      d_factPg(c, pnm),
38
      d_pnm(pnm),
39
14330
      d_proof(pnm, nullptr, c, "pfee::LazyCDProof::" + ee.identify()),
40
35825
      d_keep(c)
41
{
42
7165
  NodeManager* nm = NodeManager::currentNM();
43
7165
  d_true = nm->mkConst(true);
44
7165
  d_false = nm->mkConst(false);
45
7165
  AlwaysAssert(pnm != nullptr)
46
      << "Should not construct ProofEqEngine without proof node manager";
47
7165
}
48
49
bool ProofEqEngine::assertFact(Node lit,
50
                               PfRule id,
51
                               const std::vector<Node>& exp,
52
                               const std::vector<Node>& args)
53
{
54
  Trace("pfee") << "pfee::assertFact " << lit << " " << id << ", exp = " << exp
55
                << ", args = " << args << std::endl;
56
57
  Node atom = lit.getKind() == NOT ? lit[0] : lit;
58
  bool polarity = lit.getKind() != NOT;
59
  // register the step in the proof
60
  if (holds(atom, polarity))
61
  {
62
    // we do not process this fact if it already holds
63
    return false;
64
  }
65
  // Buffer the step in the fact proof generator. We do this instead of
66
  // adding explict steps to the lazy proof d_proof since CDProof has
67
  // (at most) one proof for each formula. Thus, we "claim" only the
68
  // formula that is proved by this fact. Otherwise, aliasing may occur,
69
  // which leads to cyclic or bogus proofs.
70
  ProofStep ps;
71
  ps.d_rule = id;
72
  ps.d_children = exp;
73
  ps.d_args = args;
74
  d_factPg.addStep(lit, ps);
75
  // add lazy step to proof
76
  d_proof.addLazyStep(lit, &d_factPg);
77
  // second, assert it to the equality engine
78
  Node reason = NodeManager::currentNM()->mkAnd(exp);
79
  return assertFactInternal(atom, polarity, reason);
80
}
81
82
1391
bool ProofEqEngine::assertFact(Node lit,
83
                               PfRule id,
84
                               Node exp,
85
                               const std::vector<Node>& args)
86
{
87
2782
  Trace("pfee") << "pfee::assertFact " << lit << " " << id << ", exp = " << exp
88
1391
                << ", args = " << args << std::endl;
89
2782
  Node atom = lit.getKind() == NOT ? lit[0] : lit;
90
1391
  bool polarity = lit.getKind() != NOT;
91
  // register the step in the proof
92
1391
  if (holds(atom, polarity))
93
  {
94
    // we do not process this fact if it already holds
95
81
    return false;
96
  }
97
  // must extract the explanation as a vector
98
2620
  std::vector<Node> expv;
99
  // Flatten (single occurrences) of AND. We do not allow nested AND, it is
100
  // the responsibilty of the caller to ensure these do not occur.
101
1310
  if (exp != d_true)
102
  {
103
837
    if (exp.getKind() == AND)
104
    {
105
      for (const Node& expc : exp)
106
      {
107
        // should not have doubly nested AND
108
        Assert(expc.getKind() != AND);
109
        expv.push_back(expc);
110
      }
111
    }
112
    else
113
    {
114
837
      expv.push_back(exp);
115
    }
116
  }
117
  // buffer the step in the fact proof generator
118
2620
  ProofStep ps;
119
1310
  ps.d_rule = id;
120
1310
  ps.d_children = expv;
121
1310
  ps.d_args = args;
122
1310
  d_factPg.addStep(lit, ps);
123
  // add lazy step to proof
124
1310
  d_proof.addLazyStep(lit, &d_factPg);
125
  // second, assert it to the equality engine
126
1310
  return assertFactInternal(atom, polarity, exp);
127
}
128
129
bool ProofEqEngine::assertFact(Node lit, Node exp, ProofStepBuffer& psb)
130
{
131
  Trace("pfee") << "pfee::assertFact " << lit << ", exp = " << exp
132
                << " via buffer with " << psb.getNumSteps() << " steps"
133
                << std::endl;
134
  Node atom = lit.getKind() == NOT ? lit[0] : lit;
135
  bool polarity = lit.getKind() != NOT;
136
  if (holds(atom, polarity))
137
  {
138
    // we do not process this fact if it already holds
139
    return false;
140
  }
141
  // buffer the steps in the fact proof generator
142
  const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
143
  for (const std::pair<Node, ProofStep>& step : steps)
144
  {
145
    d_factPg.addStep(step.first, step.second);
146
  }
147
  // add lazy step to proof
148
  d_proof.addLazyStep(lit, &d_factPg);
149
  // second, assert it to the equality engine
150
  return assertFactInternal(atom, polarity, exp);
151
}
152
153
97982
bool ProofEqEngine::assertFact(Node lit, Node exp, ProofGenerator* pg)
154
{
155
195964
  Trace("pfee") << "pfee::assertFact " << lit << ", exp = " << exp
156
97982
                << " via generator" << std::endl;
157
195964
  Node atom = lit.getKind() == NOT ? lit[0] : lit;
158
97982
  bool polarity = lit.getKind() != NOT;
159
97982
  if (holds(atom, polarity))
160
  {
161
    // we do not process this fact if it already holds
162
32915
    return false;
163
  }
164
  // note the proof generator is responsible for remembering the explanation
165
65067
  d_proof.addLazyStep(lit, pg);
166
  // second, assert it to the equality engine
167
65067
  return assertFactInternal(atom, polarity, exp);
168
}
169
170
3167
TrustNode ProofEqEngine::assertConflict(Node lit)
171
{
172
3167
  Trace("pfee") << "pfee::assertConflict " << lit << std::endl;
173
6334
  std::vector<TNode> assumps;
174
3167
  explainWithProof(lit, assumps, &d_proof);
175
  // lit may not be equivalent to false, but should rewrite to false
176
3167
  if (lit != d_false)
177
  {
178
3167
    Assert(Rewriter::rewrite(lit) == d_false)
179
        << "pfee::assertConflict: conflict literal is not rewritable to "
180
           "false";
181
6334
    std::vector<Node> exp;
182
3167
    exp.push_back(lit);
183
6334
    std::vector<Node> args;
184
3167
    if (!d_proof.addStep(d_false, PfRule::MACRO_SR_PRED_ELIM, exp, args))
185
    {
186
      Assert(false) << "pfee::assertConflict: failed conflict step";
187
      return TrustNode::null();
188
    }
189
  }
190
  return ensureProofForFact(
191
3167
      d_false, assumps, TrustNodeKind::CONFLICT, &d_proof);
192
}
193
194
TrustNode ProofEqEngine::assertConflict(PfRule id,
195
                                        const std::vector<Node>& exp,
196
                                        const std::vector<Node>& args)
197
{
198
  Trace("pfee") << "pfee::assertConflict " << id << ", exp = " << exp
199
                << ", args = " << args << std::endl;
200
  // conflict is same as lemma concluding false
201
  return assertLemma(d_false, id, exp, {}, args);
202
}
203
204
931
TrustNode ProofEqEngine::assertConflict(const std::vector<Node>& exp,
205
                                        ProofGenerator* pg)
206
{
207
931
  Assert(pg != nullptr);
208
1862
  Trace("pfee") << "pfee::assertConflict " << exp << " via generator"
209
931
                << std::endl;
210
931
  return assertLemma(d_false, exp, {}, pg);
211
}
212
213
TrustNode ProofEqEngine::assertLemma(Node conc,
214
                                     PfRule id,
215
                                     const std::vector<Node>& exp,
216
                                     const std::vector<Node>& noExplain,
217
                                     const std::vector<Node>& args)
218
{
219
  Trace("pfee") << "pfee::assertLemma " << conc << " " << id
220
                << ", exp = " << exp << ", noExplain = " << noExplain
221
                << ", args = " << args << std::endl;
222
  Assert(conc != d_true);
223
  LazyCDProof tmpProof(d_pnm, &d_proof);
224
  LazyCDProof* curr;
225
  TrustNodeKind tnk;
226
  // same policy as above: for conflicts, use existing lazy proof
227
  if (conc == d_false)
228
  {
229
    curr = &d_proof;
230
    tnk = TrustNodeKind::CONFLICT;
231
  }
232
  else
233
  {
234
    curr = &tmpProof;
235
    tnk = TrustNodeKind::LEMMA;
236
  }
237
  // explain each literal in the vector
238
  std::vector<TNode> assumps;
239
  explainVecWithProof(tnk, assumps, exp, noExplain, curr);
240
  // Register the proof step. We use a separate lazy CDProof which will make
241
  // calls to curr above for the proofs of the literals in exp.
242
  LazyCDProof outer(d_pnm, curr);
243
  if (!outer.addStep(conc, id, exp, args))
244
  {
245
    // a step went wrong, e.g. during checking
246
    Assert(false) << "pfee::assertConflict: register proof step";
247
    return TrustNode::null();
248
  }
249
  // Now get the proof for conc.
250
  return ensureProofForFact(conc, assumps, tnk, &outer);
251
}
252
253
1734
TrustNode ProofEqEngine::assertLemma(Node conc,
254
                                     const std::vector<Node>& exp,
255
                                     const std::vector<Node>& noExplain,
256
                                     ProofGenerator* pg)
257
{
258
1734
  Assert(pg != nullptr);
259
3468
  Trace("pfee") << "pfee::assertLemma " << conc << ", exp = " << exp
260
1734
                << ", noExplain = " << noExplain << " via generator"
261
1734
                << std::endl;
262
3468
  LazyCDProof tmpProof(d_pnm, &d_proof);
263
  LazyCDProof* curr;
264
  TrustNodeKind tnk;
265
  // same policy as above: for conflicts, use existing lazy proof
266
1734
  if (conc == d_false)
267
  {
268
934
    curr = &d_proof;
269
934
    tnk = TrustNodeKind::CONFLICT;
270
  }
271
  else
272
  {
273
800
    curr = &tmpProof;
274
800
    tnk = TrustNodeKind::LEMMA;
275
  }
276
  // explain each literal in the vector
277
3468
  std::vector<TNode> assumps;
278
1734
  explainVecWithProof(tnk, assumps, exp, noExplain, curr);
279
  // We use a lazy proof chain here. The provided proof generator sets up the
280
  // "skeleton" that is the base of the proof we are constructing. The call to
281
  // LazyCDProofChain::getProofFor will expand the leaves of this proof via
282
  // calls to curr.
283
3468
  LazyCDProofChain outer(d_pnm, true, nullptr, curr, false);
284
1734
  outer.addLazyStep(conc, pg);
285
3468
  return ensureProofForFact(conc, assumps, tnk, &outer);
286
}
287
288
69799
TrustNode ProofEqEngine::explain(Node conc)
289
{
290
69799
  Trace("pfee") << "pfee::explain " << conc << std::endl;
291
139598
  LazyCDProof tmpProof(d_pnm, &d_proof);
292
139598
  std::vector<TNode> assumps;
293
69799
  explainWithProof(conc, assumps, &tmpProof);
294
139598
  return ensureProofForFact(conc, assumps, TrustNodeKind::PROP_EXP, &tmpProof);
295
}
296
297
1734
void ProofEqEngine::explainVecWithProof(TrustNodeKind& tnk,
298
                                        std::vector<TNode>& assumps,
299
                                        const std::vector<Node>& exp,
300
                                        const std::vector<Node>& noExplain,
301
                                        LazyCDProof* curr)
302
{
303
3468
  std::vector<Node> expn;
304
4503
  for (const Node& e : exp)
305
  {
306
2769
    if (std::find(noExplain.begin(), noExplain.end(), e) == noExplain.end())
307
    {
308
2652
      explainWithProof(e, assumps, curr);
309
    }
310
    else
311
    {
312
      // it did not have a proof; it was an assumption of the previous rule
313
117
      assumps.push_back(e);
314
      // it is not a conflict, since it may involve new literals
315
117
      tnk = TrustNodeKind::LEMMA;
316
    }
317
  }
318
1734
}
319
320
74700
TrustNode ProofEqEngine::ensureProofForFact(Node conc,
321
                                            const std::vector<TNode>& assumps,
322
                                            TrustNodeKind tnk,
323
                                            ProofGenerator* curr)
324
{
325
74700
  Trace("pfee-proof") << std::endl;
326
149400
  Trace("pfee-proof") << "pfee::ensureProofForFact: input " << conc << " via "
327
74700
                      << assumps << ", TrustNodeKind=" << tnk << std::endl;
328
74700
  NodeManager* nm = NodeManager::currentNM();
329
  // The proof
330
149400
  std::shared_ptr<ProofNode> pf;
331
74700
  ProofGenerator* pfg = nullptr;
332
  // the explanation is the conjunction of assumptions
333
149400
  Node exp;
334
  // If proofs are enabled, generate the proof and possibly modify the
335
  // assumptions to match SCOPE.
336
74700
  Assert(curr != nullptr);
337
149400
  Trace("pfee-proof") << "pfee::ensureProofForFact: make proof for fact"
338
74700
                      << std::endl;
339
  // get the proof for conc
340
149400
  std::shared_ptr<ProofNode> pfBody = curr->getProofFor(conc);
341
74700
  if (pfBody == nullptr)
342
  {
343
    Trace("pfee-proof")
344
        << "pfee::ensureProofForFact: failed to make proof for fact"
345
        << std::endl
346
        << std::endl;
347
    // should have existed
348
    Assert(false) << "pfee::assertConflict: failed to get proof for " << conc;
349
    return TrustNode::null();
350
  }
351
  // clone it so that we have a fresh copy
352
74700
  pfBody = pfBody->clone();
353
74700
  Trace("pfee-proof") << "pfee::ensureProofForFact: add scope" << std::endl;
354
  // The free assumptions must be closed by assumps, which should be passed
355
  // as arguments of SCOPE. However, some of the free assumptions may not
356
  // literally be equal to assumps, for instance, due to symmetry. In other
357
  // words, the SCOPE could be closing (= x y) in a proof with free
358
  // assumption (= y x). We modify the proof leaves to account for this
359
  // below.
360
361
149400
  std::vector<Node> scopeAssumps;
362
  // we first ensure the assumptions are flattened
363
411748
  for (const TNode& a : assumps)
364
  {
365
337048
    if (a.getKind() == AND)
366
    {
367
1381
      scopeAssumps.insert(scopeAssumps.end(), a.begin(), a.end());
368
    }
369
    else
370
    {
371
335667
      scopeAssumps.push_back(a);
372
    }
373
  }
374
  // Scope the proof constructed above, and connect the formula with the proof
375
  // minimize the assumptions.
376
74700
  pf = d_pnm->mkScope(pfBody, scopeAssumps, true, true);
377
  // If we have no assumptions, and are proving an explanation for propagation
378
74700
  if (scopeAssumps.empty() && tnk == TrustNodeKind::PROP_EXP)
379
  {
380
    // Must add "true" as an explicit argument. This is to ensure that the
381
    // propagation F from true proves (=> true F) instead of F, since this is
382
    // the form required by TrustNodeKind::PROP_EXP. We do not ensure closed or
383
    // minimize here, since we already ensured the proof was closed above, and
384
    // we do not want to minimize, or else "true" would be omitted.
385
1617
    scopeAssumps.push_back(nm->mkConst(true));
386
1617
    pf = d_pnm->mkScope(pf, scopeAssumps, false);
387
  }
388
74700
  exp = nm->mkAnd(scopeAssumps);
389
  // Make the lemma or conflict node. This must exactly match the conclusion
390
  // of SCOPE below.
391
149400
  Node formula;
392
74700
  if (tnk == TrustNodeKind::CONFLICT)
393
  {
394
    // conflict is negated
395
4098
    Assert(conc == d_false);
396
4098
    formula = exp;
397
  }
398
  else
399
  {
400
70602
    formula =
401
70602
        exp == d_true
402
209887
            ? conc
403
68683
            : (conc == d_false ? exp.negate() : nm->mkNode(IMPLIES, exp, conc));
404
  }
405
149400
  Trace("pfee-proof") << "pfee::ensureProofForFact: formula is " << formula
406
74700
                      << std::endl;
407
  // should always be non-null
408
74700
  Assert(pf != nullptr);
409
74700
  if (Trace.isOn("pfee-proof") || Trace.isOn("pfee-proof-final"))
410
  {
411
    Trace("pfee-proof") << "pfee::ensureProofForFact: printing proof"
412
                        << std::endl;
413
    std::stringstream ss;
414
    pf->printDebug(ss);
415
    Trace("pfee-proof") << "pfee::ensureProofForFact: Proof is " << ss.str()
416
                        << std::endl;
417
  }
418
  // Should be a closed proof now. If it is not, then the overall proof
419
  // is malformed.
420
74700
  Assert(pf->isClosed());
421
74700
  pfg = this;
422
  // set the proof for the conflict or lemma, which can be queried later
423
74700
  switch (tnk)
424
  {
425
4098
    case TrustNodeKind::CONFLICT: setProofForConflict(formula, pf); break;
426
803
    case TrustNodeKind::LEMMA: setProofForLemma(formula, pf); break;
427
69799
    case TrustNodeKind::PROP_EXP: setProofForPropExp(conc, exp, pf); break;
428
    default:
429
      pfg = nullptr;
430
      Unhandled() << "Unhandled trust node kind " << tnk;
431
      break;
432
  }
433
149400
  Trace("pfee-proof") << "pfee::ensureProofForFact: finish" << std::endl
434
74700
                      << std::endl;
435
  // we can provide a proof for conflict, lemma or explained propagation
436
74700
  switch (tnk)
437
  {
438
4098
    case TrustNodeKind::CONFLICT:
439
4098
      return TrustNode::mkTrustConflict(formula, pfg);
440
803
    case TrustNodeKind::LEMMA: return TrustNode::mkTrustLemma(formula, pfg);
441
69799
    case TrustNodeKind::PROP_EXP:
442
69799
      return TrustNode::mkTrustPropExp(conc, exp, pfg);
443
    default: Unhandled() << "Unhandled trust node kind " << tnk; break;
444
  }
445
  return TrustNode::null();
446
}
447
448
66377
bool ProofEqEngine::assertFactInternal(TNode atom, bool polarity, TNode reason)
449
{
450
132754
  Trace("pfee-debug") << "pfee::assertFactInternal: " << atom << " " << polarity
451
66377
                      << " " << reason << std::endl;
452
  bool ret;
453
66377
  if (atom.getKind() == EQUAL)
454
  {
455
62849
    ret = d_ee.assertEquality(atom, polarity, reason);
456
  }
457
  else
458
  {
459
3528
    ret = d_ee.assertPredicate(atom, polarity, reason);
460
  }
461
66377
  if (ret)
462
  {
463
    // must reference count the new atom and explanation
464
66377
    d_keep.insert(atom);
465
66377
    d_keep.insert(reason);
466
  }
467
66377
  return ret;
468
}
469
470
99373
bool ProofEqEngine::holds(TNode atom, bool polarity)
471
{
472
99373
  if (atom.getKind() == EQUAL)
473
  {
474
95817
    if (!d_ee.hasTerm(atom[0]) || !d_ee.hasTerm(atom[1]))
475
    {
476
26754
      return false;
477
    }
478
196242
    return polarity ? d_ee.areEqual(atom[0], atom[1])
479
127179
                    : d_ee.areDisequal(atom[0], atom[1], false);
480
  }
481
3556
  if (!d_ee.hasTerm(atom))
482
  {
483
1989
    return false;
484
  }
485
3134
  TNode b = polarity ? d_true : d_false;
486
1567
  return d_ee.areEqual(atom, b);
487
}
488
489
75618
void ProofEqEngine::explainWithProof(Node lit,
490
                                     std::vector<TNode>& assumps,
491
                                     LazyCDProof* curr)
492
{
493
75618
  if (std::find(assumps.begin(), assumps.end(), lit) != assumps.end())
494
  {
495
8
    return;
496
  }
497
151228
  std::shared_ptr<eq::EqProof> pf = std::make_shared<eq::EqProof>();
498
75614
  Trace("pfee-proof") << "pfee::explainWithProof: " << lit << std::endl;
499
75614
  bool polarity = lit.getKind() != NOT;
500
151228
  TNode atom = polarity ? lit : lit[0];
501
75614
  Assert(atom.getKind() != AND);
502
151228
  std::vector<TNode> tassumps;
503
75614
  if (atom.getKind() == EQUAL)
504
  {
505
72194
    if (atom[0] == atom[1])
506
    {
507
      return;
508
    }
509
72194
    Assert(d_ee.hasTerm(atom[0]));
510
72194
    Assert(d_ee.hasTerm(atom[1]));
511
72194
    if (!polarity)
512
    {
513
      // ensure the explanation exists
514
4889
      AlwaysAssert(d_ee.areDisequal(atom[0], atom[1], true));
515
    }
516
72194
    d_ee.explainEquality(atom[0], atom[1], polarity, tassumps, pf.get());
517
  }
518
  else
519
  {
520
3420
    Assert(d_ee.hasTerm(atom));
521
3420
    d_ee.explainPredicate(atom, polarity, tassumps, pf.get());
522
  }
523
75614
  Trace("pfee-proof") << "...got " << tassumps << std::endl;
524
  // avoid duplicates
525
509161
  for (TNode a : tassumps)
526
  {
527
433547
    if (a == lit)
528
    {
529
719
      assumps.push_back(a);
530
    }
531
432828
    else if (std::find(assumps.begin(), assumps.end(), a) == assumps.end())
532
    {
533
336212
      assumps.push_back(a);
534
    }
535
  }
536
75614
  if (Trace.isOn("pfee-proof"))
537
  {
538
    Trace("pfee-proof") << "pfee::explainWithProof: add to proof ---"
539
                        << std::endl;
540
    std::stringstream sse;
541
    pf->debug_print(sse);
542
    Trace("pfee-proof") << sse.str() << std::endl;
543
    Trace("pfee-proof") << "---" << std::endl;
544
  }
545
  // add the steps in the equality engine proof to the Proof
546
75614
  pf->addToProof(curr);
547
75614
  Trace("pfee-proof") << "pfee::explainWithProof: finished" << std::endl;
548
}
549
550
}  // namespace eq
551
}  // namespace theory
552
26685
}  // namespace CVC4