GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/term_conversion_proof_generator.cpp Lines: 249 296 84.1 %
Date: 2021-03-23 Branches: 520 1457 35.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file term_conversion_proof_generator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   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 term conversion proof generator utility
13
 **/
14
15
#include "expr/term_conversion_proof_generator.h"
16
17
#include "expr/proof_checker.h"
18
#include "expr/proof_node.h"
19
#include "expr/term_context.h"
20
#include "expr/term_context_stack.h"
21
22
using namespace CVC4::kind;
23
24
namespace CVC4 {
25
26
79395
std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol)
27
{
28
79395
  switch (tcpol)
29
  {
30
67262
    case TConvPolicy::FIXPOINT: out << "FIXPOINT"; break;
31
12133
    case TConvPolicy::ONCE: out << "ONCE"; break;
32
    default: out << "TConvPolicy:unknown"; break;
33
  }
34
79395
  return out;
35
}
36
37
79395
std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol)
38
{
39
79395
  switch (tcpol)
40
  {
41
52262
    case TConvCachePolicy::STATIC: out << "STATIC"; break;
42
    case TConvCachePolicy::DYNAMIC: out << "DYNAMIC"; break;
43
27133
    case TConvCachePolicy::NEVER: out << "NEVER"; break;
44
    default: out << "TConvCachePolicy:unknown"; break;
45
  }
46
79395
  return out;
47
}
48
49
16935
TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm,
50
                                         context::Context* c,
51
                                         TConvPolicy pol,
52
                                         TConvCachePolicy cpol,
53
                                         std::string name,
54
                                         TermContext* tccb,
55
16935
                                         bool rewriteOps)
56
33870
    : d_proof(pnm, nullptr, c, name + "::LazyCDProof"),
57
      d_preRewriteMap(c ? c : &d_context),
58
      d_postRewriteMap(c ? c : &d_context),
59
      d_policy(pol),
60
      d_cpolicy(cpol),
61
      d_name(name),
62
      d_tcontext(tccb),
63
50805
      d_rewriteOps(rewriteOps)
64
{
65
16935
}
66
67
22723
TConvProofGenerator::~TConvProofGenerator() {}
68
69
673669
void TConvProofGenerator::addRewriteStep(Node t,
70
                                         Node s,
71
                                         ProofGenerator* pg,
72
                                         bool isPre,
73
                                         PfRule trustId,
74
                                         bool isClosed,
75
                                         uint32_t tctx)
76
{
77
1347338
  Node eq = registerRewriteStep(t, s, tctx, isPre);
78
673669
  if (!eq.isNull())
79
  {
80
673638
    d_proof.addLazyStep(eq, pg, trustId, isClosed);
81
  }
82
673669
}
83
84
void TConvProofGenerator::addRewriteStep(
85
    Node t, Node s, ProofStep ps, bool isPre, uint32_t tctx)
86
{
87
  Node eq = registerRewriteStep(t, s, tctx, isPre);
88
  if (!eq.isNull())
89
  {
90
    d_proof.addStep(eq, ps);
91
  }
92
}
93
94
204554
void TConvProofGenerator::addRewriteStep(Node t,
95
                                         Node s,
96
                                         PfRule id,
97
                                         const std::vector<Node>& children,
98
                                         const std::vector<Node>& args,
99
                                         bool isPre,
100
                                         uint32_t tctx)
101
{
102
409108
  Node eq = registerRewriteStep(t, s, tctx, isPre);
103
204554
  if (!eq.isNull())
104
  {
105
132702
    d_proof.addStep(eq, id, children, args);
106
  }
107
204554
}
108
109
bool TConvProofGenerator::hasRewriteStep(Node t,
110
                                         uint32_t tctx,
111
                                         bool isPre) const
112
{
113
  return !getRewriteStep(t, tctx, isPre).isNull();
114
}
115
116
Node TConvProofGenerator::getRewriteStep(Node t,
117
                                         uint32_t tctx,
118
                                         bool isPre) const
