GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp Lines: 257 277 92.8 %
Date: 2021-03-22 Branches: 474 1000 47.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inst_strategy_cegqi.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Gereon Kremer
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Implementation of counterexample-guided quantifier instantiation
13
 **  strategies
14
 **/
15
#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
16
17
#include "expr/node_algorithm.h"
18
#include "options/quantifiers_options.h"
19
#include "theory/arith/partial_model.h"
20
#include "theory/arith/theory_arith.h"
21
#include "theory/arith/theory_arith_private.h"
22
#include "theory/quantifiers/first_order_model.h"
23
#include "theory/quantifiers/instantiate.h"
24
#include "theory/quantifiers/quantifiers_attributes.h"
25
#include "theory/quantifiers/quantifiers_rewriter.h"
26
#include "theory/quantifiers/term_database.h"
27
#include "theory/quantifiers/term_util.h"
28
#include "theory/quantifiers_engine.h"
29
#include "theory/rewriter.h"
30
31
using namespace std;
32
using namespace CVC4::kind;
33
using namespace CVC4::context;
34
35
namespace CVC4 {
36
namespace theory {
37
namespace quantifiers {
38
39
5975
InstRewriterCegqi::InstRewriterCegqi(InstStrategyCegqi* p)
40
5975
    : InstantiationRewriter(), d_parent(p)
41
{
42
5975
}
43
44
238589
TrustNode InstRewriterCegqi::rewriteInstantiation(Node q,
45
                                                  std::vector<Node>& terms,
46
                                                  Node inst,
47
                                                  bool doVts)
48
{
49
238589
  return d_parent->rewriteInstantiation(q, terms, inst, doVts);
50
}
51
52
5975
InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe,
53
                                     QuantifiersState& qs,
54
                                     QuantifiersInferenceManager& qim,
55
5975
                                     QuantifiersRegistry& qr)
56
    : QuantifiersModule(qs, qim, qr, qe),
57
5975
      d_irew(new InstRewriterCegqi(this)),
58
      d_cbqi_set_quant_inactive(false),
59
      d_incomplete_check(false),
60
5975
      d_added_cbqi_lemma(qs.getUserContext()),
61
5975
      d_vtsCache(new VtsTermCache(qim)),
62
23900
      d_bv_invert(nullptr)
63
{
64
5975
  d_small_const =
65
11950
      NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000));
66
5975
  d_check_vts_lemma_lc = false;
67
5975
  if (options::cegqiBv())
68
  {
69
    // if doing instantiation for BV, need the inverter class
70
3790
    d_bv_invert.reset(new BvInverter);
71
  }
72
5975
  if (options::cegqiNestedQE())
73
  {
74
30
    d_nestedQe.reset(new NestedQe(qs.getUserContext()));
75
  }
76
5975
}
77
78
11944
InstStrategyCegqi::~InstStrategyCegqi() {}
79
80
71507
bool InstStrategyCegqi::needsCheck(Theory::Effort e)
81
{
82
71507
  return e>=Theory::EFFORT_LAST_CALL;
83
}
84
85
14376
QuantifiersModule::QEffort InstStrategyCegqi::needsModel(Theory::Effort e)
86
{
87
14376
  size_t nquant = d_quantEngine->getModel()->getNumAssertedQuantifiers();
88
54756
  for (size_t i = 0; i < nquant; i++)
89
  {
90
84493
    Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
91
44113
    if (doCbqi(q))
92
    {
93
3733
      return QEFFORT_STANDARD;
94
    }
95
  }
96
10643
  return QEFFORT_NONE;
97
}
98
99
1859
bool InstStrategyCegqi::registerCbqiLemma(Node q)
100
{
101
1859
  if( !hasAddedCbqiLemma( q ) ){
102
1732
    NodeManager* nm = NodeManager::currentNM();
103
1732
    d_added_cbqi_lemma.insert( q );
104
1732
    Trace("cegqi-debug") << "Do cbqi for " << q << std::endl;
105
    //add cbqi lemma
106
    //get the counterexample literal
107
3464
    Node ceLit = getCounterexampleLiteral(q);
108
3464
    Node ceBody = d_qreg.getInstConstantBody(q);
109
1732
    if( !ceBody.isNull() ){
110
      //add counterexample lemma
111
3464
      Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() );
112
      //require any decision on cel to be phase=true
113
1732
      d_qim.addPendingPhaseRequirement(ceLit, true);
114
1732
      Debug("cegqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
115
      //add counterexample lemma
116
1732
      lem = Rewriter::rewrite( lem );
117
1732
      Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl;
118
1733
      registerCounterexampleLemma( q, lem );
119
120
      //compute dependencies between quantified formulas
121
3462
      std::vector<Node> ics;
122
1731
      TermUtil::computeInstConstContains(q, ics);
123
1731
      d_parent_quant[q].clear();
124
1731
      d_children_quant[q].clear();
125
3462
      std::vector<Node> dep;
126
2134
      for (const Node& ic : ics)
127
      {
128
806
        Node qi = ic.getAttribute(InstConstantAttribute());
129
1209
        if (std::find(d_parent_quant[q].begin(), d_parent_quant[q].end(), qi)
130
1209
            == d_parent_quant[q].end())
131
        {
132
243
          d_parent_quant[q].push_back(qi);
133
243
          d_children_quant[qi].push_back(q);
134
          // may not have added the CEX lemma, but the literal is created by
135
          // the following call regardless. One rare case where this can happen
136
          // is if both sygus-inst and CEGQI are being run in parallel, and
137
          // a parent quantified formula is not handled by CEGQI, but a child
138
          // is.
139
486
          Node qicel = getCounterexampleLiteral(qi);
140
243
          dep.push_back(qi);
141
243
          dep.push_back(qicel);
142
        }
143
      }
144
1731
      if (!dep.empty())
145
      {
146
        // This lemma states that if the child is active, then the parent must
147
        // be asserted, in particular G => Q where G is the CEX literal for the
148
        // child and Q is the parent.
149
326
        Node dep_lemma = nm->mkNode(IMPLIES, ceLit, nm->mkNode(AND, dep));
150
326
        Trace("cegqi-lemma")
151
163
            << "Counterexample dependency lemma : " << dep_lemma << std::endl;
152
163
        d_qim.lemma(dep_lemma, InferenceId::QUANTIFIERS_CEGQI_CEX_DEP);
153
      }
154
155
      //must register all sub-quantifiers of counterexample lemma, register their lemmas
156
3462
      std::vector< Node > quants;
157
1731
      TermUtil::computeQuantContains( lem, quants );
158
1863
      for( unsigned i=0; i<quants.size(); i++ ){
159
132
        if( doCbqi( quants[i] ) ){
160
127
          registerCbqiLemma( quants[i] );
161
        }
162
      }
163
    }
164
    // The decision strategy for this quantified formula ensures that its
165
    // counterexample literal is decided on first. It is user-context dependent.
166
    std::map<Node, std::unique_ptr<DecisionStrategy>>::iterator itds =
167
1731
        d_dstrat.find(q);
168
1731
    DecisionStrategy* dlds = nullptr;
169
1731
    if (itds == d_dstrat.end())
170
    {
171
5193
      d_dstrat[q].reset(new DecisionStrategySingleton("CexLiteral",
172
                                                      ceLit,
173
1731
                                                      d_qstate.getSatContext(),
174
3462
                                                      d_qstate.getValuation()));
175
1731
      dlds = d_dstrat[q].get();
176
    }
177
    else
178
    {
179
      dlds = itds->second.get();
180
    }
181
    // it is appended to the list of strategies
182
1731
    d_quantEngine->getDecisionManager()->registerStrategy(
183
        DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE, dlds);
184
1731
    return true;
185
  }else{
186
127
    return false;
187
  }
188
}
189
190
27648
void InstStrategyCegqi::reset_round(Theory::Effort effort)
191
{
192
27648
  d_cbqi_set_quant_inactive = false;
193
27648
  d_incomplete_check = false;
194
27648
  d_active_quant.clear();
195
  //check if any cbqi lemma has not been added yet
196
251517
  for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
197
447738
    Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
198
    //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
199
223869
    if( doCbqi( q ) ){
200
8470
      if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
201
8470
        d_active_quant[q] = true;
202
8470
        Debug("cegqi-debug") << "Check quantified formula " << q << "..." << std::endl;
203
16940
        Node cel = getCounterexampleLiteral(q);
204
        bool value;
205
8470
        if (d_qstate.getValuation().hasSatValue(cel, value))
206
        {
207
8446
          Debug("cegqi-debug") << "...CE Literal has value " << value << std::endl;
208
8446
          if( !value ){
209
1515
            if (d_qstate.getValuation().isDecision(cel))
210
            {
211
              Trace("cegqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl;
212
            }else{
213
1515
              Trace("cegqi") << "Inactive : " << q << std::endl;
214
1515
              d_quantEngine->getModel()->setQuantifierActive( q, false );
215
1515
              d_cbqi_set_quant_inactive = true;
216
1515
              d_active_quant.erase( q );
217
            }
218
          }
219
        }else{
220
24
          Debug("cegqi-debug") << "...CE Literal does not have value " << std::endl;
221
        }
222
      }
223
    }
224
  }
