GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/term_formula_removal.cpp Lines: 268 285 94.0 %
Date: 2021-03-22 Branches: 499 1060 47.1 %

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
9027
RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u,
34
9027
                                       ProofNodeManager* pnm)
35
    : d_tfCache(u),
36
      d_skolem_cache(u),
37
      d_lemmaCache(u),
38
      d_pnm(pnm),
39
      d_tpg(nullptr),
40
9027
      d_lp(nullptr)
41
{
42
  // enable proofs if necessary
43
9027
  if (d_pnm != nullptr)
44
  {
45
1932
    d_tpg.reset(
46
        new TConvProofGenerator(d_pnm,
47
                                nullptr,
48
                                TConvPolicy::FIXPOINT,
49
                                TConvCachePolicy::NEVER,
50
                                "RemoveTermFormulas::TConvProofGenerator",
51
966
                                &d_rtfc));
52
1932
    d_lp.reset(new LazyCDProof(
53
966
        d_pnm, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof"));
54
  }
55
9027
}
56
57
9024
RemoveTermFormulas::~RemoveTermFormulas() {}
58
59
544172
theory::TrustNode RemoveTermFormulas::run(
60
    TNode assertion,
61
    std::vector<theory::TrustNode>& newAsserts,
62
    std::vector<Node>& newSkolems,
63
    bool fixedPoint)
64
{
65
1088344
  Node itesRemoved = runInternal(assertion, newAsserts, newSkolems);
66
544172
  Assert(newAsserts.size() == newSkolems.size());
67
544172
  if (itesRemoved == assertion)
68
  {
69
478276
    return theory::TrustNode::null();
70
  }
71
  // if running to fixed point, we run each new assertion through the
72
  // run lemma method
73
65896
  if (fixedPoint)
74
  {
75
1
    size_t i = 0;
76
649
    while (i < newAsserts.size())
77
    {
78
648
      theory::TrustNode trn = newAsserts[i];
79
      // do not run to fixed point on subcall, since we are processing all
80
      // lemmas in this loop
81
324
      newAsserts[i] = runLemma(trn, newAsserts, newSkolems, false);
82
324
      i++;
83
    }
84
  }
85
  // The rewriting of assertion can be justified by the term conversion proof
86
  // generator d_tpg.
87
65896
  return theory::TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get());
88
}
89
90
theory::TrustNode RemoveTermFormulas::run(TNode assertion)
91
{
92
  std::vector<theory::TrustNode> newAsserts;
93
  std::vector<Node> newSkolems;
94
  return run(assertion, newAsserts, newSkolems, false);
95
}
96
97
324
theory::TrustNode RemoveTermFormulas::runLemma(
98
    theory::TrustNode lem,
99
    std::vector<theory::TrustNode>& newAsserts,
100
    std::vector<Node>& newSkolems,
101
    bool fixedPoint)
102
{
103
  theory::TrustNode trn =
104
648
      run(lem.getProven(), newAsserts, newSkolems, fixedPoint);
105
324
  if (trn.isNull())
106
  {
107
    // no change
108
68
    return lem;
109
  }
110
256
  Assert(trn.getKind() == theory::TrustNodeKind::REWRITE);
111
512
  Node newAssertion = trn.getNode();
112
256
  if (!isProofEnabled())
113
  {
114
    // proofs not enabled, just take result
115
256
    return theory::TrustNode::mkTrustLemma(newAssertion, nullptr);
116
  }
117
  Trace("rtf-proof-debug")
118
      << "RemoveTermFormulas::run: setup proof for processed new lemma"
119
      << std::endl;
120
  Node assertionPre = lem.getProven();
121
  Node naEq = trn.getProven();
122
  // this method is applying this method to TrustNode whose generator is
123
  // already d_lp (from the run method above), in which case this link is
124
  // not necessary.
125
  if (trn.getGenerator() != d_lp.get())
126
  {
127
    d_lp->addLazyStep(naEq, trn.getGenerator());
128
  }
129
  // ---------------- from input  ------------------------------- from trn
130
  // assertionPre                 assertionPre = newAssertion
131
  // ------------------------------------------------------- EQ_RESOLVE
132
  // newAssertion
133
  d_lp->addStep(newAssertion, PfRule::EQ_RESOLVE, {assertionPre, naEq}, {});
134
  return theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get());
135
}
136
137
544172
Node RemoveTermFormulas::runInternal(TNode assertion,
138
                                     std::vector<theory::TrustNode>& output,
139
                                     std::vector<Node>& newSkolems)