119
{
120
  Node thash = t;
121
  if (d_tcontext != nullptr)
122
  {
123
    thash = TCtxNode::computeNodeHash(t, tctx);
124
  }
125
  return getRewriteStepInternal(thash, isPre);
126
}
127
128
878223
Node TConvProofGenerator::registerRewriteStep(Node t,
129
                                              Node s,
130
                                              uint32_t tctx,
131
                                              bool isPre)
132
{
133
878223
  if (t == s)
134
  {
135
    return Node::null();
136
  }
137
1756446
  Node thash = t;
138
878223
  if (d_tcontext != nullptr)
139
  {
140
20327
    thash = TCtxNode::computeNodeHash(t, tctx);
141
  }
142
  else
143
  {
144
    // don't use term context ids if not using term context
145
857896
    Assert(tctx == 0);
146
  }
147
  // should not rewrite term to two different things
148
878223
  if (!getRewriteStepInternal(thash, isPre).isNull())
149
  {
150
143766
    Assert(getRewriteStepInternal(thash, isPre) == s)
151
71883
        << identify() << " rewriting " << t << " to both " << s << " and "
152
71883
        << getRewriteStepInternal(thash, isPre);
153
71883
    return Node::null();
154
  }
155
806340
  NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap;
156
806340
  rm[thash] = s;
157
806340
  if (d_cpolicy == TConvCachePolicy::DYNAMIC)
158
  {
159
    // clear the cache
160
    d_cache.clear();
161
  }
162
806340
  return t.eqNode(s);
163
}
164
165
79395
std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f)
166
{
167
158790
  Trace("tconv-pf-gen") << "TConvProofGenerator::getProofFor: " << identify()
168
79395
                        << ": " << f << std::endl;
169
79395
  if (f.getKind() != EQUAL)
170
  {
171
    std::stringstream serr;
172
    serr << "TConvProofGenerator::getProofFor: " << identify()
173
         << ": fail, non-equality " << f;
174
    Unhandled() << serr.str();
175
    Trace("tconv-pf-gen") << serr.str() << std::endl;
176
    return nullptr;
177
  }
178
  // we use the existing proofs
179
  LazyCDProof lpf(
180
158790
      d_proof.getManager(), &d_proof, nullptr, d_name + "::LazyCDProof");
181
79395
  if (f[0] == f[1])
182
  {
183
    // assertion failure in debug
184
    Assert(false) << "TConvProofGenerator::getProofFor: " << identify()
185
                  << ": don't ask for trivial proofs";
186
    lpf.addStep(f, PfRule::REFL, {}, {f[0]});
187
  }
188
  else
189
  {
190
158790
    Node conc = getProofForRewriting(f[0], lpf, d_tcontext);
191
79395
    if (conc != f)
192
    {
193
      bool debugTraceEnabled = Trace.isOn("tconv-pf-gen-debug");
194
      Assert(conc.getKind() == EQUAL && conc[0] == f[0]);
195
      std::stringstream serr;
196
      serr << "TConvProofGenerator::getProofFor: " << toStringDebug()
197
           << ": failed, mismatch";
198
      if (!debugTraceEnabled)
199
      {
200
        serr << " (see -t tconv-pf-gen-debug for details)";
201
      }
202
      serr << std::endl;
203
      serr << "                   source: " << f[0] << std::endl;
204
      serr << "     requested conclusion: " << f[1] << std::endl;
205
      serr << "conclusion from generator: " << conc[1] << std::endl;
206
207
      if (debugTraceEnabled)
208
      {
209
        Trace("tconv-pf-gen-debug") << "Printing rewrite steps..." << std::endl;
210
        for (size_t r = 0; r < 2; r++)
211
        {
212
          const NodeNodeMap& rm = r == 0 ? d_preRewriteMap : d_postRewriteMap;
213
          serr << "Rewrite steps (" << (r == 0 ? "pre" : "post")
214
               << "):" << std::endl;
215
          for (NodeNodeMap::const_iterator it = rm.begin(); it != rm.end();
216
               ++it)
217
          {
218
            serr << (*it).first << " -> " << (*it).second << std::endl;
219
          }
220
        }
221
      }
222
      Unhandled() << serr.str();
223
      return nullptr;
224
    }
225
  }
226
158790
  std::shared_ptr<ProofNode> pfn = lpf.getProofFor(f);
227
79395
  Trace("tconv-pf-gen") << "... success" << std::endl;
228
79395
  Assert (pfn!=nullptr);
229
79395
  Trace("tconv-pf-gen-debug") << "... proof is " << *pfn << std::endl;
230
79395
  return pfn;
231
}
232
233
79395
Node TConvProofGenerator::getProofForRewriting(Node t,
234
                                               LazyCDProof& pf,
235
                                               TermContext* tctx)
