GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers_engine.cpp Lines: 321 374 85.8 %
Date: 2021-03-22 Branches: 527 1248 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
8995
QuantifiersEngine::QuantifiersEngine(
50
    quantifiers::QuantifiersState& qstate,
51
    quantifiers::QuantifiersRegistry& qr,
52
    quantifiers::TermRegistry& tr,
53
    quantifiers::QuantifiersInferenceManager& qim,
54
    quantifiers::FirstOrderModel* qm,
55
8995
    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
8995
      d_tr_trie(new inst::TriggerTrie),
64
      d_model(qm),
65
8995
      d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(qstate, qm)),
66
      d_instantiate(
67
8995
          new quantifiers::Instantiate(this, qstate, qim, d_qreg, pnm)),
68
8995
      d_skolemize(new quantifiers::Skolemize(d_qstate, d_pnm)),
69
8995
      d_quants_prereg(qstate.getUserContext()),
70
53970
      d_quants_red(qstate.getUserContext())
71
{
72
  // initialize the utilities
73
8995
  d_util.push_back(d_eq_query.get());
74
  // quantifiers registry must come before the remaining utilities
75
8995
  d_util.push_back(&d_qreg);
76
8995
  d_util.push_back(tr.getTermDatabase());
77
8995
  d_util.push_back(d_instantiate.get());
78
8995
}
79
80
8992
QuantifiersEngine::~QuantifiersEngine() {}
81
82
6052
void QuantifiersEngine::finishInit(TheoryEngine* te, DecisionManager* dm)
83
{
84
6052
  d_te = te;
85
6052
  d_decManager = dm;
86
  // Initialize the modules and the utilities here.
87
6052
  d_qmodules.reset(new quantifiers::QuantifiersModules);
88
6052
  d_qmodules->initialize(this, d_qstate, d_qim, d_qreg, dm, d_modules);
89
6052
  if (d_qmodules->d_rel_dom.get())
90
  {
91
79
    d_util.push_back(d_qmodules->d_rel_dom.get());
92
  }
93
94
  // handle any circular dependencies
95
96
  // quantifiers bound inference needs to be informed of the bounded integers
97
  // module, which has information about which quantifiers have finite bounds
98
6052
  d_qreg.getQuantifiersBoundInference().finishInit(d_qmodules->d_bint.get());
99
6052
}
100
101
2287
DecisionManager* QuantifiersEngine::getDecisionManager()
102
{
103
2287
  return d_decManager;
104
}
105
106
3246754
quantifiers::QuantifiersState& QuantifiersEngine::getState()
107
{
108
3246754
  return d_qstate;
109
}
110
quantifiers::QuantifiersInferenceManager&
111
QuantifiersEngine::getInferenceManager()
112
{
113
  return d_qim;
114
}
115
116
6
quantifiers::QuantifiersRegistry& QuantifiersEngine::getQuantifiersRegistry()
117
{
118
6
  return d_qreg;
119
}
120
121
17256
quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
122
{
123
17256
  return d_qmodules->d_builder.get();
124
}
125
748286
quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const
126
{
127
748286
  return d_model;
128
}
129
18046097
quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const
130
{
131
18046097
  return d_treg.getTermDatabase();
132
}
133
30467
quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() const
134
{
135
30467
  return d_treg.getTermDatabaseSygus();
136
}
137
1745
quantifiers::TermEnumeration* QuantifiersEngine::getTermEnumeration() const
138
{
139
1745
  return d_treg.getTermEnumeration();
140
}
141
531070
quantifiers::Instantiate* QuantifiersEngine::getInstantiate() const
142
{
143
531070
  return d_instantiate.get();
144
}
145
33
quantifiers::Skolemize* QuantifiersEngine::getSkolemize() const
146
{
147
33
  return d_skolemize.get();
148
}
149
29565
inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
150
{
151
29565
  return d_tr_trie.get();
152
}
153
154
6438
void QuantifiersEngine::presolve() {
155
6438
  Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
156
6438
  d_qim.clearPending();
157
32139
  for( unsigned i=0; i<d_modules.size(); i++ ){
158
25701
    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
6438
  d_treg.presolve();
163
6438
}
164
165
5907
void QuantifiersEngine::ppNotifyAssertions(
166
    const std::vector<Node>& assertions) {
167
11814
  Trace("quant-engine-proc")
168
11814
      << "ppNotifyAssertions in QE, #assertions = " << assertions.size()
169
5907
      << std::endl;
170
5907
  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
5907
  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
5907
  if (options::sygusInst())
189
  {
190
19
    quantifiers::SygusInst* si = d_qmodules->d_sygus_inst.get();
191
19
    si->ppNotifyAssertions(assertions);
192
  }
193
5907
}
194
195
86191
void QuantifiersEngine::check( Theory::Effort e ){
196
172382
  CodeTimer codeTimer(d_statistics.d_time);
197
86191
  Assert(d_qstate.getEqualityEngine() != nullptr);
198
86191
  if (!d_qstate.getEqualityEngine()->consistent())
199
  {
200
    Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl;
201
    return;
202
  }
203
86191
  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
86191
  bool needsCheck = d_qim.hasPendingLemma();
229
86191
  QuantifiersModule::QEffort needsModelE = QuantifiersModule::QEFFORT_NONE;
230
172382
  std::vector< QuantifiersModule* > qm;
231
86191
  if( d_model->checkNeeded() ){
232
72173
    needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL;  //always need to check at or above last call
233
363852
    for (QuantifiersModule*& mdl : d_modules)
234
    {
235
291679
      if (mdl->needsCheck(e))
236
      {
237
56331
        qm.push_back(mdl);
238
56331
        needsCheck = true;
239
        //can only request model at last call since theory combination can find inconsistencies
240
56331
        if( e>=Theory::EFFORT_LAST_CALL ){
241
39991
          QuantifiersModule::QEffort me = mdl->needsModel(e);
242
39991
          needsModelE = me<needsModelE ? me : needsModelE;
243
        }
244
      }
245
    }
246
  }
247
248
86191
  d_qim.reset();
249
86191
  bool setIncomplete = false;
250
251
86191
  Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
252
86191
  if( needsCheck ){
253
    //flush previous lemmas (for instance, if was interrupted), or other lemmas to process
254
28251
    d_qim.doPending();
255
28251
    if (d_qim.hasSentLemma())
256
    {
257
      return;
258
    }
259
260
28251
    double clSet = 0;
261
28251
    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
28251
    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
28251
    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
28251
    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
28251
    Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl;
299
142371
    for (QuantifiersUtil*& util : d_util)
300
    {
301
228240
      Trace("quant-engine-debug2") << "Reset " << util->identify().c_str()
302
114120
                                   << "..." << std::endl;
303
114120
      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
28251
    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
28251
    Trace("quant-engine-debug") << "Reset model..." << std::endl;
323
28251
    d_model->reset_round();
324
325
    //reset the modules
326
28251
    Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
327
145216
    for (QuantifiersModule*& mdl : d_modules)
328
    {
329
233930
      Trace("quant-engine-debug2") << "Reset " << mdl->identify().c_str()
330
116965
                                   << std::endl;
331
116965
      mdl->reset_round(e);
332
    }
333
28251
    Trace("quant-engine-debug") << "Done resetting all modules." << std::endl;
334
    //reset may have added lemmas
335
28251
    d_qim.doPending();
336
28251
    if (d_qim.hasSentLemma())
337
    {
338
      return;
339
    }
340
341
28251
    if( e==Theory::EFFORT_LAST_CALL ){
342
14464
      ++(d_statistics.d_instantiation_rounds_lc);
343
13787
    }else if( e==Theory::EFFORT_FULL ){
344
13787
      ++(d_statistics.d_instantiation_rounds);
345
    }
346
28251
    Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
347
108125
    for (unsigned qef = QuantifiersModule::QEFFORT_CONFLICT;
348
108125
         qef <= QuantifiersModule::QEFFORT_LAST_CALL;
349
         ++qef)
350
    {
351
92959
      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
92959
      if (needsModelE == quant_e)
355
      {
356
13650
        Trace("quant-engine-debug") << "Build model..." << std::endl;
357
13650
        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
13072
          break;
363
        }
364
      }
365
92959
      if (!d_qim.hasSentLemma())
366
      {
367
        //check each module
368
271841
        for (QuantifiersModule*& mdl : qm)
369
        {
370
357800
          Trace("quant-engine-debug") << "Check " << mdl->identify().c_str()
371
178900
                                      << " at effort " << quant_e << "..."
372
178900
                                      << std::endl;
373
178900
          mdl->check(e, quant_e);
374
178888
          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
92947
        d_qim.doPending();
382
      }
383
      //if we have added one, stop
384
92946
      if (d_qim.hasSentLemma())
385
      {
386
12604
        break;
387
      }else{
388
80342
        Assert(!d_qstate.isInConflict());
389
80342
        if (quant_e == QuantifiersModule::QEFFORT_CONFLICT)
390
        {
391
26968
          d_qstate.incrementInstRoundCounters(e);
392
        }
393
53374
        else if (quant_e == QuantifiersModule::QEFFORT_MODEL)
394
        {
395
15761
          if( e==Theory::EFFORT_LAST_CALL ){
396
            //sources of incompleteness
397
18248
            for (QuantifiersUtil*& util : d_util)
398
            {
399
14636
              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
3612
            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
3612
            if( !setIncomplete ){
414
              //check if we should set the incomplete flag
415
17922
              for (QuantifiersModule*& mdl : d_modules)
416
              {
417
14375
                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
3611
              if( !setIncomplete ){
428
                //look at individual quantified formulas, one module must claim completeness for each one
429
4847
                for( unsigned i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
430
4379
                  bool hasCompleteM = false;
431
5679
                  Node q = d_model->getAssertedQuantifier( i );
432
4379
                  QuantifiersModule* qmd = d_qreg.getOwner(q);
433
4379
                  if( qmd!=NULL ){
434
3072
                    hasCompleteM = qmd->checkCompleteFor( q );
435
                  }else{
436
4988
                    for( unsigned j=0; j<d_modules.size(); j++ ){
437
4793
                      if( d_modules[j]->checkCompleteFor( q ) ){
438
1112
                        qmd = d_modules[j];
439
1112
                        hasCompleteM = true;
440
1112
                        break;
441
                      }
442
                    }
443
                  }
444
4379
                  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
1300
                    Assert(qmd != NULL);
450
1300
                    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
3612
            if( !setIncomplete ){
457
468
              break;
458
            }
459
          }
460
        }
461
      }
462
    }
463
28238
    Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
464
    // debug print
465
28238
    if (d_qim.hasSentLemma())
466
    {
467
12604
      bool debugInstTrace = Trace.isOn("inst-per-quant-round");
468
12604
      if (options::debugInst() || debugInstTrace)
469
      {
470
2
        Options& sopts = smt::currentSmtEngine()->getOptions();
471
2
        std::ostream& out = *sopts.getOut();
472
2
        d_instantiate->debugPrint(out);
473
      }
474
    }
475
28238
    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
28238
    Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl;
483
  }else{
484
57940
    Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl;
485
  }
486
487
  //SAT case
488
86178
  if (e == Theory::EFFORT_LAST_CALL && !d_qim.hasSentLemma())
489
  {
490
5822
    if( setIncomplete ){
491
3017
      Trace("quant-engine") << "Set incomplete flag." << std::endl;
492
3017
      d_qim.setIncomplete();
493
    }
494
    //output debug stats
495
5822
    d_instantiate->debugPrintModel();
496
  }
497
}
498
499
15756
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
15756
}
504
505
93221
bool QuantifiersEngine::reduceQuantifier( Node q ) {
506
  //TODO: this can be unified with preregistration: AlphaEquivalence takes ownership of reducable quants
507
93221
  BoolMap::const_iterator it = d_quants_red.find( q );
508
93221
  if( it==d_quants_red.end() ){
509
50814
    Node lem;
510
25407
    InferenceId id = InferenceId::UNKNOWN;
511
25407
    std::map< Node, Node >::iterator itr = d_quants_red_lem.find( q );
512
25407
    if( itr==d_quants_red_lem.end() ){
513
25386
      if (d_qmodules->d_alpha_equiv)
514
      {
515
25386
        Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl;
516
        //add equivalence with another quantified formula
517
25386
        lem = d_qmodules->d_alpha_equiv->reduceQuantifier(q);
518
25386
        id = InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ;
519
25386
        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
25386
      d_quants_red_lem[q] = lem;
525
    }else{
526
21
      lem = itr->second;
527
    }
528
25407
    if( !lem.isNull() ){
529
1905
      d_qim.lemma(lem, id);
530
    }
531
25407
    d_quants_red[q] = !lem.isNull();
532
25407
    return !lem.isNull();
533
  }else{
534
67814
    return (*it).second;
535
  }
536
}
537
538
58637
void QuantifiersEngine::registerQuantifierInternal(Node f)
539
{
540
58637
  std::map< Node, bool >::iterator it = d_quants.find( f );
541
58637
  if( it==d_quants.end() ){
542
23481
    Trace("quant") << "QuantifiersEngine : Register quantifier ";
543
23481
    Trace("quant") << " : " << f << std::endl;
544
23481
    size_t prev_lemma_waiting = d_qim.numPendingLemmas();
545
23481
    ++(d_statistics.d_num_quant);
546
23481
    Assert(f.getKind() == FORALL);
547
    // register with utilities
548
121094
    for (unsigned i = 0; i < d_util.size(); i++)
549
    {
550
97613
      d_util[i]->registerQuantifier(f);
551
    }
552
553
109427
    for (QuantifiersModule*& mdl : d_modules)
554
    {
555
171892
      Trace("quant-debug") << "check ownership with " << mdl->identify()
556
85946
                           << "..." << std::endl;
557
85946
      mdl->checkOwnership(f);
558
    }
559
23481
    QuantifiersModule* qm = d_qreg.getOwner(f);
560
46962
    Trace("quant") << " Owner : " << (qm == nullptr ? "[none]" : qm->identify())
561
23481
                   << std::endl;
562
    // register with each module
563
109427
    for (QuantifiersModule*& mdl : d_modules)
564
    {
565
171892
      Trace("quant-debug") << "register with " << mdl->identify() << "..."
566
85946
                           << std::endl;
567
85946
      mdl->registerQuantifier(f);
568
      // since this is context-independent, we should not add any lemmas during
569
      // this call
570
85946
      Assert(d_qim.numPendingLemmas() == prev_lemma_waiting);
571
    }
572
23481
    Trace("quant-debug") << "...finish." << std::endl;
573
23481
    d_quants[f] = true;
574
23481
    AlwaysAssert(d_qim.numPendingLemmas() == prev_lemma_waiting);
575
  }
576
58637
}
577
578
27722
void QuantifiersEngine::preRegisterQuantifier(Node q)
579
{
580
27722
  NodeSet::const_iterator it = d_quants_prereg.find(q);
581
27722
  if (it != d_quants_prereg.end())
582
  {
583
6535
    return;
584
  }
585
25407
  Trace("quant-debug") << "QuantifiersEngine : Pre-register " << q << std::endl;
586
25407
  d_quants_prereg.insert(q);
587
  // try to reduce
588
25407
  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
23502
  registerQuantifierInternal(q);
595
  // register with each module
596
109530
  for (QuantifiersModule*& mdl : d_modules)
597
  {
598
172058
    Trace("quant-debug") << "pre-register with " << mdl->identify() << "..."
599
86029
                         << std::endl;
600
86030
    mdl->preRegisterQuantifier(q);
601
  }
602
  // flush the lemmas
603
23501
  d_qim.doPending();
604
23501
  Trace("quant-debug") << "...finish pre-register " << q << "..." << std::endl;
605
}
606
607
67814
void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
608
67814
  if (reduceQuantifier(f))
609
  {
610
    // if we can reduce it, nothing left to do
611
10487
    return;
612
  }
613
57327
  if( !pol ){
614
    // do skolemization
615
44384
    TrustNode lem = d_skolemize->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
35135
  registerQuantifierInternal(f);
632
  // assert it to each module
633
35135
  d_model->assertQuantifier(f);
634
167478
  for (QuantifiersModule*& mdl : d_modules)
635
  {
636
132343
    mdl->assertNode(f);
637
  }
638
  // add term to the registry
639
35135
  d_treg.addTerm(d_qreg.getInstConstantBody(f), true);
640
}
641
642
743568
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_instantiate->getInstantiationTermVectors(q, tvecs);
650
79
}
651
652
6
void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
653
6
  d_instantiate->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_instantiate->getInstantiatedQuantifiedFormulas(qs);
668
88
}
669
670
7
void QuantifiersEngine::getSkolemTermVectors(
671
    std::map<Node, std::vector<Node> >& sks) const
672
{
673
7
  d_skolemize->getSkolemTermVectors(sks);
674
7
}
675
676
8995
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
8995
      d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0)
688
{
689
8995
  smtStatisticsRegistry()->registerStat(&d_time);
690
8995
  smtStatisticsRegistry()->registerStat(&d_qcf_time);
691
8995
  smtStatisticsRegistry()->registerStat(&d_ematching_time);
692
8995
  smtStatisticsRegistry()->registerStat(&d_num_quant);
693
8995
  smtStatisticsRegistry()->registerStat(&d_instantiation_rounds);
694
8995
  smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc);
695
8995
  smtStatisticsRegistry()->registerStat(&d_triggers);
696
8995
  smtStatisticsRegistry()->registerStat(&d_simple_triggers);
697
8995
  smtStatisticsRegistry()->registerStat(&d_multi_triggers);
698
8995
  smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv);
699
8995
}
700
701
17984
QuantifiersEngine::Statistics::~Statistics(){
702
8992
  smtStatisticsRegistry()->unregisterStat(&d_time);
703
8992
  smtStatisticsRegistry()->unregisterStat(&d_qcf_time);
704
8992
  smtStatisticsRegistry()->unregisterStat(&d_ematching_time);
705
8992
  smtStatisticsRegistry()->unregisterStat(&d_num_quant);
706
8992
  smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds);
707
8992
  smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc);
708
8992
  smtStatisticsRegistry()->unregisterStat(&d_triggers);
709
8992
  smtStatisticsRegistry()->unregisterStat(&d_simple_triggers);
710
8992
  smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
711
8992
  smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv);
712
8992
}
713
714
75368
Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
715
75368
  return d_eq_query->getInternalRepresentative(a, q, index);
716
}
717
718
Node QuantifiersEngine::getNameForQuant(Node q) const
719
{
720
  return d_qreg.getNameForQuant(q);
721
}
722
723
24
bool QuantifiersEngine::getNameForQuant(Node q, Node& name, bool req) const
724
{
725
24
  return d_qreg.getNameForQuant(q, name, req);
726
}
727
728
250
bool QuantifiersEngine::getSynthSolutions(
729
    std::map<Node, std::map<Node, Node> >& sol_map)
730
{
731
250
  return d_qmodules->d_synth_e->getSynthSolutions(sol_map);
732
}
733
734
}  // namespace theory
735
26676
}  // namespace CVC4