140
{
141
544172
  NodeManager* nm = NodeManager::currentNM();
142
1088344
  TCtxStack ctx(&d_rtfc);
143
1088344
  std::vector<bool> processedChildren;
144
544172
  ctx.pushInitial(assertion);
145
544172
  processedChildren.push_back(false);
146
1088344
  std::pair<Node, uint32_t> initial = ctx.getCurrent();
147
1088344
  std::pair<Node, uint32_t> curr;
148
1088344
  Node node;
149
  uint32_t nodeVal;
150
544172
  TermFormulaCache::const_iterator itc;
151
7507322
  while (!ctx.empty())
152
  {
153
3481575
    curr = ctx.getCurrent();
154
3481575
    itc = d_tfCache.find(curr);
155
3481575
    node = curr.first;
156
3481575
    nodeVal = curr.second;
157
3481575
    Trace("rtf-debug") << "Visit " << node << ", " << nodeVal << std::endl;
158
4857279
    if (itc != d_tfCache.end())
159
    {
160
1375704
      Trace("rtf-debug") << "...already computed" << std::endl;
161
1375704
      ctx.pop();
162
1375704
      processedChildren.pop_back();
163
      // already computed
164
3944978
      continue;
165
    }
166
    // if we have yet to process children
167
2105871
    if (!processedChildren.back())
168
    {
169
      // check if we should replace the current node
170
2387140
      theory::TrustNode newLem;
171
2387140
      Node currt = runCurrent(curr, newLem);
172
      // if we replaced by a skolem, we do not recurse
173
1193570
      if (!currt.isNull())
174
      {
175
        // if this is the first time we've seen this term, we have a new lemma
176
        // which we add to our vectors
177
33279
        if (!newLem.isNull())
178
        {
179
28110
          output.push_back(newLem);
180
28110
          newSkolems.push_back(currt);
181
        }
182
33279
        Trace("rtf-debug") << "...replace by skolem" << std::endl;
183
33279
        d_tfCache.insert(curr, currt);
184
33279
        ctx.pop();
185
33279
        processedChildren.pop_back();
186
      }
187
1160291
      else if (node.isClosure())
188
      {
189
        // currently, we never do any term formula removal in quantifier bodies
190
25451
        d_tfCache.insert(curr, node);
191
      }
192
      else
193
      {
194
1134840
        size_t nchild = node.getNumChildren();
195
1134840
        if (nchild > 0)
196
        {
197
912301
          Trace("rtf-debug") << "...recurse to children" << std::endl;
198
          // recurse if we have children
199
912301
          processedChildren[processedChildren.size() - 1] = true;
200
2911952
          for (size_t i = 0; i < nchild; i++)
201
          {
202
1999651
            ctx.pushChild(node, nodeVal, i);
203
1999651
            processedChildren.push_back(false);
204
          }
205
        }
206
        else
207
        {
208
222539
          Trace("rtf-debug") << "...base case" << std::endl;
209
222539
          d_tfCache.insert(curr, node);
210
222539
          ctx.pop();
211
222539
          processedChildren.pop_back();
212
        }
213
      }
214
1193570
      continue;
215
    }
216
912301
    Trace("rtf-debug") << "...reconstruct" << std::endl;
217
    // otherwise, we are now finished processing children, pop the current node
218
    // and compute the result
219
912301
    ctx.pop();
220
912301
    processedChildren.pop_back();
221
    // if we have not already computed the result
222
1824602
    std::vector<Node> newChildren;
223
912301
    bool childChanged = false;
224
912301
    if (node.getMetaKind() == kind::metakind::PARAMETERIZED)
225
    {
226
148582
      newChildren.push_back(node.getOperator());
227
    }
228
    // reconstruct from the children
229
1824602
    std::pair<Node, uint32_t> currChild;
230
2911952
    for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; i++)
231
    {
232
      // recompute the value of the child
233
1999651
      uint32_t val = d_rtfc.computeValue(node, nodeVal, i);
234
1999651
      currChild = std::pair<Node, uint32_t>(node[i], val);
235
1999651
      itc = d_tfCache.find(currChild);
236
1999651
      Assert(itc != d_tfCache.end());
237
3999302
      Node newChild = (*itc).second;
238
1999651
      Assert(!newChild.isNull());
239
1999651
      childChanged |= (newChild != node[i]);
240
1999651
      newChildren.push_back(newChild);
241
    }
242
    // If changes, we reconstruct the node
243
1824602
    Node ret = node;
244
912301
    if (childChanged)
245
    {
246
109483
      ret = nm->mkNode(node.getKind(), newChildren);
247
    }
248
    // cache
249
912301
    d_tfCache.insert(curr, ret);
250
  }
