GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/term_formula_removal.cpp Lines: 209 225 92.9 %
Date: 2021-03-23 Branches: 422 904 46.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file term_formula_removal.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Dejan Jovanovic, Mudathir Mohamed
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 Removal of term formulas
13
 **
14
 ** Removal of term formulas.
15
 **/
16
#include "smt/term_formula_removal.h"
17
18
#include <vector>
19
20
#include "expr/attribute.h"
21
#include "expr/lazy_proof.h"
22
#include "expr/node_algorithm.h"
23
#include "expr/skolem_manager.h"
24
#include "expr/term_context_stack.h"
25
#include "expr/term_conversion_proof_generator.h"
26
#include "options/smt_options.h"
27
#include "proof/proof_manager.h"
28
29
using namespace std;
30
31
namespace CVC4 {
32
33
9029
RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u,
34
9029
                                       ProofNodeManager* pnm)
35
    : d_tfCache(u),
36
      d_skolem_cache(u),
37
      d_pnm(pnm),
38
      d_tpg(nullptr),
39
9029
      d_lp(nullptr)
40
{
41
  // enable proofs if necessary
42
9029
  if (d_pnm != nullptr)
43
  {
44
1932
    d_tpg.reset(
45
        new TConvProofGenerator(d_pnm,
46
                                nullptr,
47
                                TConvPolicy::FIXPOINT,
48
                                TConvCachePolicy::NEVER,
49
                                "RemoveTermFormulas::TConvProofGenerator",
50
966
                                &d_rtfc));
51
1932
    d_lp.reset(new LazyCDProof(
52
966
        d_pnm, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof"));
53
  }
54
9029
}
55
56
9026
RemoveTermFormulas::~RemoveTermFormulas() {}
57
58
544574
theory::TrustNode RemoveTermFormulas::run(
59
    TNode assertion,
60
    std::vector<theory::TrustNode>& newAsserts,
61
    std::vector<Node>& newSkolems,
62
    bool fixedPoint)
63
{
64
1089148
  Node itesRemoved = runInternal(assertion, newAsserts, newSkolems);
65
544574
  Assert(newAsserts.size() == newSkolems.size());
66
544574
  if (itesRemoved == assertion)
67
  {
68
478656
    return theory::TrustNode::null();
69
  }
70
  // if running to fixed point, we run each new assertion through the
71
  // run lemma method
72
65918
  if (fixedPoint)
73
  {
74
1
    size_t i = 0;
75
649
    while (i < newAsserts.size())
76
    {
77
648
      theory::TrustNode trn = newAsserts[i];
78
      // do not run to fixed point on subcall, since we are processing all
79
      // lemmas in this loop
80
324
      newAsserts[i] = runLemma(trn, newAsserts, newSkolems, false);
81
324
      i++;
82
    }
83
  }
84
  // The rewriting of assertion can be justified by the term conversion proof
85
  // generator d_tpg.
86
65918
  return theory::TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get());
87
}
88
89
theory::TrustNode RemoveTermFormulas::run(TNode assertion)
90
{
91
  std::vector<theory::TrustNode> newAsserts;
92
  std::vector<Node> newSkolems;
93
  return run(assertion, newAsserts, newSkolems, false);
94
}
95
96
324
theory::TrustNode RemoveTermFormulas::runLemma(
97
    theory::TrustNode lem,
98
    std::vector<theory::TrustNode>& newAsserts,
99
    std::vector<Node>& newSkolems,
100
    bool fixedPoint)
101
{
102
  theory::TrustNode trn =
103
648
      run(lem.getProven(), newAsserts, newSkolems, fixedPoint);
104
324
  if (trn.isNull())
105
  {
106
    // no change
107
68
    return lem;
108
  }
109
256
  Assert(trn.getKind() == theory::TrustNodeKind::REWRITE);
110
512
  Node newAssertion = trn.getNode();
111
256
  if (!isProofEnabled())
112
  {
113
    // proofs not enabled, just take result
114
256
    return theory::TrustNode::mkTrustLemma(newAssertion, nullptr);
115
  }
116
  Trace("rtf-proof-debug")
117
      << "RemoveTermFormulas::run: setup proof for processed new lemma"
118
      << std::endl;
119
  Node assertionPre = lem.getProven();
120
  Node naEq = trn.getProven();
121
  // this method is applying this method to TrustNode whose generator is
122
  // already d_lp (from the run method above), in which case this link is
123
  // not necessary.
124
  if (trn.getGenerator() != d_lp.get())
125
  {
126
    d_lp->addLazyStep(naEq, trn.getGenerator());
127
  }
128
  // ---------------- from input  ------------------------------- from trn
129
  // assertionPre                 assertionPre = newAssertion
130
  // ------------------------------------------------------- EQ_RESOLVE
131
  // newAssertion
132
  d_lp->addStep(newAssertion, PfRule::EQ_RESOLVE, {assertionPre, naEq}, {});
133
  return theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get());
134
}
135
136
544574
Node RemoveTermFormulas::runInternal(TNode assertion,
137
                                     std::vector<theory::TrustNode>& output,
138
                                     std::vector<Node>& newSkolems)