236
{
237
79395
  NodeManager* nm = NodeManager::currentNM();
238
  // Invariant: if visited[hash(t)] = s or rewritten[hash(t)] = s and t,s are
239
  // distinct, then pf is able to generate a proof of t=s. We must
240
  // Node in the domains of the maps below due to hashing creating new (SEXPR)
241
  // nodes.
242
243
  // the final rewritten form of terms
244
158790
  std::unordered_map<Node, Node, TNodeHashFunction> visited;
245
  // the rewritten form of terms we have processed so far
246
158790
  std::unordered_map<Node, Node, TNodeHashFunction> rewritten;
247
79395
  std::unordered_map<Node, Node, TNodeHashFunction>::iterator it;
248
79395
  std::unordered_map<Node, Node, TNodeHashFunction>::iterator itr;
249
79395
  std::map<Node, std::shared_ptr<ProofNode> >::iterator itc;
250
158790
  Trace("tconv-pf-gen-rewrite")
251
158790
      << "TConvProofGenerator::getProofForRewriting: " << toStringDebug()
252
79395
      << std::endl;
253
79395
  Trace("tconv-pf-gen-rewrite") << "Input: " << t << std::endl;
254
  // if provided, we use term context for cache
255
158790
  std::shared_ptr<TCtxStack> visitctx;
256
  // otherwise, visit is used if we don't have a term context
257
158790
  std::vector<TNode> visit;
258
158790
  Node tinitialHash;
259
79395
  if (tctx != nullptr)
260
  {
261
8208
    visitctx = std::make_shared<TCtxStack>(tctx);
262
8208
    visitctx->pushInitial(t);
263
8208
    tinitialHash = TCtxNode::computeNodeHash(t, tctx->initialValue());
264
  }
265
  else
266
  {
267
71187
    visit.push_back(t);
268
71187
    tinitialHash = t;
269
  }
270
158790
  Node cur;
271
79395
  uint32_t curCVal = 0;
272
158790
  Node curHash;
273
3875410
  do
274
  {
275
    // pop the top element
276
3954805
    if (tctx != nullptr)
277
    {
278
668030
      std::pair<Node, uint32_t> curPair = visitctx->getCurrent();
279
334015
      cur = curPair.first;
280
334015
      curCVal = curPair.second;
281
334015
      curHash = TCtxNode::computeNodeHash(cur, curCVal);
282
334015
      visitctx->pop();
283
    }
284
    else
285
    {
286
3620790
      cur = visit.back();
287
3620790
      curHash = cur;
288
3620790
      visit.pop_back();
289
    }
290
3954805
    Trace("tconv-pf-gen-rewrite") << "* visit : " << curHash << std::endl;
291
    // has the proof for cur been cached?
292
3954805
    itc = d_cache.find(curHash);
293
3954805
    if (itc != d_cache.end())
294
    {
295
1289800
      Node res = itc->second->getResult();
296
644900
      Assert(res.getKind() == EQUAL);
297
644900
      Assert(!res[1].isNull());
298
644900
      visited[curHash] = res[1];
299
644900
      pf.addProof(itc->second);
300
644900
      continue;
301
    }
302
3309905
    it = visited.find(curHash);
303
3309905
    if (it == visited.end())
304
    {
305
1293984
      Trace("tconv-pf-gen-rewrite") << "- previsit" << std::endl;
306
1293984
      visited[curHash] = Node::null();
307
      // did we rewrite the current node (at pre-rewrite)?
308
2587968
      Node rcur = getRewriteStepInternal(curHash, true);
309
1293984
      if (!rcur.isNull())
310
      {
311
211728
        Trace("tconv-pf-gen-rewrite")
312
105864
            << "*** " << curHash << " prerewrites to " << rcur << std::endl;
313
        // d_proof has a proof of cur = rcur. Hence there is nothing
314
        // to do here, as pf will reference d_proof to get its proof.
315
105864
        if (d_policy == TConvPolicy::FIXPOINT)
316
        {
317
          // It may be the case that rcur also rewrites, thus we cannot assign
318
          // the final rewritten form for cur yet. Instead we revisit cur after
319
          // finishing visiting rcur.
320
91528
          rewritten[curHash] = rcur;
321
91528
          if (tctx != nullptr)
322
          {
323
20544
            visitctx->push(cur, curCVal);
324
20544
            visitctx->push(rcur, curCVal);
325
          }
326
          else
327
          {
328
70984
            visit.push_back(cur);
329
70984
            visit.push_back(rcur);
330
          }
331
        }
332
        else
333
        {
334
14336
          Assert(d_policy == TConvPolicy::ONCE);
335
28672
          Trace("tconv-pf-gen-rewrite") << "-> (once, prewrite) " << curHash
336
14336
                                        << " = " << rcur << std::endl;
337
          // not rewriting again, rcur is final
338
14336
          Assert(!rcur.isNull());
339
14336
          visited[curHash] = rcur;
340
14336
          doCache(curHash, cur, rcur, pf);
341
        }
342
      }
343
1188120
      else if (tctx != nullptr)
344
      {
345
118281
        visitctx->push(cur, curCVal);
346
        // visit operator if apply uf
347
118281
        if (d_rewriteOps && cur.getKind() == APPLY_UF)
348
        {
349
          visitctx->pushOp(cur, curCVal);
350
        }
351
118281
        visitctx->pushChildren(cur, curCVal);
352
      }
353
      else
354
      {
355
1069839
        visit.push_back(cur);
356
        // visit operator if apply uf
357
1069839
        if (d_rewriteOps && cur.getKind() == APPLY_UF)
358
        {
359
71732
          visit.push_back(cur.getOperator());
360
        }
361
1069839
        visit.insert(visit.end(), cur.begin(), cur.end());
362
      }
363
    }
364
2015921
    else if (it->second.isNull())
365
    {
366
1350764
      itr = rewritten.find(curHash);
367
1350764
      if (itr != rewritten.end())
368
      {
369
        // only can generate partially rewritten nodes when rewrite again is
370
        // true.
371
192308
        Assert(d_policy != TConvPolicy::ONCE);
372
        // if it was rewritten, check the status of the rewritten node,
373
        // which should be finished now
374
384616
        Node rcur = itr->second;
375
384616
        Trace("tconv-pf-gen-rewrite")
376
192308
            << "- postvisit, previously rewritten to " << rcur << std::endl;
377
384616
        Node rcurHash = rcur;
378
192308
        if (tctx != nullptr)
379
        {
380
24262
          rcurHash = TCtxNode::computeNodeHash(rcur, curCVal);
381
        }
382
192308
        Assert(cur != rcur);
383
        // the final rewritten form of cur is the final form of rcur
384
384616
        Node rcurFinal = visited[rcurHash];
385
192308
        Assert(!rcurFinal.isNull());
386
192308
        if (rcurFinal != rcur)
387
        {
388
          // must connect via TRANS
389
134302
          std::vector<Node> pfChildren;
390
67151
          pfChildren.push_back(cur.eqNode(rcur));
391
67151
          pfChildren.push_back(rcur.eqNode(rcurFinal));
392
134302
          Node result = cur.eqNode(rcurFinal);
393
67151
          pf.addStep(result, PfRule::TRANS, pfChildren, {});
394
        }
395
384616
        Trace("tconv-pf-gen-rewrite")
396
192308
            << "-> (rewritten postrewrite) " << curHash << " = " << rcurFinal
397
192308
            << std::endl;
398
192308
        visited[curHash] = rcurFinal;
399
192308
        doCache(curHash, cur, rcurFinal, pf);
400
      }
401
      else
402
      {
403
1158456
        Trace("tconv-pf-gen-rewrite") << "- postvisit" << std::endl;
404
2316912
        Node ret = cur;
405
2316912
        Node retHash = curHash;
406
1158456
        bool childChanged = false;
407
2316912
        std::vector<Node> children;
408
1158456
        Kind ck = cur.getKind();
409
1158456
        if (d_rewriteOps && ck == APPLY_UF)
410
        {
411
          // the operator of APPLY_UF is visited
412
143464
          Node cop = cur.getOperator();
413
71732
          if (tctx != nullptr)
414
          {
415
            uint32_t coval = tctx->computeValueOp(cur, curCVal);
416
            Node coHash = TCtxNode::computeNodeHash(cop, coval);
417
            it = visited.find(coHash);
418
          }
419
          else
420
          {
421
71732
            it = visited.find(cop);
422
          }
423
71732
          Assert(it != visited.end());
424
71732
          Assert(!it->second.isNull());
425
71732
          childChanged = childChanged || cop != it->second;
426
143464
          children.push_back(it->second);
427
        }
428
1086724
        else if (cur.getMetaKind() == metakind::PARAMETERIZED)
429
        {
430
          // all other parametrized operators are unchanged
431
73197
          children.push_back(cur.getOperator());
432
        }
433
        // get the results of the children
434
1158456
        if (tctx != nullptr)
435
        {
436
276237
          for (size_t i = 0, nchild = cur.getNumChildren(); i < nchild; i++)
437
          {
438
317154
            Node cn = cur[i];
439
158577
            uint32_t cnval = tctx->computeValue(cur, curCVal, i);
440
317154
            Node cnHash = TCtxNode::computeNodeHash(cn, cnval);
441
158577
            it = visited.find(cnHash);
442
158577
            Assert(it != visited.end());
443
158577
            Assert(!it->second.isNull());
444
158577
            childChanged = childChanged || cn != it->second;
445
158577
            children.push_back(it->second);
446
          }
447
        }
448
        else
449
        {
450
          // can use simple loop if not term-context-sensitive
451
3034536
          for (const Node& cn : cur)
452
          {
453
1993740
            it = visited.find(cn);
454
1993740
            Assert(it != visited.end());
455
1993740
            Assert(!it->second.isNull());
456
1993740
            childChanged = childChanged || cn != it->second;
457
1993740
            children.push_back(it->second);
458
          }
459
        }
460
1158456
        if (childChanged)
461
        {
462
215552
          ret = nm->mkNode(ck, children);
463
215552
          rewritten[curHash] = ret;
464
          // congruence to show (cur = ret)
465
215552
          PfRule congRule = PfRule::CONG;
466
431104
          std::vector<Node> pfChildren;
467
431104
          std::vector<Node> pfArgs;
468
215552
          pfArgs.push_back(ProofRuleChecker::mkKindNode(ck));
469
215552
          if (ck == APPLY_UF && children[0] != cur.getOperator())
470
          {
471
            // use HO_CONG if the operator changed
472
221
            congRule = PfRule::HO_CONG;
473
221
            pfChildren.push_back(cur.getOperator().eqNode(children[0]));
474
          }
475
215331
          else if (kind::metaKindOf(ck) == kind::metakind::PARAMETERIZED)
476
          {
477
11742
            pfArgs.push_back(cur.getOperator());
478
          }
479
755603
          for (size_t i = 0, size = cur.getNumChildren(); i < size; i++)
480
          {
481
540051
            if (cur[i] == ret[i])
482
            {
483
              // ensure REFL proof for unchanged children
484
161171
              pf.addStep(cur[i].eqNode(cur[i]), PfRule::REFL, {}, {cur[i]});
485
            }
486
540051
            pfChildren.push_back(cur[i].eqNode(ret[i]));
487
          }
488
431104
          Node result = cur.eqNode(ret);
489
215552
          pf.addStep(result, congRule, pfChildren, pfArgs);
490
          // must update the hash
491
215552
          retHash = ret;
492
215552
          if (tctx != nullptr)
493
          {
494
38454
            retHash = TCtxNode::computeNodeHash(ret, curCVal);
495
          }
496
        }
497
942904
        else if (tctx != nullptr)
498
        {
499
          // now we need the hash
500
79206
          retHash = TCtxNode::computeNodeHash(cur, curCVal);
501
        }
502
        // did we rewrite ret (at post-rewrite)?
503
2316912
        Node rret = getRewriteStepInternal(retHash, false);
504
1158456
        if (!rret.isNull() && d_policy == TConvPolicy::FIXPOINT)
505
        {
506
142232
          Trace("tconv-pf-gen-rewrite")
507
71116
              << "*** " << retHash << " postrewrites to " << rret << std::endl;
508
          // d_proof should have a proof of ret = rret, hence nothing to do
509
          // here, for the same reasons as above. It also may be the case that
510
          // rret rewrites, hence we must revisit ret.
511
71116
          rewritten[retHash] = rret;
512
71116
          if (tctx != nullptr)
513
          {
514
3097
            if (cur != ret)
515
            {
516
625
              visitctx->push(cur, curCVal);
517
            }
518
3097
            visitctx->push(ret, curCVal);
519
3097
            visitctx->push(rret, curCVal);
520
          }
521
          else
522
          {
523
68019
            if (cur != ret)
524
            {
525
38041
              visit.push_back(cur);
526
            }
527
68019
            visit.push_back(ret);
528
68019
            visit.push_back(rret);
529
          }
530
        }
531
        else
532
        {
533
          // take its rewrite if it rewrote and we have ONCE rewriting policy
534
1087340
          ret = rret.isNull() ? ret : rret;
535
2174680
          Trace("tconv-pf-gen-rewrite")
536
1087340
              << "-> (postrewrite) " << curHash << " = " << ret << std::endl;
537
          // it is final
538
1087340
          Assert(!ret.isNull());
539
1087340
          visited[curHash] = ret;
540
1087340
          doCache(curHash, cur, ret, pf);
541
        }
542
      }
543
    }
544
    else
545
    {
546
665157
      Trace("tconv-pf-gen-rewrite") << "- already visited" << std::endl;
547
    }
548
3954805
  } while (!(tctx != nullptr ? visitctx->empty() : visit.empty()));
549
79395
  Assert(visited.find(tinitialHash) != visited.end());
550
79395
  Assert(!visited.find(tinitialHash)->second.isNull());
551
158790
  Trace("tconv-pf-gen-rewrite")
552
79395
      << "...finished, return " << visited[tinitialHash] << std::endl;
553
  // return the conclusion of the overall proof
554
158790
  return t.eqNode(visited[tinitialHash]);
555
}
556
557
1293984
void TConvProofGenerator::doCache(Node curHash,
558
                                  Node cur,
559
                                  Node r,
560
                                  LazyCDProof& pf)
561
{
562
1293984
  if (d_cpolicy != TConvCachePolicy::NEVER)
563
  {
564
830330
    Node eq = cur.eqNode(r);
565
415165
    d_cache[curHash] = pf.getProofFor(eq);
566
  }
567
1293984
}
568
569
3402546
Node TConvProofGenerator::getRewriteStepInternal(Node t, bool isPre) const
570
{
571
3402546
  const NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap;
572
3402546
  NodeNodeMap::const_iterator it = rm.find(t);
573
3402546
  if (it == rm.end())
574
  {
575
3081800
    return Node::null();
576
  }
577
320746
  return (*it).second;
578
}
579
199932
std::string TConvProofGenerator::identify() const { return d_name; }
580
581
79395
std::string TConvProofGenerator::toStringDebug() const
582
{
583
158790
  std::stringstream ss;
584
158790
  ss << identify() << " (policy=" << d_policy << ", cache policy=" << d_cpolicy
585
79395
     << (d_tcontext != nullptr ? ", term-context-sensitive" : "") << ")";
586
158790
  return ss.str();
587
}
588
589
26685
}  // namespace CVC4