251
544172
  itc = d_tfCache.find(initial);
252
544172
  Assert(itc != d_tfCache.end());
253
1088344
  return (*itc).second;
254
}
255
256
1193570
Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
257
                                    theory::TrustNode& newLem)
258
{
259
2387140
  TNode node = curr.first;
260
1193570
  uint32_t cval = curr.second;
261
  bool inQuant, inTerm;
262
1193570
  RtfTermContext::getFlags(curr.second, inQuant, inTerm);
263
2387140
  Debug("ite") << "removeITEs(" << node << ")"
264
1193570
               << " " << inQuant << " " << inTerm << std::endl;
265
1193570
  Assert(!inQuant);
266
267
1193570
  NodeManager *nodeManager = NodeManager::currentNM();
268
269
2387140
  TypeNode nodeType = node.getType();
270
2387140
  Node skolem;
271
2387140
  Node newAssertion;
272
  // the exists form of the assertion
273
1193570
  ProofGenerator* newAssertionPg = nullptr;
274
  // Handle non-Boolean ITEs here. Boolean ones (within terms) are handled
275
  // in the "non-variable Boolean term within term" case below.
276
1193570
  if (node.getKind() == kind::ITE && !nodeType.isBoolean())
277
  {
278
    // Here, we eliminate the ITE if we are not Boolean and if we are
279
    // not in a quantified formula. This policy should be in sync with
280
    // the policy for when to apply theory preprocessing to terms, see PR
281
    // #5497.
282
31648
    skolem = getSkolemForNode(node);
283
31648
    if (skolem.isNull())
284
    {
285
52998
      Trace("rtf-proof-debug")
286
26499
          << "RemoveTermFormulas::run: make ITE skolem" << std::endl;
287
      // Make the skolem to represent the ITE
288
26499
      SkolemManager* sm = nodeManager->getSkolemManager();
289
26499
      skolem = sm->mkPurifySkolem(
290
          node,
291
          "termITE",
292
          "a variable introduced due to term-level ITE removal");
293
26499
      d_skolem_cache.insert(node, skolem);
294
295
      // The new assertion
296
79497
      newAssertion = nodeManager->mkNode(
297
105996
          kind::ITE, node[0], skolem.eqNode(node[1]), skolem.eqNode(node[2]));
298
299
      // we justify it internally
300
26499
      if (isProofEnabled())
301
      {
302
7686
        Trace("rtf-proof-debug")
303
3843
            << "RemoveTermFormulas::run: justify " << newAssertion
304
3843
            << " with ITE axiom" << std::endl;
305
        // ---------------------- REMOVE_TERM_FORMULA_AXIOM
306
        // (ite node[0]
307
        //      (= node node[1])            ------------- MACRO_SR_PRED_INTRO
308
        //      (= node node[2]))           node = skolem
309
        // ------------------------------------------ MACRO_SR_PRED_TRANSFORM
310
        // (ite node[0] (= skolem node[1]) (= skolem node[2]))
311
        //
312
        // Note that the MACRO_SR_PRED_INTRO step holds due to conversion
313
        // of skolem into its witness form, which is node.
314
7686
        Node axiom = getAxiomFor(node);
315
3843
        d_lp->addStep(axiom, PfRule::REMOVE_TERM_FORMULA_AXIOM, {}, {node});
316
7686
        Node eq = node.eqNode(skolem);
317
3843
        d_lp->addStep(eq, PfRule::MACRO_SR_PRED_INTRO, {}, {eq});
318
15372
        d_lp->addStep(newAssertion,
319
                      PfRule::MACRO_SR_PRED_TRANSFORM,
320
                      {axiom, eq},
321
11529
                      {newAssertion});
322
3843
        newAssertionPg = d_lp.get();
323
      }
324
    }
325
  }
326
1161922
  else if (node.getKind() == kind::LAMBDA)
327
  {
328
    // if a lambda, do lambda-lifting
329
18
    if (!expr::hasFreeVar(node))
330
    {
331
18
      skolem = getSkolemForNode(node);
332
18
      if (skolem.isNull())
333
      {
334
36
        Trace("rtf-proof-debug")
335
18
            << "RemoveTermFormulas::run: make LAMBDA skolem" << std::endl;
336
        // Make the skolem to represent the lambda
337
18
        SkolemManager* sm = nodeManager->getSkolemManager();
338
18
        skolem = sm->mkPurifySkolem(
339
            node,
340
            "lambdaF",
341
            "a function introduced due to term-level lambda removal");
342
18
        d_skolem_cache.insert(node, skolem);
343
344
        // The new assertion
345
36
        std::vector<Node> children;
346
        // bound variable list
347
18
        children.push_back(node[0]);
348
        // body
349
36
        std::vector<Node> skolem_app_c;
350
18
        skolem_app_c.push_back(skolem);
351
18
        skolem_app_c.insert(skolem_app_c.end(), node[0].begin(), node[0].end());
352
36
        Node skolem_app = nodeManager->mkNode(kind::APPLY_UF, skolem_app_c);
353
18
        children.push_back(skolem_app.eqNode(node[1]));
354
        // axiom defining skolem
355
18
        newAssertion = nodeManager->mkNode(kind::FORALL, children);
356
357
        // Lambda lifting is trivial to justify, hence we don't set a proof
358
        // generator here. In particular, replacing the skolem introduced
359
        // here with its original lambda ensures the new assertion rewrites
360
        // to true.
361
        // For example, if (lambda y. t[y]) has skolem k, then this lemma is:
362
        //   forall x. k(x)=t[x]
363
        // whose witness form rewrites
364
        //   forall x. (lambda y. t[y])(x)=t[x] --> forall x. t[x]=t[x] --> true
365
      }
366
    }
367
  }
368
1161904
  else if (node.getKind() == kind::WITNESS)
369
  {
370
    // If a witness choice
371
    //   For details on this operator, see
372
    //   http://planetmath.org/hilbertsvarepsilonoperator.
373
572
    if (!expr::hasFreeVar(node))
374
    {
375
      // NOTE: we can replace by t if body is of the form (and (= z t) ...)
376
572
      skolem = getSkolemForNode(node);
377
572
      if (skolem.isNull())
378
      {
379
1104
        Trace("rtf-proof-debug")
380
552
            << "RemoveTermFormulas::run: make WITNESS skolem" << std::endl;
381
        // Make the skolem to witness the choice, which notice is handled
382
        // as a special case within SkolemManager::mkPurifySkolem.
383
552
        SkolemManager* sm = nodeManager->getSkolemManager();
384
552
        skolem = sm->mkPurifySkolem(
385
            node,
386
            "witnessK",
387
            "a skolem introduced due to term-level witness removal");
388
552
        d_skolem_cache.insert(node, skolem);
389
390
552
        Assert(node[0].getNumChildren() == 1);
391
392
        // The new assertion is the assumption that the body
393
        // of the witness operator holds for the Skolem
394
552
        newAssertion = node[1].substitute(node[0][0], skolem);
395
396
        // Get the proof generator, if one exists, which was responsible for
397
        // constructing this witness term. This may not exist, in which case
398
        // the witness term was trivial to justify. This is the case e.g. for
399
        // purification witness terms.
400
552
        if (isProofEnabled())
401
        {
402
          Node existsAssertion =
403
46
              nodeManager->mkNode(kind::EXISTS, node[0], node[1]);
404
          // -------------------- from skolem manager
405
          // (exists x. node[1])
406
          // -------------------- SKOLEMIZE
407
          // node[1] * { x -> skolem }
408
23
          ProofGenerator* expg = sm->getProofGenerator(existsAssertion);
409
23
          d_lp->addLazyStep(existsAssertion,
410
                            expg,
411
                            PfRule::WITNESS_AXIOM,
412
                            true,
413
                            "RemoveTermFormulas::run:skolem_pf");
414
23
          d_lp->addStep(newAssertion, PfRule::SKOLEMIZE, {existsAssertion}, {});
415
23
          newAssertionPg = d_lp.get();
416
        }
417
      }
418
    }
419
  }
420
3482529
  else if (node.getKind() != kind::BOOLEAN_TERM_VARIABLE && nodeType.isBoolean()
421
1726812
           && inTerm)
422
  {
423
    // if a non-variable Boolean term within another term, replace it
424
1041
    skolem = getSkolemForNode(node);
425
1041
    if (skolem.isNull())
426
    {
427
2082
      Trace("rtf-proof-debug")
428
1041
          << "RemoveTermFormulas::run: make BOOLEAN_TERM_VARIABLE skolem"
429
1041
          << std::endl;
430
      // Make the skolem to represent the Boolean term
431
      // Skolems introduced for Boolean formulas appearing in terms have a
432
      // special kind (BOOLEAN_TERM_VARIABLE) that ensures they are handled
433
      // properly in theory combination. We must use this kind here instead of a
434
      // generic skolem. Notice that the name/comment are currently ignored
435
      // within SkolemManager::mkPurifySkolem, since BOOLEAN_TERM_VARIABLE
436
      // variables cannot be given names.
437
1041
      SkolemManager* sm = nodeManager->getSkolemManager();
438
1041
      skolem = sm->mkPurifySkolem(
439
          node,
440
          "btvK",
441
          "a Boolean term variable introduced during term formula removal",
442
          NodeManager::SKOLEM_BOOL_TERM_VAR);
443
1041
      d_skolem_cache.insert(node, skolem);
444
445
      // The new assertion
446
1041
      newAssertion = skolem.eqNode(node);
447
448
      // Boolean term removal is trivial to justify, hence we don't set a proof
449
      // generator here. It is trivial to justify since it is an instance of
450
      // purification, which is justified by conversion to witness forms.
451
    }
452
  }
453
454
  // if the term should be replaced by a skolem
455
1193570
  if( !skolem.isNull() ){
456
    // this must be done regardless of whether the assertion was new below,
457
    // since a formula-term may rewrite to the same skolem in multiple contexts.
458
33279
    if (isProofEnabled())
459
    {
460
      // justify the introduction of the skolem
461
      // ------------------- MACRO_SR_PRED_INTRO
462
      // t = witness x. x=t
463
      // The above step is trivial, since the skolems introduced above are
464
      // all purification skolems. We record this equality in the term
465
      // conversion proof generator.
466
9430
      d_tpg->addRewriteStep(node,
467
                            skolem,
468
                            PfRule::MACRO_SR_PRED_INTRO,
469
                            {},
470
                            {node.eqNode(skolem)},
471
                            true,
472
4715
                            cval);
473
    }
474
475
    // if the skolem was introduced in this call
476
33279
    if (!newAssertion.isNull())
477
    {
478
56220
      Trace("rtf-proof-debug")
479
28110
          << "RemoveTermFormulas::run: setup proof for new assertion "
480
28110
          << newAssertion << std::endl;
481
      // if proofs are enabled
482
28110
      if (isProofEnabled())
483
      {
484
        // justify the axiom that defines the skolem, if not already done so
485
3986
        if (newAssertionPg == nullptr)
486
        {
487
          // Should have trivial justification if not yet provided. This is the
488
          // case of lambda lifting and Boolean term removal.
489
          // ---------------- MACRO_SR_PRED_INTRO
490
          // newAssertion
491
240
          d_lp->addStep(
492
120
              newAssertion, PfRule::MACRO_SR_PRED_INTRO, {}, {newAssertion});
493
        }
494
      }
495
56220
      Trace("rtf-debug") << "*** term formula removal introduced " << skolem
496
28110
                         << " for " << node << std::endl;
497
498
28110
      newLem = theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get());
499
500
      // store in the lemma cache
501
28110
      d_lemmaCache.insert(skolem, newLem);
502
503
28110
      Trace("rtf-proof-debug") << "Checking closed..." << std::endl;
504
28110
      newLem.debugCheckClosed("rtf-proof-debug",
505
                              "RemoveTermFormulas::run:new_assert");
506
    }
507
508
    // The representation is now the skolem
509
33279
    return skolem;
510
  }
