GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers_engine.cpp Lines: 316 369 85.6 %
Date: 2021-03-23 Branches: 524 1242 42.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quantifiers_engine.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, 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 Implementation of quantifiers engine class
13
 **/
14
15
#include "theory/quantifiers_engine.h"
16
17
#include "options/printer_options.h"
18
#include "options/quantifiers_options.h"
19
#include "options/smt_options.h"
20
#include "options/uf_options.h"
21
#include "smt/smt_engine_scope.h"
22
#include "smt/smt_statistics_registry.h"
23
#include "theory/quantifiers/ematching/trigger_trie.h"
24
#include "theory/quantifiers/equality_query.h"
25
#include "theory/quantifiers/first_order_model.h"
26
#include "theory/quantifiers/fmf/first_order_model_fmc.h"
27
#include "theory/quantifiers/fmf/full_model_check.h"
28
#include "theory/quantifiers/fmf/model_builder.h"
29
#include "theory/quantifiers/quant_module.h"
30
#include "theory/quantifiers/quantifiers_inference_manager.h"
31
#include "theory/quantifiers/quantifiers_modules.h"
32
#include "theory/quantifiers/quantifiers_registry.h"
33
#include "theory/quantifiers/quantifiers_rewriter.h"
34
#include "theory/quantifiers/quantifiers_state.h"
35
#include "theory/quantifiers/relevant_domain.h"
36
#include "theory/quantifiers/skolemize.h"
37
#include "theory/quantifiers/term_enumeration.h"
38
#include "theory/quantifiers/term_registry.h"
39
#include "theory/quantifiers/term_util.h"
40
#include "theory/theory_engine.h"
41
#include "theory/uf/equality_engine.h"
42
43
using namespace std;
44
using namespace CVC4::kind;
45
46
namespace CVC4 {
47
namespace theory {
48
49
8997
QuantifiersEngine::QuantifiersEngine(
50
    quantifiers::QuantifiersState& qstate,
51
    quantifiers::QuantifiersRegistry& qr,
52
    quantifiers::TermRegistry& tr,
53
    quantifiers::QuantifiersInferenceManager& qim,
54
    quantifiers::FirstOrderModel* qm,
55
8997
    ProofNodeManager* pnm)
56
    : d_qstate(qstate),
57
      d_qim(qim),
58
      d_te(nullptr),
59
      d_decManager(nullptr),
60
      d_pnm(pnm),
61
      d_qreg(qr),
62
      d_treg(tr),
63
8997
      d_tr_trie(new inst::TriggerTrie),
64
      d_model(qm),
65
8997
      d_quants_prereg(qstate.getUserContext()),
66
26991
      d_quants_red(qstate.getUserContext())
67
{
68
  // initialize the utilities
69
8997
  d_util.push_back(d_model->getEqualityQuery());
70
  // quantifiers registry must come before the remaining utilities
71
8997
  d_util.push_back(&d_qreg);
72
8997
  d_util.push_back(tr.getTermDatabase());
73
8997
  d_util.push_back(qim.getInstantiate());
74
8997
}
75
76
8994
QuantifiersEngine::~QuantifiersEngine() {}
77
78
6054
void QuantifiersEngine::finishInit(TheoryEngine* te, DecisionManager* dm)
79
{
80
6054
  d_te = te;
81
6054
  d_decManager = dm;
82
  // Initialize the modules and the utilities here.
83
6054
  d_qmodules.reset(new quantifiers::QuantifiersModules);
84
6054
  d_qmodules->initialize(this, d_qstate, d_qim, d_qreg, dm, d_modules);
85
6054
  if (d_qmodules->d_rel_dom.get())
86
  {
87
79
    d_util.push_back(d_qmodules->d_rel_dom.get());
88
  }
89
90
  // handle any circular dependencies
91
92
  // quantifiers bound inference needs to be informed of the bounded integers
93
  // module, which has information about which quantifiers have finite bounds
94
6054
  d_qreg.getQuantifiersBoundInference().finishInit(d_qmodules->d_bint.get());
95
6054
}
96
97
2287
DecisionManager* QuantifiersEngine::getDecisionManager()
98
{
99
2287
  return d_decManager;
100
}
101
102
3246763
quantifiers::QuantifiersState& QuantifiersEngine::getState()
103
{
104
3246763
  return d_qstate;
105
}
106
quantifiers::QuantifiersInferenceManager&
107
QuantifiersEngine::getInferenceManager()
108
{
109
  return d_qim;
110
}
111
112
6
quantifiers::QuantifiersRegistry& QuantifiersEngine::getQuantifiersRegistry()
113
{
114
6
  return d_qreg;
115
}
116
117
17262
quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
118
{
119
17262
  return d_qmodules->d_builder.get();
120
}
121
749811
quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const
122
{
123
749811
  return d_model;
124
}
125
126
/// !!!!!!!!!!!!!! temporary (project #15)
127
128
18015704
quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const
129
{
130
18015704
  return d_treg.getTermDatabase();
131
}
132
30467
quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() const
133
{
134
30467
  return d_treg.getTermDatabaseSygus();
135
}
136
1637
quantifiers::TermEnumeration* QuantifiersEngine::getTermEnumeration() const
137
{
138
1637
  return d_treg.getTermEnumeration();
139
}
140
531076
quantifiers::Instantiate* QuantifiersEngine::getInstantiate() const
141
{
142
531076
  return d_qim.getInstantiate();
143
}
144
33
quantifiers::Skolemize* QuantifiersEngine::getSkolemize() const
145
{
146
33
  return d_qim.getSkolemize();
147
}
148
29565
inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
149
{
150
29565
  return d_tr_trie.get();
151
}
152
/// !!!!!!!!!!!!!!
153
154
6440
void QuantifiersEngine::presolve() {
155
6440
  Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
156
6440
  d_qim.clearPending();
157
32153
  for( unsigned i=0; i<d_modules.size(); i++ ){
158
25713
    d_modules[i]->presolve();
159
  }
160
  // presolve with term registry, which populates the term database based on
161
  // terms registered before presolve when in incremental mode
162
6440
  d_treg.presolve();
163
6440
}
164
165
5909
void QuantifiersEngine::ppNotifyAssertions(
166
    const std::vector<Node>& assertions) {
167
11818
  Trace("quant-engine-proc")
168
11818
      << "ppNotifyAssertions in QE, #assertions = " << assertions.size()
169
5909
      << std::endl;
170
5909
  if (options::instLevelInputOnly() && options::instMaxLevel() != -1)
171
  {
172
229
    for (const Node& a : assertions)
173
    {
174
225
      quantifiers::QuantAttributes::setInstantiationLevelAttr(a, 0);
175
    }
176
  }
177
5909
  if (options::sygus())
178
  {
179
1906
    quantifiers::SynthEngine* sye = d_qmodules->d_synth_e.get();
180
8259
    for (const Node& a : assertions)
181
    {
182
6353
      sye->preregisterAssertion(a);
183
    }
184
  }
185
  /* The SyGuS instantiation module needs a global view of all available
186
   * assertions to collect global terms that get added to each grammar.
187
   */
188
5909
  if (options::sygusInst())
189
  {
190
19
    quantifiers::SygusInst* si = d_qmodules->d_sygus_inst.get();
191
19
    si->ppNotifyAssertions(assertions);
192
  }
193
5909
}
194
195
86229
void QuantifiersEngine::check( Theory::Effort e ){
196
172458
  CodeTimer codeTimer(d_statistics.d_time);
197
86229
  Assert(d_qstate.getEqualityEngine() != nullptr);
198
86229
  if (!d_qstate.getEqualityEngine()->consistent())
199
  {
200
    Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl;
201
    return;
202
  }
203
86229
  if (d_qstate.isInConflict())
204
  {
205
    if (e < Theory::EFFORT_LAST_CALL)
206
    {
207
      // this can happen in rare cases when quantifiers is the first to realize
208
      // there is a quantifier-free conflict, for example, when it discovers
209
      // disequal and congruent terms in the master equality engine during
210
      // term indexing. In such cases, quantifiers reports a "conflicting lemma"
211
      // that is, one that is entailed to be false by the current assignment.
212
      // If this lemma is not a SAT conflict, we may get another call to full
213
      // effort check and the quantifier-free solvers still haven't realized
214
      // there is a conflict. In this case, we return, trusting that theory
215
      // combination will do the right thing (split on equalities until there is
216
      // a conflict at the quantifier-free level).
217
      Trace("quant-engine-debug")
218
          << "Conflicting lemma already reported by quantifiers, return."
219
          << std::endl;
220
      return;
221
    }
222
    // we reported what we thought was a conflicting lemma, but now we have
223
    // gotten a check at LAST_CALL effort, indicating that the lemma we reported
224
    // was not conflicting. This should never happen, but in production mode, we
225
    // proceed with the check.
226
    Assert(false);
227
  }
228
86229
  bool needsCheck = d_qim.hasPendingLemma();
229
86229
  QuantifiersModule::QEffort needsModelE = QuantifiersModule::QEFFORT_NONE;
230
172458
  std::vector< QuantifiersModule* > qm;
231
86229
  if( d_model->checkNeeded() ){
232
72207
    needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL;  //always need to check at or above last call
233
364010
    for (QuantifiersModule*& mdl : d_modules)
234
    {
235
291803
      if (mdl->needsCheck(e))
236
      {
237
56361
        qm.push_back(mdl);
238
56361
        needsCheck = true;
239
        //can only request model at last call since theory combination can find inconsistencies
240
56361
        if( e>=Theory::EFFORT_LAST_CALL ){
241
40015
          QuantifiersModule::QEffort me = mdl->needsModel(e);
242
40015
          needsModelE = me<needsModelE ? me : needsModelE;
243
        }
244
      }
245
    }
246
  }
247
248
86229
  d_qim.reset();
249
86229
  bool setIncomplete = false;
250
251
86229
  Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
252
86229
  if( needsCheck ){
253
    //flush previous lemmas (for instance, if was interrupted), or other lemmas to process
254
28265
    d_qim.doPending();
255
28265
    if (d_qim.hasSentLemma())
256
    {
257
      return;
258
    }
259
260
28265
    double clSet = 0;
261
28265
    if( Trace.isOn("quant-engine") ){
262
      clSet = double(clock())/double(CLOCKS_PER_SEC);
263
      Trace("quant-engine") << ">>>>> Quantifiers Engine Round, effort = " << e << " <<<<<" << std::endl;
264
    }
265
266
28265
    if( Trace.isOn("quant-engine-debug") ){
267
      Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl;
268
      Trace("quant-engine-debug")
269
          << "  depth : " << d_qstate.getInstRoundDepth() << std::endl;
270
      Trace("quant-engine-debug") << "  modules to check : ";
271
      for( unsigned i=0; i<qm.size(); i++ ){
272
        Trace("quant-engine-debug") << qm[i]->identify() << " ";
273
      }
274
      Trace("quant-engine-debug") << std::endl;
275
      Trace("quant-engine-debug") << "  # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl;
276
      if (d_qim.hasPendingLemma())
277
      {
278
        Trace("quant-engine-debug")
279
            << "  lemmas waiting = " << d_qim.numPendingLemmas() << std::endl;
280
      }
281
      Trace("quant-engine-debug")
282
          << "  Theory engine finished : "
283
          << !d_qstate.getValuation().needCheck() << std::endl;
284
      Trace("quant-engine-debug") << "  Needs model effort : " << needsModelE << std::endl;
285
      Trace("quant-engine-debug")
286
          << "  In conflict : " << d_qstate.isInConflict() << std::endl;
287
    }
288
28265
    if( Trace.isOn("quant-engine-ee-pre") ){
289
      Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl;
290
      d_qstate.debugPrintEqualityEngine("quant-engine-ee-pre");
291
    }
292
28265
    if( Trace.isOn("quant-engine-assert") ){
293
      Trace("quant-engine-assert") << "Assertions : " << std::endl;
294
      d_te->printAssertions("quant-engine-assert");
295
    }
296
297
    //reset utilities
298
28265
    Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl;
299
142441
    for (QuantifiersUtil*& util : d_util)
300
    {
301
228352
      Trace("quant-engine-debug2") << "Reset " << util->identify().c_str()
302
114176
                                   << "..." << std::endl;
303
114176
      if (!util->reset(e))
304
      {
305
        d_qim.doPending();
306
        if (d_qim.hasSentLemma())
307
        {
308
          return;
309
        }else{
310
          //should only fail reset if added a lemma
311
          Assert(false);
312
        }
313
      }
314
    }
315
316
28265
    if( Trace.isOn("quant-engine-ee") ){
317
      Trace("quant-engine-ee") << "Equality engine : " << std::endl;
318
      d_qstate.debugPrintEqualityEngine("quant-engine-ee");
319
    }
320
321
    //reset the model
322
28265
    Trace("quant-engine-debug") << "Reset model..." << std::endl;
323
28265
    d_model->reset_round();
324
325
    //reset the modules
326
28265
    Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
327
145298
    for (QuantifiersModule*& mdl : d_modules)
328
    {
329
234066
      Trace("quant-engine-debug2") << "Reset " << mdl->identify().c_str()
330
117033
                                   << std::endl;
331
117033
      mdl->reset_round(e);
332
    }
333
28265
    Trace("quant-engine-debug") << "Done resetting all modules." << std::endl;
334
    //reset may have added lemmas
335
28265
    d_qim.doPending();
336
28265
    if (d_qim.hasSentLemma())
337
    {
338
      return;
339
    }
340
341
28265
    if( e==Theory::EFFORT_LAST_CALL ){
342
14472
      ++(d_statistics.d_instantiation_rounds_lc);
343
13793
    }else if( e==Theory::EFFORT_FULL ){
344
13793
      ++(d_statistics.d_instantiation_rounds);
345
    }
346
28265
    Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
347
108175
    for (unsigned qef = QuantifiersModule::QEFFORT_CONFLICT;
348
108175
         qef <= QuantifiersModule::QEFFORT_LAST_CALL;
349
         ++qef)
350
    {
351
93003
      QuantifiersModule::QEffort quant_e =
352
          static_cast<QuantifiersModule::QEffort>(qef);
353
      // Force the theory engine to build the model if any module requested it.
354
93003
      if (needsModelE == quant_e)
355
      {
356
13658
        Trace("quant-engine-debug") << "Build model..." << std::endl;
357
13658
        if (!d_te->buildModel())
358
        {
359
          // If we failed to build the model, flush all pending lemmas and
360
          // finish.
361
          d_qim.doPending();
362
13080
          break;
363
        }
364
      }
365
93003
      if (!d_qim.hasSentLemma())
366
      {
367
        //check each module
368
271973
        for (QuantifiersModule*& mdl : qm)
369
        {
370
357976
          Trace("quant-engine-debug") << "Check " << mdl->identify().c_str()
371
178988
                                      << " at effort " << quant_e << "..."
372
178988
                                      << std::endl;
373
178988
          mdl->check(e, quant_e);
374
178976
          if (d_qstate.isInConflict())
375
          {
376
6
            Trace("quant-engine-debug") << "...conflict!" << std::endl;
377
6
            break;
378
          }
379
        }
380
        //flush all current lemmas
381
92991
        d_qim.doPending();
382
      }
383
      //if we have added one, stop
384
92990
      if (d_qim.hasSentLemma())
385
      {
386
12610
        break;
387
      }else{
388
80380
        Assert(!d_qstate.isInConflict());
389
80380
        if (quant_e == QuantifiersModule::QEFFORT_CONFLICT)
390
        {
391
26982
          d_qstate.incrementInstRoundCounters(e);
392
        }
393
53398
        else if (quant_e == QuantifiersModule::QEFFORT_MODEL)
394
        {
395
15769
          if( e==Theory::EFFORT_LAST_CALL ){
396
            //sources of incompleteness
397
18258
            for (QuantifiersUtil*& util : d_util)
398
            {
399
14644
              if (!util->checkComplete())
400
              {
401
2
                Trace("quant-engine-debug") << "Set incomplete because utility "
402
2
                                            << util->identify().c_str()
403
1
                                            << " was incomplete." << std::endl;
404
1
                setIncomplete = true;
405
              }
406
            }
407
3614
            if (d_qstate.isInConflict())
408
            {
409
              // we reported a conflicting lemma, should return
410
              setIncomplete = true;
411
            }
412
            //if we have a chance not to set incomplete
413
3614
            if( !setIncomplete ){
414
              //check if we should set the incomplete flag
415
17936
              for (QuantifiersModule*& mdl : d_modules)
416
              {
417
14387
                if (!mdl->checkComplete())
418
                {
419
128
                  Trace("quant-engine-debug")
420
64
                      << "Set incomplete because module "
421
128
                      << mdl->identify().c_str() << " was incomplete."
422
64
                      << std::endl;
423
64
                  setIncomplete = true;
424
64
                  break;
425
                }
426
              }
427
3613
              if( !setIncomplete ){
428
                //look at individual quantified formulas, one module must claim completeness for each one
429
4851
                for( unsigned i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
430
4381
                  bool hasCompleteM = false;
431
5683
                  Node q = d_model->getAssertedQuantifier( i );
432
4381
                  QuantifiersModule* qmd = d_qreg.getOwner(q);
433
4381
                  if( qmd!=NULL ){
434
3072
                    hasCompleteM = qmd->checkCompleteFor( q );
435
                  }else{
436
4998
                    for( unsigned j=0; j<d_modules.size(); j++ ){
437
4803
                      if( d_modules[j]->checkCompleteFor( q ) ){
438
1114
                        qmd = d_modules[j];
439
1114
                        hasCompleteM = true;
440
1114
                        break;
441
                      }
442
                    }
443
                  }
444
4381
                  if( !hasCompleteM ){
445
3079
                    Trace("quant-engine-debug") << "Set incomplete because " << q << " was not fully processed." << std::endl;
446
3079
                    setIncomplete = true;
447
3079
                    break;
448
                  }else{
449
1302
                    Assert(qmd != NULL);
450
1302
                    Trace("quant-engine-debug2") << "Complete for " << q << " due to " << qmd->identify().c_str() << std::endl;
451
                  }
452
                }
453
              }
454
            }
455
            //if setIncomplete = false, we will answer SAT, otherwise we will run at quant_e QEFFORT_LAST_CALL
456
3614
            if( !setIncomplete ){
457
470
              break;
458
            }
459
          }
460
        }
461
      }
462
    }
463
28252
    Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
464
    // debug print
465
28252
    if (d_qim.hasSentLemma())
466
    {
467
12610
      bool debugInstTrace = Trace.isOn("inst-per-quant-round");
468
12610
      if (options::debugInst() || debugInstTrace)
469
      {
470
2
        Options& sopts = smt::currentSmtEngine()->getOptions();
471
2
        std::ostream& out = *sopts.getOut();
472
2
        d_qim.getInstantiate()->debugPrint(out);
473
      }
474
    }
475
28252
    if( Trace.isOn("quant-engine") ){
476
      double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
477
      Trace("quant-engine") << "Finished quantifiers engine, total time = " << (clSet2-clSet);
478
      Trace("quant-engine") << ", sent lemma = " << d_qim.hasSentLemma();
479
      Trace("quant-engine") << std::endl;
480
    }
481
482
28252
    Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl;
483
  }else{
484
57964
    Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl;
485
  }
486
487
  //SAT case
488
86216
  if (e == Theory::EFFORT_LAST_CALL && !d_qim.hasSentLemma())
489
  {
490
5824
    if( setIncomplete ){
491
3017
      Trace("quant-engine") << "Set incomplete flag." << std::endl;
492
3017
      d_qim.setIncomplete();
493
    }
494
    //output debug stats
495
5824
    d_qim.getInstantiate()->debugPrintModel();
496
  }
497
}
498
499
15760
void QuantifiersEngine::notifyCombineTheories() {
500
  // If allowing theory combination to happen at most once between instantiation
501
  // rounds, this would reset d_ierCounter to 1 and d_ierCounterLastLc to -1
502
  // in quantifiers state.
503
15760
}
504
505
93227
bool QuantifiersEngine::reduceQuantifier( Node q ) {
506
  //TODO: this can be unified with preregistration: AlphaEquivalence takes ownership of reducable quants
507
93227
  BoolMap::const_iterator it = d_quants_red.find( q );
508
93227
  if( it==d_quants_red.end() ){
509
50818
    Node lem;
510
25409
    InferenceId id = InferenceId::UNKNOWN;
511
25409
    std::map< Node, Node >::iterator itr = d_quants_red_lem.find( q );
512
25409
    if( itr==d_quants_red_lem.end() ){
513
25388
      if (d_qmodules->d_alpha_equiv)
514
      {
515
25388
        Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl;
516
        //add equivalence with another quantified formula
517
25388
        lem = d_qmodules->d_alpha_equiv->reduceQuantifier(q);
518
25388
        id = InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ;
519
25388
        if( !lem.isNull() ){
520
1905
          Trace("quant-engine-red") << "...alpha equivalence success." << std::endl;
521
1905
          ++(d_statistics.d_red_alpha_equiv);
522
        }
523
      }
524
25388
      d_quants_red_lem[q] = lem;
525
    }else{
526
21
      lem = itr->second;
527
    }
528
25409
    if( !lem.isNull() ){
529
1905
      d_qim.lemma(lem, id);
530
    }
531
25409
    d_quants_red[q] = !lem.isNull();
532
25409
    return !lem.isNull();
533
  }else{
534
67818
    return (*it).second;
535
  }
536
}
537
538
58643
void QuantifiersEngine::registerQuantifierInternal(Node f)
539
{
540
58643
  std::map< Node, bool >::iterator it = d_quants.find( f );
541
58643
  if( it==d_quants.end() ){
542
23483
    Trace("quant") << "QuantifiersEngine : Register quantifier ";
543
23483
    Trace("quant") << " : " << f << std::endl;
544
23483
    size_t prev_lemma_waiting = d_qim.numPendingLemmas();
545
23483
    ++(d_statistics.d_num_quant);
546
23483
    Assert(f.getKind() == FORALL);
547
    // register with utilities
548
121104
    for (unsigned i = 0; i < d_util.size(); i++)
549
    {
550
97621
      d_util[i]->registerQuantifier(f);
551
    }
552
553
109441
    for (QuantifiersModule*& mdl : d_modules)
554
    {
555
171916
      Trace("quant-debug") << "check ownership with " << mdl->identify()
556
85958
                           << "..." << std::endl;
557
85958
      mdl->checkOwnership(f);
558
    }
559
23483
    QuantifiersModule* qm = d_qreg.getOwner(f);
560
46966
    Trace("quant") << " Owner : " << (qm == nullptr ? "[none]" : qm->identify())
561
23483
                   << std::endl;
562
    // register with each module
563
109441
    for (QuantifiersModule*& mdl : d_modules)
564
    {
565
171916
      Trace("quant-debug") << "register with " << mdl->identify() << "..."
566
85958
                           << std::endl;
567
85958
      mdl->registerQuantifier(f);
568
      // since this is context-independent, we should not add any lemmas during
569
      // this call
570
85958
      Assert(d_qim.numPendingLemmas() == prev_lemma_waiting);
571
    }
572
23483
    Trace("quant-debug") << "...finish." << std::endl;
573
23483
    d_quants[f] = true;
574
23483
    AlwaysAssert(d_qim.numPendingLemmas() == prev_lemma_waiting);
575
  }
576
58643
}
577
578
27726
void QuantifiersEngine::preRegisterQuantifier(Node q)
579
{
580
27726
  NodeSet::const_iterator it = d_quants_prereg.find(q);
581
27726
  if (it != d_quants_prereg.end())
582
  {
583
6539
    return;
584
  }
585
25409
  Trace("quant-debug") << "QuantifiersEngine : Pre-register " << q << std::endl;
586
25409
  d_quants_prereg.insert(q);
587
  // try to reduce
588
25409
  if (reduceQuantifier(q))
589
  {
590
    // if we can reduce it, nothing left to do
591
1905
    return;
592
  }
593
  // ensure that it is registered
594
23504
  registerQuantifierInternal(q);
595
  // register with each module
596
109544
  for (QuantifiersModule*& mdl : d_modules)
597
  {
598
172082
    Trace("quant-debug") << "pre-register with " << mdl->identify() << "..."
599
86041
                         << std::endl;
600
86042
    mdl->preRegisterQuantifier(q);
601
  }
602
  // flush the lemmas
603
23503
  d_qim.doPending();
604
23503
  Trace("quant-debug") << "...finish pre-register " << q << "..." << std::endl;
605
}
606
607
67818
void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
608
67818
  if (reduceQuantifier(f))
609
  {
610
    // if we can reduce it, nothing left to do
611
10487
    return;
612
  }
613
57331
  if( !pol ){
614
    // do skolemization
615
44384
    TrustNode lem = d_qim.getSkolemize()->process(f);
616
22192
    if (!lem.isNull())
617
    {
618
2442
      if (Trace.isOn("quantifiers-sk-debug"))
619
      {
620
        Node slem = Rewriter::rewrite(lem.getNode());
621
        Trace("quantifiers-sk-debug")
622
            << "Skolemize lemma : " << slem << std::endl;
623
      }
624
2442
      d_qim.trustedLemma(lem,
625
                         InferenceId::QUANTIFIERS_SKOLEMIZE,
626
                         LemmaProperty::NEEDS_JUSTIFY);
627
    }
628
22192
    return;
629
  }
630
  // ensure the quantified formula is registered
631
35139
  registerQuantifierInternal(f);
632
  // assert it to each module
633
35139
  d_model->assertQuantifier(f);
634
167506
  for (QuantifiersModule*& mdl : d_modules)
635
  {
636
132367
    mdl->assertNode(f);
637
  }
638
  // add term to the registry
639
35139
  d_treg.addTerm(d_qreg.getInstConstantBody(f), true);
640
}
641
642
743708
void QuantifiersEngine::eqNotifyNewClass(TNode t) { d_treg.addTerm(t); }
643
644
1970
void QuantifiersEngine::markRelevant( Node q ) {
645
1970
  d_model->markRelevant( q );
646
1970
}
647
648
79
void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
649
79
  d_qim.getInstantiate()->getInstantiationTermVectors(q, tvecs);
650
79
}
651
652
6
void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
653
6
  d_qim.getInstantiate()->getInstantiationTermVectors(insts);
