1 /********************* */
2 /*! \file quantifiers_engine.cpp
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
12 ** \brief Implementation of quantifiers engine class
15 #include "theory/quantifiers_engine.h"
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"
40 using namespace CVC4::kind
;
45 class QuantifiersEnginePrivate
48 QuantifiersEnginePrivate()
49 : d_inst_prop(nullptr),
50 d_alpha_equiv(nullptr),
51 d_inst_engine(nullptr),
52 d_model_engine(nullptr),
58 d_lte_part_inst(nullptr),
62 d_anti_skolem(nullptr)
65 ~QuantifiersEnginePrivate() {}
66 //------------------------------ private quantifier utilities
67 /** quantifiers instantiation propagator */
68 std::unique_ptr
<quantifiers::InstPropagator
> d_inst_prop
;
69 //------------------------------ end private quantifier utilities
70 //------------------------------ quantifiers modules
71 /** alpha equivalence */
72 std::unique_ptr
<quantifiers::AlphaEquivalence
> d_alpha_equiv
;
73 /** instantiation engine */
74 std::unique_ptr
<quantifiers::InstantiationEngine
> d_inst_engine
;
76 std::unique_ptr
<quantifiers::ModelEngine
> d_model_engine
;
77 /** bounded integers utility */
78 std::unique_ptr
<quantifiers::BoundedIntegers
> d_bint
;
79 /** Conflict find mechanism for quantifiers */
80 std::unique_ptr
<quantifiers::QuantConflictFind
> d_qcf
;
81 /** rewrite rules utility */
82 std::unique_ptr
<quantifiers::RewriteEngine
> d_rr_engine
;
83 /** subgoal generator */
84 std::unique_ptr
<quantifiers::ConjectureGenerator
> d_sg_gen
;
85 /** ceg instantiation */
86 std::unique_ptr
<quantifiers::SynthEngine
> d_synth_e
;
87 /** lte partial instantiation */
88 std::unique_ptr
<quantifiers::LtePartialInst
> d_lte_part_inst
;
89 /** full saturation */
90 std::unique_ptr
<quantifiers::InstStrategyEnum
> d_fs
;
91 /** counterexample-based quantifier instantiation */
92 std::unique_ptr
<quantifiers::InstStrategyCegqi
> d_i_cbqi
;
93 /** quantifiers splitting */
94 std::unique_ptr
<quantifiers::QuantDSplit
> d_qsplit
;
95 /** quantifiers anti-skolemization */
96 std::unique_ptr
<quantifiers::QuantAntiSkolem
> d_anti_skolem
;
97 //------------------------------ end quantifiers modules
100 * This constructs the above modules based on the current options. It adds
101 * a pointer to each module it constructs to modules. This method sets
102 * needsBuilder to true if we require a strategy-specific model builder
103 * utility, and needsRelDom to true if we require the relevant domain
106 void initialize(QuantifiersEngine
* qe
,
108 std::vector
<QuantifiersModule
*>& modules
,
112 // add quantifiers modules
113 if (options::quantConflictFind() || options::quantRewriteRules())
115 d_qcf
.reset(new quantifiers::QuantConflictFind(qe
, c
));
116 modules
.push_back(d_qcf
.get());
118 if (options::conjectureGen())
120 d_sg_gen
.reset(new quantifiers::ConjectureGenerator(qe
, c
));
121 modules
.push_back(d_sg_gen
.get());
123 if (!options::finiteModelFind() || options::fmfInstEngine())
125 d_inst_engine
.reset(new quantifiers::InstantiationEngine(qe
));
126 modules
.push_back(d_inst_engine
.get());
130 d_i_cbqi
.reset(new quantifiers::InstStrategyCegqi(qe
));
131 modules
.push_back(d_i_cbqi
.get());
132 qe
->getInstantiate()->addRewriter(d_i_cbqi
->getInstRewriter());
134 if (options::ceGuidedInst())
136 d_synth_e
.reset(new quantifiers::SynthEngine(qe
, c
));
137 modules
.push_back(d_synth_e
.get());
139 // finite model finding
140 if (options::finiteModelFind())
142 if (options::fmfBound())
144 d_bint
.reset(new quantifiers::BoundedIntegers(c
, qe
));
145 modules
.push_back(d_bint
.get());
147 d_model_engine
.reset(new quantifiers::ModelEngine(c
, qe
));
148 modules
.push_back(d_model_engine
.get());
149 // finite model finder has special ways of building the model
152 if (options::quantRewriteRules())
154 d_rr_engine
.reset(new quantifiers::RewriteEngine(c
, qe
, d_qcf
.get()));
155 modules
.push_back(d_rr_engine
.get());
157 if (options::ltePartialInst())
159 d_lte_part_inst
.reset(new quantifiers::LtePartialInst(qe
, c
));
160 modules
.push_back(d_lte_part_inst
.get());
162 if (options::quantDynamicSplit() != quantifiers::QUANT_DSPLIT_MODE_NONE
)
164 d_qsplit
.reset(new quantifiers::QuantDSplit(qe
, c
));
165 modules
.push_back(d_qsplit
.get());
167 if (options::quantAntiSkolem())
169 d_anti_skolem
.reset(new quantifiers::QuantAntiSkolem(qe
));
170 modules
.push_back(d_anti_skolem
.get());
172 if (options::quantAlphaEquiv())
174 d_alpha_equiv
.reset(new quantifiers::AlphaEquivalence(qe
));
176 // full saturation : instantiate from relevant domain, then arbitrary terms
177 if (options::fullSaturateQuant() || options::fullSaturateInterleave())
179 d_fs
.reset(new quantifiers::InstStrategyEnum(qe
));
180 modules
.push_back(d_fs
.get());
186 QuantifiersEngine::QuantifiersEngine(context::Context
* c
,
187 context::UserContext
* u
,
190 d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c
, this)),
191 d_eq_inference(nullptr),
192 d_tr_trie(new inst::TriggerTrie
),
197 d_term_util(new quantifiers::TermUtil(this)),
198 d_term_canon(new expr::TermCanonize
),
199 d_term_db(new quantifiers::TermDb(c
, u
, this)),
200 d_sygus_tdb(nullptr),
201 d_quant_attr(new quantifiers::QuantAttributes(this)),
202 d_instantiate(new quantifiers::Instantiate(this, u
)),
203 d_skolemize(new quantifiers::Skolemize(this, u
)),
204 d_term_enum(new quantifiers::TermEnumeration
),
205 d_conflict_c(c
, false),
209 d_lemmas_produced_c(u
),
212 // d_ierCounter_lc(c),
213 // d_ierCounterLastLc(c),
217 d_presolve_cache_wq(u
),
218 d_presolve_cache_wic(u
)
220 // initialize the private utility
221 d_private
.reset(new QuantifiersEnginePrivate
);
224 d_util
.push_back(d_eq_query
.get());
225 // term util must come before the other utilities
226 d_util
.push_back(d_term_util
.get());
227 d_util
.push_back(d_term_db
.get());
229 if (options::ceGuidedInst()) {
230 d_sygus_tdb
.reset(new quantifiers::TermDbSygus(c
, this));
233 if( options::instPropagate() ){
234 // notice that this option is incompatible with options::qcfAllConflict()
235 d_private
->d_inst_prop
.reset(new quantifiers::InstPropagator(this));
236 d_util
.push_back(d_private
->d_inst_prop
.get());
237 d_instantiate
->addNotify(d_private
->d_inst_prop
->getInstantiationNotify());
240 if( options::inferArithTriggerEq() ){
241 d_eq_inference
.reset(new quantifiers::EqualityInference(c
, false));
244 d_util
.push_back(d_instantiate
.get());
246 d_curr_effort_level
= QuantifiersModule::QEFFORT_NONE
;
248 d_hasAddedLemma
= false;
249 d_useModelEe
= false;
250 //don't add true lemma
251 d_lemmas_produced_c
[d_term_util
->d_true
] = true;
253 Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl
;
254 Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl
;
256 if( options::quantEpr() ){
257 Assert( !options::incrementalSolving() );
258 d_qepr
.reset(new quantifiers::QuantEPR
);
262 //allow theory combination to go first, once initially
263 d_ierCounter
= options::instWhenTcFirst() ? 0 : 1;
264 d_ierCounter_c
= d_ierCounter
;
266 d_ierCounterLastLc
= 0;
267 d_inst_when_phase
= 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
269 bool needsBuilder
= false;
270 bool needsRelDom
= false;
271 d_private
->initialize(this, c
, d_modules
, needsBuilder
, needsRelDom
);
274 d_rel_dom
.reset(new quantifiers::RelevantDomain(this));
275 d_util
.push_back(d_rel_dom
.get());
278 // if we require specialized ways of building the model
280 Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl
;
281 if (options::mbqiMode() == quantifiers::MBQI_FMC
282 || options::mbqiMode() == quantifiers::MBQI_TRUST
283 || options::fmfBound())
285 Trace("quant-engine-debug") << "...make fmc builder." << std::endl
;
286 d_model
.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
287 this, c
, "FirstOrderModelFmc"));
288 d_builder
.reset(new quantifiers::fmcheck::FullModelChecker(c
, this));
290 Trace("quant-engine-debug") << "...make default model builder." << std::endl
;
292 new quantifiers::FirstOrderModel(this, c
, "FirstOrderModel"));
293 d_builder
.reset(new quantifiers::QModelBuilder(c
, this));
296 d_model
.reset(new quantifiers::FirstOrderModel(this, c
, "FirstOrderModel"));
300 QuantifiersEngine::~QuantifiersEngine() {}
302 context::Context
* QuantifiersEngine::getSatContext()
304 return d_te
->theoryOf(THEORY_QUANTIFIERS
)->getSatContext();
307 context::UserContext
* QuantifiersEngine::getUserContext()
309 return d_te
->theoryOf(THEORY_QUANTIFIERS
)->getUserContext();
312 OutputChannel
& QuantifiersEngine::getOutputChannel()
314 return d_te
->theoryOf(THEORY_QUANTIFIERS
)->getOutputChannel();
316 /** get default valuation for the quantifiers engine */
317 Valuation
& QuantifiersEngine::getValuation()
319 return d_te
->theoryOf(THEORY_QUANTIFIERS
)->getValuation();
322 const LogicInfo
& QuantifiersEngine::getLogicInfo() const
324 return d_te
->getLogicInfo();
327 EqualityQuery
* QuantifiersEngine::getEqualityQuery() const
329 return d_eq_query
.get();
331 quantifiers::EqualityInference
* QuantifiersEngine::getEqualityInference() const
333 return d_eq_inference
.get();
335 quantifiers::RelevantDomain
* QuantifiersEngine::getRelevantDomain() const
337 return d_rel_dom
.get();
339 quantifiers::QModelBuilder
* QuantifiersEngine::getModelBuilder() const
341 return d_builder
.get();
343 quantifiers::QuantEPR
* QuantifiersEngine::getQuantEPR() const
347 quantifiers::FirstOrderModel
* QuantifiersEngine::getModel() const
349 return d_model
.get();
351 quantifiers::TermDb
* QuantifiersEngine::getTermDatabase() const
353 return d_term_db
.get();
355 quantifiers::TermDbSygus
* QuantifiersEngine::getTermDatabaseSygus() const
357 return d_sygus_tdb
.get();
359 quantifiers::TermUtil
* QuantifiersEngine::getTermUtil() const
361 return d_term_util
.get();
363 expr::TermCanonize
* QuantifiersEngine::getTermCanonize() const
365 return d_term_canon
.get();
367 quantifiers::QuantAttributes
* QuantifiersEngine::getQuantAttributes() const
369 return d_quant_attr
.get();
371 quantifiers::Instantiate
* QuantifiersEngine::getInstantiate() const
373 return d_instantiate
.get();
375 quantifiers::Skolemize
* QuantifiersEngine::getSkolemize() const
377 return d_skolemize
.get();
379 quantifiers::TermEnumeration
* QuantifiersEngine::getTermEnumeration() const
381 return d_term_enum
.get();
383 inst::TriggerTrie
* QuantifiersEngine::getTriggerDatabase() const
385 return d_tr_trie
.get();
388 quantifiers::SynthEngine
* QuantifiersEngine::getSynthEngine() const
390 return d_private
->d_synth_e
.get();
393 QuantifiersModule
* QuantifiersEngine::getOwner( Node q
) {
394 std::map
< Node
, QuantifiersModule
* >::iterator it
= d_owner
.find( q
);
395 if( it
==d_owner
.end() ){
402 void QuantifiersEngine::setOwner( Node q
, QuantifiersModule
* m
, int priority
) {
403 QuantifiersModule
* mo
= getOwner( q
);
406 if( priority
<=d_owner_priority
[q
] ){
407 Trace("quant-warn") << "WARNING: setting owner of " << q
<< " to " << ( m
? m
->identify() : "null" ) << ", but already has owner " << mo
->identify() << " with higher priority!" << std::endl
;
412 d_owner_priority
[q
] = priority
;
416 void QuantifiersEngine::setOwner(Node q
, quantifiers::QAttributes
& qa
)
418 if (!qa
.d_rr
.isNull())
420 if (d_private
->d_rr_engine
.get() == nullptr)
422 Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : "
425 // set rewrite engine as owner
426 setOwner(q
, d_private
->d_rr_engine
.get(), 2);
430 if (d_private
->d_synth_e
.get() == nullptr)
432 Trace("quant-warn") << "WARNING : synth engine is null, and we have : "
435 // set synth engine as owner
436 setOwner(q
, d_private
->d_synth_e
.get(), 2);
440 bool QuantifiersEngine::hasOwnership( Node q
, QuantifiersModule
* m
) {
441 QuantifiersModule
* mo
= getOwner( q
);
442 return mo
==m
|| mo
==NULL
;
445 bool QuantifiersEngine::isFiniteBound(Node q
, Node v
) const
447 quantifiers::BoundedIntegers
* bi
= d_private
->d_bint
.get();
448 if (bi
&& bi
->isBound(q
, v
))
452 TypeNode tn
= v
.getType();
453 if (tn
.isSort() && options::finiteModelFind())
457 else if (d_term_enum
->mayComplete(tn
))
464 BoundVarType
QuantifiersEngine::getBoundVarType(Node q
, Node v
) const
466 quantifiers::BoundedIntegers
* bi
= d_private
->d_bint
.get();
469 return bi
->getBoundVarType(q
, v
);
471 return isFiniteBound(q
, v
) ? BOUND_FINITE
: BOUND_NONE
;
474 void QuantifiersEngine::getBoundVarIndices(Node q
,
475 std::vector
<unsigned>& indices
) const
477 Assert(indices
.empty());
478 // we take the bounded variables first
479 quantifiers::BoundedIntegers
* bi
= d_private
->d_bint
.get();
482 bi
->getBoundVarIndices(q
, indices
);
484 // then get the remaining ones
485 for (unsigned i
= 0, nvars
= q
[0].getNumChildren(); i
< nvars
; i
++)
487 if (std::find(indices
.begin(), indices
.end(), i
) == indices
.end())
489 indices
.push_back(i
);
494 bool QuantifiersEngine::getBoundElements(RepSetIterator
* rsi
,
498 std::vector
<Node
>& elements
) const
500 quantifiers::BoundedIntegers
* bi
= d_private
->d_bint
.get();
503 return bi
->getBoundElements(rsi
, initial
, q
, v
, elements
);
508 void QuantifiersEngine::presolve() {
509 Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl
;
510 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
511 d_modules
[i
]->presolve();
513 d_term_db
->presolve();
515 //add all terms to database
516 if( options::incrementalSolving() ){
517 Trace("quant-engine-proc") << "Add presolve cache " << d_presolve_cache
.size() << std::endl
;
518 for( unsigned i
=0; i
<d_presolve_cache
.size(); i
++ ){
519 addTermToDatabase( d_presolve_cache
[i
], d_presolve_cache_wq
[i
], d_presolve_cache_wic
[i
] );
521 Trace("quant-engine-proc") << "Done add presolve cache " << std::endl
;
525 void QuantifiersEngine::ppNotifyAssertions(
526 const std::vector
<Node
>& assertions
) {
527 Trace("quant-engine-proc")
528 << "ppNotifyAssertions in QE, #assertions = " << assertions
.size()
529 << " check epr = " << (d_qepr
!= NULL
) << std::endl
;
530 if ((options::instLevelInputOnly() && options::instMaxLevel() != -1) ||
532 for (unsigned i
= 0; i
< assertions
.size(); i
++) {
533 if (options::instLevelInputOnly() && options::instMaxLevel() != -1) {
534 quantifiers::QuantAttributes::setInstantiationLevelAttr(assertions
[i
],
537 if (d_qepr
!= NULL
) {
538 d_qepr
->registerAssertion(assertions
[i
]);
541 if (d_qepr
!= NULL
) {
542 // must handle sources of other new constants e.g. separation logic
544 sep::TheorySep
* theory_sep
=
545 static_cast<sep::TheorySep
*>(getTheoryEngine()->theoryOf(THEORY_SEP
));
546 theory_sep
->initializeBounds();
547 d_qepr
->finishInit();
552 void QuantifiersEngine::check( Theory::Effort e
){
553 CodeTimer
codeTimer(d_statistics
.d_time
);
554 d_useModelEe
= options::quantModelEe() && ( e
>=Theory::EFFORT_LAST_CALL
);
555 // if we want to use the model's equality engine, build the model now
556 if( d_useModelEe
&& !d_model
->isBuilt() ){
557 Trace("quant-engine-debug") << "Build the model." << std::endl
;
558 if (!d_te
->getModelBuilder()->buildModel(d_model
.get()))
560 //we are done if model building was unsuccessful
562 if( d_hasAddedLemma
){
563 Trace("quant-engine-debug") << "...failed." << std::endl
;
569 if( !getActiveEqualityEngine()->consistent() ){
570 Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl
;
573 if (d_conflict_c
.get())
575 if (e
< Theory::EFFORT_LAST_CALL
)
577 // this can happen in rare cases when quantifiers is the first to realize
578 // there is a quantifier-free conflict, for example, when it discovers
579 // disequal and congruent terms in the master equality engine during
580 // term indexing. In such cases, quantifiers reports a "conflicting lemma"
581 // that is, one that is entailed to be false by the current assignment.
582 // If this lemma is not a SAT conflict, we may get another call to full
583 // effort check and the quantifier-free solvers still haven't realized
584 // there is a conflict. In this case, we return, trusting that theory
585 // combination will do the right thing (split on equalities until there is
586 // a conflict at the quantifier-free level).
587 Trace("quant-engine-debug")
588 << "Conflicting lemma already reported by quantifiers, return."
592 // we reported what we thought was a conflicting lemma, but now we have
593 // gotten a check at LAST_CALL effort, indicating that the lemma we reported
594 // was not conflicting. This should never happen, but in production mode, we
595 // proceed with the check.
598 bool needsCheck
= !d_lemmas_waiting
.empty();
599 QuantifiersModule::QEffort needsModelE
= QuantifiersModule::QEFFORT_NONE
;
600 std::vector
< QuantifiersModule
* > qm
;
601 if( d_model
->checkNeeded() ){
602 needsCheck
= needsCheck
|| e
>=Theory::EFFORT_LAST_CALL
; //always need to check at or above last call
603 for (QuantifiersModule
*& mdl
: d_modules
)
605 if (mdl
->needsCheck(e
))
609 //can only request model at last call since theory combination can find inconsistencies
610 if( e
>=Theory::EFFORT_LAST_CALL
){
611 QuantifiersModule::QEffort me
= mdl
->needsModel(e
);
612 needsModelE
= me
<needsModelE
? me
: needsModelE
;
619 d_hasAddedLemma
= false;
620 bool setIncomplete
= false;
622 Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e
<< ", needsCheck=" << needsCheck
<< std::endl
;
624 //flush previous lemmas (for instance, if was interupted), or other lemmas to process
626 if( d_hasAddedLemma
){
631 if( Trace
.isOn("quant-engine") ){
632 clSet
= double(clock())/double(CLOCKS_PER_SEC
);
633 Trace("quant-engine") << ">>>>> Quantifiers Engine Round, effort = " << e
<< " <<<<<" << std::endl
;
636 if( Trace
.isOn("quant-engine-debug") ){
637 Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e
<< std::endl
;
638 Trace("quant-engine-debug") << " depth : " << d_ierCounter_c
<< std::endl
;
639 Trace("quant-engine-debug") << " modules to check : ";
640 for( unsigned i
=0; i
<qm
.size(); i
++ ){
641 Trace("quant-engine-debug") << qm
[i
]->identify() << " ";
643 Trace("quant-engine-debug") << std::endl
;
644 Trace("quant-engine-debug") << " # quantified formulas = " << d_model
->getNumAssertedQuantifiers() << std::endl
;
645 if( !d_lemmas_waiting
.empty() ){
646 Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting
.size() << std::endl
;
648 Trace("quant-engine-debug") << " Theory engine finished : " << !d_te
->needCheck() << std::endl
;
649 Trace("quant-engine-debug") << " Needs model effort : " << needsModelE
<< std::endl
;
651 if( Trace
.isOn("quant-engine-ee-pre") ){
652 Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl
;
653 debugPrintEqualityEngine( "quant-engine-ee-pre" );
655 if( Trace
.isOn("quant-engine-assert") ){
656 Trace("quant-engine-assert") << "Assertions : " << std::endl
;
657 getTheoryEngine()->printAssertions("quant-engine-assert");
661 Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl
;
662 for (QuantifiersUtil
*& util
: d_util
)
664 Trace("quant-engine-debug2") << "Reset " << util
->identify().c_str()
665 << "..." << std::endl
;
669 if( d_hasAddedLemma
){
672 //should only fail reset if added a lemma
678 if( Trace
.isOn("quant-engine-ee") ){
679 Trace("quant-engine-ee") << "Equality engine : " << std::endl
;
680 debugPrintEqualityEngine( "quant-engine-ee" );
684 Trace("quant-engine-debug") << "Reset model..." << std::endl
;
685 d_model
->reset_round();
688 Trace("quant-engine-debug") << "Resetting all modules..." << std::endl
;
689 for (QuantifiersModule
*& mdl
: d_modules
)
691 Trace("quant-engine-debug2") << "Reset " << mdl
->identify().c_str()
695 Trace("quant-engine-debug") << "Done resetting all modules." << std::endl
;
696 //reset may have added lemmas
698 if( d_hasAddedLemma
){
702 if( e
==Theory::EFFORT_LAST_CALL
){
703 ++(d_statistics
.d_instantiation_rounds_lc
);
704 }else if( e
==Theory::EFFORT_FULL
){
705 ++(d_statistics
.d_instantiation_rounds
);
707 Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl
;
708 for (unsigned qef
= QuantifiersModule::QEFFORT_CONFLICT
;
709 qef
<= QuantifiersModule::QEFFORT_LAST_CALL
;
712 QuantifiersModule::QEffort quant_e
=
713 static_cast<QuantifiersModule::QEffort
>(qef
);
714 d_curr_effort_level
= quant_e
;
715 //build the model if any module requested it
716 if (needsModelE
== quant_e
)
718 if (!d_model
->isBuilt())
720 // theory engine's model builder is quantifier engine's builder if it
722 Assert(!getModelBuilder()
723 || getModelBuilder() == d_te
->getModelBuilder());
724 Trace("quant-engine-debug") << "Build model..." << std::endl
;
725 if (!d_te
->getModelBuilder()->buildModel(d_model
.get()))
730 if (!d_model
->isBuiltSuccess())
735 if( !d_hasAddedLemma
){
737 for (QuantifiersModule
*& mdl
: qm
)
739 Trace("quant-engine-debug") << "Check " << mdl
->identify().c_str()
740 << " at effort " << quant_e
<< "..."
742 mdl
->check(e
, quant_e
);
744 Trace("quant-engine-debug") << "...conflict!" << std::endl
;
748 //flush all current lemmas
751 //if we have added one, stop
752 if( d_hasAddedLemma
){
755 Assert( !d_conflict
);
756 if (quant_e
== QuantifiersModule::QEFFORT_CONFLICT
)
758 if( e
==Theory::EFFORT_FULL
){
759 //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase
760 if( d_ierCounterLastLc
!=d_ierCounter_lc
|| !options::instWhenStrictInterleave() || d_ierCounter
%d_inst_when_phase
!=0 ){
761 d_ierCounter
= d_ierCounter
+ 1;
762 d_ierCounterLastLc
= d_ierCounter_lc
;
763 d_ierCounter_c
= d_ierCounter_c
.get() + 1;
765 }else if( e
==Theory::EFFORT_LAST_CALL
){
766 d_ierCounter_lc
= d_ierCounter_lc
+ 1;
769 else if (quant_e
== QuantifiersModule::QEFFORT_MODEL
)
771 if( e
==Theory::EFFORT_LAST_CALL
){
772 //sources of incompleteness
773 for (QuantifiersUtil
*& util
: d_util
)
775 if (!util
->checkComplete())
777 Trace("quant-engine-debug") << "Set incomplete because utility "
778 << util
->identify().c_str()
779 << " was incomplete." << std::endl
;
780 setIncomplete
= true;
783 if (d_conflict_c
.get())
785 // we reported a conflicting lemma, should return
786 setIncomplete
= true;
788 //if we have a chance not to set incomplete
789 if( !setIncomplete
){
790 //check if we should set the incomplete flag
791 for (QuantifiersModule
*& mdl
: d_modules
)
793 if (!mdl
->checkComplete())
795 Trace("quant-engine-debug")
796 << "Set incomplete because module "
797 << mdl
->identify().c_str() << " was incomplete."
799 setIncomplete
= true;
803 if( !setIncomplete
){
804 //look at individual quantified formulas, one module must claim completeness for each one
805 for( unsigned i
=0; i
<d_model
->getNumAssertedQuantifiers(); i
++ ){
806 bool hasCompleteM
= false;
807 Node q
= d_model
->getAssertedQuantifier( i
);
808 QuantifiersModule
* qmd
= getOwner( q
);
810 hasCompleteM
= qmd
->checkCompleteFor( q
);
812 for( unsigned j
=0; j
<d_modules
.size(); j
++ ){
813 if( d_modules
[j
]->checkCompleteFor( q
) ){
821 Trace("quant-engine-debug") << "Set incomplete because " << q
<< " was not fully processed." << std::endl
;
822 setIncomplete
= true;
826 Trace("quant-engine-debug2") << "Complete for " << q
<< " due to " << qmd
->identify().c_str() << std::endl
;
831 //if setIncomplete = false, we will answer SAT, otherwise we will run at quant_e QEFFORT_LAST_CALL
832 if( !setIncomplete
){
839 d_curr_effort_level
= QuantifiersModule::QEFFORT_NONE
;
840 Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl
;
841 if( d_hasAddedLemma
){
842 d_instantiate
->debugPrint();
844 if( Trace
.isOn("quant-engine") ){
845 double clSet2
= double(clock())/double(CLOCKS_PER_SEC
);
846 Trace("quant-engine") << "Finished quantifiers engine, total time = " << (clSet2
-clSet
);
847 Trace("quant-engine") << ", added lemma = " << d_hasAddedLemma
;
848 Trace("quant-engine") << std::endl
;
851 Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl
;
853 Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl
;
857 if( e
==Theory::EFFORT_LAST_CALL
&& !d_hasAddedLemma
){
859 Trace("quant-engine") << "Set incomplete flag." << std::endl
;
860 getOutputChannel().setIncomplete();
863 d_instantiate
->debugPrintModel();
867 void QuantifiersEngine::notifyCombineTheories() {
868 //if allowing theory combination to happen at most once between instantiation rounds
870 //d_ierCounterLastLc = -1;
873 bool QuantifiersEngine::reduceQuantifier( Node q
) {
874 //TODO: this can be unified with preregistration: AlphaEquivalence takes ownership of reducable quants
875 BoolMap::const_iterator it
= d_quants_red
.find( q
);
876 if( it
==d_quants_red
.end() ){
878 std::map
< Node
, Node
>::iterator itr
= d_quants_red_lem
.find( q
);
879 if( itr
==d_quants_red_lem
.end() ){
880 if (d_private
->d_alpha_equiv
)
882 Trace("quant-engine-red") << "Alpha equivalence " << q
<< "?" << std::endl
;
883 //add equivalence with another quantified formula
884 lem
= d_private
->d_alpha_equiv
->reduceQuantifier(q
);
886 Trace("quant-engine-red") << "...alpha equivalence success." << std::endl
;
887 ++(d_statistics
.d_red_alpha_equiv
);
890 d_quants_red_lem
[q
] = lem
;
895 getOutputChannel().lemma( lem
);
897 d_quants_red
[q
] = !lem
.isNull();
898 return !lem
.isNull();
904 void QuantifiersEngine::registerQuantifierInternal(Node f
)
906 std::map
< Node
, bool >::iterator it
= d_quants
.find( f
);
907 if( it
==d_quants
.end() ){
908 Trace("quant") << "QuantifiersEngine : Register quantifier ";
909 Trace("quant") << " : " << f
<< std::endl
;
910 unsigned prev_lemma_waiting
= d_lemmas_waiting
.size();
911 ++(d_statistics
.d_num_quant
);
912 Assert( f
.getKind()==FORALL
);
913 // register with utilities
914 for (unsigned i
= 0; i
< d_util
.size(); i
++)
916 d_util
[i
]->registerQuantifier(f
);
918 // compute attributes
919 d_quant_attr
->computeAttributes(f
);
921 for (QuantifiersModule
*& mdl
: d_modules
)
923 Trace("quant-debug") << "check ownership with " << mdl
->identify()
924 << "..." << std::endl
;
925 mdl
->checkOwnership(f
);
927 QuantifiersModule
* qm
= getOwner(f
);
928 Trace("quant") << " Owner : " << (qm
== nullptr ? "[none]" : qm
->identify())
930 // register with each module
931 for (QuantifiersModule
*& mdl
: d_modules
)
933 Trace("quant-debug") << "register with " << mdl
->identify() << "..."
935 mdl
->registerQuantifier(f
);
936 // since this is context-independent, we should not add any lemmas during
938 Assert(d_lemmas_waiting
.size() == prev_lemma_waiting
);
940 Trace("quant-debug") << "...finish." << std::endl
;
942 AlwaysAssert(d_lemmas_waiting
.size() == prev_lemma_waiting
);
946 void QuantifiersEngine::preRegisterQuantifier(Node q
)
948 NodeSet::const_iterator it
= d_quants_prereg
.find(q
);
949 if (it
!= d_quants_prereg
.end())
953 Trace("quant-debug") << "QuantifiersEngine : Pre-register " << q
<< std::endl
;
954 d_quants_prereg
.insert(q
);
956 if (reduceQuantifier(q
))
958 // if we can reduce it, nothing left to do
961 // ensure that it is registered
962 registerQuantifierInternal(q
);
963 // register with each module
964 for (QuantifiersModule
*& mdl
: d_modules
)
966 Trace("quant-debug") << "pre-register with " << mdl
->identify() << "..."
968 mdl
->preRegisterQuantifier(q
);
972 Trace("quant-debug") << "...finish pre-register " << q
<< "..." << std::endl
;
975 void QuantifiersEngine::registerPattern( std::vector
<Node
> & pattern
) {
976 for(std::vector
<Node
>::iterator p
= pattern
.begin(); p
!= pattern
.end(); ++p
){
977 std::set
< Node
> added
;
978 getTermDatabase()->addTerm( *p
, added
);
982 void QuantifiersEngine::assertQuantifier( Node f
, bool pol
){
983 if (reduceQuantifier(f
))
985 // if we can reduce it, nothing left to do
990 Node lem
= d_skolemize
->process(f
);
993 if (Trace
.isOn("quantifiers-sk-debug"))
995 Node slem
= Rewriter::rewrite(lem
);
996 Trace("quantifiers-sk-debug")
997 << "Skolemize lemma : " << slem
<< std::endl
;
999 getOutputChannel().lemma(lem
, false, true);
1003 // ensure the quantified formula is registered
1004 registerQuantifierInternal(f
);
1005 // assert it to each module
1006 d_model
->assertQuantifier(f
);
1007 for (QuantifiersModule
*& mdl
: d_modules
)
1011 addTermToDatabase(d_term_util
->getInstConstantBody(f
), true);
1014 void QuantifiersEngine::addTermToDatabase( Node n
, bool withinQuant
, bool withinInstClosure
){
1015 if( options::incrementalSolving() ){
1016 if( d_presolve_in
.find( n
)==d_presolve_in
.end() ){
1017 d_presolve_in
.insert( n
);
1018 d_presolve_cache
.push_back( n
);
1019 d_presolve_cache_wq
.push_back( withinQuant
);
1020 d_presolve_cache_wic
.push_back( withinInstClosure
);
1023 //only wait if we are doing incremental solving
1024 if( !d_presolve
|| !options::incrementalSolving() ){
1025 std::set
< Node
> added
;
1026 d_term_db
->addTerm(n
, added
, withinQuant
, withinInstClosure
);
1032 d_sygus_tdb
->getEvalUnfold()->registerEvalTerm(n
);
1038 void QuantifiersEngine::eqNotifyNewClass(TNode t
) {
1039 addTermToDatabase( t
);
1040 if( d_eq_inference
){
1041 d_eq_inference
->eqNotifyNewClass( t
);
1045 void QuantifiersEngine::eqNotifyPreMerge(TNode t1
, TNode t2
) {
1046 if( d_eq_inference
){
1047 d_eq_inference
->eqNotifyMerge( t1
, t2
);
1051 void QuantifiersEngine::eqNotifyPostMerge(TNode t1
, TNode t2
) {
1055 void QuantifiersEngine::eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
) {
1057 // d_qcf->assertDisequal( t1, t2 );
1061 bool QuantifiersEngine::addLemma( Node lem
, bool doCache
, bool doRewrite
){
1064 lem
= Rewriter::rewrite(lem
);
1066 Trace("inst-add-debug") << "Adding lemma : " << lem
<< std::endl
;
1067 BoolMap::const_iterator itp
= d_lemmas_produced_c
.find( lem
);
1068 if( itp
==d_lemmas_produced_c
.end() || !(*itp
).second
){
1069 //d_curr_out->lemma( lem, false, true );
1070 d_lemmas_produced_c
[ lem
] = true;
1071 d_lemmas_waiting
.push_back( lem
);
1072 Trace("inst-add-debug") << "Added lemma" << std::endl
;
1075 Trace("inst-add-debug") << "Duplicate." << std::endl
;
1079 //do not need to rewrite, will be rewritten after sending
1080 d_lemmas_waiting
.push_back( lem
);
1085 bool QuantifiersEngine::removeLemma( Node lem
) {
1086 std::vector
< Node
>::iterator it
= std::find( d_lemmas_waiting
.begin(), d_lemmas_waiting
.end(), lem
);
1087 if( it
!=d_lemmas_waiting
.end() ){
1088 d_lemmas_waiting
.erase( it
, it
+ 1 );
1089 d_lemmas_produced_c
[ lem
] = false;
1096 void QuantifiersEngine::addRequirePhase( Node lit
, bool req
){
1097 d_phase_req_waiting
[lit
] = req
;
1100 void QuantifiersEngine::markRelevant( Node q
) {
1101 d_model
->markRelevant( q
);
1104 void QuantifiersEngine::setConflict() {
1106 d_conflict_c
= true;
1109 bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e
) {
1110 Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter
<< ", " << d_ierCounter_lc
<< std::endl
;
1111 //determine if we should perform check, based on instWhenMode
1112 bool performCheck
= false;
1113 if( options::instWhenMode()==quantifiers::INST_WHEN_FULL
){
1114 performCheck
= ( e
>= Theory::EFFORT_FULL
);
1115 }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY
){
1116 performCheck
= ( e
>= Theory::EFFORT_FULL
) && !getTheoryEngine()->needCheck();
1117 }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL
){
1118 performCheck
= ( ( e
==Theory::EFFORT_FULL
&& d_ierCounter
%d_inst_when_phase
!=0 ) || e
==Theory::EFFORT_LAST_CALL
);
1119 }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL
){
1120 performCheck
= ( ( e
==Theory::EFFORT_FULL
&& !getTheoryEngine()->needCheck() && d_ierCounter
%d_inst_when_phase
!=0 ) || e
==Theory::EFFORT_LAST_CALL
);
1121 }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL
){
1122 performCheck
= ( e
>= Theory::EFFORT_LAST_CALL
);
1124 performCheck
= true;
1126 if( e
==Theory::EFFORT_LAST_CALL
){
1127 //with bounded integers, skip every other last call,
1128 // since matching loops may occur with infinite quantification
1129 if( d_ierCounter_lc
%2==0 && options::fmfBound() ){
1130 performCheck
= false;
1133 return performCheck
;
1136 quantifiers::UserPatMode
QuantifiersEngine::getInstUserPatMode() {
1137 if( options::userPatternsQuant()==quantifiers::USER_PAT_MODE_INTERLEAVE
){
1138 return d_ierCounter
%2==0 ? quantifiers::USER_PAT_MODE_USE
: quantifiers::USER_PAT_MODE_RESORT
;
1140 return options::userPatternsQuant();
1144 void QuantifiersEngine::flushLemmas(){
1145 if( !d_lemmas_waiting
.empty() ){
1146 //filter based on notify classes
1147 if (d_instantiate
->hasNotify())
1149 unsigned prev_lem_sz
= d_lemmas_waiting
.size();
1150 d_instantiate
->notifyFlushLemmas();
1151 if( prev_lem_sz
!=d_lemmas_waiting
.size() ){
1152 Trace("quant-engine") << "...filtered instances : " << d_lemmas_waiting
.size() << " / " << prev_lem_sz
<< std::endl
;
1155 //take default output channel if none is provided
1156 d_hasAddedLemma
= true;
1157 for( unsigned i
=0; i
<d_lemmas_waiting
.size(); i
++ ){
1158 Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting
[i
] << std::endl
;
1159 getOutputChannel().lemma( d_lemmas_waiting
[i
], false, true );
1161 d_lemmas_waiting
.clear();
1163 if( !d_phase_req_waiting
.empty() ){
1164 for( std::map
< Node
, bool >::iterator it
= d_phase_req_waiting
.begin(); it
!= d_phase_req_waiting
.end(); ++it
){
1165 Trace("qe-lemma") << "Require phase : " << it
->first
<< " -> " << it
->second
<< std::endl
;
1166 getOutputChannel().requirePhase( it
->first
, it
->second
);
1168 d_phase_req_waiting
.clear();
1172 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector
< Node
>& active_lemmas
) {
1173 return d_instantiate
->getUnsatCoreLemmas(active_lemmas
);
1176 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector
< Node
>& active_lemmas
, std::map
< Node
, Node
>& weak_imp
) {
1177 return d_instantiate
->getUnsatCoreLemmas(active_lemmas
, weak_imp
);
1180 void QuantifiersEngine::getInstantiationTermVectors( Node q
, std::vector
< std::vector
< Node
> >& tvecs
) {
1181 d_instantiate
->getInstantiationTermVectors(q
, tvecs
);
1184 void QuantifiersEngine::getInstantiationTermVectors( std::map
< Node
, std::vector
< std::vector
< Node
> > >& insts
) {
1185 d_instantiate
->getInstantiationTermVectors(insts
);
1188 void QuantifiersEngine::getExplanationForInstLemmas(
1189 const std::vector
<Node
>& lems
,
1190 std::map
<Node
, Node
>& quant
,
1191 std::map
<Node
, std::vector
<Node
> >& tvec
)
1193 d_instantiate
->getExplanationForInstLemmas(lems
, quant
, tvec
);
1196 void QuantifiersEngine::printInstantiations( std::ostream
& out
) {
1197 bool printed
= false;
1198 // print the skolemizations
1199 if (d_skolemize
->printSkolemization(out
))
1203 // print the instantiations
1204 if (d_instantiate
->printInstantiations(out
))
1209 out
<< "No instantiations" << std::endl
;
1213 void QuantifiersEngine::printSynthSolution( std::ostream
& out
) {
1214 if (d_private
->d_synth_e
)
1216 d_private
->d_synth_e
->printSynthSolution(out
);
1218 out
<< "Internal error : module for synth solution not found." << std::endl
;
1222 void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector
< Node
>& qs
) {
1223 d_instantiate
->getInstantiatedQuantifiedFormulas(qs
);
1226 void QuantifiersEngine::getInstantiations( std::map
< Node
, std::vector
< Node
> >& insts
) {
1227 d_instantiate
->getInstantiations(insts
);
1230 void QuantifiersEngine::getInstantiations( Node q
, std::vector
< Node
>& insts
) {
1231 d_instantiate
->getInstantiations(q
, insts
);
1234 Node
QuantifiersEngine::getInstantiatedConjunction( Node q
) {
1235 return d_instantiate
->getInstantiatedConjunction(q
);
1238 QuantifiersEngine::Statistics::Statistics()
1239 : d_time("theory::QuantifiersEngine::time"),
1240 d_qcf_time("theory::QuantifiersEngine::time_qcf"),
1241 d_ematching_time("theory::QuantifiersEngine::time_ematching"),
1242 d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
1243 d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
1244 d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
1245 d_triggers("QuantifiersEngine::Triggers", 0),
1246 d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
1247 d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
1248 d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
1249 d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0),
1250 d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0),
1251 d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0),
1252 d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0),
1253 d_instantiations_qcf("QuantifiersEngine::Instantiations_Qcf_Conflict", 0),
1254 d_instantiations_qcf_prop("QuantifiersEngine::Instantiations_Qcf_Prop", 0),
1255 d_instantiations_fmf_exh("QuantifiersEngine::Instantiations_Fmf_Exh", 0),
1256 d_instantiations_fmf_mbqi("QuantifiersEngine::Instantiations_Fmf_Mbqi", 0),
1257 d_instantiations_cbqi("QuantifiersEngine::Instantiations_Cbqi", 0),
1258 d_instantiations_rr("QuantifiersEngine::Instantiations_Rewrite_Rules", 0)
1260 smtStatisticsRegistry()->registerStat(&d_time
);
1261 smtStatisticsRegistry()->registerStat(&d_qcf_time
);
1262 smtStatisticsRegistry()->registerStat(&d_ematching_time
);
1263 smtStatisticsRegistry()->registerStat(&d_num_quant
);
1264 smtStatisticsRegistry()->registerStat(&d_instantiation_rounds
);
1265 smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc
);
1266 smtStatisticsRegistry()->registerStat(&d_triggers
);
1267 smtStatisticsRegistry()->registerStat(&d_simple_triggers
);
1268 smtStatisticsRegistry()->registerStat(&d_multi_triggers
);
1269 smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations
);
1270 smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv
);
1271 smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns
);
1272 smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen
);
1273 smtStatisticsRegistry()->registerStat(&d_instantiations_guess
);
1274 smtStatisticsRegistry()->registerStat(&d_instantiations_qcf
);
1275 smtStatisticsRegistry()->registerStat(&d_instantiations_qcf_prop
);
1276 smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_exh
);
1277 smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_mbqi
);
1278 smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi
);
1279 smtStatisticsRegistry()->registerStat(&d_instantiations_rr
);
1282 QuantifiersEngine::Statistics::~Statistics(){
1283 smtStatisticsRegistry()->unregisterStat(&d_time
);
1284 smtStatisticsRegistry()->unregisterStat(&d_qcf_time
);
1285 smtStatisticsRegistry()->unregisterStat(&d_ematching_time
);
1286 smtStatisticsRegistry()->unregisterStat(&d_num_quant
);
1287 smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds
);
1288 smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc
);
1289 smtStatisticsRegistry()->unregisterStat(&d_triggers
);
1290 smtStatisticsRegistry()->unregisterStat(&d_simple_triggers
);
1291 smtStatisticsRegistry()->unregisterStat(&d_multi_triggers
);
1292 smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations
);
1293 smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv
);
1294 smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns
);
1295 smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen
);
1296 smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess
);
1297 smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf
);
1298 smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf_prop
);
1299 smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_exh
);
1300 smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_mbqi
);
1301 smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi
);
1302 smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr
);
1305 eq::EqualityEngine
* QuantifiersEngine::getMasterEqualityEngine() const
1307 return d_te
->getMasterEqualityEngine();
1310 eq::EqualityEngine
* QuantifiersEngine::getActiveEqualityEngine() const
1313 return d_model
->getEqualityEngine();
1315 return d_te
->getMasterEqualityEngine();
1318 Node
QuantifiersEngine::getInternalRepresentative( Node a
, Node q
, int index
){
1319 bool prevModelEe
= d_useModelEe
;
1320 d_useModelEe
= false;
1321 Node ret
= d_eq_query
->getInternalRepresentative( a
, q
, index
);
1322 d_useModelEe
= prevModelEe
;
1326 void QuantifiersEngine::getSynthSolutions(std::map
<Node
, Node
>& sol_map
)
1328 d_private
->d_synth_e
->getSynthSolutions(sol_map
);
1331 void QuantifiersEngine::debugPrintEqualityEngine( const char * c
) {
1332 eq::EqualityEngine
* ee
= getActiveEqualityEngine();
1333 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( ee
);
1334 std::map
< TypeNode
, int > typ_num
;
1335 while( !eqcs_i
.isFinished() ){
1336 TNode r
= (*eqcs_i
);
1337 TypeNode tr
= r
.getType();
1338 if( typ_num
.find( tr
)==typ_num
.end() ){
1342 bool firstTime
= true;
1343 Trace(c
) << " " << r
;
1344 Trace(c
) << " : { ";
1345 eq::EqClassIterator eqc_i
= eq::EqClassIterator( r
, ee
);
1346 while( !eqc_i
.isFinished() ){
1350 Trace(c
) << std::endl
;
1353 Trace(c
) << " " << n
<< std::endl
;
1357 if( !firstTime
){ Trace(c
) << " "; }
1358 Trace(c
) << "}" << std::endl
;
1361 Trace(c
) << std::endl
;
1362 for( std::map
< TypeNode
, int >::iterator it
= typ_num
.begin(); it
!= typ_num
.end(); ++it
){
1363 Trace(c
) << "# eqc for " << it
->first
<< " : " << it
->second
<< std::endl
;
1367 } // namespace theory