139
{
140
544574
  NodeManager* nm = NodeManager::currentNM();
141
1089148
  TCtxStack ctx(&d_rtfc);
142
1089148
  std::vector<bool> processedChildren;
143
544574
  ctx.pushInitial(assertion);
144
544574
  processedChildren.push_back(false);
145
1089148
  std::pair<Node, uint32_t> initial = ctx.getCurrent();
146
1089148
  std::pair<Node, uint32_t> curr;
147
1089148
  Node node;
148
  uint32_t nodeVal;
149
544574
  TermFormulaCache::const_iterator itc;
150
7511540
  while (!ctx.empty())
151
  {
152
3483483
    curr = ctx.getCurrent();
153
3483483
    itc = d_tfCache.find(curr);
154
3483483
    node = curr.first;
155
3483483
    nodeVal = curr.second;
156
3483483
    Trace("rtf-debug") << "Visit " << node << ", " << nodeVal << std::endl;
157
4859947
    if (itc != d_tfCache.end())
158
    {
159
1376464
      Trace("rtf-debug") << "...already computed" << std::endl;
160
1376464
      ctx.pop();
161
1376464
      processedChildren.pop_back();
162
      // already computed
163
3947128
      continue;
164
    }
165
    // if we have yet to process children
166
2107019
    if (!processedChildren.back())
167
    {
168
      // check if we should replace the current node
169
2388400
      theory::TrustNode newLem;
170
2388400
      Node currt = runCurrent(curr, newLem);
171
      // if we replaced by a skolem, we do not recurse
172
1194200
      if (!currt.isNull())
173
      {
174
        // if this is the first time we've seen this term, we have a new lemma
175
        // which we add to our vectors
176
33295
        if (!newLem.isNull())
177
        {
178
28120
          output.push_back(newLem);
179
28120
          newSkolems.push_back(currt);
180
        }
181
33295
        Trace("rtf-debug") << "...replace by skolem" << std::endl;
182
33295
        d_tfCache.insert(curr, currt);
183
33295
        ctx.pop();
184
33295
        processedChildren.pop_back();
185
      }
186
1160905
      else if (node.isClosure())
187
      {
188
        // currently, we never do any term formula removal in quantifier bodies
189
25453
        d_tfCache.insert(curr, node);
190
      }
191
      else
192
      {
193
1135452
        size_t nchild = node.getNumChildren();
194
1135452
        if (nchild > 0)
195
        {
196
912819
          Trace("rtf-debug") << "...recurse to children" << std::endl;
197
          // recurse if we have children
198
912819
          processedChildren[processedChildren.size() - 1] = true;
199
2913456
          for (size_t i = 0; i < nchild; i++)
200
          {
201
2000637
            ctx.pushChild(node, nodeVal, i);
202
2000637
            processedChildren.push_back(false);
203
          }
204
        }
205
        else
206
        {
207
222633
          Trace("rtf-debug") << "...base case" << std::endl;
208
222633
          d_tfCache.insert(curr, node);
209
222633
          ctx.pop();
210
222633
          processedChildren.pop_back();
211
        }
212
      }
213
1194200
      continue;
214
    }
215
912819
    Trace("rtf-debug") << "...reconstruct" << std::endl;
216
    // otherwise, we are now finished processing children, pop the current node
217
    // and compute the result
218
912819
    ctx.pop();
219
912819
    processedChildren.pop_back();
220
    // if we have not already computed the result
221
1825638
    std::vector<Node> newChildren;
222
912819
    bool childChanged = false;
223
912819
    if (node.getMetaKind() == kind::metakind::PARAMETERIZED)
224
    {
225
148601
      newChildren.push_back(node.getOperator());
226
    }
227
    // reconstruct from the children
228
1825638
    std::pair<Node, uint32_t> currChild;
229
2913456
    for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; i++)
230
    {
231
      // recompute the value of the child
232
2000637
      uint32_t val = d_rtfc.computeValue(node, nodeVal, i);
233
2000637
      currChild = std::pair<Node, uint32_t>(node[i], val);
234
2000637
      itc = d_tfCache.find(currChild);
235
2000637
      Assert(itc != d_tfCache.end());
236
4001274
      Node newChild = (*itc).second;
237
2000637
      Assert(!newChild.isNull());
238
2000637
      childChanged |= (newChild != node[i]);
239
2000637
      newChildren.push_back(newChild);
240
    }
241
    // If changes, we reconstruct the node
242
1825638
    Node ret = node;
243
912819
    if (childChanged)
244
    {
245
109509
      ret = nm->mkNode(node.getKind(), newChildren);
246
    }
247
    // cache
248
912819
    d_tfCache.insert(curr, ret);
249
  }