511
512
  // return null, indicating we will traverse children within runInternal
513
1160291
  return Node::null();
514
}
515
516
33279
Node RemoveTermFormulas::getSkolemForNode(Node k) const
517
{
518
  context::CDInsertHashMap<Node, Node, NodeHashFunction>::const_iterator itk =
519
33279
      d_skolem_cache.find(k);
520
33279
  if (itk != d_skolem_cache.end())
521
  {
522
5169
    return itk->second;
523
  }
524
28110
  return Node::null();
525
}
526
527
struct HasSkolemTag
528
{
529
};
530
struct HasSkolemComputedTag
531
{
532
};
533
/** Attribute true for nodes with skolems in them */
534
typedef expr::Attribute<HasSkolemTag, bool> HasSkolemAttr;
535
/** Attribute true for nodes where we have computed the above attribute */
536
typedef expr::Attribute<HasSkolemComputedTag, bool> HasSkolemComputedAttr;
537
538
11471
bool RemoveTermFormulas::hasSkolems(TNode n) const
539
{
540
22942
  std::unordered_set<TNode, TNodeHashFunction> visited;
541
11471
  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
542
22942
  std::vector<TNode> visit;
543
22942
  TNode cur;
544
11471
  visit.push_back(n);
545
112006
  do
546
  {
547
123477
    cur = visit.back();
548
163305
    if (cur.getAttribute(HasSkolemComputedAttr()))
549
    {
550
39828
      visit.pop_back();
551
      // already computed
552
39828
      continue;
553
    }
554
83649
    it = visited.find(cur);
555
83649
    if (it == visited.end())
556
    {
557
47422
      visited.insert(cur);
558
47422
      if (cur.getNumChildren() == 0)
559
      {
560
11195
        visit.pop_back();
561
11195
        bool hasSkolem = false;
562
11195
        if (cur.isVar())
563
        {
564
8034
          hasSkolem = (d_lemmaCache.find(cur) != d_lemmaCache.end());
565
        }
566
11195
        cur.setAttribute(HasSkolemAttr(), hasSkolem);
567
11195
        cur.setAttribute(HasSkolemComputedAttr(), true);
568
      }
569
      else
570
      {
571
36227
        visit.insert(visit.end(), cur.begin(), cur.end());
572
      }
573
    }
574
    else
575
    {
576
36227
      visit.pop_back();
577
36227
      bool hasSkolem = false;
578
105217
      for (TNode i : cur)
579
      {
580
72703
        Assert(i.getAttribute(HasSkolemComputedAttr()));
581
72703
        if (i.getAttribute(HasSkolemAttr()))
582
        {
583
3713
          hasSkolem = true;
584
3713
          break;
585
        }
586
      }
587
36227
      cur.setAttribute(HasSkolemAttr(), hasSkolem);
588
36227
      cur.setAttribute(HasSkolemComputedAttr(), true);
589
    }
590
123477
  } while (!visit.empty());
591
11471
  Assert(n.getAttribute(HasSkolemComputedAttr()));
592
22942
  return n.getAttribute(HasSkolemAttr());
593
}
594
595
2471
void RemoveTermFormulas::getSkolems(
596
    TNode n, std::unordered_set<Node, NodeHashFunction>& skolems) const
