1 /********************* */
2 /*! \file quantifiers_engine.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Mathias Preiner
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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_engine_scope.h"
20 #include "smt/smt_statistics_registry.h"
21 #include "theory/quantifiers/alpha_equivalence.h"
22 #include "theory/quantifiers/anti_skolem.h"
23 #include "theory/quantifiers/conjecture_generator.h"
24 #include "theory/quantifiers/ematching/instantiation_engine.h"
25 #include "theory/quantifiers/fmf/bounded_integers.h"
26 #include "theory/quantifiers/fmf/full_model_check.h"
27 #include "theory/quantifiers/fmf/model_engine.h"
28 #include "theory/quantifiers/inst_strategy_enumerative.h"
29 #include "theory/quantifiers/quant_conflict_find.h"
30 #include "theory/quantifiers/quant_split.h"
31 #include "theory/quantifiers/quantifiers_rewriter.h"
32 #include "theory/quantifiers/sygus/synth_engine.h"
33 #include "theory/quantifiers/sygus_inst.h"
34 #include "theory/sep/theory_sep.h"
35 #include "theory/theory_engine.h"
36 #include "theory/uf/equality_engine.h"
39 using namespace CVC4::kind
;
44 class QuantifiersEnginePrivate
47 QuantifiersEnginePrivate()
49 d_alpha_equiv(nullptr),
50 d_inst_engine(nullptr),
51 d_model_engine(nullptr),
59 d_anti_skolem(nullptr),
63 ~QuantifiersEnginePrivate() {}
64 //------------------------------ private quantifier utilities
65 /** relevant domain */
66 std::unique_ptr
<quantifiers::RelevantDomain
> d_rel_dom
;
67 //------------------------------ end private quantifier utilities
68 //------------------------------ quantifiers modules
69 /** alpha equivalence */
70 std::unique_ptr
<quantifiers::AlphaEquivalence
> d_alpha_equiv
;
71 /** instantiation engine */
72 std::unique_ptr
<quantifiers::InstantiationEngine
> d_inst_engine
;
74 std::unique_ptr
<quantifiers::ModelEngine
> d_model_engine
;
75 /** bounded integers utility */
76 std::unique_ptr
<quantifiers::BoundedIntegers
> d_bint
;
77 /** Conflict find mechanism for quantifiers */
78 std::unique_ptr
<quantifiers::QuantConflictFind
> d_qcf
;
79 /** subgoal generator */
80 std::unique_ptr
<quantifiers::ConjectureGenerator
> d_sg_gen
;
81 /** ceg instantiation */
82 std::unique_ptr
<quantifiers::SynthEngine
> d_synth_e
;
83 /** full saturation */
84 std::unique_ptr
<quantifiers::InstStrategyEnum
> d_fs
;
85 /** counterexample-based quantifier instantiation */
86 std::unique_ptr
<quantifiers::InstStrategyCegqi
> d_i_cbqi
;
87 /** quantifiers splitting */
88 std::unique_ptr
<quantifiers::QuantDSplit
> d_qsplit
;
89 /** quantifiers anti-skolemization */
90 std::unique_ptr
<quantifiers::QuantAntiSkolem
> d_anti_skolem
;
91 /** SyGuS instantiation engine */
92 std::unique_ptr
<quantifiers::SygusInst
> d_sygus_inst
;
93 //------------------------------ end quantifiers modules
96 * This constructs the above modules based on the current options. It adds
97 * a pointer to each module it constructs to modules. This method sets
98 * needsBuilder to true if we require a strategy-specific model builder
101 void initialize(QuantifiersEngine
* qe
,
103 std::vector
<QuantifiersModule
*>& modules
,
106 // add quantifiers modules
107 if (options::quantConflictFind())
109 d_qcf
.reset(new quantifiers::QuantConflictFind(qe
, c
));
110 modules
.push_back(d_qcf
.get());
112 if (options::conjectureGen())
114 d_sg_gen
.reset(new quantifiers::ConjectureGenerator(qe
, c
));
115 modules
.push_back(d_sg_gen
.get());
117 if (!options::finiteModelFind() || options::fmfInstEngine())
119 d_inst_engine
.reset(new quantifiers::InstantiationEngine(qe
));
120 modules
.push_back(d_inst_engine
.get());
122 if (options::cegqi())
124 d_i_cbqi
.reset(new quantifiers::InstStrategyCegqi(qe
));
125 modules
.push_back(d_i_cbqi
.get());
126 qe
->getInstantiate()->addRewriter(d_i_cbqi
->getInstRewriter());
128 if (options::sygus())
130 d_synth_e
.reset(new quantifiers::SynthEngine(qe
, c
));
131 modules
.push_back(d_synth_e
.get());
133 // finite model finding
134 if (options::fmfBound())
136 d_bint
.reset(new quantifiers::BoundedIntegers(c
, qe
));
137 modules
.push_back(d_bint
.get());
139 if (options::finiteModelFind() || options::fmfBound())
141 d_model_engine
.reset(new quantifiers::ModelEngine(c
, qe
));
142 modules
.push_back(d_model_engine
.get());
143 // finite model finder has special ways of building the model
146 if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE
)
148 d_qsplit
.reset(new quantifiers::QuantDSplit(qe
, c
));
149 modules
.push_back(d_qsplit
.get());
151 if (options::quantAntiSkolem())
153 d_anti_skolem
.reset(new quantifiers::QuantAntiSkolem(qe
));
154 modules
.push_back(d_anti_skolem
.get());
156 if (options::quantAlphaEquiv())
158 d_alpha_equiv
.reset(new quantifiers::AlphaEquivalence(qe
));
160 // full saturation : instantiate from relevant domain, then arbitrary terms
161 if (options::fullSaturateQuant() || options::fullSaturateInterleave())
163 d_rel_dom
.reset(new quantifiers::RelevantDomain(qe
));
164 d_fs
.reset(new quantifiers::InstStrategyEnum(qe
, d_rel_dom
.get()));
165 modules
.push_back(d_fs
.get());
167 if (options::sygusInst())
169 d_sygus_inst
.reset(new quantifiers::SygusInst(qe
));
170 modules
.push_back(d_sygus_inst
.get());
175 QuantifiersEngine::QuantifiersEngine(context::Context
* c
,
176 context::UserContext
* u
,
179 d_masterEqualityEngine(nullptr),
180 d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c
, this)),
181 d_tr_trie(new inst::TriggerTrie
),
185 d_term_util(new quantifiers::TermUtil(this)),
186 d_term_canon(new expr::TermCanonize
),
187 d_term_db(new quantifiers::TermDb(c
, u
, this)),
188 d_sygus_tdb(nullptr),
189 d_quant_attr(new quantifiers::QuantAttributes(this)),
190 d_instantiate(new quantifiers::Instantiate(this, u
)),
191 d_skolemize(new quantifiers::Skolemize(this, u
)),
192 d_term_enum(new quantifiers::TermEnumeration
),
193 d_conflict_c(c
, false),
197 d_lemmas_produced_c(u
),
200 // d_ierCounter_lc(c),
201 // d_ierCounterLastLc(c),
205 d_presolve_cache_wq(u
),
206 d_presolve_cache_wic(u
)
208 // initialize the private utility
209 d_private
.reset(new QuantifiersEnginePrivate
);
212 d_util
.push_back(d_eq_query
.get());
213 // term util must come before the other utilities
214 d_util
.push_back(d_term_util
.get());
215 d_util
.push_back(d_term_db
.get());
217 if (options::sygus() || options::sygusInst())
219 d_sygus_tdb
.reset(new quantifiers::TermDbSygus(c
, this));
222 d_util
.push_back(d_instantiate
.get());
224 d_curr_effort_level
= QuantifiersModule::QEFFORT_NONE
;
226 d_hasAddedLemma
= false;
227 //don't add true lemma
228 d_lemmas_produced_c
[d_term_util
->d_true
] = true;
230 Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl
;
231 Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl
;
233 if( options::quantEpr() ){
234 Assert(!options::incrementalSolving());
235 d_qepr
.reset(new quantifiers::QuantEPR
);
239 //allow theory combination to go first, once initially
240 d_ierCounter
= options::instWhenTcFirst() ? 0 : 1;
241 d_ierCounter_c
= d_ierCounter
;
243 d_ierCounterLastLc
= 0;
244 d_inst_when_phase
= 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
246 bool needsBuilder
= false;
247 d_private
->initialize(this, c
, d_modules
, needsBuilder
);
249 if (d_private
->d_rel_dom
.get())
251 d_util
.push_back(d_private
->d_rel_dom
.get());
254 // if we require specialized ways of building the model
256 Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl
;
257 if (options::mbqiMode() == options::MbqiMode::FMC
258 || options::mbqiMode() == options::MbqiMode::TRUST
259 || options::fmfBound())
261 Trace("quant-engine-debug") << "...make fmc builder." << std::endl
;
262 d_model
.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
263 this, c
, "FirstOrderModelFmc"));
264 d_builder
.reset(new quantifiers::fmcheck::FullModelChecker(c
, this));
266 Trace("quant-engine-debug") << "...make default model builder." << std::endl
;
268 new quantifiers::FirstOrderModel(this, c
, "FirstOrderModel"));
269 d_builder
.reset(new quantifiers::QModelBuilder(c
, this));
272 d_model
.reset(new quantifiers::FirstOrderModel(this, c
, "FirstOrderModel"));
276 QuantifiersEngine::~QuantifiersEngine() {}
278 void QuantifiersEngine::setMasterEqualityEngine(eq::EqualityEngine
* mee
)
280 d_masterEqualityEngine
= mee
;
283 context::Context
* QuantifiersEngine::getSatContext()
285 return d_te
->theoryOf(THEORY_QUANTIFIERS
)->getSatContext();
288 context::UserContext
* QuantifiersEngine::getUserContext()
290 return d_te
->theoryOf(THEORY_QUANTIFIERS
)->getUserContext();
293 OutputChannel
& QuantifiersEngine::getOutputChannel()
295 return d_te
->theoryOf(THEORY_QUANTIFIERS
)->getOutputChannel();
297 /** get default valuation for the quantifiers engine */
298 Valuation
& QuantifiersEngine::getValuation()
300 return d_te
->theoryOf(THEORY_QUANTIFIERS
)->getValuation();
303 const LogicInfo
& QuantifiersEngine::getLogicInfo() const
305 return d_te
->getLogicInfo();
308 EqualityQuery
* QuantifiersEngine::getEqualityQuery() const
310 return d_eq_query
.get();
312 quantifiers::QModelBuilder
* QuantifiersEngine::getModelBuilder() const
314 return d_builder
.get();
316 quantifiers::QuantEPR
* QuantifiersEngine::getQuantEPR() const
320 quantifiers::FirstOrderModel
* QuantifiersEngine::getModel() const
322 return d_model
.get();
324 quantifiers::TermDb
* QuantifiersEngine::getTermDatabase() const
326 return d_term_db
.get();
328 quantifiers::TermDbSygus
* QuantifiersEngine::getTermDatabaseSygus() const
330 return d_sygus_tdb
.get();
332 quantifiers::TermUtil
* QuantifiersEngine::getTermUtil() const
334 return d_term_util
.get();
336 expr::TermCanonize
* QuantifiersEngine::getTermCanonize() const
338 return d_term_canon
.get();
340 quantifiers::QuantAttributes
* QuantifiersEngine::getQuantAttributes() const
342 return d_quant_attr
.get();
344 quantifiers::Instantiate
* QuantifiersEngine::getInstantiate() const
346 return d_instantiate
.get();
348 quantifiers::Skolemize
* QuantifiersEngine::getSkolemize() const
350 return d_skolemize
.get();
352 quantifiers::TermEnumeration
* QuantifiersEngine::getTermEnumeration() const
354 return d_term_enum
.get();
356 inst::TriggerTrie
* QuantifiersEngine::getTriggerDatabase() const
358 return d_tr_trie
.get();
361 QuantifiersModule
* QuantifiersEngine::getOwner( Node q
) {
362 std::map
< Node
, QuantifiersModule
* >::iterator it
= d_owner
.find( q
);
363 if( it
==d_owner
.end() ){
370 void QuantifiersEngine::setOwner( Node q
, QuantifiersModule
* m
, int priority
) {
371 QuantifiersModule
* mo
= getOwner( q
);
374 if( priority
<=d_owner_priority
[q
] ){
375 Trace("quant-warn") << "WARNING: setting owner of " << q
<< " to " << ( m
? m
->identify() : "null" ) << ", but already has owner " << mo
->identify() << " with higher priority!" << std::endl
;
380 d_owner_priority
[q
] = priority
;
384 void QuantifiersEngine::setOwner(Node q
, quantifiers::QAttributes
& qa
)
386 if (qa
.d_sygus
|| (options::sygusRecFun() && !qa
.d_fundef_f
.isNull()))
388 if (d_private
->d_synth_e
.get() == nullptr)
390 Trace("quant-warn") << "WARNING : synth engine is null, and we have : "
393 // set synth engine as owner since this is either a conjecture or a function
394 // definition to be used by sygus
395 setOwner(q
, d_private
->d_synth_e
.get(), 2);
399 bool QuantifiersEngine::hasOwnership( Node q
, QuantifiersModule
* m
) {
400 QuantifiersModule
* mo
= getOwner( q
);
401 return mo
==m
|| mo
==NULL
;
404 bool QuantifiersEngine::isFiniteBound(Node q
, Node v
) const
406 quantifiers::BoundedIntegers
* bi
= d_private
->d_bint
.get();
407 if (bi
&& bi
->isBound(q
, v
))
411 TypeNode tn
= v
.getType();
412 if (tn
.isSort() && options::finiteModelFind())
416 else if (d_term_enum
->mayComplete(tn
))
423 BoundVarType
QuantifiersEngine::getBoundVarType(Node q
, Node v
) const
425 quantifiers::BoundedIntegers
* bi
= d_private
->d_bint
.get();
428 return bi
->getBoundVarType(q
, v
);
430 return isFiniteBound(q
, v
) ? BOUND_FINITE
: BOUND_NONE
;
433 void QuantifiersEngine::getBoundVarIndices(Node q
,
434 std::vector
<unsigned>& indices
) const
436 Assert(indices
.empty());
437 // we take the bounded variables first
438 quantifiers::BoundedIntegers
* bi
= d_private
->d_bint
.get();
441 bi
->getBoundVarIndices(q
, indices
);
443 // then get the remaining ones
444 for (unsigned i
= 0, nvars
= q
[0].getNumChildren(); i
< nvars
; i
++)
446 if (std::find(indices
.begin(), indices
.end(), i
) == indices
.end())
448 indices
.push_back(i
);
453 bool QuantifiersEngine::getBoundElements(RepSetIterator
* rsi
,
457 std::vector
<Node
>& elements
) const
459 quantifiers::BoundedIntegers
* bi
= d_private
->d_bint
.get();
462 return bi
->getBoundElements(rsi
, initial
, q
, v
, elements
);
467 void QuantifiersEngine::presolve() {
468 Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl
;
469 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
470 d_modules
[i
]->presolve();
472 d_term_db
->presolve();
474 //add all terms to database
475 if( options::incrementalSolving() ){
476 Trace("quant-engine-proc") << "Add presolve cache " << d_presolve_cache
.size() << std::endl
;
477 for( unsigned i
=0; i
<d_presolve_cache
.size(); i
++ ){
478 addTermToDatabase( d_presolve_cache
[i
], d_presolve_cache_wq
[i
], d_presolve_cache_wic
[i
] );
480 Trace("quant-engine-proc") << "Done add presolve cache " << std::endl
;
484 void QuantifiersEngine::ppNotifyAssertions(
485 const std::vector
<Node
>& assertions
) {
486 Trace("quant-engine-proc")
487 << "ppNotifyAssertions in QE, #assertions = " << assertions
.size()
488 << " check epr = " << (d_qepr
!= NULL
) << std::endl
;
489 if (options::instLevelInputOnly() && options::instMaxLevel() != -1)
491 for (const Node
& a
: assertions
)
493 quantifiers::QuantAttributes::setInstantiationLevelAttr(a
, 0);
498 for (const Node
& a
: assertions
)
500 d_qepr
->registerAssertion(a
);
502 // must handle sources of other new constants e.g. separation logic
503 // FIXME (as part of project 3) : cleanup
504 sep::TheorySep
* theory_sep
=
505 static_cast<sep::TheorySep
*>(getTheoryEngine()->theoryOf(THEORY_SEP
));
506 theory_sep
->initializeBounds();
507 d_qepr
->finishInit();
509 if (options::sygus())
511 quantifiers::SynthEngine
* sye
= d_private
->d_synth_e
.get();
512 for (const Node
& a
: assertions
)
514 sye
->preregisterAssertion(a
);
519 void QuantifiersEngine::check( Theory::Effort e
){
520 CodeTimer
codeTimer(d_statistics
.d_time
);
522 if (!getMasterEqualityEngine()->consistent())
524 Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl
;
527 if (d_conflict_c
.get())
529 if (e
< Theory::EFFORT_LAST_CALL
)
531 // this can happen in rare cases when quantifiers is the first to realize
532 // there is a quantifier-free conflict, for example, when it discovers
533 // disequal and congruent terms in the master equality engine during
534 // term indexing. In such cases, quantifiers reports a "conflicting lemma"
535 // that is, one that is entailed to be false by the current assignment.
536 // If this lemma is not a SAT conflict, we may get another call to full
537 // effort check and the quantifier-free solvers still haven't realized
538 // there is a conflict. In this case, we return, trusting that theory
539 // combination will do the right thing (split on equalities until there is
540 // a conflict at the quantifier-free level).
541 Trace("quant-engine-debug")
542 << "Conflicting lemma already reported by quantifiers, return."
546 // we reported what we thought was a conflicting lemma, but now we have
547 // gotten a check at LAST_CALL effort, indicating that the lemma we reported
548 // was not conflicting. This should never happen, but in production mode, we
549 // proceed with the check.
552 bool needsCheck
= !d_lemmas_waiting
.empty();
553 QuantifiersModule::QEffort needsModelE
= QuantifiersModule::QEFFORT_NONE
;
554 std::vector
< QuantifiersModule
* > qm
;
555 if( d_model
->checkNeeded() ){
556 needsCheck
= needsCheck
|| e
>=Theory::EFFORT_LAST_CALL
; //always need to check at or above last call
557 for (QuantifiersModule
*& mdl
: d_modules
)
559 if (mdl
->needsCheck(e
))
563 //can only request model at last call since theory combination can find inconsistencies
564 if( e
>=Theory::EFFORT_LAST_CALL
){
565 QuantifiersModule::QEffort me
= mdl
->needsModel(e
);
566 needsModelE
= me
<needsModelE
? me
: needsModelE
;
573 d_hasAddedLemma
= false;
574 bool setIncomplete
= false;
576 Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e
<< ", needsCheck=" << needsCheck
<< std::endl
;
578 //flush previous lemmas (for instance, if was interrupted), or other lemmas to process
580 if( d_hasAddedLemma
){
585 if( Trace
.isOn("quant-engine") ){
586 clSet
= double(clock())/double(CLOCKS_PER_SEC
);
587 Trace("quant-engine") << ">>>>> Quantifiers Engine Round, effort = " << e
<< " <<<<<" << std::endl
;
590 if( Trace
.isOn("quant-engine-debug") ){
591 Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e
<< std::endl
;
592 Trace("quant-engine-debug") << " depth : " << d_ierCounter_c
<< std::endl
;
593 Trace("quant-engine-debug") << " modules to check : ";
594 for( unsigned i
=0; i
<qm
.size(); i
++ ){
595 Trace("quant-engine-debug") << qm
[i
]->identify() << " ";
597 Trace("quant-engine-debug") << std::endl
;
598 Trace("quant-engine-debug") << " # quantified formulas = " << d_model
->getNumAssertedQuantifiers() << std::endl
;
599 if( !d_lemmas_waiting
.empty() ){
600 Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting
.size() << std::endl
;
602 Trace("quant-engine-debug")
603 << " Theory engine finished : " << !theoryEngineNeedsCheck()
605 Trace("quant-engine-debug") << " Needs model effort : " << needsModelE
<< std::endl
;
606 Trace("quant-engine-debug")
607 << " In conflict : " << d_conflict
<< std::endl
;
609 if( Trace
.isOn("quant-engine-ee-pre") ){
610 Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl
;
611 debugPrintEqualityEngine( "quant-engine-ee-pre" );
613 if( Trace
.isOn("quant-engine-assert") ){
614 Trace("quant-engine-assert") << "Assertions : " << std::endl
;
615 getTheoryEngine()->printAssertions("quant-engine-assert");
619 Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl
;
620 for (QuantifiersUtil
*& util
: d_util
)
622 Trace("quant-engine-debug2") << "Reset " << util
->identify().c_str()
623 << "..." << std::endl
;
627 if( d_hasAddedLemma
){
630 //should only fail reset if added a lemma
636 if( Trace
.isOn("quant-engine-ee") ){
637 Trace("quant-engine-ee") << "Equality engine : " << std::endl
;
638 debugPrintEqualityEngine( "quant-engine-ee" );
642 Trace("quant-engine-debug") << "Reset model..." << std::endl
;
643 d_model
->reset_round();
646 Trace("quant-engine-debug") << "Resetting all modules..." << std::endl
;
647 for (QuantifiersModule
*& mdl
: d_modules
)
649 Trace("quant-engine-debug2") << "Reset " << mdl
->identify().c_str()
653 Trace("quant-engine-debug") << "Done resetting all modules." << std::endl
;
654 //reset may have added lemmas
656 if( d_hasAddedLemma
){
660 if( e
==Theory::EFFORT_LAST_CALL
){
661 ++(d_statistics
.d_instantiation_rounds_lc
);
662 }else if( e
==Theory::EFFORT_FULL
){
663 ++(d_statistics
.d_instantiation_rounds
);
665 Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl
;
666 for (unsigned qef
= QuantifiersModule::QEFFORT_CONFLICT
;
667 qef
<= QuantifiersModule::QEFFORT_LAST_CALL
;
670 QuantifiersModule::QEffort quant_e
=
671 static_cast<QuantifiersModule::QEffort
>(qef
);
672 d_curr_effort_level
= quant_e
;
673 // Force the theory engine to build the model if any module requested it.
674 if (needsModelE
== quant_e
)
676 Trace("quant-engine-debug") << "Build model..." << std::endl
;
677 if (!d_te
->buildModel())
679 // If we failed to build the model, flush all pending lemmas and
685 if( !d_hasAddedLemma
){
687 for (QuantifiersModule
*& mdl
: qm
)
689 Trace("quant-engine-debug") << "Check " << mdl
->identify().c_str()
690 << " at effort " << quant_e
<< "..."
692 mdl
->check(e
, quant_e
);
694 Trace("quant-engine-debug") << "...conflict!" << std::endl
;
698 //flush all current lemmas
701 //if we have added one, stop
702 if( d_hasAddedLemma
){
706 if (quant_e
== QuantifiersModule::QEFFORT_CONFLICT
)
708 if( e
==Theory::EFFORT_FULL
){
709 //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase
710 if( d_ierCounterLastLc
!=d_ierCounter_lc
|| !options::instWhenStrictInterleave() || d_ierCounter
%d_inst_when_phase
!=0 ){
711 d_ierCounter
= d_ierCounter
+ 1;
712 d_ierCounterLastLc
= d_ierCounter_lc
;
713 d_ierCounter_c
= d_ierCounter_c
.get() + 1;
715 }else if( e
==Theory::EFFORT_LAST_CALL
){
716 d_ierCounter_lc
= d_ierCounter_lc
+ 1;
719 else if (quant_e
== QuantifiersModule::QEFFORT_MODEL
)
721 if( e
==Theory::EFFORT_LAST_CALL
){
722 //sources of incompleteness
723 for (QuantifiersUtil
*& util
: d_util
)
725 if (!util
->checkComplete())
727 Trace("quant-engine-debug") << "Set incomplete because utility "
728 << util
->identify().c_str()
729 << " was incomplete." << std::endl
;
730 setIncomplete
= true;
733 if (d_conflict_c
.get())
735 // we reported a conflicting lemma, should return
736 setIncomplete
= true;
738 //if we have a chance not to set incomplete
739 if( !setIncomplete
){
740 //check if we should set the incomplete flag
741 for (QuantifiersModule
*& mdl
: d_modules
)
743 if (!mdl
->checkComplete())
745 Trace("quant-engine-debug")
746 << "Set incomplete because module "
747 << mdl
->identify().c_str() << " was incomplete."
749 setIncomplete
= true;
753 if( !setIncomplete
){
754 //look at individual quantified formulas, one module must claim completeness for each one
755 for( unsigned i
=0; i
<d_model
->getNumAssertedQuantifiers(); i
++ ){
756 bool hasCompleteM
= false;
757 Node q
= d_model
->getAssertedQuantifier( i
);
758 QuantifiersModule
* qmd
= getOwner( q
);
760 hasCompleteM
= qmd
->checkCompleteFor( q
);
762 for( unsigned j
=0; j
<d_modules
.size(); j
++ ){
763 if( d_modules
[j
]->checkCompleteFor( q
) ){
771 Trace("quant-engine-debug") << "Set incomplete because " << q
<< " was not fully processed." << std::endl
;
772 setIncomplete
= true;
776 Trace("quant-engine-debug2") << "Complete for " << q
<< " due to " << qmd
->identify().c_str() << std::endl
;
781 //if setIncomplete = false, we will answer SAT, otherwise we will run at quant_e QEFFORT_LAST_CALL
782 if( !setIncomplete
){
789 d_curr_effort_level
= QuantifiersModule::QEFFORT_NONE
;
790 Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl
;
794 bool debugInstTrace
= Trace
.isOn("inst-per-quant-round");
795 if (options::debugInst() || debugInstTrace
)
797 Options
& sopts
= smt::currentSmtEngine()->getOptions();
798 std::ostream
& out
= *sopts
.getOut();
799 d_instantiate
->debugPrint(out
);
802 if( Trace
.isOn("quant-engine") ){
803 double clSet2
= double(clock())/double(CLOCKS_PER_SEC
);
804 Trace("quant-engine") << "Finished quantifiers engine, total time = " << (clSet2
-clSet
);
805 Trace("quant-engine") << ", added lemma = " << d_hasAddedLemma
;
806 Trace("quant-engine") << std::endl
;
809 Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl
;
811 Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl
;
815 if( e
==Theory::EFFORT_LAST_CALL
&& !d_hasAddedLemma
){
817 Trace("quant-engine") << "Set incomplete flag." << std::endl
;
818 getOutputChannel().setIncomplete();
821 d_instantiate
->debugPrintModel();
825 void QuantifiersEngine::notifyCombineTheories() {
826 //if allowing theory combination to happen at most once between instantiation rounds
828 //d_ierCounterLastLc = -1;
831 bool QuantifiersEngine::reduceQuantifier( Node q
) {
832 //TODO: this can be unified with preregistration: AlphaEquivalence takes ownership of reducable quants
833 BoolMap::const_iterator it
= d_quants_red
.find( q
);
834 if( it
==d_quants_red
.end() ){
836 std::map
< Node
, Node
>::iterator itr
= d_quants_red_lem
.find( q
);
837 if( itr
==d_quants_red_lem
.end() ){
838 if (d_private
->d_alpha_equiv
)
840 Trace("quant-engine-red") << "Alpha equivalence " << q
<< "?" << std::endl
;
841 //add equivalence with another quantified formula
842 lem
= d_private
->d_alpha_equiv
->reduceQuantifier(q
);
844 Trace("quant-engine-red") << "...alpha equivalence success." << std::endl
;
845 ++(d_statistics
.d_red_alpha_equiv
);
848 d_quants_red_lem
[q
] = lem
;
853 getOutputChannel().lemma( lem
);
855 d_quants_red
[q
] = !lem
.isNull();
856 return !lem
.isNull();
862 void QuantifiersEngine::registerQuantifierInternal(Node f
)
864 std::map
< Node
, bool >::iterator it
= d_quants
.find( f
);
865 if( it
==d_quants
.end() ){
866 Trace("quant") << "QuantifiersEngine : Register quantifier ";
867 Trace("quant") << " : " << f
<< std::endl
;
868 unsigned prev_lemma_waiting
= d_lemmas_waiting
.size();
869 ++(d_statistics
.d_num_quant
);
870 Assert(f
.getKind() == FORALL
);
871 // register with utilities
872 for (unsigned i
= 0; i
< d_util
.size(); i
++)
874 d_util
[i
]->registerQuantifier(f
);
876 // compute attributes
877 d_quant_attr
->computeAttributes(f
);
879 for (QuantifiersModule
*& mdl
: d_modules
)
881 Trace("quant-debug") << "check ownership with " << mdl
->identify()
882 << "..." << std::endl
;
883 mdl
->checkOwnership(f
);
885 QuantifiersModule
* qm
= getOwner(f
);
886 Trace("quant") << " Owner : " << (qm
== nullptr ? "[none]" : qm
->identify())
888 // register with each module
889 for (QuantifiersModule
*& mdl
: d_modules
)
891 Trace("quant-debug") << "register with " << mdl
->identify() << "..."
893 mdl
->registerQuantifier(f
);
894 // since this is context-independent, we should not add any lemmas during
896 Assert(d_lemmas_waiting
.size() == prev_lemma_waiting
);
898 Trace("quant-debug") << "...finish." << std::endl
;
900 AlwaysAssert(d_lemmas_waiting
.size() == prev_lemma_waiting
);
904 void QuantifiersEngine::preRegisterQuantifier(Node q
)
906 NodeSet::const_iterator it
= d_quants_prereg
.find(q
);
907 if (it
!= d_quants_prereg
.end())
911 Trace("quant-debug") << "QuantifiersEngine : Pre-register " << q
<< std::endl
;
912 d_quants_prereg
.insert(q
);
914 if (reduceQuantifier(q
))
916 // if we can reduce it, nothing left to do
919 // ensure that it is registered
920 registerQuantifierInternal(q
);
921 // register with each module
922 for (QuantifiersModule
*& mdl
: d_modules
)
924 Trace("quant-debug") << "pre-register with " << mdl
->identify() << "..."
926 mdl
->preRegisterQuantifier(q
);
930 Trace("quant-debug") << "...finish pre-register " << q
<< "..." << std::endl
;
933 void QuantifiersEngine::registerPattern( std::vector
<Node
> & pattern
) {
934 for(std::vector
<Node
>::iterator p
= pattern
.begin(); p
!= pattern
.end(); ++p
){
935 std::set
< Node
> added
;
936 getTermDatabase()->addTerm( *p
, added
);
940 void QuantifiersEngine::assertQuantifier( Node f
, bool pol
){
941 if (reduceQuantifier(f
))
943 // if we can reduce it, nothing left to do
948 Node lem
= d_skolemize
->process(f
);
951 if (Trace
.isOn("quantifiers-sk-debug"))
953 Node slem
= Rewriter::rewrite(lem
);
954 Trace("quantifiers-sk-debug")
955 << "Skolemize lemma : " << slem
<< std::endl
;
957 getOutputChannel().lemma(
958 lem
, LemmaProperty::PREPROCESS
| LemmaProperty::NEEDS_JUSTIFY
);
962 // ensure the quantified formula is registered
963 registerQuantifierInternal(f
);
964 // assert it to each module
965 d_model
->assertQuantifier(f
);
966 for (QuantifiersModule
*& mdl
: d_modules
)
970 addTermToDatabase(d_term_util
->getInstConstantBody(f
), true);
973 void QuantifiersEngine::addTermToDatabase( Node n
, bool withinQuant
, bool withinInstClosure
){
974 if( options::incrementalSolving() ){
975 if( d_presolve_in
.find( n
)==d_presolve_in
.end() ){
976 d_presolve_in
.insert( n
);
977 d_presolve_cache
.push_back( n
);
978 d_presolve_cache_wq
.push_back( withinQuant
);
979 d_presolve_cache_wic
.push_back( withinInstClosure
);
982 //only wait if we are doing incremental solving
983 if( !d_presolve
|| !options::incrementalSolving() ){
984 std::set
< Node
> added
;
985 d_term_db
->addTerm(n
, added
, withinQuant
, withinInstClosure
);
989 if (d_sygus_tdb
&& options::sygusEvalUnfold())
991 d_sygus_tdb
->getEvalUnfold()->registerEvalTerm(n
);
997 void QuantifiersEngine::eqNotifyNewClass(TNode t
) {
998 addTermToDatabase( t
);
1001 bool QuantifiersEngine::addLemma( Node lem
, bool doCache
, bool doRewrite
){
1004 lem
= Rewriter::rewrite(lem
);
1006 Trace("inst-add-debug") << "Adding lemma : " << lem
<< std::endl
;
1007 BoolMap::const_iterator itp
= d_lemmas_produced_c
.find( lem
);
1008 if( itp
==d_lemmas_produced_c
.end() || !(*itp
).second
){
1009 d_lemmas_produced_c
[ lem
] = true;
1010 d_lemmas_waiting
.push_back( lem
);
1011 Trace("inst-add-debug") << "Added lemma" << std::endl
;
1014 Trace("inst-add-debug") << "Duplicate." << std::endl
;
1018 //do not need to rewrite, will be rewritten after sending
1019 d_lemmas_waiting
.push_back( lem
);
1024 bool QuantifiersEngine::removeLemma( Node lem
) {
1025 std::vector
< Node
>::iterator it
= std::find( d_lemmas_waiting
.begin(), d_lemmas_waiting
.end(), lem
);
1026 if( it
!=d_lemmas_waiting
.end() ){
1027 d_lemmas_waiting
.erase( it
, it
+ 1 );
1028 d_lemmas_produced_c
[ lem
] = false;
1035 void QuantifiersEngine::addRequirePhase( Node lit
, bool req
){
1036 d_phase_req_waiting
[lit
] = req
;
1039 void QuantifiersEngine::markRelevant( Node q
) {
1040 d_model
->markRelevant( q
);
1042 bool QuantifiersEngine::hasAddedLemma() const
1044 return !d_lemmas_waiting
.empty() || d_hasAddedLemma
;
1046 bool QuantifiersEngine::theoryEngineNeedsCheck() const
1048 return d_te
->needCheck();
1051 void QuantifiersEngine::setConflict()
1054 d_conflict_c
= true;
1057 bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e
) {
1058 Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter
<< ", " << d_ierCounter_lc
<< std::endl
;
1059 //determine if we should perform check, based on instWhenMode
1060 bool performCheck
= false;
1061 if (options::instWhenMode() == options::InstWhenMode::FULL
)
1063 performCheck
= ( e
>= Theory::EFFORT_FULL
);
1065 else if (options::instWhenMode() == options::InstWhenMode::FULL_DELAY
)
1067 performCheck
= (e
>= Theory::EFFORT_FULL
) && !theoryEngineNeedsCheck();
1069 else if (options::instWhenMode() == options::InstWhenMode::FULL_LAST_CALL
)
1071 performCheck
= ( ( e
==Theory::EFFORT_FULL
&& d_ierCounter
%d_inst_when_phase
!=0 ) || e
==Theory::EFFORT_LAST_CALL
);
1073 else if (options::instWhenMode()
1074 == options::InstWhenMode::FULL_DELAY_LAST_CALL
)
1076 performCheck
= ((e
== Theory::EFFORT_FULL
&& !theoryEngineNeedsCheck()
1077 && d_ierCounter
% d_inst_when_phase
!= 0)
1078 || e
== Theory::EFFORT_LAST_CALL
);
1080 else if (options::instWhenMode() == options::InstWhenMode::LAST_CALL
)
1082 performCheck
= ( e
>= Theory::EFFORT_LAST_CALL
);
1086 performCheck
= true;
1088 return performCheck
;
1091 options::UserPatMode
QuantifiersEngine::getInstUserPatMode()
1093 if (options::userPatternsQuant() == options::UserPatMode::INTERLEAVE
)
1095 return d_ierCounter
% 2 == 0 ? options::UserPatMode::USE
1096 : options::UserPatMode::RESORT
;
1100 return options::userPatternsQuant();
1104 void QuantifiersEngine::flushLemmas(){
1105 if( !d_lemmas_waiting
.empty() ){
1106 //take default output channel if none is provided
1107 d_hasAddedLemma
= true;
1108 for( unsigned i
=0; i
<d_lemmas_waiting
.size(); i
++ ){
1109 Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting
[i
] << std::endl
;
1110 getOutputChannel().lemma(d_lemmas_waiting
[i
], LemmaProperty::PREPROCESS
);
1112 d_lemmas_waiting
.clear();
1114 if( !d_phase_req_waiting
.empty() ){
1115 for( std::map
< Node
, bool >::iterator it
= d_phase_req_waiting
.begin(); it
!= d_phase_req_waiting
.end(); ++it
){
1116 Trace("qe-lemma") << "Require phase : " << it
->first
<< " -> " << it
->second
<< std::endl
;
1117 getOutputChannel().requirePhase( it
->first
, it
->second
);
1119 d_phase_req_waiting
.clear();
1123 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector
< Node
>& active_lemmas
) {
1124 return d_instantiate
->getUnsatCoreLemmas(active_lemmas
);
1127 void QuantifiersEngine::getInstantiationTermVectors( Node q
, std::vector
< std::vector
< Node
> >& tvecs
) {
1128 d_instantiate
->getInstantiationTermVectors(q
, tvecs
);
1131 void QuantifiersEngine::getInstantiationTermVectors( std::map
< Node
, std::vector
< std::vector
< Node
> > >& insts
) {
1132 d_instantiate
->getInstantiationTermVectors(insts
);
1135 void QuantifiersEngine::getExplanationForInstLemmas(
1136 const std::vector
<Node
>& lems
,
1137 std::map
<Node
, Node
>& quant
,
1138 std::map
<Node
, std::vector
<Node
> >& tvec
)
1140 d_instantiate
->getExplanationForInstLemmas(lems
, quant
, tvec
);
1143 void QuantifiersEngine::printInstantiations( std::ostream
& out
) {
1144 bool printed
= false;
1145 // print the skolemizations
1146 if (options::printInstMode() == options::PrintInstMode::LIST
)
1148 if (d_skolemize
->printSkolemization(out
))
1153 // print the instantiations
1154 if (d_instantiate
->printInstantiations(out
))
1159 out
<< "No instantiations" << std::endl
;
1163 void QuantifiersEngine::printSynthSolution( std::ostream
& out
) {
1164 if (d_private
->d_synth_e
)
1166 d_private
->d_synth_e
->printSynthSolution(out
);
1168 out
<< "Internal error : module for synth solution not found." << std::endl
;
1172 void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector
< Node
>& qs
) {
1173 d_instantiate
->getInstantiatedQuantifiedFormulas(qs
);
1176 void QuantifiersEngine::getInstantiations( std::map
< Node
, std::vector
< Node
> >& insts
) {
1177 d_instantiate
->getInstantiations(insts
);
1180 void QuantifiersEngine::getInstantiations( Node q
, std::vector
< Node
>& insts
) {
1181 d_instantiate
->getInstantiations(q
, insts
);
1184 Node
QuantifiersEngine::getInstantiatedConjunction( Node q
) {
1185 return d_instantiate
->getInstantiatedConjunction(q
);
1188 QuantifiersEngine::Statistics::Statistics()
1189 : d_time("theory::QuantifiersEngine::time"),
1190 d_qcf_time("theory::QuantifiersEngine::time_qcf"),
1191 d_ematching_time("theory::QuantifiersEngine::time_ematching"),
1192 d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
1193 d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
1194 d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
1195 d_triggers("QuantifiersEngine::Triggers", 0),
1196 d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
1197 d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
1198 d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
1199 d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0),
1200 d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0),
1201 d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0),
1202 d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0),
1203 d_instantiations_qcf("QuantifiersEngine::Instantiations_Qcf_Conflict", 0),
1204 d_instantiations_qcf_prop("QuantifiersEngine::Instantiations_Qcf_Prop", 0),
1205 d_instantiations_fmf_exh("QuantifiersEngine::Instantiations_Fmf_Exh", 0),
1206 d_instantiations_fmf_mbqi("QuantifiersEngine::Instantiations_Fmf_Mbqi", 0),
1207 d_instantiations_cbqi("QuantifiersEngine::Instantiations_Cbqi", 0),
1208 d_instantiations_rr("QuantifiersEngine::Instantiations_Rewrite_Rules", 0)
1210 smtStatisticsRegistry()->registerStat(&d_time
);
1211 smtStatisticsRegistry()->registerStat(&d_qcf_time
);
1212 smtStatisticsRegistry()->registerStat(&d_ematching_time
);
1213 smtStatisticsRegistry()->registerStat(&d_num_quant
);
1214 smtStatisticsRegistry()->registerStat(&d_instantiation_rounds
);
1215 smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc
);
1216 smtStatisticsRegistry()->registerStat(&d_triggers
);
1217 smtStatisticsRegistry()->registerStat(&d_simple_triggers
);
1218 smtStatisticsRegistry()->registerStat(&d_multi_triggers
);
1219 smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations
);
1220 smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv
);
1221 smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns
);
1222 smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen
);
1223 smtStatisticsRegistry()->registerStat(&d_instantiations_guess
);
1224 smtStatisticsRegistry()->registerStat(&d_instantiations_qcf
);
1225 smtStatisticsRegistry()->registerStat(&d_instantiations_qcf_prop
);
1226 smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_exh
);
1227 smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_mbqi
);
1228 smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi
);
1229 smtStatisticsRegistry()->registerStat(&d_instantiations_rr
);
1232 QuantifiersEngine::Statistics::~Statistics(){
1233 smtStatisticsRegistry()->unregisterStat(&d_time
);
1234 smtStatisticsRegistry()->unregisterStat(&d_qcf_time
);
1235 smtStatisticsRegistry()->unregisterStat(&d_ematching_time
);
1236 smtStatisticsRegistry()->unregisterStat(&d_num_quant
);
1237 smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds
);
1238 smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc
);
1239 smtStatisticsRegistry()->unregisterStat(&d_triggers
);
1240 smtStatisticsRegistry()->unregisterStat(&d_simple_triggers
);
1241 smtStatisticsRegistry()->unregisterStat(&d_multi_triggers
);
1242 smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations
);
1243 smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv
);
1244 smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns
);
1245 smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen
);
1246 smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess
);
1247 smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf
);
1248 smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf_prop
);
1249 smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_exh
);
1250 smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_mbqi
);
1251 smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi
);
1252 smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr
);
1255 eq::EqualityEngine
* QuantifiersEngine::getMasterEqualityEngine() const
1257 return d_masterEqualityEngine
;
1260 Node
QuantifiersEngine::getInternalRepresentative( Node a
, Node q
, int index
){
1261 return d_eq_query
->getInternalRepresentative(a
, q
, index
);
1264 bool QuantifiersEngine::getSynthSolutions(
1265 std::map
<Node
, std::map
<Node
, Node
> >& sol_map
)
1267 return d_private
->d_synth_e
->getSynthSolutions(sol_map
);
1270 void QuantifiersEngine::debugPrintEqualityEngine( const char * c
) {
1271 eq::EqualityEngine
* ee
= getMasterEqualityEngine();
1272 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( ee
);
1273 std::map
< TypeNode
, int > typ_num
;
1274 while( !eqcs_i
.isFinished() ){
1275 TNode r
= (*eqcs_i
);
1276 TypeNode tr
= r
.getType();
1277 if( typ_num
.find( tr
)==typ_num
.end() ){
1281 bool firstTime
= true;
1282 Trace(c
) << " " << r
;
1283 Trace(c
) << " : { ";
1284 eq::EqClassIterator eqc_i
= eq::EqClassIterator( r
, ee
);
1285 while( !eqc_i
.isFinished() ){
1289 Trace(c
) << std::endl
;
1292 Trace(c
) << " " << n
<< std::endl
;
1296 if( !firstTime
){ Trace(c
) << " "; }
1297 Trace(c
) << "}" << std::endl
;
1300 Trace(c
) << std::endl
;
1301 for( std::map
< TypeNode
, int >::iterator it
= typ_num
.begin(); it
!= typ_num
.end(); ++it
){
1302 Trace(c
) << "# eqc for " << it
->first
<< " : " << it
->second
<< std::endl
;
1306 } // namespace theory