GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/rewriter.cpp Lines: 169 193 87.6 %
Date: 2021-03-23 Branches: 331 766 43.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file rewriter.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, Dejan Jovanovic
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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "theory/rewriter.h"
19
20
#include "expr/term_conversion_proof_generator.h"
21
#include "options/theory_options.h"
22
#include "smt/smt_engine.h"
23
#include "smt/smt_engine_scope.h"
24
#include "smt/smt_statistics_registry.h"
25
#include "theory/builtin/proof_checker.h"
26
#include "theory/rewriter_tables.h"
27
#include "theory/theory.h"
28
#include "util/resource_manager.h"
29
30
using namespace std;
31
32
namespace CVC4 {
33
namespace theory {
34
35
/** Attribute true for nodes that have been rewritten with proofs enabled */
36
struct RewriteWithProofsAttributeId
37
{
38
};
39
typedef expr::Attribute<RewriteWithProofsAttributeId, bool>
40
    RewriteWithProofsAttribute;
41
42
// Note that this function is a simplified version of Theory::theoryOf for
43
// (type-based) theoryOfMode. We expand and simplify it here for the sake of
44
// efficiency.
45
153813099
static TheoryId theoryOf(TNode node) {
46
153813099
  if (node.getKind() == kind::EQUAL)
47
  {
48
    // Equality is owned by the theory that owns the domain
49
21940298
    return Theory::theoryOf(node[0].getType());
50
  }
51
  // Regular nodes are owned by the kind
52
131872801
  return kindToTheoryId(node.getKind());
53
}
54
55
/**
56
 * TheoryEngine::rewrite() keeps a stack of things that are being pre-
57
 * and post-rewritten.  Each element of the stack is a
58
 * RewriteStackElement.
59
 */
60
131847389
struct RewriteStackElement {
61
  /**
62
   * Construct a fresh stack element.
63
   */
64
39298505
  RewriteStackElement(TNode node, TheoryId theoryId)
65
39298505
      : d_node(node),
66
        d_original(node),
67
        d_theoryId(theoryId),
68
        d_originalTheoryId(theoryId),
69
39298505
        d_nextChild(0)
70
  {
71
39298505
  }
72
73
232847658
  TheoryId getTheoryId() { return static_cast<TheoryId>(d_theoryId); }
74
75
23014410
  TheoryId getOriginalTheoryId()
76
  {
77
23014410
    return static_cast<TheoryId>(d_originalTheoryId);
78
  }
79
80
  /** The node we're currently rewriting */
81
  Node d_node;
82
  /** Original node (either the unrewritten node or the node after prerewriting)
83
   */
84
  Node d_original;
85
  /** Id of the theory that's currently rewriting this node */
86
  unsigned d_theoryId : 8;
87
  /** Id of the original theory that started the rewrite */
88
  unsigned d_originalTheoryId : 8;
89
  /** Index of the child this node is done rewriting */
90
  unsigned d_nextChild : 32;
91
  /** Builder for this node */
92
  NodeBuilder<> d_builder;
93
};
94
95
RewriteResponse identityRewrite(RewriteEnvironment* re, TNode n)
96
{
97
  return RewriteResponse(REWRITE_DONE, n);
98
}
99
100
38723178
Node Rewriter::rewrite(TNode node) {
101
38723178
  if (node.getNumChildren() == 0)
102
  {
103
    // Nodes with zero children should never change via rewriting. We return
104
    // eagerly for the sake of efficiency here.
105
8369932
    return node;
106
  }
107
30353246
  return getInstance()->rewriteTo(theoryOf(node), node);
108
}
109
110
52268
TrustNode Rewriter::rewriteWithProof(TNode node,
111
                                     bool isExtEq)
112
{
113
  // must set the proof checker before calling this
114
52268
  Assert(d_tpg != nullptr);
115
52268
  if (isExtEq)
116
  {
117
    // theory rewriter is responsible for rewriting the equality
118
6
    TheoryRewriter* tr = getInstance()->d_theoryRewriters[theoryOf(node)];
119
6
    Assert(tr != nullptr);
120
6
    return tr->rewriteEqualityExtWithProof(node);
121
  }
122
104524
  Node ret = getInstance()->rewriteTo(theoryOf(node), node, d_tpg.get());
123
52262
  return TrustNode::mkTrustRewrite(node, ret, d_tpg.get());
124
}
125
126
962
void Rewriter::setProofNodeManager(ProofNodeManager* pnm)
127
{
128
  // if not already initialized with proof support
129
962
  if (d_tpg == nullptr)
130
  {
131
962
    Trace("rewriter") << "Rewriter::setProofNodeManager" << std::endl;
132
    // the rewriter is staticly determinstic, thus use static cache policy
133
    // for the term conversion proof generator
134
1924
    d_tpg.reset(new TConvProofGenerator(pnm,
135
                                        nullptr,
136
                                        TConvPolicy::FIXPOINT,
137
                                        TConvCachePolicy::STATIC,
138
962
                                        "Rewriter::TConvProofGenerator"));
139
  }
140
962
}
141
142
93
Node Rewriter::rewriteEqualityExt(TNode node)
143
{
144
93
  Assert(node.getKind() == kind::EQUAL);
145
  // note we don't force caching of this method currently
146
186
  return getInstance()->d_theoryRewriters[theoryOf(node)]->rewriteEqualityExt(
147
186
      node);
148
}
149
150
116997
void Rewriter::registerTheoryRewriter(theory::TheoryId tid,
151
                                      TheoryRewriter* trew)
152
{
153
116997
  getInstance()->d_theoryRewriters[tid] = trew;
154
116997
}
155
156
void Rewriter::registerPreRewrite(
157
    Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn)
158
{
159
  Assert(k != kind::EQUAL) << "Register pre-rewrites for EQUAL with registerPreRewriteEqual.";
160
  d_preRewriters[k] = fn;
161
}
162
163
void Rewriter::registerPostRewrite(
164
    Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn)
165
{
166
  Assert(k != kind::EQUAL) << "Register post-rewrites for EQUAL with registerPostRewriteEqual.";
167
  d_postRewriters[k] = fn;
168
}
169
170
void Rewriter::registerPreRewriteEqual(
171
    theory::TheoryId tid,
172
    std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn)
173
{
174
  d_preRewritersEqual[tid] = fn;
175
}
176
177
void Rewriter::registerPostRewriteEqual(
178
    theory::TheoryId tid,
179
    std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn)
180
{
181
  d_postRewritersEqual[tid] = fn;
182
}
183
184
30522604
Rewriter* Rewriter::getInstance()
185
{
186
30522604
  return smt::currentSmtEngine()->getRewriter();
187
}
188
189
31699561
Node Rewriter::rewriteTo(theory::TheoryId theoryId,
190
                         Node node,
191
                         TConvProofGenerator* tcpg)
192
{
193
  RewriteWithProofsAttribute rpfa;
194
#ifdef CVC4_ASSERTIONS
195
31699561
  bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean());
196
197
31699561
  if (d_rewriteStack == nullptr)
198
  {
199
8698
    d_rewriteStack.reset(new std::unordered_set<Node, NodeHashFunction>());
200
  }
201
#endif
202
203
31699561
  Trace("rewriter") << "Rewriter::rewriteTo(" << theoryId << "," << node << ")"<< std::endl;
204
205
  // Check if it's been cached already
206
63399122
  Node cached = getPostRewriteCache(theoryId, node);
207
31699561
  if (!cached.isNull() && (tcpg == nullptr || node.getAttribute(rpfa)))
208
  {
209
25586310
    return cached;
210
  }
211
212
  // Put the node on the stack in order to start the "recursive" rewrite
213
12226502
  vector<RewriteStackElement> rewriteStack;
214
6113251
  rewriteStack.push_back(RewriteStackElement(node, theoryId));
215
216
6113251
  ResourceManager* rm = NULL;
217
6113251
  bool hasSmtEngine = smt::smtEngineInScope();
218
6113251
  if (hasSmtEngine) {
219
6113251
    rm = smt::currentResourceManager();
220
  }
221
  // Rewrite until the stack is empty
222
  for (;;){
223
72483757
    if (hasSmtEngine)
224
    {
225
72483757
      rm->spendResource(ResourceManager::Resource::RewriteStep);
226
    }
227
228
    // Get the top of the recursion stack
229
72483757
    RewriteStackElement& rewriteStackTop = rewriteStack.back();
230
231
144967514
    Trace("rewriter") << "Rewriter::rewriting: "
232
144967514
                      << rewriteStackTop.getTheoryId() << ","
233
72483757
                      << rewriteStackTop.d_node << std::endl;
234
235
    // Before rewriting children we need to do a pre-rewrite of the node
236
72483757
    if (rewriteStackTop.d_nextChild == 0)
237
    {
238
      // Check if the pre-rewrite has already been done (it's in the cache)
239
39298505
      cached = getPreRewriteCache(rewriteStackTop.getTheoryId(),
240
                                  rewriteStackTop.d_node);
241
78597010
      if (cached.isNull()
242
39298505
          || (tcpg != nullptr && !rewriteStackTop.d_node.getAttribute(rpfa)))
243
      {
244
        // Rewrite until fix-point is reached
245
        for(;;) {
246
          // Perform the pre-rewrite
247
          RewriteResponse response = preRewrite(
248
13744727
              rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg);
249
250
          // Put the rewritten node to the top of the stack
251
12852254
          rewriteStackTop.d_node = response.d_node;
252
12852254
          TheoryId newTheory = theoryOf(rewriteStackTop.d_node);
253
          // In the pre-rewrite, if changing theories, we just call the other theories pre-rewrite
254
25704508
          if (newTheory == rewriteStackTop.getTheoryId()
255
12852254
              && response.d_status == REWRITE_DONE)
256
          {
257
11959781
            break;
258
          }
259
892473
          rewriteStackTop.d_theoryId = newTheory;
260
892473
        }
261
262
        // Cache the rewrite
263
11959781
        setPreRewriteCache(rewriteStackTop.getOriginalTheoryId(),
264
                           rewriteStackTop.d_original,
265
                           rewriteStackTop.d_node);
266
      }
267
      // Otherwise we're have already been pre-rewritten (in pre-rewrite cache)
268
      else {
269
        // Continue with the cached version
270
27338724
        rewriteStackTop.d_node = cached;
271
27338724
        rewriteStackTop.d_theoryId = theoryOf(cached);
272
      }
273
    }
274
275
72483757
    rewriteStackTop.d_original = rewriteStackTop.d_node;
276
    // Now it's time to rewrite the children, check if this has already been done
277
72483757
    cached = getPostRewriteCache(rewriteStackTop.getTheoryId(),
278
                                 rewriteStackTop.d_node);
279
    // If not, go through the children
280
144967514
    if (cached.isNull()
281
72483757
        || (tcpg != nullptr && !rewriteStackTop.d_node.getAttribute(rpfa)))
282
    {
283
      // The child we need to rewrite
284
44239885
      unsigned child = rewriteStackTop.d_nextChild++;
285
286
      // To build the rewritten expression we set up the builder
287
44239885
      if(child == 0) {
288
11054633
        if (rewriteStackTop.d_node.getNumChildren() > 0)
289
        {
290
          // The children will add themselves to the builder once they're done
291
10476804
          rewriteStackTop.d_builder << rewriteStackTop.d_node.getKind();
292
10476804
          kind::MetaKind metaKind = rewriteStackTop.d_node.getMetaKind();
293
10476804
          if (metaKind == kind::metakind::PARAMETERIZED) {
294
709866
            rewriteStackTop.d_builder << rewriteStackTop.d_node.getOperator();
295
          }
296
        }
297
      }
298
299
      // Process the next child
300
44239885
      if (child < rewriteStackTop.d_node.getNumChildren())
301
      {
302
        // The child node
303
66370508
        Node childNode = rewriteStackTop.d_node[child];
304
        // Push the rewrite request to the stack (NOTE: rewriteStackTop might be a bad reference now)
305
33185254
        rewriteStack.push_back(RewriteStackElement(childNode, theoryOf(childNode)));
306
        // Go on with the rewriting
307
33185254
        continue;
308
      }
309
310
      // Incorporate the children if necessary
311
11054631
      if (rewriteStackTop.d_node.getNumChildren() > 0)
312
      {
313
20953604
        Node rewritten = rewriteStackTop.d_builder;
314
10476802
        rewriteStackTop.d_node = rewritten;
315
10476802
        rewriteStackTop.d_theoryId = theoryOf(rewriteStackTop.d_node);
316
      }
317
318
      // Done with all pre-rewriting, so let's do the post rewrite
319
      for(;;) {
320
        // Do the post-rewrite
321
        RewriteResponse response = postRewrite(
322
11566547
            rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg);
323
324
        // We continue with the response we got
325
11310586
        TheoryId newTheoryId = theoryOf(response.d_node);
326
22621172
        if (newTheoryId != rewriteStackTop.getTheoryId()
327
11310586
            || response.d_status == REWRITE_AGAIN_FULL)
328
        {
329
          // In the post rewrite if we've changed theories, we must do a full rewrite
330
1294053
          Assert(response.d_node != rewriteStackTop.d_node);
331
          //TODO: this is not thread-safe - should make this assertion dependent on sequential build
332
#ifdef CVC4_ASSERTIONS
333
1294053
          Assert(d_rewriteStack->find(response.d_node)
334
                 == d_rewriteStack->end());
335
1294053
          d_rewriteStack->insert(response.d_node);
336
#endif
337
2588106
          Node rewritten = rewriteTo(newTheoryId, response.d_node, tcpg);
338
1294053
          rewriteStackTop.d_node = rewritten;
339
#ifdef CVC4_ASSERTIONS
340
1294053
          d_rewriteStack->erase(response.d_node);
341
#endif
342
1294053
          break;
343
        }
344
10016533
        else if (response.d_status == REWRITE_DONE)
345
        {
346
#ifdef CVC4_ASSERTIONS
347
          RewriteResponse r2 =
348
19521152
              d_theoryRewriters[newTheoryId]->postRewrite(response.d_node);
349
19521152
          Assert(r2.d_node == response.d_node)
350
9760576
              << r2.d_node << " != " << response.d_node;
351
#endif
352
9760576
          rewriteStackTop.d_node = response.d_node;
353
9760576
          break;
354
        }
355
        // Check for trivial rewrite loops of size 1 or 2
356
255957
        Assert(response.d_node != rewriteStackTop.d_node);
357
255957
        Assert(d_theoryRewriters[rewriteStackTop.getTheoryId()]
358
                   ->postRewrite(response.d_node)
359
                   .d_node
360
               != rewriteStackTop.d_node);
361
255957
        rewriteStackTop.d_node = response.d_node;
362
255957
      }
363
364
      // We're done with the post rewrite, so we add to the cache
365
11054629
      if (tcpg != nullptr)
366
      {
367
        // if proofs are enabled, mark that we've rewritten with proofs
368
293140
        rewriteStackTop.d_original.setAttribute(rpfa, true);
369
293140
        if (!cached.isNull())
370
        {
371
          // We may have gotten a different node, due to non-determinism in
372
          // theory rewriters (e.g. quantifiers rewriter which introduces
373
          // fresh BOUND_VARIABLE). This can happen if we wrote once without
374
          // proofs and then rewrote again with proofs.
375
279808
          if (rewriteStackTop.d_node != cached)
376
          {
377
78
            Trace("rewriter-proof") << "WARNING: Rewritten forms with and "
378
39
                                       "without proofs were not equivalent"
379
39
                                    << std::endl;
380
78
            Trace("rewriter-proof")
381
39
                << "   original: " << rewriteStackTop.d_original << std::endl;
382
78
            Trace("rewriter-proof")
383
39
                << "with proofs: " << rewriteStackTop.d_node << std::endl;
384
39
            Trace("rewriter-proof") << " w/o proofs: " << cached << std::endl;
385
78
            Node eq = rewriteStackTop.d_node.eqNode(cached);
386
            // we make this a post-rewrite, since we are processing a node that
387
            // has finished post-rewriting above
388
78
            tcpg->addRewriteStep(rewriteStackTop.d_node,
389
                                 cached,
390
                                 PfRule::TRUST_REWRITE,
391
                                 {},
392
                                 {eq},
393
39
                                 false);
394
            // don't overwrite the cache, should be the same
395
39
            rewriteStackTop.d_node = cached;
396
          }
397
        }
398
      }
399
11054629
      setPostRewriteCache(rewriteStackTop.getOriginalTheoryId(),
400
                          rewriteStackTop.d_original,
401
                          rewriteStackTop.d_node);
402
    }
403
    else
404
    {
405
      // We were already in cache, so just remember it
406
28243872
      rewriteStackTop.d_node = cached;
407
28243872
      rewriteStackTop.d_theoryId = theoryOf(cached);
408
    }
409
410
    // If this is the last node, just return
411
39298501
    if (rewriteStack.size() == 1) {
412
6113249
      Assert(!isEquality || rewriteStackTop.d_node.getKind() == kind::EQUAL
413
             || rewriteStackTop.d_node.isConst());
414
6113249
      return rewriteStackTop.d_node;
415
    }
416
417
    // We're done with this node, append it to the parent
418
33185252
    rewriteStack[rewriteStack.size() - 2].d_builder << rewriteStackTop.d_node;
419
33185252
    rewriteStack.pop_back();
420
66370506
  }
421
422
  Unreachable();
423
} /* Rewriter::rewriteTo() */
424
425
12852254
RewriteResponse Rewriter::preRewrite(theory::TheoryId theoryId,
426
                                     TNode n,
427
                                     TConvProofGenerator* tcpg)
428
{
429
12852254
  Kind k = n.getKind();
430
  std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn =
431
25704508
      (k == kind::EQUAL) ? d_preRewritersEqual[theoryId] : d_preRewriters[k];
432
12852254
  if (fn == nullptr)
433
  {
434
12852254
    if (tcpg != nullptr)
435
    {
436
      // call the trust rewrite response interface
437
      TrustRewriteResponse tresponse =
438
798880
          d_theoryRewriters[theoryId]->preRewriteWithProof(n);
439
      // process the trust rewrite response: store the proof step into
440
      // tcpg if necessary and then convert to rewrite response.
441
399440
      return processTrustRewriteResponse(theoryId, tresponse, true, tcpg);
442
    }
443
12452814
    return d_theoryRewriters[theoryId]->preRewrite(n);
444
  }
445
  return fn(&d_re, n);
446
}
447
448
11310588
RewriteResponse Rewriter::postRewrite(theory::TheoryId theoryId,
449
                                      TNode n,
450
                                      TConvProofGenerator* tcpg)
451
{
452
11310588
  Kind k = n.getKind();
453
  std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn =
454
22621176
      (k == kind::EQUAL) ? d_postRewritersEqual[theoryId] : d_postRewriters[k];
455
11310588
  if (fn == nullptr)
456
  {
457
11310588
    if (tcpg != nullptr)
458
    {
459
      // same as above, for post-rewrite
460
      TrustRewriteResponse tresponse =
461
589790
          d_theoryRewriters[theoryId]->postRewriteWithProof(n);
462
294895
      return processTrustRewriteResponse(theoryId, tresponse, false, tcpg);
463
    }
464
11015695
    return d_theoryRewriters[theoryId]->postRewrite(n);
465
  }
466
  return fn(&d_re, n);
467
}
468
469
694335
RewriteResponse Rewriter::processTrustRewriteResponse(
470
    theory::TheoryId theoryId,
471
    const TrustRewriteResponse& tresponse,
472
    bool isPre,
473
    TConvProofGenerator* tcpg)
474
{
475
694335
  Assert(tcpg != nullptr);
476
1388670
  TrustNode trn = tresponse.d_node;
477
694335
  Assert(trn.getKind() == TrustNodeKind::REWRITE);
478
1388670
  Node proven = trn.getProven();
479
694335
  if (proven[0] != proven[1])
480
  {
481
165465
    ProofGenerator* pg = trn.getGenerator();
482
165465
    if (pg == nullptr)
483
    {
484
330930
      Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId);
485
      // add small step trusted rewrite
486
      Node rid = mkMethodId(isPre ? MethodId::RW_REWRITE_THEORY_PRE
487
330930
                                  : MethodId::RW_REWRITE_THEORY_POST);
488
661860
      tcpg->addRewriteStep(proven[0],
489
                           proven[1],
490
                           PfRule::THEORY_REWRITE,
491
                           {},
492
                           {proven, tidn, rid},
493
496395
                           isPre);
494
    }
495
    else
496
    {
497
      // store proven rewrite step
498
      tcpg->addRewriteStep(proven[0], proven[1], pg, isPre);
499
    }
500
  }
501
1388670
  return RewriteResponse(tresponse.d_status, trn.getNode());
502
}
503
504
void Rewriter::clearCaches() {
505
  Rewriter* rewriter = getInstance();
506
507
#ifdef CVC4_ASSERTIONS
508
  rewriter->d_rewriteStack.reset(nullptr);
509
#endif
510
511
  rewriter->clearCachesInternal();
512
}
513
514
}/* CVC4::theory namespace */
515
26685
}/* CVC4 namespace */