Generate code for options with modes. (#3561)
[cvc5.git] / src / theory / quantifiers_engine.cpp
1 /********************* */
2 /*! \file quantifiers_engine.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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/quantifiers_options.h"
18 #include "options/uf_options.h"
19 #include "smt/smt_statistics_registry.h"
20 #include "theory/quantifiers/alpha_equivalence.h"
21 #include "theory/quantifiers/anti_skolem.h"
22 #include "theory/quantifiers/conjecture_generator.h"
23 #include "theory/quantifiers/ematching/instantiation_engine.h"
24 #include "theory/quantifiers/fmf/bounded_integers.h"
25 #include "theory/quantifiers/fmf/full_model_check.h"
26 #include "theory/quantifiers/fmf/model_engine.h"
27 #include "theory/quantifiers/inst_propagator.h"
28 #include "theory/quantifiers/inst_strategy_enumerative.h"
29 #include "theory/quantifiers/local_theory_ext.h"
30 #include "theory/quantifiers/quant_conflict_find.h"
31 #include "theory/quantifiers/quant_split.h"
32 #include "theory/quantifiers/quantifiers_rewriter.h"
33 #include "theory/quantifiers/rewrite_engine.h"
34 #include "theory/quantifiers/sygus/synth_engine.h"
35 #include "theory/sep/theory_sep.h"
36 #include "theory/theory_engine.h"
37 #include "theory/uf/equality_engine.h"
38
39 using namespace std;
40 using namespace CVC4::kind;
41
42 namespace CVC4 {
43 namespace theory {
44
45 class QuantifiersEnginePrivate
46 {
47 public:
48 QuantifiersEnginePrivate()
49 : d_inst_prop(nullptr),
50 d_rel_dom(nullptr),
51 d_alpha_equiv(nullptr),
52 d_inst_engine(nullptr),
53 d_model_engine(nullptr),
54 d_bint(nullptr),
55 d_qcf(nullptr),
56 d_rr_engine(nullptr),
57 d_sg_gen(nullptr),
58 d_synth_e(nullptr),
59 d_lte_part_inst(nullptr),
60 d_fs(nullptr),
61 d_i_cbqi(nullptr),
62 d_qsplit(nullptr),
63 d_anti_skolem(nullptr)
64 {
65 }
66 ~QuantifiersEnginePrivate() {}
67 //------------------------------ private quantifier utilities
68 /** quantifiers instantiation propagator */
69 std::unique_ptr<quantifiers::InstPropagator> d_inst_prop;
70 /** relevant domain */
71 std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom;
72 //------------------------------ end private quantifier utilities
73 //------------------------------ quantifiers modules
74 /** alpha equivalence */
75 std::unique_ptr<quantifiers::AlphaEquivalence> d_alpha_equiv;
76 /** instantiation engine */
77 std::unique_ptr<quantifiers::InstantiationEngine> d_inst_engine;
78 /** model engine */
79 std::unique_ptr<quantifiers::ModelEngine> d_model_engine;
80 /** bounded integers utility */
81 std::unique_ptr<quantifiers::BoundedIntegers> d_bint;
82 /** Conflict find mechanism for quantifiers */
83 std::unique_ptr<quantifiers::QuantConflictFind> d_qcf;
84 /** rewrite rules utility */
85 std::unique_ptr<quantifiers::RewriteEngine> d_rr_engine;
86 /** subgoal generator */
87 std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen;
88 /** ceg instantiation */
89 std::unique_ptr<quantifiers::SynthEngine> d_synth_e;
90 /** lte partial instantiation */
91 std::unique_ptr<quantifiers::LtePartialInst> d_lte_part_inst;
92 /** full saturation */
93 std::unique_ptr<quantifiers::InstStrategyEnum> d_fs;
94 /** counterexample-based quantifier instantiation */
95 std::unique_ptr<quantifiers::InstStrategyCegqi> d_i_cbqi;
96 /** quantifiers splitting */
97 std::unique_ptr<quantifiers::QuantDSplit> d_qsplit;
98 /** quantifiers anti-skolemization */
99 std::unique_ptr<quantifiers::QuantAntiSkolem> d_anti_skolem;
100 //------------------------------ end quantifiers modules
101 /** initialize
102 *
103 * This constructs the above modules based on the current options. It adds
104 * a pointer to each module it constructs to modules. This method sets
105 * needsBuilder to true if we require a strategy-specific model builder
106 * utility.
107 */
108 void initialize(QuantifiersEngine* qe,
109 context::Context* c,
110 std::vector<QuantifiersModule*>& modules,
111 bool& needsBuilder)
112 {
113 // add quantifiers modules
114 if (options::quantConflictFind() || options::quantRewriteRules())
115 {
116 d_qcf.reset(new quantifiers::QuantConflictFind(qe, c));
117 modules.push_back(d_qcf.get());
118 }
119 if (options::conjectureGen())
120 {
121 d_sg_gen.reset(new quantifiers::ConjectureGenerator(qe, c));
122 modules.push_back(d_sg_gen.get());
123 }
124 if (!options::finiteModelFind() || options::fmfInstEngine())
125 {
126 d_inst_engine.reset(new quantifiers::InstantiationEngine(qe));
127 modules.push_back(d_inst_engine.get());
128 }
129 if (options::cbqi())
130 {
131 d_i_cbqi.reset(new quantifiers::InstStrategyCegqi(qe));
132 modules.push_back(d_i_cbqi.get());
133 qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter());
134 }
135 if (options::ceGuidedInst())
136 {
137 d_synth_e.reset(new quantifiers::SynthEngine(qe, c));
138 modules.push_back(d_synth_e.get());
139 }
140 // finite model finding
141 if (options::fmfBound())
142 {
143 d_bint.reset(new quantifiers::BoundedIntegers(c, qe));
144 modules.push_back(d_bint.get());
145 }
146 if (options::finiteModelFind() || options::fmfBound())
147 {
148 d_model_engine.reset(new quantifiers::ModelEngine(c, qe));
149 modules.push_back(d_model_engine.get());
150 // finite model finder has special ways of building the model
151 needsBuilder = true;
152 }
153 if (options::quantRewriteRules())
154 {
155 d_rr_engine.reset(new quantifiers::RewriteEngine(c, qe, d_qcf.get()));
156 modules.push_back(d_rr_engine.get());
157 }
158 if (options::ltePartialInst())
159 {
160 d_lte_part_inst.reset(new quantifiers::LtePartialInst(qe, c));
161 modules.push_back(d_lte_part_inst.get());
162 }
163 if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE)
164 {
165 d_qsplit.reset(new quantifiers::QuantDSplit(qe, c));
166 modules.push_back(d_qsplit.get());
167 }
168 if (options::quantAntiSkolem())
169 {
170 d_anti_skolem.reset(new quantifiers::QuantAntiSkolem(qe));
171 modules.push_back(d_anti_skolem.get());
172 }
173 if (options::quantAlphaEquiv())
174 {
175 d_alpha_equiv.reset(new quantifiers::AlphaEquivalence(qe));
176 }
177 // full saturation : instantiate from relevant domain, then arbitrary terms
178 if (options::fullSaturateQuant() || options::fullSaturateInterleave())
179 {
180 d_rel_dom.reset(new quantifiers::RelevantDomain(qe));
181 d_fs.reset(new quantifiers::InstStrategyEnum(qe, d_rel_dom.get()));
182 modules.push_back(d_fs.get());
183 }
184 }
185 };
186
187 QuantifiersEngine::QuantifiersEngine(context::Context* c,
188 context::UserContext* u,
189 TheoryEngine* te)
190 : d_te(te),
191 d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)),
192 d_tr_trie(new inst::TriggerTrie),
193 d_model(nullptr),
194 d_builder(nullptr),
195 d_qepr(nullptr),
196 d_term_util(new quantifiers::TermUtil(this)),
197 d_term_canon(new expr::TermCanonize),
198 d_term_db(new quantifiers::TermDb(c, u, this)),
199 d_sygus_tdb(nullptr),
200 d_quant_attr(new quantifiers::QuantAttributes(this)),
201 d_instantiate(new quantifiers::Instantiate(this, u)),
202 d_skolemize(new quantifiers::Skolemize(this, u)),
203 d_term_enum(new quantifiers::TermEnumeration),
204 d_conflict_c(c, false),
205 // d_quants(u),
206 d_quants_prereg(u),
207 d_quants_red(u),
208 d_lemmas_produced_c(u),
209 d_ierCounter_c(c),
210 // d_ierCounter(c),
211 // d_ierCounter_lc(c),
212 // d_ierCounterLastLc(c),
213 d_presolve(u, true),
214 d_presolve_in(u),
215 d_presolve_cache(u),
216 d_presolve_cache_wq(u),
217 d_presolve_cache_wic(u)
218 {
219 // initialize the private utility
220 d_private.reset(new QuantifiersEnginePrivate);
221
222 //---- utilities
223 d_util.push_back(d_eq_query.get());
224 // term util must come before the other utilities
225 d_util.push_back(d_term_util.get());
226 d_util.push_back(d_term_db.get());
227
228 if (options::ceGuidedInst()) {
229 d_sygus_tdb.reset(new quantifiers::TermDbSygus(c, this));
230 }
231
232 if( options::instPropagate() ){
233 // notice that this option is incompatible with options::qcfAllConflict()
234 d_private->d_inst_prop.reset(new quantifiers::InstPropagator(this));
235 d_util.push_back(d_private->d_inst_prop.get());
236 d_instantiate->addNotify(d_private->d_inst_prop->getInstantiationNotify());
237 }
238
239
240 d_util.push_back(d_instantiate.get());
241
242 d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
243 d_conflict = false;
244 d_hasAddedLemma = false;
245 d_useModelEe = false;
246 //don't add true lemma
247 d_lemmas_produced_c[d_term_util->d_true] = true;
248
249 Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
250 Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
251
252 if( options::quantEpr() ){
253 Assert(!options::incrementalSolving());
254 d_qepr.reset(new quantifiers::QuantEPR);
255 }
256 //---- end utilities
257
258 //allow theory combination to go first, once initially
259 d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
260 d_ierCounter_c = d_ierCounter;
261 d_ierCounter_lc = 0;
262 d_ierCounterLastLc = 0;
263 d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
264
265 bool needsBuilder = false;
266 d_private->initialize(this, c, d_modules, needsBuilder);
267
268 if (d_private->d_rel_dom.get())
269 {
270 d_util.push_back(d_private->d_rel_dom.get());
271 }
272
273 // if we require specialized ways of building the model
274 if( needsBuilder ){
275 Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl;
276 if (options::mbqiMode() == options::MbqiMode::FMC
277 || options::mbqiMode() == options::MbqiMode::TRUST
278 || options::fmfBound())
279 {
280 Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
281 d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
282 this, c, "FirstOrderModelFmc"));
283 d_builder.reset(new quantifiers::fmcheck::FullModelChecker(c, this));
284 }else{
285 Trace("quant-engine-debug") << "...make default model builder." << std::endl;
286 d_model.reset(
287 new quantifiers::FirstOrderModel(this, c, "FirstOrderModel"));
288 d_builder.reset(new quantifiers::QModelBuilder(c, this));
289 }
290 }else{
291 d_model.reset(new quantifiers::FirstOrderModel(this, c, "FirstOrderModel"));
292 }
293 }
294
295 QuantifiersEngine::~QuantifiersEngine() {}
296
297 context::Context* QuantifiersEngine::getSatContext()
298 {
299 return d_te->theoryOf(THEORY_QUANTIFIERS)->getSatContext();
300 }
301
302 context::UserContext* QuantifiersEngine::getUserContext()
303 {
304 return d_te->theoryOf(THEORY_QUANTIFIERS)->getUserContext();
305 }
306
307 OutputChannel& QuantifiersEngine::getOutputChannel()
308 {
309 return d_te->theoryOf(THEORY_QUANTIFIERS)->getOutputChannel();
310 }
311 /** get default valuation for the quantifiers engine */
312 Valuation& QuantifiersEngine::getValuation()
313 {
314 return d_te->theoryOf(THEORY_QUANTIFIERS)->getValuation();
315 }
316
317 const LogicInfo& QuantifiersEngine::getLogicInfo() const
318 {
319 return d_te->getLogicInfo();
320 }
321
322 EqualityQuery* QuantifiersEngine::getEqualityQuery() const
323 {
324 return d_eq_query.get();
325 }
326 quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
327 {
328 return d_builder.get();
329 }
330 quantifiers::QuantEPR* QuantifiersEngine::getQuantEPR() const
331 {
332 return d_qepr.get();
333 }
334 quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const
335 {
336 return d_model.get();
337 }
338 quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const
339 {
340 return d_term_db.get();
341 }
342 quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() const
343 {
344 return d_sygus_tdb.get();
345 }
346 quantifiers::TermUtil* QuantifiersEngine::getTermUtil() const
347 {
348 return d_term_util.get();
349 }
350 expr::TermCanonize* QuantifiersEngine::getTermCanonize() const
351 {
352 return d_term_canon.get();
353 }
354 quantifiers::QuantAttributes* QuantifiersEngine::getQuantAttributes() const
355 {
356 return d_quant_attr.get();
357 }
358 quantifiers::Instantiate* QuantifiersEngine::getInstantiate() const
359 {
360 return d_instantiate.get();
361 }
362 quantifiers::Skolemize* QuantifiersEngine::getSkolemize() const
363 {
364 return d_skolemize.get();
365 }
366 quantifiers::TermEnumeration* QuantifiersEngine::getTermEnumeration() const
367 {
368 return d_term_enum.get();
369 }
370 inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
371 {
372 return d_tr_trie.get();
373 }
374
375 QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
376 std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q );
377 if( it==d_owner.end() ){
378 return NULL;
379 }else{
380 return it->second;
381 }
382 }
383
384 void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m, int priority ) {
385 QuantifiersModule * mo = getOwner( q );
386 if( mo!=m ){
387 if( mo!=NULL ){
388 if( priority<=d_owner_priority[q] ){
389 Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << ( m ? m->identify() : "null" ) << ", but already has owner " << mo->identify() << " with higher priority!" << std::endl;
390 return;
391 }
392 }
393 d_owner[q] = m;
394 d_owner_priority[q] = priority;
395 }
396 }
397
398 void QuantifiersEngine::setOwner(Node q, quantifiers::QAttributes& qa)
399 {
400 if (!qa.d_rr.isNull())
401 {
402 if (d_private->d_rr_engine.get() == nullptr)
403 {
404 Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : "
405 << q << std::endl;
406 }
407 // set rewrite engine as owner
408 setOwner(q, d_private->d_rr_engine.get(), 2);
409 }
410 if (qa.d_sygus || (options::sygusRecFun() && !qa.d_fundef_f.isNull()))
411 {
412 if (d_private->d_synth_e.get() == nullptr)
413 {
414 Trace("quant-warn") << "WARNING : synth engine is null, and we have : "
415 << q << std::endl;
416 }
417 // set synth engine as owner since this is either a conjecture or a function
418 // definition to be used by sygus
419 setOwner(q, d_private->d_synth_e.get(), 2);
420 }
421 }
422
423 bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) {
424 QuantifiersModule * mo = getOwner( q );
425 return mo==m || mo==NULL;
426 }
427
428 bool QuantifiersEngine::isFiniteBound(Node q, Node v) const
429 {
430 quantifiers::BoundedIntegers* bi = d_private->d_bint.get();
431 if (bi && bi->isBound(q, v))
432 {
433 return true;
434 }
435 TypeNode tn = v.getType();
436 if (tn.isSort() && options::finiteModelFind())
437 {
438 return true;
439 }
440 else if (d_term_enum->mayComplete(tn))
441 {
442 return true;
443 }
444 return false;
445 }
446
447 BoundVarType QuantifiersEngine::getBoundVarType(Node q, Node v) const
448 {
449 quantifiers::BoundedIntegers* bi = d_private->d_bint.get();
450 if (bi)
451 {
452 return bi->getBoundVarType(q, v);
453 }
454 return isFiniteBound(q, v) ? BOUND_FINITE : BOUND_NONE;
455 }
456
457 void QuantifiersEngine::getBoundVarIndices(Node q,
458 std::vector<unsigned>& indices) const
459 {
460 Assert(indices.empty());
461 // we take the bounded variables first
462 quantifiers::BoundedIntegers* bi = d_private->d_bint.get();
463 if (bi)
464 {
465 bi->getBoundVarIndices(q, indices);
466 }
467 // then get the remaining ones
468 for (unsigned i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
469 {
470 if (std::find(indices.begin(), indices.end(), i) == indices.end())
471 {
472 indices.push_back(i);
473 }
474 }
475 }
476
477 bool QuantifiersEngine::getBoundElements(RepSetIterator* rsi,
478 bool initial,
479 Node q,
480 Node v,
481 std::vector<Node>& elements) const
482 {
483 quantifiers::BoundedIntegers* bi = d_private->d_bint.get();
484 if (bi)
485 {
486 return bi->getBoundElements(rsi, initial, q, v, elements);
487 }
488 return false;
489 }
490
491 void QuantifiersEngine::presolve() {
492 Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
493 for( unsigned i=0; i<d_modules.size(); i++ ){
494 d_modules[i]->presolve();
495 }
496 d_term_db->presolve();
497 d_presolve = false;
498 //add all terms to database
499 if( options::incrementalSolving() ){
500 Trace("quant-engine-proc") << "Add presolve cache " << d_presolve_cache.size() << std::endl;
501 for( unsigned i=0; i<d_presolve_cache.size(); i++ ){
502 addTermToDatabase( d_presolve_cache[i], d_presolve_cache_wq[i], d_presolve_cache_wic[i] );
503 }
504 Trace("quant-engine-proc") << "Done add presolve cache " << std::endl;
505 }
506 }
507
508 void QuantifiersEngine::ppNotifyAssertions(
509 const std::vector<Node>& assertions) {
510 Trace("quant-engine-proc")
511 << "ppNotifyAssertions in QE, #assertions = " << assertions.size()
512 << " check epr = " << (d_qepr != NULL) << std::endl;
513 if (options::instLevelInputOnly() && options::instMaxLevel() != -1)
514 {
515 for (const Node& a : assertions)
516 {
517 quantifiers::QuantAttributes::setInstantiationLevelAttr(a, 0);
518 }
519 }
520 if (d_qepr != NULL)
521 {
522 for (const Node& a : assertions)
523 {
524 d_qepr->registerAssertion(a);
525 }
526 // must handle sources of other new constants e.g. separation logic
527 // FIXME (as part of project 3) : cleanup
528 sep::TheorySep* theory_sep =
529 static_cast<sep::TheorySep*>(getTheoryEngine()->theoryOf(THEORY_SEP));
530 theory_sep->initializeBounds();
531 d_qepr->finishInit();
532 }
533 if (options::ceGuidedInst())
534 {
535 quantifiers::SynthEngine* sye = d_private->d_synth_e.get();
536 for (const Node& a : assertions)
537 {
538 sye->preregisterAssertion(a);
539 }
540 }
541 }
542
543 void QuantifiersEngine::check( Theory::Effort e ){
544 CodeTimer codeTimer(d_statistics.d_time);
545 d_useModelEe = options::quantModelEe() && ( e>=Theory::EFFORT_LAST_CALL );
546 // if we want to use the model's equality engine, build the model now
547 if( d_useModelEe && !d_model->isBuilt() ){
548 Trace("quant-engine-debug") << "Build the model." << std::endl;
549 if (!d_te->getModelBuilder()->buildModel(d_model.get()))
550 {
551 //we are done if model building was unsuccessful
552 flushLemmas();
553 if( d_hasAddedLemma ){
554 Trace("quant-engine-debug") << "...failed." << std::endl;
555 return;
556 }
557 }
558 }
559
560 if( !getActiveEqualityEngine()->consistent() ){
561 Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl;
562 return;
563 }
564 if (d_conflict_c.get())
565 {
566 if (e < Theory::EFFORT_LAST_CALL)
567 {
568 // this can happen in rare cases when quantifiers is the first to realize
569 // there is a quantifier-free conflict, for example, when it discovers
570 // disequal and congruent terms in the master equality engine during
571 // term indexing. In such cases, quantifiers reports a "conflicting lemma"
572 // that is, one that is entailed to be false by the current assignment.
573 // If this lemma is not a SAT conflict, we may get another call to full
574 // effort check and the quantifier-free solvers still haven't realized
575 // there is a conflict. In this case, we return, trusting that theory
576 // combination will do the right thing (split on equalities until there is
577 // a conflict at the quantifier-free level).
578 Trace("quant-engine-debug")
579 << "Conflicting lemma already reported by quantifiers, return."
580 << std::endl;
581 return;
582 }
583 // we reported what we thought was a conflicting lemma, but now we have
584 // gotten a check at LAST_CALL effort, indicating that the lemma we reported
585 // was not conflicting. This should never happen, but in production mode, we
586 // proceed with the check.
587 Assert(false);
588 }
589 bool needsCheck = !d_lemmas_waiting.empty();
590 QuantifiersModule::QEffort needsModelE = QuantifiersModule::QEFFORT_NONE;
591 std::vector< QuantifiersModule* > qm;
592 if( d_model->checkNeeded() ){
593 needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call
594 for (QuantifiersModule*& mdl : d_modules)
595 {
596 if (mdl->needsCheck(e))
597 {
598 qm.push_back(mdl);
599 needsCheck = true;
600 //can only request model at last call since theory combination can find inconsistencies
601 if( e>=Theory::EFFORT_LAST_CALL ){
602 QuantifiersModule::QEffort me = mdl->needsModel(e);
603 needsModelE = me<needsModelE ? me : needsModelE;
604 }
605 }
606 }
607 }
608
609 d_conflict = false;
610 d_hasAddedLemma = false;
611 bool setIncomplete = false;
612
613 Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
614 if( needsCheck ){
615 //flush previous lemmas (for instance, if was interupted), or other lemmas to process
616 flushLemmas();
617 if( d_hasAddedLemma ){
618 return;
619 }
620
621 double clSet = 0;
622 if( Trace.isOn("quant-engine") ){
623 clSet = double(clock())/double(CLOCKS_PER_SEC);
624 Trace("quant-engine") << ">>>>> Quantifiers Engine Round, effort = " << e << " <<<<<" << std::endl;
625 }
626
627 if( Trace.isOn("quant-engine-debug") ){
628 Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl;
629 Trace("quant-engine-debug") << " depth : " << d_ierCounter_c << std::endl;
630 Trace("quant-engine-debug") << " modules to check : ";
631 for( unsigned i=0; i<qm.size(); i++ ){
632 Trace("quant-engine-debug") << qm[i]->identify() << " ";
633 }
634 Trace("quant-engine-debug") << std::endl;
635 Trace("quant-engine-debug") << " # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl;
636 if( !d_lemmas_waiting.empty() ){
637 Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting.size() << std::endl;
638 }
639 Trace("quant-engine-debug") << " Theory engine finished : " << !d_te->needCheck() << std::endl;
640 Trace("quant-engine-debug") << " Needs model effort : " << needsModelE << std::endl;
641 }
642 if( Trace.isOn("quant-engine-ee-pre") ){
643 Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl;
644 debugPrintEqualityEngine( "quant-engine-ee-pre" );
645 }
646 if( Trace.isOn("quant-engine-assert") ){
647 Trace("quant-engine-assert") << "Assertions : " << std::endl;
648 getTheoryEngine()->printAssertions("quant-engine-assert");
649 }
650
651 //reset utilities
652 Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl;
653 for (QuantifiersUtil*& util : d_util)
654 {
655 Trace("quant-engine-debug2") << "Reset " << util->identify().c_str()
656 << "..." << std::endl;
657 if (!util->reset(e))
658 {
659 flushLemmas();
660 if( d_hasAddedLemma ){
661 return;
662 }else{
663 //should only fail reset if added a lemma
664 Assert(false);
665 }
666 }
667 }
668
669 if( Trace.isOn("quant-engine-ee") ){
670 Trace("quant-engine-ee") << "Equality engine : " << std::endl;
671 debugPrintEqualityEngine( "quant-engine-ee" );
672 }
673
674 //reset the model
675 Trace("quant-engine-debug") << "Reset model..." << std::endl;
676 d_model->reset_round();
677
678 //reset the modules
679 Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
680 for (QuantifiersModule*& mdl : d_modules)
681 {
682 Trace("quant-engine-debug2") << "Reset " << mdl->identify().c_str()
683 << std::endl;
684 mdl->reset_round(e);
685 }
686 Trace("quant-engine-debug") << "Done resetting all modules." << std::endl;
687 //reset may have added lemmas
688 flushLemmas();
689 if( d_hasAddedLemma ){
690 return;
691 }
692
693 if( e==Theory::EFFORT_LAST_CALL ){
694 ++(d_statistics.d_instantiation_rounds_lc);
695 }else if( e==Theory::EFFORT_FULL ){
696 ++(d_statistics.d_instantiation_rounds);
697 }
698 Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
699 for (unsigned qef = QuantifiersModule::QEFFORT_CONFLICT;
700 qef <= QuantifiersModule::QEFFORT_LAST_CALL;
701 ++qef)
702 {
703 QuantifiersModule::QEffort quant_e =
704 static_cast<QuantifiersModule::QEffort>(qef);
705 d_curr_effort_level = quant_e;
706 //build the model if any module requested it
707 if (needsModelE == quant_e)
708 {
709 if (!d_model->isBuilt())
710 {
711 // theory engine's model builder is quantifier engine's builder if it
712 // has one
713 Assert(!getModelBuilder()
714 || getModelBuilder() == d_te->getModelBuilder());
715 Trace("quant-engine-debug") << "Build model..." << std::endl;
716 if (!d_te->getModelBuilder()->buildModel(d_model.get()))
717 {
718 flushLemmas();
719 }
720 }
721 if (!d_model->isBuiltSuccess())
722 {
723 break;
724 }
725 }
726 if( !d_hasAddedLemma ){
727 //check each module
728 for (QuantifiersModule*& mdl : qm)
729 {
730 Trace("quant-engine-debug") << "Check " << mdl->identify().c_str()
731 << " at effort " << quant_e << "..."
732 << std::endl;
733 mdl->check(e, quant_e);
734 if( d_conflict ){
735 Trace("quant-engine-debug") << "...conflict!" << std::endl;
736 break;
737 }
738 }
739 //flush all current lemmas
740 flushLemmas();
741 }
742 //if we have added one, stop
743 if( d_hasAddedLemma ){
744 break;
745 }else{
746 Assert(!d_conflict);
747 if (quant_e == QuantifiersModule::QEFFORT_CONFLICT)
748 {
749 if( e==Theory::EFFORT_FULL ){
750 //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase
751 if( d_ierCounterLastLc!=d_ierCounter_lc || !options::instWhenStrictInterleave() || d_ierCounter%d_inst_when_phase!=0 ){
752 d_ierCounter = d_ierCounter + 1;
753 d_ierCounterLastLc = d_ierCounter_lc;
754 d_ierCounter_c = d_ierCounter_c.get() + 1;
755 }
756 }else if( e==Theory::EFFORT_LAST_CALL ){
757 d_ierCounter_lc = d_ierCounter_lc + 1;
758 }
759 }
760 else if (quant_e == QuantifiersModule::QEFFORT_MODEL)
761 {
762 if( e==Theory::EFFORT_LAST_CALL ){
763 //sources of incompleteness
764 for (QuantifiersUtil*& util : d_util)
765 {
766 if (!util->checkComplete())
767 {
768 Trace("quant-engine-debug") << "Set incomplete because utility "
769 << util->identify().c_str()
770 << " was incomplete." << std::endl;
771 setIncomplete = true;
772 }
773 }
774 if (d_conflict_c.get())
775 {
776 // we reported a conflicting lemma, should return
777 setIncomplete = true;
778 }
779 //if we have a chance not to set incomplete
780 if( !setIncomplete ){
781 //check if we should set the incomplete flag
782 for (QuantifiersModule*& mdl : d_modules)
783 {
784 if (!mdl->checkComplete())
785 {
786 Trace("quant-engine-debug")
787 << "Set incomplete because module "
788 << mdl->identify().c_str() << " was incomplete."
789 << std::endl;
790 setIncomplete = true;
791 break;
792 }
793 }
794 if( !setIncomplete ){
795 //look at individual quantified formulas, one module must claim completeness for each one
796 for( unsigned i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
797 bool hasCompleteM = false;
798 Node q = d_model->getAssertedQuantifier( i );
799 QuantifiersModule * qmd = getOwner( q );
800 if( qmd!=NULL ){
801 hasCompleteM = qmd->checkCompleteFor( q );
802 }else{
803 for( unsigned j=0; j<d_modules.size(); j++ ){
804 if( d_modules[j]->checkCompleteFor( q ) ){
805 qmd = d_modules[j];
806 hasCompleteM = true;
807 break;
808 }
809 }
810 }
811 if( !hasCompleteM ){
812 Trace("quant-engine-debug") << "Set incomplete because " << q << " was not fully processed." << std::endl;
813 setIncomplete = true;
814 break;
815 }else{
816 Assert(qmd != NULL);
817 Trace("quant-engine-debug2") << "Complete for " << q << " due to " << qmd->identify().c_str() << std::endl;
818 }
819 }
820 }
821 }
822 //if setIncomplete = false, we will answer SAT, otherwise we will run at quant_e QEFFORT_LAST_CALL
823 if( !setIncomplete ){
824 break;
825 }
826 }
827 }
828 }
829 }
830 d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
831 Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
832 if( d_hasAddedLemma ){
833 d_instantiate->debugPrint();
834 }
835 if( Trace.isOn("quant-engine") ){
836 double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
837 Trace("quant-engine") << "Finished quantifiers engine, total time = " << (clSet2-clSet);
838 Trace("quant-engine") << ", added lemma = " << d_hasAddedLemma;
839 Trace("quant-engine") << std::endl;
840 }
841
842 Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl;
843 }else{
844 Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl;
845 }
846
847 //SAT case
848 if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
849 if( setIncomplete ){
850 Trace("quant-engine") << "Set incomplete flag." << std::endl;
851 getOutputChannel().setIncomplete();
852 }
853 //output debug stats
854 d_instantiate->debugPrintModel();
855 }
856 }
857
858 void QuantifiersEngine::notifyCombineTheories() {
859 //if allowing theory combination to happen at most once between instantiation rounds
860 //d_ierCounter = 1;
861 //d_ierCounterLastLc = -1;
862 }
863
864 bool QuantifiersEngine::reduceQuantifier( Node q ) {
865 //TODO: this can be unified with preregistration: AlphaEquivalence takes ownership of reducable quants
866 BoolMap::const_iterator it = d_quants_red.find( q );
867 if( it==d_quants_red.end() ){
868 Node lem;
869 std::map< Node, Node >::iterator itr = d_quants_red_lem.find( q );
870 if( itr==d_quants_red_lem.end() ){
871 if (d_private->d_alpha_equiv)
872 {
873 Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl;
874 //add equivalence with another quantified formula
875 lem = d_private->d_alpha_equiv->reduceQuantifier(q);
876 if( !lem.isNull() ){
877 Trace("quant-engine-red") << "...alpha equivalence success." << std::endl;
878 ++(d_statistics.d_red_alpha_equiv);
879 }
880 }
881 d_quants_red_lem[q] = lem;
882 }else{
883 lem = itr->second;
884 }
885 if( !lem.isNull() ){
886 getOutputChannel().lemma( lem );
887 }
888 d_quants_red[q] = !lem.isNull();
889 return !lem.isNull();
890 }else{
891 return (*it).second;
892 }
893 }
894
895 void QuantifiersEngine::registerQuantifierInternal(Node f)
896 {
897 std::map< Node, bool >::iterator it = d_quants.find( f );
898 if( it==d_quants.end() ){
899 Trace("quant") << "QuantifiersEngine : Register quantifier ";
900 Trace("quant") << " : " << f << std::endl;
901 unsigned prev_lemma_waiting = d_lemmas_waiting.size();
902 ++(d_statistics.d_num_quant);
903 Assert(f.getKind() == FORALL);
904 // register with utilities
905 for (unsigned i = 0; i < d_util.size(); i++)
906 {
907 d_util[i]->registerQuantifier(f);
908 }
909 // compute attributes
910 d_quant_attr->computeAttributes(f);
911
912 for (QuantifiersModule*& mdl : d_modules)
913 {
914 Trace("quant-debug") << "check ownership with " << mdl->identify()
915 << "..." << std::endl;
916 mdl->checkOwnership(f);
917 }
918 QuantifiersModule* qm = getOwner(f);
919 Trace("quant") << " Owner : " << (qm == nullptr ? "[none]" : qm->identify())
920 << std::endl;
921 // register with each module
922 for (QuantifiersModule*& mdl : d_modules)
923 {
924 Trace("quant-debug") << "register with " << mdl->identify() << "..."
925 << std::endl;
926 mdl->registerQuantifier(f);
927 // since this is context-independent, we should not add any lemmas during
928 // this call
929 Assert(d_lemmas_waiting.size() == prev_lemma_waiting);
930 }
931 Trace("quant-debug") << "...finish." << std::endl;
932 d_quants[f] = true;
933 AlwaysAssert(d_lemmas_waiting.size() == prev_lemma_waiting);
934 }
935 }
936
937 void QuantifiersEngine::preRegisterQuantifier(Node q)
938 {
939 NodeSet::const_iterator it = d_quants_prereg.find(q);
940 if (it != d_quants_prereg.end())
941 {
942 return;
943 }
944 Trace("quant-debug") << "QuantifiersEngine : Pre-register " << q << std::endl;
945 d_quants_prereg.insert(q);
946 // try to reduce
947 if (reduceQuantifier(q))
948 {
949 // if we can reduce it, nothing left to do
950 return;
951 }
952 // ensure that it is registered
953 registerQuantifierInternal(q);
954 // register with each module
955 for (QuantifiersModule*& mdl : d_modules)
956 {
957 Trace("quant-debug") << "pre-register with " << mdl->identify() << "..."
958 << std::endl;
959 mdl->preRegisterQuantifier(q);
960 }
961 // flush the lemmas
962 flushLemmas();
963 Trace("quant-debug") << "...finish pre-register " << q << "..." << std::endl;
964 }
965
966 void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
967 for(std::vector<Node>::iterator p = pattern.begin(); p != pattern.end(); ++p){
968 std::set< Node > added;
969 getTermDatabase()->addTerm( *p, added );
970 }
971 }
972
973 void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
974 if (reduceQuantifier(f))
975 {
976 // if we can reduce it, nothing left to do
977 return;
978 }
979 if( !pol ){
980 // do skolemization
981 Node lem = d_skolemize->process(f);
982 if (!lem.isNull())
983 {
984 if (Trace.isOn("quantifiers-sk-debug"))
985 {
986 Node slem = Rewriter::rewrite(lem);
987 Trace("quantifiers-sk-debug")
988 << "Skolemize lemma : " << slem << std::endl;
989 }
990 getOutputChannel().lemma(lem, false, true);
991 }
992 return;
993 }
994 // ensure the quantified formula is registered
995 registerQuantifierInternal(f);
996 // assert it to each module
997 d_model->assertQuantifier(f);
998 for (QuantifiersModule*& mdl : d_modules)
999 {
1000 mdl->assertNode(f);
1001 }
1002 addTermToDatabase(d_term_util->getInstConstantBody(f), true);
1003 }
1004
1005 void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){
1006 if( options::incrementalSolving() ){
1007 if( d_presolve_in.find( n )==d_presolve_in.end() ){
1008 d_presolve_in.insert( n );
1009 d_presolve_cache.push_back( n );
1010 d_presolve_cache_wq.push_back( withinQuant );
1011 d_presolve_cache_wic.push_back( withinInstClosure );
1012 }
1013 }
1014 //only wait if we are doing incremental solving
1015 if( !d_presolve || !options::incrementalSolving() ){
1016 std::set< Node > added;
1017 d_term_db->addTerm(n, added, withinQuant, withinInstClosure);
1018
1019 if (!withinQuant)
1020 {
1021 if (d_sygus_tdb)
1022 {
1023 d_sygus_tdb->getEvalUnfold()->registerEvalTerm(n);
1024 }
1025 }
1026 }
1027 }
1028
1029 void QuantifiersEngine::eqNotifyNewClass(TNode t) {
1030 addTermToDatabase( t );
1031 }
1032
1033 bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
1034 if( doCache ){
1035 if( doRewrite ){
1036 lem = Rewriter::rewrite(lem);
1037 }
1038 Trace("inst-add-debug") << "Adding lemma : " << lem << std::endl;
1039 BoolMap::const_iterator itp = d_lemmas_produced_c.find( lem );
1040 if( itp==d_lemmas_produced_c.end() || !(*itp).second ){
1041 //d_curr_out->lemma( lem, false, true );
1042 d_lemmas_produced_c[ lem ] = true;
1043 d_lemmas_waiting.push_back( lem );
1044 Trace("inst-add-debug") << "Added lemma" << std::endl;
1045 return true;
1046 }else{
1047 Trace("inst-add-debug") << "Duplicate." << std::endl;
1048 return false;
1049 }
1050 }else{
1051 //do not need to rewrite, will be rewritten after sending
1052 d_lemmas_waiting.push_back( lem );
1053 return true;
1054 }
1055 }
1056
1057 bool QuantifiersEngine::removeLemma( Node lem ) {
1058 std::vector< Node >::iterator it = std::find( d_lemmas_waiting.begin(), d_lemmas_waiting.end(), lem );
1059 if( it!=d_lemmas_waiting.end() ){
1060 d_lemmas_waiting.erase( it, it + 1 );
1061 d_lemmas_produced_c[ lem ] = false;
1062 return true;
1063 }else{
1064 return false;
1065 }
1066 }
1067
1068 void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
1069 d_phase_req_waiting[lit] = req;
1070 }
1071
1072 void QuantifiersEngine::markRelevant( Node q ) {
1073 d_model->markRelevant( q );
1074 }
1075
1076 void QuantifiersEngine::setConflict() {
1077 d_conflict = true;
1078 d_conflict_c = true;
1079 }
1080
1081 bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
1082 Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl;
1083 //determine if we should perform check, based on instWhenMode
1084 bool performCheck = false;
1085 if (options::instWhenMode() == options::InstWhenMode::FULL)
1086 {
1087 performCheck = ( e >= Theory::EFFORT_FULL );
1088 }
1089 else if (options::instWhenMode() == options::InstWhenMode::FULL_DELAY)
1090 {
1091 performCheck = ( e >= Theory::EFFORT_FULL ) && !getTheoryEngine()->needCheck();
1092 }
1093 else if (options::instWhenMode() == options::InstWhenMode::FULL_LAST_CALL)
1094 {
1095 performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL );
1096 }
1097 else if (options::instWhenMode()
1098 == options::InstWhenMode::FULL_DELAY_LAST_CALL)
1099 {
1100 performCheck = ( ( e==Theory::EFFORT_FULL && !getTheoryEngine()->needCheck() && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL );
1101 }
1102 else if (options::instWhenMode() == options::InstWhenMode::LAST_CALL)
1103 {
1104 performCheck = ( e >= Theory::EFFORT_LAST_CALL );
1105 }
1106 else
1107 {
1108 performCheck = true;
1109 }
1110 if( e==Theory::EFFORT_LAST_CALL ){
1111 //with bounded integers, skip every other last call,
1112 // since matching loops may occur with infinite quantification
1113 if( d_ierCounter_lc%2==0 && options::fmfBound() ){
1114 performCheck = false;
1115 }
1116 }
1117 return performCheck;
1118 }
1119
1120 options::UserPatMode QuantifiersEngine::getInstUserPatMode()
1121 {
1122 if (options::userPatternsQuant() == options::UserPatMode::INTERLEAVE)
1123 {
1124 return d_ierCounter % 2 == 0 ? options::UserPatMode::USE
1125 : options::UserPatMode::RESORT;
1126 }
1127 else
1128 {
1129 return options::userPatternsQuant();
1130 }
1131 }
1132
1133 void QuantifiersEngine::flushLemmas(){
1134 if( !d_lemmas_waiting.empty() ){
1135 //filter based on notify classes
1136 if (d_instantiate->hasNotify())
1137 {
1138 unsigned prev_lem_sz = d_lemmas_waiting.size();
1139 d_instantiate->notifyFlushLemmas();
1140 if( prev_lem_sz!=d_lemmas_waiting.size() ){
1141 Trace("quant-engine") << "...filtered instances : " << d_lemmas_waiting.size() << " / " << prev_lem_sz << std::endl;
1142 }
1143 }
1144 //take default output channel if none is provided
1145 d_hasAddedLemma = true;
1146 for( unsigned i=0; i<d_lemmas_waiting.size(); i++ ){
1147 Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting[i] << std::endl;
1148 getOutputChannel().lemma( d_lemmas_waiting[i], false, true );
1149 }
1150 d_lemmas_waiting.clear();
1151 }
1152 if( !d_phase_req_waiting.empty() ){
1153 for( std::map< Node, bool >::iterator it = d_phase_req_waiting.begin(); it != d_phase_req_waiting.end(); ++it ){
1154 Trace("qe-lemma") << "Require phase : " << it->first << " -> " << it->second << std::endl;
1155 getOutputChannel().requirePhase( it->first, it->second );
1156 }
1157 d_phase_req_waiting.clear();
1158 }
1159 }
1160
1161 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas ) {
1162 return d_instantiate->getUnsatCoreLemmas(active_lemmas);
1163 }
1164
1165 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp ) {
1166 return d_instantiate->getUnsatCoreLemmas(active_lemmas, weak_imp);
1167 }
1168
1169 void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
1170 d_instantiate->getInstantiationTermVectors(q, tvecs);
1171 }
1172
1173 void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
1174 d_instantiate->getInstantiationTermVectors(insts);
1175 }
1176
1177 void QuantifiersEngine::getExplanationForInstLemmas(
1178 const std::vector<Node>& lems,
1179 std::map<Node, Node>& quant,
1180 std::map<Node, std::vector<Node> >& tvec)
1181 {
1182 d_instantiate->getExplanationForInstLemmas(lems, quant, tvec);
1183 }
1184
1185 void QuantifiersEngine::printInstantiations( std::ostream& out ) {
1186 bool printed = false;
1187 // print the skolemizations
1188 if (d_skolemize->printSkolemization(out))
1189 {
1190 printed = true;
1191 }
1192 // print the instantiations
1193 if (d_instantiate->printInstantiations(out))
1194 {
1195 printed = true;
1196 }
1197 if( !printed ){
1198 out << "No instantiations" << std::endl;
1199 }
1200 }
1201
1202 void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
1203 if (d_private->d_synth_e)
1204 {
1205 d_private->d_synth_e->printSynthSolution(out);
1206 }else{
1207 out << "Internal error : module for synth solution not found." << std::endl;
1208 }
1209 }
1210
1211 void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) {
1212 d_instantiate->getInstantiatedQuantifiedFormulas(qs);
1213 }
1214
1215 void QuantifiersEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) {
1216 d_instantiate->getInstantiations(insts);
1217 }
1218
1219 void QuantifiersEngine::getInstantiations( Node q, std::vector< Node >& insts ) {
1220 d_instantiate->getInstantiations(q, insts);
1221 }
1222
1223 Node QuantifiersEngine::getInstantiatedConjunction( Node q ) {
1224 return d_instantiate->getInstantiatedConjunction(q);
1225 }
1226
1227 QuantifiersEngine::Statistics::Statistics()
1228 : d_time("theory::QuantifiersEngine::time"),
1229 d_qcf_time("theory::QuantifiersEngine::time_qcf"),
1230 d_ematching_time("theory::QuantifiersEngine::time_ematching"),
1231 d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
1232 d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
1233 d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
1234 d_triggers("QuantifiersEngine::Triggers", 0),
1235 d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
1236 d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
1237 d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
1238 d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0),
1239 d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0),
1240 d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0),
1241 d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0),
1242 d_instantiations_qcf("QuantifiersEngine::Instantiations_Qcf_Conflict", 0),
1243 d_instantiations_qcf_prop("QuantifiersEngine::Instantiations_Qcf_Prop", 0),
1244 d_instantiations_fmf_exh("QuantifiersEngine::Instantiations_Fmf_Exh", 0),
1245 d_instantiations_fmf_mbqi("QuantifiersEngine::Instantiations_Fmf_Mbqi", 0),
1246 d_instantiations_cbqi("QuantifiersEngine::Instantiations_Cbqi", 0),
1247 d_instantiations_rr("QuantifiersEngine::Instantiations_Rewrite_Rules", 0)
1248 {
1249 smtStatisticsRegistry()->registerStat(&d_time);
1250 smtStatisticsRegistry()->registerStat(&d_qcf_time);
1251 smtStatisticsRegistry()->registerStat(&d_ematching_time);
1252 smtStatisticsRegistry()->registerStat(&d_num_quant);
1253 smtStatisticsRegistry()->registerStat(&d_instantiation_rounds);
1254 smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc);
1255 smtStatisticsRegistry()->registerStat(&d_triggers);
1256 smtStatisticsRegistry()->registerStat(&d_simple_triggers);
1257 smtStatisticsRegistry()->registerStat(&d_multi_triggers);
1258 smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations);
1259 smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv);
1260 smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns);
1261 smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen);
1262 smtStatisticsRegistry()->registerStat(&d_instantiations_guess);
1263 smtStatisticsRegistry()->registerStat(&d_instantiations_qcf);
1264 smtStatisticsRegistry()->registerStat(&d_instantiations_qcf_prop);
1265 smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_exh);
1266 smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_mbqi);
1267 smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi);
1268 smtStatisticsRegistry()->registerStat(&d_instantiations_rr);
1269 }
1270
1271 QuantifiersEngine::Statistics::~Statistics(){
1272 smtStatisticsRegistry()->unregisterStat(&d_time);
1273 smtStatisticsRegistry()->unregisterStat(&d_qcf_time);
1274 smtStatisticsRegistry()->unregisterStat(&d_ematching_time);
1275 smtStatisticsRegistry()->unregisterStat(&d_num_quant);
1276 smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds);
1277 smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc);
1278 smtStatisticsRegistry()->unregisterStat(&d_triggers);
1279 smtStatisticsRegistry()->unregisterStat(&d_simple_triggers);
1280 smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
1281 smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations);
1282 smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv);
1283 smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns);
1284 smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen);
1285 smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess);
1286 smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf);
1287 smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf_prop);
1288 smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_exh);
1289 smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_mbqi);
1290 smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi);
1291 smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr);
1292 }
1293
1294 eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine() const
1295 {
1296 return d_te->getMasterEqualityEngine();
1297 }
1298
1299 eq::EqualityEngine* QuantifiersEngine::getActiveEqualityEngine() const
1300 {
1301 if( d_useModelEe ){
1302 return d_model->getEqualityEngine();
1303 }
1304 return d_te->getMasterEqualityEngine();
1305 }
1306
1307 Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
1308 bool prevModelEe = d_useModelEe;
1309 d_useModelEe = false;
1310 Node ret = d_eq_query->getInternalRepresentative( a, q, index );
1311 d_useModelEe = prevModelEe;
1312 return ret;
1313 }
1314
1315 bool QuantifiersEngine::getSynthSolutions(
1316 std::map<Node, std::map<Node, Node> >& sol_map)
1317 {
1318 return d_private->d_synth_e->getSynthSolutions(sol_map);
1319 }
1320
1321 void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
1322 eq::EqualityEngine* ee = getActiveEqualityEngine();
1323 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
1324 std::map< TypeNode, int > typ_num;
1325 while( !eqcs_i.isFinished() ){
1326 TNode r = (*eqcs_i);
1327 TypeNode tr = r.getType();
1328 if( typ_num.find( tr )==typ_num.end() ){
1329 typ_num[tr] = 0;
1330 }
1331 typ_num[tr]++;
1332 bool firstTime = true;
1333 Trace(c) << " " << r;
1334 Trace(c) << " : { ";
1335 eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
1336 while( !eqc_i.isFinished() ){
1337 TNode n = (*eqc_i);
1338 if( r!=n ){
1339 if( firstTime ){
1340 Trace(c) << std::endl;
1341 firstTime = false;
1342 }
1343 Trace(c) << " " << n << std::endl;
1344 }
1345 ++eqc_i;
1346 }
1347 if( !firstTime ){ Trace(c) << " "; }
1348 Trace(c) << "}" << std::endl;
1349 ++eqcs_i;
1350 }
1351 Trace(c) << std::endl;
1352 for( std::map< TypeNode, int >::iterator it = typ_num.begin(); it != typ_num.end(); ++it ){
1353 Trace(c) << "# eqc for " << it->first << " : " << it->second << std::endl;
1354 }
1355 }
1356
1357 } // namespace theory
1358 } // namespace CVC4