654
6
}
655
656
4
void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
657
4
  if (d_qmodules->d_synth_e)
658
  {
659
4
    d_qmodules->d_synth_e->printSynthSolution(out);
660
  }else{
661
    out << "Internal error : module for synth solution not found." << std::endl;
662
  }
663
4
}
664
665
88
void QuantifiersEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
666
{
667
88
  d_qim.getInstantiate()->getInstantiatedQuantifiedFormulas(qs);
668
88
}
669
670
7
void QuantifiersEngine::getSkolemTermVectors(
671
    std::map<Node, std::vector<Node> >& sks) const
672
{
673
7
  d_qim.getSkolemize()->getSkolemTermVectors(sks);
674
7
}
675
676
8997
QuantifiersEngine::Statistics::Statistics()
677
    : d_time("theory::QuantifiersEngine::time"),
678
      d_qcf_time("theory::QuantifiersEngine::time_qcf"),
679
      d_ematching_time("theory::QuantifiersEngine::time_ematching"),
680
      d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
681
      d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
682
      d_instantiation_rounds_lc(
683
          "QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
684
      d_triggers("QuantifiersEngine::Triggers", 0),
685
      d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
686
      d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
687
8997
      d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0)
688
{
689
8997
  smtStatisticsRegistry()->registerStat(&d_time);
690
8997
  smtStatisticsRegistry()->registerStat(&d_qcf_time);
691
8997
  smtStatisticsRegistry()->registerStat(&d_ematching_time);
692
8997
  smtStatisticsRegistry()->registerStat(&d_num_quant);
693
8997
  smtStatisticsRegistry()->registerStat(&d_instantiation_rounds);
694
8997
  smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc);