225
226
  //refinement: only consider innermost active quantified formulas
227
55296
  if( options::cegqiInnermost() ){
228
27648
    if( !d_children_quant.empty() && !d_active_quant.empty() ){
229
5963
      Trace("cegqi-debug") << "Find non-innermost quantifiers..." << std::endl;
230
11926
      std::vector< Node > ninner;
231
12898
      for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
232
6935
        std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( it->first );
233
6935
        if( itc!=d_children_quant.end() ){
234
7293
          for( unsigned j=0; j<itc->second.size(); j++ ){
235
482
            if( d_active_quant.find( itc->second[j] )!=d_active_quant.end() ){
236
120
              Trace("cegqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl;
237
120
              ninner.push_back( it->first );
238
120
              break;
239
            }
240
          }
241
        }
242
      }
243
5963
      Trace("cegqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl;
244
6083
      for( unsigned i=0; i<ninner.size(); i++ ){
245
120
        Assert(d_active_quant.find(ninner[i]) != d_active_quant.end());
246
120
        d_active_quant.erase( ninner[i] );
247
      }
248
5963
      Assert(!d_active_quant.empty());
249
5963
      Trace("cegqi-debug") << "...done removing." << std::endl;
250
    }
251
  }
252
27648
  d_check_vts_lemma_lc = false;
253
27648
}
254
255
42120
void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e)
256
{
257
42120
  if (quant_e == QEFFORT_STANDARD)
258
  {
259
14376
    Assert(!d_qstate.isInConflict());
260
14376
    double clSet = 0;
261
14376
    if( Trace.isOn("cegqi-engine") ){
262
      clSet = double(clock())/double(CLOCKS_PER_SEC);
263
      Trace("cegqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl;
264
    }
265
14376
    size_t lastWaiting = d_qim.numPendingLemmas();
266
36174
    for( int ee=0; ee<=1; ee++ ){
267
      //for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
268
      //  Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
269
      //  if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
270
29571
      for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
271
8592
        Node q = it->first;
272
4296
        Trace("cegqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl;
273
4296
        process(q, e, ee);
274
4296
        if (d_qstate.isInConflict())
275
        {
276
          break;
277
        }
278
      }
279
25275
      if (d_qstate.isInConflict() || d_qim.numPendingLemmas() > lastWaiting)
280
      {
281
3477
        break;
282
      }
283
    }
284
14376
    if( Trace.isOn("cegqi-engine") ){
285
      if (d_qim.numPendingLemmas() > lastWaiting)
286
      {
287
        Trace("cegqi-engine")
288
            << "Added lemmas = " << (d_qim.numPendingLemmas() - lastWaiting)
289
            << std::endl;
290
      }
291
      double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
292
      Trace("cegqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl;
293
    }
294
  }
295
42120
}
296
297
3589
bool InstStrategyCegqi::checkComplete()
298
{
299
7178
  if( ( !options::cegqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){
300
64
    return false;
301
  }else{
302
3525
    return true;
303
  }
304
}
305
306
1394
bool InstStrategyCegqi::checkCompleteFor(Node q)
307
{
308
1394
  std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q);
309
1394
  if( it!=d_do_cbqi.end() ){
310
1394
    return it->second != CEG_UNHANDLED;
311
  }else{
312
    return false;
313
  }
314
}
315
316
23208
void InstStrategyCegqi::checkOwnership(Node q)
317
{
318
23208
  if (d_qreg.getOwner(q) == nullptr && doCbqi(q))
319
  {
320
1748
    if (d_do_cbqi[q] == CEG_HANDLED)
321
    {
322
      //take full ownership of the quantified formula
323
1737
      d_qreg.setOwner(q, this);
324
    }
325
  }
326
23208
}
327
328
23225
void InstStrategyCegqi::preRegisterQuantifier(Node q)
329
{
330
23225
  if (doCbqi(q))
331
  {
332
1748
    if (processNestedQe(q, true))
333
    {
334
      // will process using nested quantifier elimination
335
16
      return;
336
    }
337
    // register the cbqi lemma
338
1733
    if( registerCbqiLemma( q ) ){
339
1604
      Trace("cegqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
340
    }
341
  }
342
}
343
238589
TrustNode InstStrategyCegqi::rewriteInstantiation(Node q,
344
                                                  std::vector<Node>& terms,
345
                                                  Node inst,
346
                                                  bool doVts)
347
{
348
477178
  Node prevInst = inst;
349
238589
  if (doVts)
350
  {
351
    // do virtual term substitution
352
67
    inst = Rewriter::rewrite(inst);
353
67
    Trace("quant-vts-debug") << "Rewrite vts symbols in " << inst << std::endl;
354
67
    inst = d_vtsCache->rewriteVtsSymbols(inst);
355
67
    Trace("quant-vts-debug") << "...got " << inst << std::endl;
356
  }
357
238589
  if (prevInst != inst)
358
  {
359
    // not proof producing yet
360
67
    return TrustNode::mkTrustRewrite(prevInst, inst, nullptr);
361
  }
362
238522
  return TrustNode::null();
363
}
364
365
5975
InstantiationRewriter* InstStrategyCegqi::getInstRewriter() const
366
{
367
5975
  return d_irew.get();
368
}
369
370
1732
void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem)
371
{
372
  // must register with the instantiator
373
  // must explicitly remove ITEs so that we record dependencies
374
3464
  std::vector<Node> ce_vars;
375
5167
  for (size_t i = 0, nics = d_qreg.getNumInstantiationConstants(q); i < nics;
376
       i++)
377
  {
378
3435
    ce_vars.push_back(d_qreg.getInstantiationConstant(q, i));
379
  }
380
  // send the lemma
381
1733
  d_qim.lemma(lem, InferenceId::UNKNOWN);
382
  // get the preprocessed form of the lemma we just sent
383
3462
  std::vector<Node> skolems;
384
3462
  std::vector<Node> skAsserts;
385
  Node ppLem =
386
3462
      d_qstate.getValuation().getPreprocessedTerm(lem, skAsserts, skolems);
387
3462
  std::vector<Node> lemp{ppLem};
388
1731
  lemp.insert(lemp.end(), skAsserts.begin(), skAsserts.end());
389
1731
  ppLem = NodeManager::currentNM()->mkAnd(lemp);
390
3462
  Trace("cegqi-debug") << "Counterexample lemma (post-preprocess): " << ppLem
391
1731
                       << std::endl;
392
3462
  std::vector<Node> auxLems;
393
1731
  CegInstantiator* cinst = getInstantiator(q);
394
1731
  cinst->registerCounterexampleLemma(ppLem, ce_vars, auxLems);
395
1869
  for (unsigned i = 0, size = auxLems.size(); i < size; i++)
396
  {
397
276
    Trace("cegqi-debug") << "Auxiliary CE lemma " << i << " : " << auxLems[i]
398
138
                         << std::endl;
399
138
    d_qim.addPendingLemma(auxLems[i], InferenceId::UNKNOWN);
400
  }
401
1731
}
402
403
314547
bool InstStrategyCegqi::doCbqi(Node q)
404
{
405
314547
  std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q);
406
314547
  if( it==d_do_cbqi.end() ){
407
23208
    CegHandledStatus ret = CegInstantiator::isCbqiQuant(q, d_quantEngine);
408
23208
    Trace("cegqi-quant") << "doCbqi " << q << " returned " << ret << std::endl;
409
23208
    d_do_cbqi[q] = ret;
410
23208
    return ret != CEG_UNHANDLED;
411
  }
412
291339
  return it->second != CEG_UNHANDLED;
413
}
414
415
4296
void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
416
  // If we are doing nested quantifier elimination, check if q was already
417
  // processed.
418
4296
  if (processNestedQe(q, false))
419
  {
420
    // don't need to process this, since it has been reduced
421
26
    return;
422
  }
423
4270
  if( e==0 ){
424
3985
    CegInstantiator * cinst = getInstantiator( q );
425
3985
    Trace("inst-alg") << "-> Run cegqi for " << q << std::endl;
426
3985
    d_curr_quant = q;
427
3985
    if( !cinst->check() ){
428
292
      d_incomplete_check = true;
429
292
      d_check_vts_lemma_lc = true;
430
    }
431
3985
    d_curr_quant = Node::null();
432
285
  }else if( e==1 ){
433
    //minimize the free delta heuristically on demand
434
285
    if( d_check_vts_lemma_lc ){
435
92
      Trace("inst-alg") << "-> Minimize delta heuristic, for " << q << std::endl;
436
92
      d_check_vts_lemma_lc = false;
437
92
      d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const );
438
92
      d_small_const = Rewriter::rewrite( d_small_const );
439
      //heuristic for now, until we know how to do nested quantification
440
184
      Node delta = d_vtsCache->getVtsDelta(true, false);
441
92
      if( !delta.isNull() ){
442
        Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl;
443
        Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const );
444
        d_qim.lemma(delta_lem_ub, InferenceId::QUANTIFIERS_CEGQI_VTS_UB_DELTA);
445
      }
446
184
      std::vector< Node > inf;
447
92
      d_vtsCache->getVtsTerms(inf, true, false, false);
448
92
      for( unsigned i=0; i<inf.size(); i++ ){
449
        Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl;
450
        Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) );