250
544574
  itc = d_tfCache.find(initial);
251
544574
  Assert(itc != d_tfCache.end());
252
1089148
  return (*itc).second;
253
}
254
255
1194200
Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
256
                                    theory::TrustNode& newLem)
257
{
258
2388400
  TNode node = curr.first;
259
1194200
  uint32_t cval = curr.second;
260
  bool inQuant, inTerm;
261
1194200
  RtfTermContext::getFlags(curr.second, inQuant, inTerm);
262
2388400
  Debug("ite") << "removeITEs(" << node << ")"
263
1194200
               << " " << inQuant << " " << inTerm << std::endl;
264
1194200
  Assert(!inQuant);
265
266
1194200
  NodeManager *nodeManager = NodeManager::currentNM();
267
268
2388400
  TypeNode nodeType = node.getType();
269
2388400
  Node skolem;
270
2388400
  Node newAssertion;
271
  // the exists form of the assertion
272
1194200
  ProofGenerator* newAssertionPg = nullptr;
273
  // Handle non-Boolean ITEs here. Boolean ones (within terms) are handled
274
  // in the "non-variable Boolean term within term" case below.
275
1194200
  if (node.getKind() == kind::ITE && !nodeType.isBoolean())
276
  {
277
    // Here, we eliminate the ITE if we are not Boolean and if we are
278
    // not in a quantified formula. This policy should be in sync with
279
    // the policy for when to apply theory preprocessing to terms, see PR
280
    // #5497.
281
31664
    skolem = getSkolemForNode(node);
282
31664
    if (skolem.isNull())
283
    {
284
53018
      Trace("rtf-proof-debug")
285
26509
          << "RemoveTermFormulas::run: make ITE skolem" << std::endl;
286
      // Make the skolem to represent the ITE
287
26509
      SkolemManager* sm = nodeManager->getSkolemManager();
288
26509
      skolem = sm->mkPurifySkolem(
289
          node,
290
          "termITE",
291
          "a variable introduced due to term-level ITE removal");
292
26509
      d_skolem_cache.insert(node, skolem);
293
294
      // Notice that in very rare cases, two different terms may have the
295
      // same purification skolem (see SkolemManager::mkPurifySkolem) For such
296
      // cases, for simplicity, we repeat the work of constructing the
297
      // assertion and proofs below. This is so that the proof for the new form
298
      // of the lemma is used.
299
300
      // The new assertion
301
79527
      newAssertion = nodeManager->mkNode(
302
106036
          kind::ITE, node[0], skolem.eqNode(node[1]), skolem.eqNode(node[2]));
303
304
      // we justify it internally
305
26509
      if (isProofEnabled())
306
      {
307
7686
        Trace("rtf-proof-debug")
308
3843
            << "RemoveTermFormulas::run: justify " << newAssertion
309
3843
            << " with ITE axiom" << std::endl;
310
        // ---------------------- REMOVE_TERM_FORMULA_AXIOM
311
        // (ite node[0]
312
        //      (= node node[1])            ------------- MACRO_SR_PRED_INTRO
313
        //      (= node node[2]))           node = skolem
314
        // ------------------------------------------ MACRO_SR_PRED_TRANSFORM
315
        // (ite node[0] (= skolem node[1]) (= skolem node[2]))
316
        //
317
        // Note that the MACRO_SR_PRED_INTRO step holds due to conversion
318
        // of skolem into its witness form, which is node.
319
7686
        Node axiom = getAxiomFor(node);
320
3843
        d_lp->addStep(axiom, PfRule::REMOVE_TERM_FORMULA_AXIOM, {}, {node});
321
7686
        Node eq = node.eqNode(skolem);
322
3843
        d_lp->addStep(eq, PfRule::MACRO_SR_PRED_INTRO, {}, {eq});
323
15372
        d_lp->addStep(newAssertion,
324
                      PfRule::MACRO_SR_PRED_TRANSFORM,
325
                      {axiom, eq},
326
11529
                      {newAssertion});
327
3843
        newAssertionPg = d_lp.get();
328
      }
329
    }
330
  }
331
1162536
  else if (node.getKind() == kind::LAMBDA)
332
  {
333
    // if a lambda, do lambda-lifting
334
18
    if (!expr::hasFreeVar(node))
335
    {
336
18
      skolem = getSkolemForNode(node);
337
18
      if (skolem.isNull())
338
      {
339
36
        Trace("rtf-proof-debug")
340
18
            << "RemoveTermFormulas::run: make LAMBDA skolem" << std::endl;
341
        // Make the skolem to represent the lambda
342
18
        SkolemManager* sm = nodeManager->getSkolemManager();
343
18
        skolem = sm->mkPurifySkolem(
344
            node,
345
            "lambdaF",
346
            "a function introduced due to term-level lambda removal");
347
18
        d_skolem_cache.insert(node, skolem);
348
349
        // The new assertion
350
36
        std::vector<Node> children;
351
        // bound variable list
352
18
        children.push_back(node[0]);
353
        // body
354
36
        std::vector<Node> skolem_app_c;
355
18
        skolem_app_c.push_back(skolem);
356
18
        skolem_app_c.insert(skolem_app_c.end(), node[0].begin(), node[0].end());
357
36
        Node skolem_app = nodeManager->mkNode(kind::APPLY_UF, skolem_app_c);
358
18
        children.push_back(skolem_app.eqNode(node[1]));
359
        // axiom defining skolem
360
18
        newAssertion = nodeManager->mkNode(kind::FORALL, children);
361
362
        // Lambda lifting is trivial to justify, hence we don't set a proof
363
        // generator here. In particular, replacing the skolem introduced
364
        // here with its original lambda ensures the new assertion rewrites
365
        // to true.
366
        // For example, if (lambda y. t[y]) has skolem k, then this lemma is:
367
        //   forall x. k(x)=t[x]
368
        // whose witness form rewrites
369
        //   forall x. (lambda y. t[y])(x)=t[x] --> forall x. t[x]=t[x] --> true
370
      }
371
    }
372
  }
373
1162518
  else if (node.getKind() == kind::WITNESS)
374
  {
375
    // If a witness choice
376
    //   For details on this operator, see
377
    //   http://planetmath.org/hilbertsvarepsilonoperator.
378
572
    if (!expr::hasFreeVar(node))
379
    {
380
      // NOTE: we can replace by t if body is of the form (and (= z t) ...)
381
572
      skolem = getSkolemForNode(node);
382
572
      if (skolem.isNull())
383
      {
384
1104
        Trace("rtf-proof-debug")
385
552
            << "RemoveTermFormulas::run: make WITNESS skolem" << std::endl;
386
        // Make the skolem to witness the choice, which notice is handled
387
        // as a special case within SkolemManager::mkPurifySkolem.
388
552
        SkolemManager* sm = nodeManager->getSkolemManager();
389
552
        skolem = sm->mkPurifySkolem(
390
            node,
391
            "witnessK",
392
            "a skolem introduced due to term-level witness removal");
393
552
        d_skolem_cache.insert(node, skolem);
394
395
552
        Assert(node[0].getNumChildren() == 1);
396
397
        // The new assertion is the assumption that the body
398
        // of the witness operator holds for the Skolem
399
552
        newAssertion = node[1].substitute(node[0][0], skolem);
400
401
        // Get the proof generator, if one exists, which was responsible for
402
        // constructing this witness term. This may not exist, in which case
403
        // the witness term was trivial to justify. This is the case e.g. for
404
        // purification witness terms.
405
552
        if (isProofEnabled())
406
        {
407
          Node existsAssertion =
408
46
              nodeManager->mkNode(kind::EXISTS, node[0], node[1]);
409
          // -------------------- from skolem manager
410
          // (exists x. node[1])
411
          // -------------------- SKOLEMIZE
412
          // node[1] * { x -> skolem }
413
23
          ProofGenerator* expg = sm->getProofGenerator(existsAssertion);
414
23
          d_lp->addLazyStep(existsAssertion,
415
                            expg,
416
                            PfRule::WITNESS_AXIOM,
417
                            true,
418
                            "RemoveTermFormulas::run:skolem_pf");
419
23
          d_lp->addStep(newAssertion, PfRule::SKOLEMIZE, {existsAssertion}, {});
420
23
          newAssertionPg = d_lp.get();
421
        }
422
      }
423
    }
424
  }
425
3484371
  else if (node.getKind() != kind::BOOLEAN_TERM_VARIABLE && nodeType.isBoolean()
426
1727824
           && inTerm)
427
  {
428
    // if a non-variable Boolean term within another term, replace it
429
1041
    skolem = getSkolemForNode(node);
430
1041
    if (skolem.isNull())
431
    {
432
2082
      Trace("rtf-proof-debug")
433
1041
          << "RemoveTermFormulas::run: make BOOLEAN_TERM_VARIABLE skolem"
434
1041
          << std::endl;
435
      // Make the skolem to represent the Boolean term
436
      // Skolems introduced for Boolean formulas appearing in terms have a
437
      // special kind (BOOLEAN_TERM_VARIABLE) that ensures they are handled
438
      // properly in theory combination. We must use this kind here instead of a
439
      // generic skolem. Notice that the name/comment are currently ignored
440
      // within SkolemManager::mkPurifySkolem, since BOOLEAN_TERM_VARIABLE
441
      // variables cannot be given names.
442
1041
      SkolemManager* sm = nodeManager->getSkolemManager();
443
1041
      skolem = sm->mkPurifySkolem(
444
          node,
445
          "btvK",
446
          "a Boolean term variable introduced during term formula removal",
447
          NodeManager::SKOLEM_BOOL_TERM_VAR);
448
1041
      d_skolem_cache.insert(node, skolem);
449
450
      // The new assertion
451
1041
      newAssertion = skolem.eqNode(node);
452
453
      // Boolean term removal is trivial to justify, hence we don't set a proof
454
      // generator here. It is trivial to justify since it is an instance of
455
      // purification, which is justified by conversion to witness forms.
456
    }
457
  }
458
459
  // if the term should be replaced by a skolem
460
1194200
  if( !skolem.isNull() ){
461
    // this must be done regardless of whether the assertion was new below,
462
    // since a formula-term may rewrite to the same skolem in multiple contexts.
463
33295
    if (isProofEnabled())
464
    {
465
      // justify the introduction of the skolem
466
      // ------------------- MACRO_SR_PRED_INTRO
467
      // t = witness x. x=t
468
      // The above step is trivial, since the skolems introduced above are
469
      // all purification skolems. We record this equality in the term
470
      // conversion proof generator.
471
9430
      d_tpg->addRewriteStep(node,
472
                            skolem,
473
                            PfRule::MACRO_SR_PRED_INTRO,
474
                            {},
475
                            {node.eqNode(skolem)},
476
                            true,
477
4715
                            cval);
478
    }
479
480
    // if the skolem was introduced in this call
481
33295
    if (!newAssertion.isNull())
482
    {
483
56240
      Trace("rtf-proof-debug")
484
28120
          << "RemoveTermFormulas::run: setup proof for new assertion "
485
28120
          << newAssertion << std::endl;
486
      // if proofs are enabled
487
28120
      if (isProofEnabled())
488
      {
489
        // justify the axiom that defines the skolem, if not already done so
490
3986
        if (newAssertionPg == nullptr)
491
        {
492
          // Should have trivial justification if not yet provided. This is the
493
          // case of lambda lifting and Boolean term removal.
494
          // ---------------- MACRO_SR_PRED_INTRO
495
          // newAssertion
496
240
          d_lp->addStep(
497
120
              newAssertion, PfRule::MACRO_SR_PRED_INTRO, {}, {newAssertion});
498
        }
499
      }
500
56240
      Trace("rtf-debug") << "*** term formula removal introduced " << skolem
501
28120
                         << " for " << node << std::endl;
502
503
28120
      newLem = theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get());
504
505
28120
      Trace("rtf-proof-debug") << "Checking closed..." << std::endl;
506
28120
      newLem.debugCheckClosed("rtf-proof-debug",
507
                              "RemoveTermFormulas::run:new_assert");
508
    }
509
510
    // The representation is now the skolem
511
33295
    return skolem;
512
  }
513
514
  // return null, indicating we will traverse children within runInternal
515
1160905
  return Node::null();
516
}
517
518
33295
Node RemoveTermFormulas::getSkolemForNode(Node k) const
519
{
520
  context::CDInsertHashMap<Node, Node, NodeHashFunction>::const_iterator itk =
521
33295
      d_skolem_cache.find(k);
522
33295
  if (itk != d_skolem_cache.end())
523
  {
524
5175
    return itk->second;
525
  }
526
28120
  return Node::null();
527
}
528
529
8607
Node RemoveTermFormulas::getAxiomFor(Node n)
530
{
531
8607
  NodeManager* nm = NodeManager::currentNM();
532
8607
  Kind k = n.getKind();
533
8607
  if (k == kind::ITE)
534
  {
535
8607
    return nm->mkNode(kind::ITE, n[0], n.eqNode(n[1]), n.eqNode(n[2]));
536
  }
537
  return Node::null();
538
}
539
540
ProofGenerator* RemoveTermFormulas::getTConvProofGenerator()
541
{
542
  return d_tpg.get();
543
}
544
545
88732
bool RemoveTermFormulas::isProofEnabled() const { return d_pnm != nullptr; }
546
547
26685
}/* CVC4 namespace */