597
{
598
4942
  std::unordered_set<TNode, TNodeHashFunction> visited;
599
2471
  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
600
4942
  std::vector<TNode> visit;
601
4942
  TNode cur;
602
2471
  visit.push_back(n);
603
9000
  do
604
  {
605
11471
    cur = visit.back();
606
11471
    visit.pop_back();
607
11471
    if (!hasSkolems(cur))
608
    {
609
      // does not have skolems, continue
610
4955
      continue;
611
    }
612
6516
    it = visited.find(cur);
613
6516
    if (it == visited.end())
614
    {
615
5332
      visited.insert(cur);
616
5332
      if (cur.isVar())
617
      {
618
1562
        if (d_lemmaCache.find(cur) != d_lemmaCache.end())
619
        {
620
1562
          skolems.insert(cur);
621
        }
622
      }
623
      else
624
      {
625
3770
        visit.insert(visit.end(), cur.begin(), cur.end());
626
      }
627
    }
628
11471
  } while (!visit.empty());
629
2471
}
630
631
8607
Node RemoveTermFormulas::getAxiomFor(Node n)
632
{
633
8607
  NodeManager* nm = NodeManager::currentNM();
634
8607
  Kind k = n.getKind();
635
8607
  if (k == kind::ITE)
636
  {
637
8607
    return nm->mkNode(kind::ITE, n[0], n.eqNode(n[1]), n.eqNode(n[2]));
638
  }
639
  return Node::null();
640
}
641
642
1562
theory::TrustNode RemoveTermFormulas::getLemmaForSkolem(TNode n) const
643
{
644
  context::CDInsertHashMap<Node, theory::TrustNode, NodeHashFunction>::
645
1562
      const_iterator it = d_lemmaCache.find(n);
646
1562
  if (it == d_lemmaCache.end())
647
  {
648
    return theory::TrustNode::null();
649
  }
650
1562
  return (*it).second;
651
}
652
653
ProofGenerator* RemoveTermFormulas::getTConvProofGenerator()
654
{
655
  return d_tpg.get();
656
}
657
658
88696
bool RemoveTermFormulas::isProofEnabled() const { return d_pnm != nullptr; }
659
660
26676
}/* CVC4 namespace */