451
        d_qim.lemma(inf_lem_lb, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF);
452
      }
453
    }
454
  }
455
}
456
457
10445
Node InstStrategyCegqi::getCounterexampleLiteral(Node q)
458
{
459
10445
  std::map<Node, Node>::iterator it = d_ce_lit.find(q);
460
10445
  if (it != d_ce_lit.end())
461
  {
462
8699
    return it->second;
463
  }
464
1746
  NodeManager * nm = NodeManager::currentNM();
465
3492
  Node g = nm->mkSkolem("g", nm->booleanType());
466
  // ensure that it is a SAT literal
467
3492
  Node ceLit = d_qstate.getValuation().ensureLiteral(g);
468
1746
  d_ce_lit[q] = ceLit;
469
1746
  return ceLit;
470
}
471
472
5019
bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
473
5019
  Assert(!d_curr_quant.isNull());
474
  //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
475
5019
  if (d_qreg.getQuantAttributes().isQuantElimPartial(d_curr_quant))
476
  {
477
1
    d_cbqi_set_quant_inactive = true;
478
1
    d_incomplete_check = true;
479
1
    d_quantEngine->getInstantiate()->recordInstantiation(
480
        d_curr_quant, subs, false, false);
481
1
    return true;
482
  }else{
483
    //check if we need virtual term substitution (if used delta or infinity)
484
5018
    bool used_vts = d_vtsCache->containsVtsTerm(subs, false);
485
5018
    if (d_quantEngine->getInstantiate()->addInstantiation(
486
            d_curr_quant,
487
            subs,
488
            InferenceId::QUANTIFIERS_INST_CEGQI,
489
            false,
490
            false,
491
            used_vts))
492
    {
493
3692
      return true;
494
    }else{
495
      //this should never happen for monotonic selection strategies
496
1326
      Trace("cegqi-warn") << "WARNING: Existing instantiation" << std::endl;
497
1326
      return false;
498
    }
499
  }
