GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory_preprocessor.cpp Lines: 201 216 93.1 %
Date: 2021-03-23 Branches: 476 1054 45.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_preprocessor.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Dejan Jovanovic, Morgan Deters
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 The theory preprocessor
13
 **/
14
15
#include "theory/theory_preprocessor.h"
16
17
#include "expr/lazy_proof.h"
18
#include "expr/skolem_manager.h"
19
#include "smt/logic_exception.h"
20
#include "theory/logic_info.h"
21
#include "theory/rewriter.h"
22
#include "theory/theory_engine.h"
23
24
using namespace std;
25
26
namespace CVC4 {
27
namespace theory {
28
29
9029
TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
30
                                       context::UserContext* userContext,
31
9029
                                       ProofNodeManager* pnm)
32
    : d_engine(engine),
33
9029
      d_logicInfo(engine.getLogicInfo()),
34
      d_ppCache(userContext),
35
      d_rtfCache(userContext),
36
      d_tfr(userContext, pnm),
37
      d_tpg(pnm ? new TConvProofGenerator(
38
                      pnm,
39
                      userContext,
40
                      TConvPolicy::FIXPOINT,
41
                      TConvCachePolicy::NEVER,
42
                      "TheoryPreprocessor::preprocess_rewrite",
43
966
                      &d_iqtc)
44
                : nullptr),
45
      d_tpgRtf(pnm ? new TConvProofGenerator(pnm,
46
                                             userContext,
47
                                             TConvPolicy::FIXPOINT,
48
                                             TConvCachePolicy::NEVER,
49
                                             "TheoryPreprocessor::rtf",
50
966
                                             &d_iqtc)
51
                   : nullptr),
52
      d_tpgRew(pnm ? new TConvProofGenerator(pnm,
53
                                             userContext,
54
                                             TConvPolicy::ONCE,
55
                                             TConvCachePolicy::NEVER,
56
966
                                             "TheoryPreprocessor::pprew")
57
                   : nullptr),
58
      d_tspg(nullptr),
59
      d_lp(pnm ? new LazyCDProof(pnm,
60
                                 nullptr,
61
                                 userContext,
62
966
                                 "TheoryPreprocessor::LazyCDProof")
63
21922
               : nullptr)
64
{
65
9029
  if (isProofEnabled())
66
  {
67
    // Make the main term conversion sequence generator, which tracks up to
68
    // three conversions made in succession:
69
    // (1) rewriting
70
    // (2) (theory preprocessing+rewriting until fixed point)+term formula
71
    // removal+rewriting.
72
1932
    std::vector<ProofGenerator*> ts;
73
966
    ts.push_back(d_tpgRew.get());
74
966
    ts.push_back(d_tpgRtf.get());
75
1932
    d_tspg.reset(new TConvSeqProofGenerator(
76
966
        pnm, ts, userContext, "TheoryPreprocessor::sequence"));
77
  }
78
9029
}
79
80
9026
TheoryPreprocessor::~TheoryPreprocessor() {}
81
82
278121
TrustNode TheoryPreprocessor::preprocess(TNode node,
83
                                         std::vector<TrustNode>& newLemmas,
84
                                         std::vector<Node>& newSkolems)
85
{
86
278121
  return preprocessInternal(node, newLemmas, newSkolems, true);
87
}
88
89
768703
TrustNode TheoryPreprocessor::preprocessInternal(
90
    TNode node,
91
    std::vector<TrustNode>& newLemmas,
92
    std::vector<Node>& newSkolems,
93
    bool procLemmas)
94
{
95
  // In this method, all rewriting steps of node are stored in d_tpg.
96
97
768703
  Trace("tpp") << "TheoryPreprocessor::preprocess: start " << node << std::endl;
98
99
  // We must rewrite before preprocessing, because some terms when rewritten
100
  // may introduce new terms that are not top-level and require preprocessing.
101
  // An example of this is (forall ((x Int)) (and (tail L) (P x))) which
102
  // rewrites to (and (tail L) (forall ((x Int)) (P x))). The subterm (tail L)
103
  // must be preprocessed as a child here.
104
1537406
  Node irNode = rewriteWithProof(node, d_tpgRew.get(), true);
105
106
  // run theory preprocessing
107
1537406
  TrustNode tpp = theoryPreprocess(irNode, newLemmas, newSkolems);
108
1537388
  Node ppNode = tpp.getNode();
109
110
768694
  if (Trace.isOn("tpp-debug"))
111
  {
112
    if (node != irNode)
113
    {
114
      Trace("tpp-debug") << "after initial rewriting : " << irNode << std::endl;
115
    }
116
    if (irNode != ppNode)
117
    {
118
      Trace("tpp-debug")
119
          << "after preprocessing + rewriting and term formula removal : "
120
          << ppNode << std::endl;
121
    }
122
    Trace("tpp-debug") << "TheoryPreprocessor::preprocess: finish" << std::endl;
123
  }
124
125
768694
  if (procLemmas)
126
  {
127
    // Also must preprocess the new lemmas. This is especially important for
128
    // formulas containing witness terms whose bodies are not in preprocessed
129
    // form, as term formula removal introduces new lemmas for these that
130
    // require theory-preprocessing.
131
739432
    size_t i = 0;
132
797956
    while (i < newLemmas.size())
133
    {
134
58524
      TrustNode cur = newLemmas[i];
135
29262
      newLemmas[i] = preprocessLemmaInternal(cur, newLemmas, newSkolems, false);
136
29262
      Trace("tpp") << "Final lemma : " << newLemmas[i].getProven() << std::endl;
137
29262
      i++;
138
    }
139
  }
140
141
768694
  if (node == ppNode)
142
  {
143
1089738
    Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned no change"
144
544869
                       << std::endl;
145
    // no change
146
544869
    return TrustNode::null();
147
  }
148
149
  // Now, sequence the conversion steps if proofs are enabled.
150
447650
  TrustNode tret;
151
223825
  if (isProofEnabled())
152
  {
153
64432
    std::vector<Node> cterms;
154
32216
    cterms.push_back(node);
155
32216
    cterms.push_back(irNode);
156
32216
    cterms.push_back(ppNode);
157
    // We have that:
158
    // node -> irNode via rewriting
159
    // irNode -> ppNode via theory-preprocessing + rewriting + tf removal
160
32216
    tret = d_tspg->mkTrustRewriteSequence(cterms);
161
32216
    tret.debugCheckClosed("tpp-debug", "TheoryPreprocessor::lemma_ret");
162
  }
163
  else
164
  {
165
191609
    tret = TrustNode::mkTrustRewrite(node, ppNode, nullptr);
166
  }
167
168
447650
  Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned "
169
223825
                     << tret.getNode() << std::endl;
170
447650
  Trace("tpp") << "TheoryPreprocessor::preprocess: return " << tret.getNode()
171
223825
               << ", procLemmas=" << procLemmas
172
223825
               << ", # lemmas = " << newLemmas.size() << std::endl;
173
223825
  return tret;
174
}
175
176
461320
TrustNode TheoryPreprocessor::preprocessLemma(TrustNode node,
177
                                              std::vector<TrustNode>& newLemmas,
178
                                              std::vector<Node>& newSkolems)
179
{
180
461320
  return preprocessLemmaInternal(node, newLemmas, newSkolems, true);
181
}
182
183
490582
TrustNode TheoryPreprocessor::preprocessLemmaInternal(
184
    TrustNode node,
185
    std::vector<TrustNode>& newLemmas,
186
    std::vector<Node>& newSkolems,
187
    bool procLemmas)
188
{
189
  // what was originally proven
190
981164
  Node lemma = node.getProven();
191
  TrustNode tplemma =
192
981164
      preprocessInternal(lemma, newLemmas, newSkolems, procLemmas);
193
490580
  if (tplemma.isNull())
194
  {
195
    // no change needed
196
323493
    return node;
197
  }
198
167087
  Assert(tplemma.getKind() == TrustNodeKind::REWRITE);
199
  // what it was preprocessed to
200
334174
  Node lemmap = tplemma.getNode();
201
167087
  Assert(lemmap != node.getProven());
202
  // process the preprocessing
203
167087
  if (isProofEnabled())
204
  {
205
21880
    Assert(d_lp != nullptr);
206
    // add the original proof to the lazy proof
207
43760
    d_lp->addLazyStep(
208
43760
        node.getProven(), node.getGenerator(), PfRule::THEORY_PREPROCESS_LEMMA);
209
    // only need to do anything if lemmap changed in a non-trivial way
210
21880
    if (!CDProof::isSame(lemmap, lemma))
211
    {
212
21071
      d_lp->addLazyStep(tplemma.getProven(),
213
                        tplemma.getGenerator(),
214
                        PfRule::THEORY_PREPROCESS,
215
                        true,
216
                        "TheoryEngine::lemma_pp");
217
      // ---------- from node -------------- from theory preprocess
218
      // lemma                lemma = lemmap
219
      // ------------------------------------------ EQ_RESOLVE
220
      // lemmap
221
42142
      std::vector<Node> pfChildren;
222
21071
      pfChildren.push_back(lemma);
223
21071
      pfChildren.push_back(tplemma.getProven());
224
21071
      d_lp->addStep(lemmap, PfRule::EQ_RESOLVE, pfChildren, {});
225
    }
226
  }
227
167087
  return TrustNode::mkTrustLemma(lemmap, d_lp.get());
228
}
229
230
2
RemoveTermFormulas& TheoryPreprocessor::getRemoveTermFormulas()
231
{
232
2
  return d_tfr;
233
}
234
235
9816359
struct preprocess_stack_element
236
{
237
  TNode node;
238
  bool children_added;
239
2295759
  preprocess_stack_element(TNode n) : node(n), children_added(false) {}
240
};
241
242
768703
TrustNode TheoryPreprocessor::theoryPreprocess(
243
    TNode assertion,
244
    std::vector<TrustNode>& newLemmas,
245
    std::vector<Node>& newSkolems)
246
{
247
1537406
  Trace("theory::preprocess")
248
768703
      << "TheoryPreprocessor::theoryPreprocess(" << assertion << ")" << endl;
249
  // spendResource();
250
251
  // Do a topological sort of the subexpressions and substitute them
252
1537406
  vector<preprocess_stack_element> toVisit;
253
768703
  toVisit.push_back(assertion);
254
255
9180525
  while (!toVisit.empty())
256
  {
257
    // The current node we are processing
258
4205920
    preprocess_stack_element& stackHead = toVisit.back();
259
7025886
    TNode current = stackHead.node;
260
261
8411840
    Trace("theory::preprocess-debug")
262
4205920
        << "TheoryPreprocessor::theoryPreprocess processing " << current
263
4205920
        << endl;
264
265
    // If node already in the cache we're done, pop from the stack
266
5047626
    if (d_rtfCache.find(current) != d_rtfCache.end())
267
    {
268
841706
      toVisit.pop_back();
269
841706
      continue;
270
    }
271
272
3364214
    TheoryId tid = Theory::theoryOf(current);
273
274
3364214
    if (!d_logicInfo.isTheoryEnabled(tid) && tid != THEORY_SAT_SOLVER)
275
    {
276
      stringstream ss;
277
      ss << "The logic was specified as " << d_logicInfo.getLogicString()
278
         << ", which doesn't include " << tid
279
         << ", but got a preprocessing-time fact for that theory." << endl
280
         << "The fact:" << endl
281
         << current;
282
      throw LogicException(ss.str());
283
    }
284
    // If this is an atom, we preprocess its terms with the theory ppRewriter
285
3364214
    if (tid != THEORY_BOOL)
286
    {
287
1088514
      std::vector<SkolemLemma> lems;
288
1088514
      Node ppRewritten = ppTheoryRewrite(current, lems);
289
545714
      for (const SkolemLemma& lem : lems)
290
      {
291
1466
        newLemmas.push_back(lem.d_lemma);
292
1466
        newSkolems.push_back(lem.d_skolem);
293
      }
294
544248
      Assert(Rewriter::rewrite(ppRewritten) == ppRewritten);
295
544248
      if (isProofEnabled() && ppRewritten != current)
296
      {
297
        TrustNode trn =
298
2312
            TrustNode::mkTrustRewrite(current, ppRewritten, d_tpg.get());
299
1156
        registerTrustedRewrite(trn, d_tpgRtf.get(), true);
300
      }
301
302
      // Term formula removal without fixed point. We do not need to do fixed
303
      // point since newLemmas are theory-preprocessed until fixed point in
304
      // preprocessInternal (at top-level, when procLemmas=true).
305
1088496
      TrustNode ttfr = d_tfr.run(ppRewritten, newLemmas, newSkolems, false);
306
1088496
      Node rtfNode = ppRewritten;
307
544248
      if (!ttfr.isNull())
308
      {
309
65661
        rtfNode = ttfr.getNode();
310
65661
        registerTrustedRewrite(ttfr, d_tpgRtf.get(), true);
311
      }
312
      // Finish the conversion by rewriting. This is registered as a
313
      // post-rewrite, since it is the last step applied for theory atoms.
314
1088496
      Node retNode = rewriteWithProof(rtfNode, d_tpgRtf.get(), false);
315
544248
      d_rtfCache[current] = retNode;
316
544248
      continue;
317
    }
318
319
    // Not yet substituted, so process
320
2819957
    if (stackHead.children_added)
321
    {
322
      // Children have been processed, so substitute
323
2731836
      NodeBuilder<> builder(current.getKind());
324
1365918
      if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
325
      {
326
        builder << current.getOperator();
327
      }
328
6197691
      for (unsigned i = 0; i < current.getNumChildren(); ++i)
329
      {
330
4831773
        Assert(d_rtfCache.find(current[i]) != d_rtfCache.end());
331
4831773
        builder << d_rtfCache[current[i]].get();
332
      }
333
      // Mark the substitution and continue
334
2731836
      Node result = builder;
335
      // always rewrite here, since current may not be in rewritten form after
336
      // reconstruction
337
1365918
      result = rewriteWithProof(result, d_tpgRtf.get(), false);
338
2731836
      Trace("theory::preprocess-debug")
339
1365918
          << "TheoryPreprocessor::theoryPreprocess setting " << current
340
1365918
          << " -> " << result << endl;
341
1365918
      d_rtfCache[current] = result;
342
1365918
      toVisit.pop_back();
343
    }
344
    else
345
    {
346
      // Mark that we have added the children if any
347
1454039
      if (current.getNumChildren() > 0)
348
      {
349
1365927
        stackHead.children_added = true;
350
        // We need to add the children
351
6197717
        for (TNode::iterator child_it = current.begin();
352
6197717
             child_it != current.end();
353
             ++child_it)
354
        {
355
9663580
          TNode childNode = *child_it;
356
4831790
          if (d_rtfCache.find(childNode) == d_rtfCache.end())
357
          {
358
1527056
            toVisit.push_back(childNode);
359
          }
360
        }
361
      }
362
      else
363
      {
364
        // No children, so we're done
365
176224
        Trace("theory::preprocess-debug")
366
88112
            << "SubstitutionMap::internalSubstitute setting " << current
367
88112
            << " -> " << current << endl;
368
88112
        d_rtfCache[current] = current;
369
88112
        toVisit.pop_back();
370
      }
371
    }
372
  }
373
768694
  Assert(d_rtfCache.find(assertion) != d_rtfCache.end());
374
  // Return the substituted version
375
1537388
  Node res = d_rtfCache[assertion];
376
1537388
  return TrustNode::mkTrustRewrite(assertion, res, d_tpg.get());
377
}
378
379
// Recursively traverse a term and call the theory rewriter on its sub-terms
380
2513248
Node TheoryPreprocessor::ppTheoryRewrite(TNode term,
381
                                         std::vector<SkolemLemma>& lems)
382
{
383
2513248
  NodeMap::iterator find = d_ppCache.find(term);
384
2513248
  if (find != d_ppCache.end())
385
  {
386
564360
    return (*find).second;
387
  }
388
1948888
  if (term.getNumChildren() == 0)
389
  {
390
1002829
    return preprocessWithProof(term, lems);
391
  }
392
  // should be in rewritten form here
393
946061
  Assert(term == Rewriter::rewrite(term));
394
946061
  Trace("theory-pp") << "ppTheoryRewrite { " << term << endl;
395
  // do not rewrite inside quantifiers
396
1892122
  Node newTerm = term;
397
946061
  if (!term.isClosure())
398
  {
399
1840118
    NodeBuilder<> newNode(term.getKind());
400
920059
    if (term.getMetaKind() == kind::metakind::PARAMETERIZED)
401
    {
402
140705
      newNode << term.getOperator();
403
    }
404
2884037
    for (const Node& nt : term)
405
    {
406
1963978
      newNode << ppTheoryRewrite(nt, lems);
407
    }
408
920047
    newTerm = Node(newNode);
409
920047
    newTerm = rewriteWithProof(newTerm, d_tpg.get(), false);
410
  }
411
946049
  newTerm = preprocessWithProof(newTerm, lems);
412
946042
  d_ppCache[term] = newTerm;
413
946042
  Trace("theory-pp") << "ppTheoryRewrite returning " << newTerm << "}" << endl;
414
946042
  return newTerm;
415
}
416
417
3603929
Node TheoryPreprocessor::rewriteWithProof(Node term,
418
                                          TConvProofGenerator* pg,
419
                                          bool isPre)
420
{
421
3603929
  Node termr = Rewriter::rewrite(term);
422
  // store rewrite step if tracking proofs and it rewrites
423
3603929
  if (isProofEnabled())
424
  {
425
    // may rewrite the same term more than once, thus check hasRewriteStep
426
467569
    if (termr != term)
427
    {
428
65364
      Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (rewriting) "
429
32682
                         << term << " -> " << termr << std::endl;
430
      // always use term context hash 0 (default)
431
32682
      pg->addRewriteStep(term, termr, PfRule::REWRITE, {}, {term}, isPre);
432
    }
433
  }
434
3603929
  return termr;
435
}
436
437
1948876
Node TheoryPreprocessor::preprocessWithProof(Node term,
438
                                             std::vector<SkolemLemma>& lems)
439
{
440
  // Important that it is in rewritten form, to ensure that the rewrite steps
441
  // recorded in d_tpg are functional. In other words, there should not
442
  // be steps from the same term to multiple rewritten forms, which would be
443
  // the case if we registered a preprocessing step for a non-rewritten term.
444
1948876
  Assert(term == Rewriter::rewrite(term));
445
3897752
  Trace("tpp-debug2") << "preprocessWithProof " << term
446
1948876
                      << ", #lems = " << lems.size() << std::endl;
447
  // We never call ppRewrite on equalities here, since equalities have a
448
  // special status. In particular, notice that theory preprocessing can be
449
  // called on all formulas asserted to theory engine, including those generated
450
  // as new literals appearing in lemmas. Calling ppRewrite on equalities is
451
  // incompatible with theory combination where a split on equality requested
452
  // by a theory could be preprocessed to something else, thus making theory
453
  // combination either non-terminating or result in solution soundness.
454
  // Notice that an alternative solution is to ensure that certain lemmas
455
  // (e.g. splits from theory combination) can never have theory preprocessing
456
  // applied to them. However, it is more uniform to say that theory
457
  // preprocessing is applied to all formulas. This makes it so that e.g.
458
  // theory solvers do not need to specify whether they want their lemmas to
459
  // be theory-preprocessed or not.
460
1948876
  if (term.getKind() == kind::EQUAL)
461
  {
462
293647
    return term;
463
  }
464
  // call ppRewrite for the given theory
465
3310458
  TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term, lems);
466
3310440
  Trace("tpp-debug2") << "preprocessWithProof returned " << trn
467
1655220
                      << ", #lems = " << lems.size() << std::endl;
468
1655220
  if (trn.isNull())
469
  {
470
    // no change, return
471
1650207
    return term;
472
  }
473
10026
  Node termr = trn.getNode();
474
5013
  Assert(term != termr);
475
5013
  if (isProofEnabled())
476
  {
477
1022
    registerTrustedRewrite(trn, d_tpg.get(), false);
478
  }
479
  // Rewrite again here, which notice is a *pre* rewrite.
480
5013
  termr = rewriteWithProof(termr, d_tpg.get(), true);
481
5013
  return ppTheoryRewrite(termr, lems);
482
}
483
484
4620970
bool TheoryPreprocessor::isProofEnabled() const { return d_tpg != nullptr; }
485
486
67839
void TheoryPreprocessor::registerTrustedRewrite(TrustNode trn,
487
                                                TConvProofGenerator* pg,
488
                                                bool isPre)
489
{
490
67839
  if (!isProofEnabled() || trn.isNull())
491
  {
492
55387
    return;
493
  }
494
12452
  Assert(trn.getKind() == TrustNodeKind::REWRITE);
495
24904
  Node eq = trn.getProven();
496
24904
  Node term = eq[0];
497
24904
  Node termr = eq[1];
498
12452
  if (trn.getGenerator() != nullptr)
499
  {
500
22864
    Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (generator) "
501
11432
                       << term << " -> " << termr << std::endl;
502
11432
    trn.debugCheckClosed("tpp-debug",
503
                         "TheoryPreprocessor::preprocessWithProof");
504
    // always use term context hash 0 (default)
505
11432
    pg->addRewriteStep(
506
        term, termr, trn.getGenerator(), isPre, PfRule::ASSUME, true);
507
  }
508
  else
509
  {
510
2040
    Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (trusted) "
511
1020
                       << term << " -> " << termr << std::endl;
512
    // small step trust
513
2040
    pg->addRewriteStep(term,
514
                       termr,
515
                       PfRule::THEORY_PREPROCESS,
516
                       {},
517
                       {term.eqNode(termr)},
518
1020
                       isPre);
519
  }
520
}
521
522
}  // namespace theory
523
26685
}  // namespace CVC4