695
8997
  smtStatisticsRegistry()->registerStat(&d_triggers);
696
8997
  smtStatisticsRegistry()->registerStat(&d_simple_triggers);
697
8997
  smtStatisticsRegistry()->registerStat(&d_multi_triggers);
698
8997
  smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv);
699
8997
}
700
701
17988
QuantifiersEngine::Statistics::~Statistics(){
702
8994
  smtStatisticsRegistry()->unregisterStat(&d_time);
703
8994
  smtStatisticsRegistry()->unregisterStat(&d_qcf_time);
704
8994
  smtStatisticsRegistry()->unregisterStat(&d_ematching_time);
705
8994
  smtStatisticsRegistry()->unregisterStat(&d_num_quant);
706
8994
  smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds);
707
8994
  smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc);
708
8994
  smtStatisticsRegistry()->unregisterStat(&d_triggers);
709
8994
  smtStatisticsRegistry()->unregisterStat(&d_simple_triggers);
710
8994
  smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
711
8994
  smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv);
712
8994
}
713
714
Node QuantifiersEngine::getNameForQuant(Node q) const
715
{
716
  return d_qreg.getNameForQuant(q);
717
}
718
719
20
bool QuantifiersEngine::getNameForQuant(Node q, Node& name, bool req) const
720
{
721
20
  return d_qreg.getNameForQuant(q, name, req);
722
}
723
724
250
bool QuantifiersEngine::getSynthSolutions(
725
    std::map<Node, std::map<Node, Node> >& sol_map)
726
{
727
250
  return d_qmodules->d_synth_e->getSynthSolutions(sol_map);
728
}
729
730
}  // namespace theory
731
26685
}  // namespace CVC4