500
}
501
502
bool InstStrategyCegqi::addPendingLemma(Node lem) const
503
{
504
  return d_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
505
}
506
507
5716
CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
508
  std::map<Node, std::unique_ptr<CegInstantiator>>::iterator it =
509
5716
      d_cinst.find(q);
510
5716
  if( it==d_cinst.end() ){
511
1731
    d_cinst[q].reset(new CegInstantiator(q, d_qstate, this));
512
1731
    return d_cinst[q].get();
513
  }
514
3985
  return it->second.get();
515
}
516
517
1663
VtsTermCache* InstStrategyCegqi::getVtsTermCache() const
518
{
519
1663
  return d_vtsCache.get();
520
}
521
522
1198
BvInverter* InstStrategyCegqi::getBvInverter() const
523
{
524
1198
  return d_bv_invert.get();
525
}
526
527
6044
bool InstStrategyCegqi::processNestedQe(Node q, bool isPreregister)
528
{
529
6044
  if (d_nestedQe != nullptr)
530
  {
531
98
    if (isPreregister)
532
    {
533
      // If at preregister, we are done if we have nested quantification.
534
      // We will process nested quantification.
535
40
      return NestedQe::hasNestedQuantification(q);
536
    }
537
    // if not a preregister, we process, which may trigger quantifier
538
    // elimination in subsolvers.
539
90
    std::vector<Node> lems;
540
58
    if (d_nestedQe->process(q, lems))
541
    {
542
      // add lemmas to process
543
40
      for (const Node& lem : lems)
544
      {
545
14
        d_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
546
      }
547
      // don't need to process this, since it has been reduced
548
26
      return true;
549
    }
550
  }
551
5978
  return false;
552
}
553
554
}  // namespace quantifiers
555
}  // namespace theory
556
57913
}  // namespace CVC4