1 /********************* */
2 /*! \file quantifiers_engine.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Tim King, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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/arrays/theory_arrays.h"
21 #include "theory/datatypes/theory_datatypes.h"
22 #include "theory/quantifiers/alpha_equivalence.h"
23 #include "theory/quantifiers/ambqi_builder.h"
24 #include "theory/quantifiers/anti_skolem.h"
25 #include "theory/quantifiers/bounded_integers.h"
26 #include "theory/quantifiers/ce_guided_instantiation.h"
27 #include "theory/quantifiers/ceg_t_instantiator.h"
28 #include "theory/quantifiers/conjecture_generator.h"
29 #include "theory/quantifiers/equality_infer.h"
30 #include "theory/quantifiers/equality_query.h"
31 #include "theory/quantifiers/first_order_model.h"
32 #include "theory/quantifiers/full_model_check.h"
33 #include "theory/quantifiers/fun_def_engine.h"
34 #include "theory/quantifiers/inst_propagator.h"
35 #include "theory/quantifiers/inst_strategy_cbqi.h"
36 #include "theory/quantifiers/inst_strategy_e_matching.h"
37 #include "theory/quantifiers/inst_strategy_enumerative.h"
38 #include "theory/quantifiers/instantiation_engine.h"
39 #include "theory/quantifiers/local_theory_ext.h"
40 #include "theory/quantifiers/model_engine.h"
41 #include "theory/quantifiers/quant_conflict_find.h"
42 #include "theory/quantifiers/quant_epr.h"
43 #include "theory/quantifiers/quant_equality_engine.h"
44 #include "theory/quantifiers/quant_relevance.h"
45 #include "theory/quantifiers/quant_split.h"
46 #include "theory/quantifiers/quantifiers_attributes.h"
47 #include "theory/quantifiers/quantifiers_rewriter.h"
48 #include "theory/quantifiers/relevant_domain.h"
49 #include "theory/quantifiers/rewrite_engine.h"
50 #include "theory/quantifiers/skolemize.h"
51 #include "theory/quantifiers/term_database.h"
52 #include "theory/quantifiers/term_database_sygus.h"
53 #include "theory/quantifiers/term_enumeration.h"
54 #include "theory/quantifiers/term_util.h"
55 #include "theory/quantifiers/trigger.h"
56 #include "theory/sep/theory_sep.h"
57 #include "theory/theory_engine.h"
58 #include "theory/uf/equality_engine.h"
59 #include "theory/uf/theory_uf.h"
60 #include "theory/uf/theory_uf_strong_solver.h"
64 using namespace CVC4::kind
;
65 using namespace CVC4::context
;
66 using namespace CVC4::theory
;
67 using namespace CVC4::theory::inst
;
69 QuantifiersEngine::QuantifiersEngine(context::Context
* c
,
70 context::UserContext
* u
,
73 d_quant_attr(new quantifiers::QuantAttributes(this)),
74 d_skolemize(new quantifiers::Skolemize(this, u
)),
75 d_term_enum(new quantifiers::TermEnumeration
),
76 d_conflict_c(c
, false),
79 d_lemmas_produced_c(u
),
82 // d_ierCounter_lc(c),
83 // d_ierCounterLastLc(c),
87 d_presolve_cache_wq(u
),
88 d_presolve_cache_wic(u
)
91 d_eq_query
= new quantifiers::EqualityQueryQuantifiersEngine( c
, this );
92 d_util
.push_back( d_eq_query
);
94 // term util must come first
95 d_term_util
= new quantifiers::TermUtil(this);
96 d_util
.push_back(d_term_util
);
98 d_term_db
= new quantifiers::TermDb( c
, u
, this );
99 d_util
.push_back( d_term_db
);
101 if (options::ceGuidedInst()) {
102 d_sygus_tdb
= new quantifiers::TermDbSygus(c
, this);
107 if( options::instPropagate() ){
108 // notice that this option is incompatible with options::qcfAllConflict()
109 d_inst_prop
= new quantifiers::InstPropagator( this );
110 d_util
.push_back( d_inst_prop
);
111 d_inst_notify
.push_back( d_inst_prop
->getInstantiationNotify() );
116 if( options::inferArithTriggerEq() ){
117 d_eq_inference
= new quantifiers::EqualityInference( c
, options::inferArithTriggerEqExp() );
119 d_eq_inference
= NULL
;
122 d_tr_trie
= new inst::TriggerTrie
;
123 d_curr_effort_level
= QuantifiersModule::QEFFORT_NONE
;
125 d_hasAddedLemma
= false;
126 d_useModelEe
= false;
127 //don't add true lemma
128 d_lemmas_produced_c
[d_term_util
->d_true
] = true;
130 Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl
;
131 Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl
;
133 if( options::relevantTriggers() ){
134 d_quant_rel
= new quantifiers::QuantRelevance(false);
135 d_util
.push_back(d_quant_rel
);
140 if( options::quantEpr() ){
141 Assert( !options::incrementalSolving() );
142 d_qepr
= new quantifiers::QuantEPR
;
150 d_inst_engine
= NULL
;
153 d_anti_skolem
= NULL
;
155 d_model_engine
= NULL
;
159 d_lte_part_inst
= NULL
;
160 d_alpha_equiv
= NULL
;
161 d_fun_def_engine
= NULL
;
168 d_total_inst_count_debug
= 0;
169 //allow theory combination to go first, once initially
170 d_ierCounter
= options::instWhenTcFirst() ? 0 : 1;
171 d_ierCounter_c
= d_ierCounter
;
173 d_ierCounterLastLc
= 0;
174 d_inst_when_phase
= 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
177 QuantifiersEngine::~QuantifiersEngine(){
178 for(std::map
< Node
, inst::CDInstMatchTrie
* >::iterator
179 i
= d_c_inst_match_trie
.begin(), iend
= d_c_inst_match_trie
.end();
184 d_c_inst_match_trie
.clear();
186 delete d_alpha_equiv
;
191 delete d_model_engine
;
192 delete d_inst_engine
;
202 delete d_eq_inference
;
206 delete d_lte_part_inst
;
207 delete d_fun_def_engine
;
212 delete d_anti_skolem
;
216 EqualityQuery
* QuantifiersEngine::getEqualityQuery() {
220 context::Context
* QuantifiersEngine::getSatContext(){
221 return d_te
->theoryOf( THEORY_QUANTIFIERS
)->getSatContext();
224 context::UserContext
* QuantifiersEngine::getUserContext(){
225 return d_te
->theoryOf( THEORY_QUANTIFIERS
)->getUserContext();
228 OutputChannel
& QuantifiersEngine::getOutputChannel(){
229 return d_te
->theoryOf( THEORY_QUANTIFIERS
)->getOutputChannel();
231 /** get default valuation for the quantifiers engine */
232 Valuation
& QuantifiersEngine::getValuation(){
233 return d_te
->theoryOf( THEORY_QUANTIFIERS
)->getValuation();
236 void QuantifiersEngine::finishInit(){
237 context::Context
* c
= getSatContext();
238 Trace("quant-engine-debug") << "QuantifiersEngine : finishInit " << std::endl
;
239 bool needsBuilder
= false;
240 bool needsRelDom
= false;
241 //add quantifiers modules
242 if( options::quantConflictFind() || options::quantRewriteRules() ){
243 d_qcf
= new quantifiers::QuantConflictFind( this, c
);
244 d_modules
.push_back( d_qcf
);
246 if( options::conjectureGen() ){
247 d_sg_gen
= new quantifiers::ConjectureGenerator( this, c
);
248 d_modules
.push_back( d_sg_gen
);
250 if( !options::finiteModelFind() || options::fmfInstEngine() ){
251 d_inst_engine
= new quantifiers::InstantiationEngine( this );
252 d_modules
.push_back( d_inst_engine
);
254 if( options::cbqi() ){
255 d_i_cbqi
= new quantifiers::InstStrategyCegqi( this );
256 d_modules
.push_back( d_i_cbqi
);
257 if( options::cbqiBv() ){
258 // if doing instantiation for BV, need the inverter class
259 d_bv_invert
= new quantifiers::BvInverter
;
262 if( options::ceGuidedInst() ){
263 d_ceg_inst
= new quantifiers::CegInstantiation( this, c
);
264 d_modules
.push_back( d_ceg_inst
);
265 //needsBuilder = true;
267 //finite model finding
268 if( options::finiteModelFind() ){
269 if( options::fmfBound() ){
270 d_bint
= new quantifiers::BoundedIntegers( c
, this );
271 d_modules
.push_back( d_bint
);
273 d_model_engine
= new quantifiers::ModelEngine( c
, this );
274 d_modules
.push_back( d_model_engine
);
275 //finite model finder has special ways of building the model
278 if( options::quantRewriteRules() ){
279 d_rr_engine
= new quantifiers::RewriteEngine( c
, this );
280 d_modules
.push_back(d_rr_engine
);
282 if( options::ltePartialInst() ){
283 d_lte_part_inst
= new quantifiers::LtePartialInst( this, c
);
284 d_modules
.push_back( d_lte_part_inst
);
286 if( options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE
){
287 d_qsplit
= new quantifiers::QuantDSplit( this, c
);
288 d_modules
.push_back( d_qsplit
);
290 if( options::quantAntiSkolem() ){
291 d_anti_skolem
= new quantifiers::QuantAntiSkolem( this );
292 d_modules
.push_back( d_anti_skolem
);
294 if( options::quantAlphaEquiv() ){
295 d_alpha_equiv
= new quantifiers::AlphaEquivalence( this );
297 //if( options::funDefs() ){
298 // d_fun_def_engine = new quantifiers::FunDefEngine( this, c );
299 // d_modules.push_back( d_fun_def_engine );
301 if( options::quantEqualityEngine() ){
302 d_uee
= new quantifiers::QuantEqualityEngine( this, c
);
303 d_modules
.push_back( d_uee
);
305 //full saturation : instantiate from relevant domain, then arbitrary terms
306 if( options::fullSaturateQuant() || options::fullSaturateInterleave() ){
307 d_fs
= new quantifiers::InstStrategyEnum(this);
308 d_modules
.push_back( d_fs
);
313 d_rel_dom
= new quantifiers::RelevantDomain( this );
314 d_util
.push_back( d_rel_dom
);
317 // if we require specialized ways of building the model
319 Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl
;
320 if( options::mbqiMode()==quantifiers::MBQI_FMC
|| options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL
||
321 options::mbqiMode()==quantifiers::MBQI_TRUST
|| options::fmfBound() ){
322 Trace("quant-engine-debug") << "...make fmc builder." << std::endl
;
323 d_model
= new quantifiers::fmcheck::FirstOrderModelFmc( this, c
, "FirstOrderModelFmc" );
324 d_builder
= new quantifiers::fmcheck::FullModelChecker( c
, this );
325 }else if( options::mbqiMode()==quantifiers::MBQI_ABS
){
326 Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl
;
327 d_model
= new quantifiers::FirstOrderModelAbs( this, c
, "FirstOrderModelAbs" );
328 d_builder
= new quantifiers::AbsMbqiBuilder( c
, this );
330 Trace("quant-engine-debug") << "...make default model builder." << std::endl
;
331 d_model
= new quantifiers::FirstOrderModelIG( this, c
, "FirstOrderModelIG" );
332 d_builder
= new quantifiers::QModelBuilderDefault( c
, this );
335 d_model
= new quantifiers::FirstOrderModelIG( this, c
, "FirstOrderModelIG" );
339 QuantifiersModule
* QuantifiersEngine::getOwner( Node q
) {
340 std::map
< Node
, QuantifiersModule
* >::iterator it
= d_owner
.find( q
);
341 if( it
==d_owner
.end() ){
348 void QuantifiersEngine::setOwner( Node q
, QuantifiersModule
* m
, int priority
) {
349 QuantifiersModule
* mo
= getOwner( q
);
352 if( priority
<=d_owner_priority
[q
] ){
353 Trace("quant-warn") << "WARNING: setting owner of " << q
<< " to " << ( m
? m
->identify() : "null" ) << ", but already has owner " << mo
->identify() << " with higher priority!" << std::endl
;
358 d_owner_priority
[q
] = priority
;
362 bool QuantifiersEngine::hasOwnership( Node q
, QuantifiersModule
* m
) {
363 QuantifiersModule
* mo
= getOwner( q
);
364 return mo
==m
|| mo
==NULL
;
367 bool QuantifiersEngine::isFiniteBound( Node q
, Node v
) {
368 if( getBoundedIntegers() && getBoundedIntegers()->isBoundVar( q
, v
) ){
371 TypeNode tn
= v
.getType();
372 if( tn
.isSort() && options::finiteModelFind() ){
375 else if (d_term_enum
->mayComplete(tn
))
383 void QuantifiersEngine::presolve() {
384 Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl
;
385 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
386 d_modules
[i
]->presolve();
388 d_term_db
->presolve();
390 //add all terms to database
391 if( options::incrementalSolving() ){
392 Trace("quant-engine-proc") << "Add presolve cache " << d_presolve_cache
.size() << std::endl
;
393 for( unsigned i
=0; i
<d_presolve_cache
.size(); i
++ ){
394 addTermToDatabase( d_presolve_cache
[i
], d_presolve_cache_wq
[i
], d_presolve_cache_wic
[i
] );
396 Trace("quant-engine-proc") << "Done add presolve cache " << std::endl
;
400 void QuantifiersEngine::ppNotifyAssertions(
401 const std::vector
<Node
>& assertions
) {
402 Trace("quant-engine-proc")
403 << "ppNotifyAssertions in QE, #assertions = " << assertions
.size()
404 << " check epr = " << (d_qepr
!= NULL
) << std::endl
;
405 if ((options::instLevelInputOnly() && options::instMaxLevel() != -1) ||
407 for (unsigned i
= 0; i
< assertions
.size(); i
++) {
408 if (options::instLevelInputOnly() && options::instMaxLevel() != -1) {
409 setInstantiationLevelAttr(assertions
[i
], 0);
411 if (d_qepr
!= NULL
) {
412 d_qepr
->registerAssertion(assertions
[i
]);
415 if (d_qepr
!= NULL
) {
416 // must handle sources of other new constants e.g. separation logic
418 sep::TheorySep
* theory_sep
=
419 static_cast<sep::TheorySep
*>(getTheoryEngine()->theoryOf(THEORY_SEP
));
420 theory_sep
->initializeBounds();
421 d_qepr
->finishInit();
426 void QuantifiersEngine::check( Theory::Effort e
){
427 CodeTimer
codeTimer(d_statistics
.d_time
);
428 d_useModelEe
= options::quantModelEe() && ( e
>=Theory::EFFORT_LAST_CALL
);
429 // if we want to use the model's equality engine, build the model now
430 if( d_useModelEe
&& !d_model
->isBuilt() ){
431 Trace("quant-engine-debug") << "Build the model." << std::endl
;
432 if( !d_te
->getModelBuilder()->buildModel( d_model
) ){
433 //we are done if model building was unsuccessful
435 if( d_hasAddedLemma
){
436 Trace("quant-engine-debug") << "...failed." << std::endl
;
442 if( !getActiveEqualityEngine()->consistent() ){
443 Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl
;
446 bool needsCheck
= !d_lemmas_waiting
.empty();
447 QuantifiersModule::QEffort needsModelE
= QuantifiersModule::QEFFORT_NONE
;
448 std::vector
< QuantifiersModule
* > qm
;
449 if( d_model
->checkNeeded() ){
450 needsCheck
= needsCheck
|| e
>=Theory::EFFORT_LAST_CALL
; //always need to check at or above last call
451 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
452 if( d_modules
[i
]->needsCheck( e
) ){
453 qm
.push_back( d_modules
[i
] );
455 //can only request model at last call since theory combination can find inconsistencies
456 if( e
>=Theory::EFFORT_LAST_CALL
){
457 QuantifiersModule::QEffort me
= d_modules
[i
]->needsModel(e
);
458 needsModelE
= me
<needsModelE
? me
: needsModelE
;
465 d_hasAddedLemma
= false;
466 bool setIncomplete
= false;
468 Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e
<< ", needsCheck=" << needsCheck
<< std::endl
;
470 //this will fail if a set of instances is marked as a conflict, but is not
471 Assert( !d_conflict_c
.get() );
472 //flush previous lemmas (for instance, if was interupted), or other lemmas to process
474 if( d_hasAddedLemma
){
477 if( !d_recorded_inst
.empty() ){
478 Trace("quant-engine-debug") << "Removing " << d_recorded_inst
.size() << " instantiations..." << std::endl
;
479 //remove explicitly recorded instantiations
480 for( unsigned i
=0; i
<d_recorded_inst
.size(); i
++ ){
481 removeInstantiationInternal( d_recorded_inst
[i
].first
, d_recorded_inst
[i
].second
);
483 d_recorded_inst
.clear();
487 if( Trace
.isOn("quant-engine") ){
488 clSet
= double(clock())/double(CLOCKS_PER_SEC
);
489 Trace("quant-engine") << ">>>>> Quantifiers Engine Round, effort = " << e
<< " <<<<<" << std::endl
;
492 if( Trace
.isOn("quant-engine-debug") ){
493 Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e
<< std::endl
;
494 Trace("quant-engine-debug") << " depth : " << d_ierCounter_c
<< std::endl
;
495 Trace("quant-engine-debug") << " modules to check : ";
496 for( unsigned i
=0; i
<qm
.size(); i
++ ){
497 Trace("quant-engine-debug") << qm
[i
]->identify() << " ";
499 Trace("quant-engine-debug") << std::endl
;
500 Trace("quant-engine-debug") << " # quantified formulas = " << d_model
->getNumAssertedQuantifiers() << std::endl
;
501 if( !d_lemmas_waiting
.empty() ){
502 Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting
.size() << std::endl
;
504 Trace("quant-engine-debug") << " Theory engine finished : " << !d_te
->needCheck() << std::endl
;
505 Trace("quant-engine-debug") << " Needs model effort : " << needsModelE
<< std::endl
;
507 if( Trace
.isOn("quant-engine-ee-pre") ){
508 Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl
;
509 debugPrintEqualityEngine( "quant-engine-ee-pre" );
511 if( Trace
.isOn("quant-engine-assert") ){
512 Trace("quant-engine-assert") << "Assertions : " << std::endl
;
513 getTheoryEngine()->printAssertions("quant-engine-assert");
517 Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl
;
518 for( unsigned i
=0; i
<d_util
.size(); i
++ ){
519 Trace("quant-engine-debug2") << "Reset " << d_util
[i
]->identify().c_str() << "..." << std::endl
;
520 if( !d_util
[i
]->reset( e
) ){
522 if( d_hasAddedLemma
){
525 //should only fail reset if added a lemma
531 if( Trace
.isOn("quant-engine-ee") ){
532 Trace("quant-engine-ee") << "Equality engine : " << std::endl
;
533 debugPrintEqualityEngine( "quant-engine-ee" );
537 Trace("quant-engine-debug") << "Reset model..." << std::endl
;
538 d_model
->reset_round();
541 Trace("quant-engine-debug") << "Resetting all modules..." << std::endl
;
542 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
543 Trace("quant-engine-debug2") << "Reset " << d_modules
[i
]->identify().c_str() << std::endl
;
544 d_modules
[i
]->reset_round( e
);
546 Trace("quant-engine-debug") << "Done resetting all modules." << std::endl
;
547 //reset may have added lemmas
549 if( d_hasAddedLemma
){
553 if( e
==Theory::EFFORT_LAST_CALL
){
554 //if effort is last call, try to minimize model first
555 //uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver();
556 //if( ufss && !ufss->minimize() ){ return; }
557 ++(d_statistics
.d_instantiation_rounds_lc
);
558 }else if( e
==Theory::EFFORT_FULL
){
559 ++(d_statistics
.d_instantiation_rounds
);
561 Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl
;
562 for (unsigned qef
= QuantifiersModule::QEFFORT_CONFLICT
;
563 qef
<= QuantifiersModule::QEFFORT_LAST_CALL
;
566 QuantifiersModule::QEffort quant_e
=
567 static_cast<QuantifiersModule::QEffort
>(qef
);
568 d_curr_effort_level
= quant_e
;
569 //build the model if any module requested it
570 if( needsModelE
==quant_e
&& !d_model
->isBuilt() ){
571 // theory engine's model builder is quantifier engine's builder if it has one
572 Assert( !d_builder
|| d_builder
==d_te
->getModelBuilder() );
573 Trace("quant-engine-debug") << "Build model..." << std::endl
;
574 if( !d_te
->getModelBuilder()->buildModel( d_model
) ){
575 //we are done if model building was unsuccessful
576 Trace("quant-engine-debug") << "...added lemmas." << std::endl
;
580 if( !d_hasAddedLemma
){
582 for( unsigned i
=0; i
<qm
.size(); i
++ ){
583 Trace("quant-engine-debug") << "Check " << qm
[i
]->identify().c_str() << " at effort " << quant_e
<< "..." << std::endl
;
584 qm
[i
]->check( e
, quant_e
);
586 Trace("quant-engine-debug") << "...conflict!" << std::endl
;
590 //flush all current lemmas
593 //if we have added one, stop
594 if( d_hasAddedLemma
){
597 Assert( !d_conflict
);
598 if (quant_e
== QuantifiersModule::QEFFORT_CONFLICT
)
600 if( e
==Theory::EFFORT_FULL
){
601 //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase
602 if( d_ierCounterLastLc
!=d_ierCounter_lc
|| !options::instWhenStrictInterleave() || d_ierCounter
%d_inst_when_phase
!=0 ){
603 d_ierCounter
= d_ierCounter
+ 1;
604 d_ierCounterLastLc
= d_ierCounter_lc
;
605 d_ierCounter_c
= d_ierCounter_c
.get() + 1;
607 }else if( e
==Theory::EFFORT_LAST_CALL
){
608 d_ierCounter_lc
= d_ierCounter_lc
+ 1;
611 else if (quant_e
== QuantifiersModule::QEFFORT_MODEL
)
613 if( e
==Theory::EFFORT_LAST_CALL
){
614 //sources of incompleteness
615 if( !d_recorded_inst
.empty() ){
616 Trace("quant-engine-debug") << "Set incomplete due to recorded instantiations." << std::endl
;
617 setIncomplete
= true;
619 //if we have a chance not to set incomplete
620 if( !setIncomplete
){
621 setIncomplete
= false;
622 //check if we should set the incomplete flag
623 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
624 if( !d_modules
[i
]->checkComplete() ){
625 Trace("quant-engine-debug") << "Set incomplete because " << d_modules
[i
]->identify().c_str() << " was incomplete." << std::endl
;
626 setIncomplete
= true;
630 if( !setIncomplete
){
631 //look at individual quantified formulas, one module must claim completeness for each one
632 for( unsigned i
=0; i
<d_model
->getNumAssertedQuantifiers(); i
++ ){
633 bool hasCompleteM
= false;
634 Node q
= d_model
->getAssertedQuantifier( i
);
635 QuantifiersModule
* qmd
= getOwner( q
);
637 hasCompleteM
= qmd
->checkCompleteFor( q
);
639 for( unsigned j
=0; j
<d_modules
.size(); j
++ ){
640 if( d_modules
[j
]->checkCompleteFor( q
) ){
648 Trace("quant-engine-debug") << "Set incomplete because " << q
<< " was not fully processed." << std::endl
;
649 setIncomplete
= true;
653 Trace("quant-engine-debug2") << "Complete for " << q
<< " due to " << qmd
->identify().c_str() << std::endl
;
658 //if setIncomplete = false, we will answer SAT, otherwise we will run at quant_e QEFFORT_LAST_CALL
659 if( !setIncomplete
){
666 d_curr_effort_level
= QuantifiersModule::QEFFORT_NONE
;
667 Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl
;
668 if( d_hasAddedLemma
){
670 if( Trace
.isOn("inst-per-quant-round") ){
671 for( std::map
< Node
, int >::iterator it
= d_temp_inst_debug
.begin(); it
!= d_temp_inst_debug
.end(); ++it
){
672 Trace("inst-per-quant-round") << " * " << it
->second
<< " for " << it
->first
<< std::endl
;
673 d_temp_inst_debug
[it
->first
] = 0;
677 if( Trace
.isOn("quant-engine") ){
678 double clSet2
= double(clock())/double(CLOCKS_PER_SEC
);
679 Trace("quant-engine") << "Finished quantifiers engine, total time = " << (clSet2
-clSet
);
680 Trace("quant-engine") << ", added lemma = " << d_hasAddedLemma
;
681 Trace("quant-engine") << std::endl
;
684 Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl
;
686 Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl
;
690 if( e
==Theory::EFFORT_LAST_CALL
&& !d_hasAddedLemma
){
691 if( options::produceModels() ){
692 if( d_model
->isBuilt() ){
693 Trace("quant-engine-debug") << "Already built model using model builder, finish..." << std::endl
;
695 //use default model builder when no module built the model
696 Trace("quant-engine-debug") << "Build the default model..." << std::endl
;
697 d_te
->getModelBuilder()->buildModel( d_model
);
698 Trace("quant-engine-debug") << "Done building the model." << std::endl
;
702 Trace("quant-engine") << "Set incomplete flag." << std::endl
;
703 getOutputChannel().setIncomplete();
706 if( Trace
.isOn("inst-per-quant") ){
707 for( std::map
< Node
, int >::iterator it
= d_total_inst_debug
.begin(); it
!= d_total_inst_debug
.end(); ++it
){
708 Trace("inst-per-quant") << " * " << it
->second
<< " for " << it
->first
<< std::endl
;
714 void QuantifiersEngine::notifyCombineTheories() {
715 //if allowing theory combination to happen at most once between instantiation rounds
717 //d_ierCounterLastLc = -1;
720 bool QuantifiersEngine::reduceQuantifier( Node q
) {
721 //TODO: this can be unified with preregistration: AlphaEquivalence takes ownership of reducable quants
722 BoolMap::const_iterator it
= d_quants_red
.find( q
);
723 if( it
==d_quants_red
.end() ){
725 std::map
< Node
, Node
>::iterator itr
= d_quants_red_lem
.find( q
);
726 if( itr
==d_quants_red_lem
.end() ){
728 Trace("quant-engine-red") << "Alpha equivalence " << q
<< "?" << std::endl
;
729 //add equivalence with another quantified formula
730 lem
= d_alpha_equiv
->reduceQuantifier( q
);
732 Trace("quant-engine-red") << "...alpha equivalence success." << std::endl
;
733 ++(d_statistics
.d_red_alpha_equiv
);
736 d_quants_red_lem
[q
] = lem
;
741 getOutputChannel().lemma( lem
);
743 d_quants_red
[q
] = !lem
.isNull();
744 return !lem
.isNull();
750 bool QuantifiersEngine::registerQuantifier( Node f
){
751 std::map
< Node
, bool >::iterator it
= d_quants
.find( f
);
752 if( it
==d_quants
.end() ){
753 Trace("quant") << "QuantifiersEngine : Register quantifier ";
754 Trace("quant") << " : " << f
<< std::endl
;
755 ++(d_statistics
.d_num_quant
);
756 Assert( f
.getKind()==FORALL
);
758 //check whether we should apply a reduction
759 if( reduceQuantifier( f
) ){
760 Trace("quant") << "...reduced." << std::endl
;
764 // register with utilities
765 for (unsigned i
= 0; i
< d_util
.size(); i
++)
767 d_util
[i
]->registerQuantifier(f
);
769 // compute attributes
770 d_quant_attr
->computeAttributes(f
);
772 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
773 Trace("quant-debug") << "pre-register with " << d_modules
[i
]->identify() << "..." << std::endl
;
774 d_modules
[i
]->preRegisterQuantifier( f
);
776 QuantifiersModule
* qm
= getOwner( f
);
778 Trace("quant") << " Owner : " << qm
->identify() << std::endl
;
780 //register with each module
781 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
782 Trace("quant-debug") << "register with " << d_modules
[i
]->identify() << "..." << std::endl
;
783 d_modules
[i
]->registerQuantifier( f
);
786 Node ceBody
= d_term_util
->getInstConstantBody( f
);
787 Trace("quant-debug") << "...finish." << std::endl
;
798 void QuantifiersEngine::registerPattern( std::vector
<Node
> & pattern
) {
799 for(std::vector
<Node
>::iterator p
= pattern
.begin(); p
!= pattern
.end(); ++p
){
800 std::set
< Node
> added
;
801 getTermDatabase()->addTerm( *p
, added
);
805 void QuantifiersEngine::assertQuantifier( Node f
, bool pol
){
808 if( !reduceQuantifier( f
) ){
810 Node lem
= d_skolemize
->process(f
);
813 if( Trace
.isOn("quantifiers-sk-debug") ){
814 Node slem
= Rewriter::rewrite( lem
);
815 Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem
<< std::endl
;
817 getOutputChannel().lemma( lem
, false, true );
821 //assert to modules TODO : also for !pol?
822 //register the quantifier, assert it to each module
823 if( registerQuantifier( f
) ){
824 d_model
->assertQuantifier( f
);
825 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
826 d_modules
[i
]->assertNode( f
);
828 addTermToDatabase( d_term_util
->getInstConstantBody( f
), true );
833 void QuantifiersEngine::propagate( Theory::Effort level
){
834 CodeTimer
codeTimer(d_statistics
.d_time
);
838 Node
QuantifiersEngine::getNextDecisionRequest( unsigned& priority
){
839 unsigned min_priority
= 0;
841 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
842 Node n
= d_modules
[i
]->getNextDecisionRequest( priority
);
843 if( !n
.isNull() && ( dec
.isNull() || priority
<min_priority
) ){
845 min_priority
= priority
;
851 void QuantifiersEngine::addTermToDatabase( Node n
, bool withinQuant
, bool withinInstClosure
){
852 if( options::incrementalSolving() ){
853 if( d_presolve_in
.find( n
)==d_presolve_in
.end() ){
854 d_presolve_in
.insert( n
);
855 d_presolve_cache
.push_back( n
);
856 d_presolve_cache_wq
.push_back( withinQuant
);
857 d_presolve_cache_wic
.push_back( withinInstClosure
);
860 //only wait if we are doing incremental solving
861 if( !d_presolve
|| !options::incrementalSolving() ){
862 std::set
< Node
> added
;
863 d_term_db
->addTerm(n
, added
, withinQuant
, withinInstClosure
);
869 d_sygus_tdb
->registerEvalTerm(n
);
872 // added contains also the Node that just have been asserted in this
876 for (std::set
<Node
>::iterator i
= added
.begin(), end
= added
.end();
880 d_quant_rel
->setRelevance( i
->getOperator(), 0 );
887 void QuantifiersEngine::eqNotifyNewClass(TNode t
) {
888 addTermToDatabase( t
);
889 if( d_eq_inference
){
890 d_eq_inference
->eqNotifyNewClass( t
);
894 void QuantifiersEngine::eqNotifyPreMerge(TNode t1
, TNode t2
) {
895 if( d_eq_inference
){
896 d_eq_inference
->eqNotifyMerge( t1
, t2
);
900 void QuantifiersEngine::eqNotifyPostMerge(TNode t1
, TNode t2
) {
904 void QuantifiersEngine::eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
) {
906 // d_qcf->assertDisequal( t1, t2 );
910 void QuantifiersEngine::computeTermVector( Node f
, InstMatch
& m
, std::vector
< Node
>& vars
, std::vector
< Node
>& terms
){
911 for( size_t i
=0; i
<f
[0].getNumChildren(); i
++ ){
914 vars
.push_back( f
[0][i
] );
915 terms
.push_back( n
);
921 bool QuantifiersEngine::recordInstantiationInternal( Node q
, std::vector
< Node
>& terms
, bool modEq
, bool addedLem
) {
923 //record the instantiation for deletion later
924 d_recorded_inst
.push_back( std::pair
< Node
, std::vector
< Node
> >( q
, terms
) );
926 if( options::incrementalSolving() ){
927 Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq
<< std::endl
;
928 inst::CDInstMatchTrie
* imt
;
929 std::map
< Node
, inst::CDInstMatchTrie
* >::iterator it
= d_c_inst_match_trie
.find( q
);
930 if( it
!=d_c_inst_match_trie
.end() ){
933 imt
= new CDInstMatchTrie( getUserContext() );
934 d_c_inst_match_trie
[q
] = imt
;
936 return imt
->addInstMatch( this, q
, terms
, getUserContext(), modEq
);
938 Trace("inst-add-debug") << "Adding into inst trie" << std::endl
;
939 return d_inst_match_trie
[q
].addInstMatch( this, q
, terms
, modEq
);
943 bool QuantifiersEngine::removeInstantiationInternal( Node q
, std::vector
< Node
>& terms
) {
944 if( options::incrementalSolving() ){
945 std::map
< Node
, inst::CDInstMatchTrie
* >::iterator it
= d_c_inst_match_trie
.find( q
);
946 if( it
!=d_c_inst_match_trie
.end() ){
947 return it
->second
->removeInstMatch( this, q
, terms
);
952 return d_inst_match_trie
[q
].removeInstMatch( this, q
, terms
);
956 void QuantifiersEngine::setInstantiationLevelAttr( Node n
, Node qn
, uint64_t level
){
957 Trace("inst-level-debug2") << "IL : " << n
<< " " << qn
<< " " << level
<< std::endl
;
958 //if not from the vector of terms we instantiatied
959 if( qn
.getKind()!=BOUND_VARIABLE
&& n
!=qn
){
960 //if this is a new term, without an instantiation level
961 if( !n
.hasAttribute(InstLevelAttribute()) ){
962 InstLevelAttribute ila
;
963 n
.setAttribute(ila
,level
);
964 Trace("inst-level-debug") << "Set instantiation level " << n
<< " to " << level
<< std::endl
;
965 Assert( n
.getNumChildren()==qn
.getNumChildren() );
966 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
967 setInstantiationLevelAttr( n
[i
], qn
[i
], level
);
973 void QuantifiersEngine::setInstantiationLevelAttr( Node n
, uint64_t level
){
974 if( !n
.hasAttribute(InstLevelAttribute()) ){
975 InstLevelAttribute ila
;
976 n
.setAttribute(ila
,level
);
977 Trace("inst-level-debug") << "Set instantiation level " << n
<< " to " << level
<< std::endl
;
978 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
979 setInstantiationLevelAttr( n
[i
], level
);
984 Node
QuantifiersEngine::getSubstitute( Node n
, std::vector
< Node
>& terms
, std::map
< Node
, Node
>& visited
){
985 std::map
< Node
, Node
>::iterator itv
= visited
.find( n
);
986 if( itv
==visited
.end() ){
988 if( n
.getKind()==INST_CONSTANT
){
989 Debug("check-inst") << "Substitute inst constant : " << n
<< std::endl
;
990 ret
= terms
[n
.getAttribute(InstVarNumAttribute())];
992 //if( !quantifiers::TermUtil::hasInstConstAttr( n ) ){
993 //Debug("check-inst") << "No inst const attr : " << n << std::endl;
996 //Debug("check-inst") << "Recurse on : " << n << std::endl;
997 std::vector
< Node
> cc
;
998 if( n
.getMetaKind() == kind::metakind::PARAMETERIZED
){
999 cc
.push_back( n
.getOperator() );
1001 bool changed
= false;
1002 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1003 Node c
= getSubstitute( n
[i
], terms
, visited
);
1005 changed
= changed
|| c
!=n
[i
];
1008 ret
= NodeManager::currentNM()->mkNode( n
.getKind(), cc
);
1019 Node
QuantifiersEngine::getInstantiation( Node q
, std::vector
< Node
>& vars
, std::vector
< Node
>& terms
, bool doVts
){
1021 Assert( vars
.size()==terms
.size() );
1022 //process partial instantiation if necessary
1023 if( q
[0].getNumChildren()!=vars
.size() ){
1024 body
= q
[ 1 ].substitute( vars
.begin(), vars
.end(), terms
.begin(), terms
.end() );
1025 std::vector
< Node
> uninst_vars
;
1026 //doing a partial instantiation, must add quantifier for all uninstantiated variables
1027 for( unsigned i
=0; i
<q
[0].getNumChildren(); i
++ ){
1028 if( std::find( vars
.begin(), vars
.end(), q
[0][i
] )==vars
.end() ){
1029 uninst_vars
.push_back( q
[0][i
] );
1032 Trace("partial-inst") << "Partially instantiating with " << vars
.size() << " / " << q
[0].getNumChildren() << " for " << q
<< std::endl
;
1033 Assert( !uninst_vars
.empty() );
1034 Node bvl
= NodeManager::currentNM()->mkNode( BOUND_VAR_LIST
, uninst_vars
);
1035 body
= NodeManager::currentNM()->mkNode( FORALL
, bvl
, body
);
1036 Trace("partial-inst") << "Partial instantiation : " << q
<< std::endl
;
1037 Trace("partial-inst") << " : " << body
<< std::endl
;
1039 if( options::cbqi() ){
1040 body
= q
[ 1 ].substitute( vars
.begin(), vars
.end(), terms
.begin(), terms
.end() );
1042 //do optimized version
1043 Node icb
= d_term_util
->getInstConstantBody( q
);
1044 std::map
< Node
, Node
> visited
;
1045 body
= getSubstitute( icb
, terms
, visited
);
1046 if( Debug
.isOn("check-inst") ){
1047 Node body2
= q
[ 1 ].substitute( vars
.begin(), vars
.end(), terms
.begin(), terms
.end() );
1049 Debug("check-inst") << "Substitution is wrong : " << body
<< " " << body2
<< std::endl
;
1055 //do virtual term substitution
1056 body
= Rewriter::rewrite( body
);
1057 Trace("quant-vts-debug") << "Rewrite vts symbols in " << body
<< std::endl
;
1058 Node body_r
= d_term_util
->rewriteVtsSymbols( body
);
1059 Trace("quant-vts-debug") << " ...result: " << body_r
<< std::endl
;
1065 Node
QuantifiersEngine::getInstantiation( Node q
, InstMatch
& m
, bool doVts
){
1066 std::vector
< Node
> vars
;
1067 std::vector
< Node
> terms
;
1068 computeTermVector( q
, m
, vars
, terms
);
1069 return getInstantiation( q
, vars
, terms
, doVts
);
1072 Node
QuantifiersEngine::getInstantiation( Node q
, std::vector
< Node
>& terms
, bool doVts
) {
1073 Assert( d_term_util
->d_vars
.find( q
)!=d_term_util
->d_vars
.end() );
1074 return getInstantiation( q
, d_term_util
->d_vars
[q
], terms
, doVts
);
1078 bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq ){
1079 if( options::incrementalSolving() ){
1080 if( d_c_inst_match_trie.find( f )!=d_c_inst_match_trie.end() ){
1081 if( d_c_inst_match_trie[f]->existsInstMatch( this, f, m, getUserContext(), modEq ) ){
1086 if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){
1087 if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq ) ){
1096 bool QuantifiersEngine::addLemma( Node lem
, bool doCache
, bool doRewrite
){
1099 lem
= Rewriter::rewrite(lem
);
1101 Trace("inst-add-debug") << "Adding lemma : " << lem
<< std::endl
;
1102 BoolMap::const_iterator itp
= d_lemmas_produced_c
.find( lem
);
1103 if( itp
==d_lemmas_produced_c
.end() || !(*itp
).second
){
1104 //d_curr_out->lemma( lem, false, true );
1105 d_lemmas_produced_c
[ lem
] = true;
1106 d_lemmas_waiting
.push_back( lem
);
1107 Trace("inst-add-debug") << "Added lemma" << std::endl
;
1110 Trace("inst-add-debug") << "Duplicate." << std::endl
;
1114 //do not need to rewrite, will be rewritten after sending
1115 d_lemmas_waiting
.push_back( lem
);
1120 bool QuantifiersEngine::removeLemma( Node lem
) {
1121 std::vector
< Node
>::iterator it
= std::find( d_lemmas_waiting
.begin(), d_lemmas_waiting
.end(), lem
);
1122 if( it
!=d_lemmas_waiting
.end() ){
1123 d_lemmas_waiting
.erase( it
, it
+ 1 );
1124 d_lemmas_produced_c
[ lem
] = false;
1131 void QuantifiersEngine::addRequirePhase( Node lit
, bool req
){
1132 d_phase_req_waiting
[lit
] = req
;
1135 bool QuantifiersEngine::addInstantiation( Node q
, InstMatch
& m
, bool mkRep
, bool modEq
, bool doVts
){
1136 std::vector
< Node
> terms
;
1137 m
.getTerms( q
, terms
);
1138 return addInstantiation( q
, terms
, mkRep
, modEq
, doVts
);
1141 bool QuantifiersEngine::addInstantiation( Node q
, std::vector
< Node
>& terms
, bool mkRep
, bool modEq
, bool doVts
) {
1142 // For resource-limiting (also does a time check).
1143 getOutputChannel().safePoint(options::quantifierStep());
1144 Assert( !d_conflict
);
1145 Assert( terms
.size()==q
[0].getNumChildren() );
1146 Trace("inst-add-debug") << "For quantified formula " << q
<< ", add instantiation: " << std::endl
;
1147 std::vector
< Node
> rlv_cond
;
1148 for( unsigned i
=0; i
<terms
.size(); i
++ ){
1149 Trace("inst-add-debug") << " " << q
[0][i
];
1150 Trace("inst-add-debug2") << " -> " << terms
[i
];
1151 TypeNode tn
= q
[0][i
].getType();
1152 if( terms
[i
].isNull() ){
1153 terms
[i
] = getTermForType(tn
);
1156 //pick the best possible representative for instantiation, based on past use and simplicity of term
1157 terms
[i
] = getInternalRepresentative( terms
[i
], q
, i
);
1159 //ensure the type is correct
1160 terms
[i
] = quantifiers::TermUtil::ensureType(terms
[i
], tn
);
1162 Trace("inst-add-debug") << " -> " << terms
[i
] << std::endl
;
1163 if( terms
[i
].isNull() ){
1164 Trace("inst-add-debug") << " --> Failed to make term vector, due to term/type restrictions." << std::endl
;
1167 //get relevancy conditions
1168 if( options::instRelevantCond() ){
1169 quantifiers::TermUtil::getRelevancyCondition( terms
[i
], rlv_cond
);
1172 #ifdef CVC4_ASSERTIONS
1173 bool bad_inst
= false;
1174 if( quantifiers::TermUtil::containsUninterpretedConstant( terms
[i
] ) ){
1175 Trace("inst") << "***& inst contains uninterpreted constant : " << terms
[i
] << std::endl
;
1177 }else if( !terms
[i
].getType().isSubtypeOf( q
[0][i
].getType() ) ){
1178 Trace("inst") << "***& inst bad type : " << terms
[i
] << " " << terms
[i
].getType() << "/" << q
[0][i
].getType() << std::endl
;
1180 }else if( options::cbqi() ){
1181 Node icf
= quantifiers::TermUtil::getInstConstAttr(terms
[i
]);
1182 if( !icf
.isNull() ){
1184 Trace("inst") << "***& inst contains inst constant attr : " << terms
[i
] << std::endl
;
1186 }else if( quantifiers::TermUtil::containsTerms( terms
[i
], d_term_util
->d_inst_constants
[q
] ) ){
1187 Trace("inst") << "***& inst contains inst constants : " << terms
[i
] << std::endl
;
1192 //this assertion is critical to soundness
1194 Trace("inst")<< "***& Bad Instantiate " << q
<< " with " << std::endl
;
1195 for( unsigned j
=0; j
<terms
.size(); j
++ ){
1196 Trace("inst") << " " << terms
[j
] << std::endl
;
1203 //check based on instantiation level
1204 if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
1205 for( unsigned i
=0; i
<terms
.size(); i
++ ){
1206 if( !d_term_db
->isTermEligibleForInstantiation( terms
[i
], q
, true ) ){
1212 //check for positive entailment
1213 if( options::instNoEntail() ){
1214 //TODO: check consistency of equality engine (if not aborting on utility's reset)
1215 std::map
< TNode
, TNode
> subs
;
1216 for( unsigned i
=0; i
<terms
.size(); i
++ ){
1217 subs
[q
[0][i
]] = terms
[i
];
1219 if( d_term_db
->isEntailed( q
[1], subs
, false, true ) ){
1220 Trace("inst-add-debug") << " --> Currently entailed." << std::endl
;
1221 ++(d_statistics
.d_inst_duplicate_ent
);
1224 //Node eval = d_term_db->evaluateTerm( q[1], subs, false, true );
1225 //Trace("inst-add-debug2") << "Instantiation evaluates to : " << std::endl;
1226 //Trace("inst-add-debug2") << " " << eval << std::endl;
1229 //check for term vector duplication
1230 bool alreadyExists
= !recordInstantiationInternal( q
, terms
, modEq
);
1231 if( alreadyExists
){
1232 Trace("inst-add-debug") << " --> Already exists." << std::endl
;
1233 ++(d_statistics
.d_inst_duplicate_eq
);
1237 //construct the instantiation
1238 Trace("inst-add-debug") << "Constructing instantiation..." << std::endl
;
1239 Assert( d_term_util
->d_vars
[q
].size()==terms
.size() );
1240 Node body
= getInstantiation( q
, d_term_util
->d_vars
[q
], terms
, doVts
); //do virtual term substitution
1241 Node orig_body
= body
;
1242 if( options::cbqiNestedQE() && d_i_cbqi
){
1243 body
= d_i_cbqi
->doNestedQE( q
, terms
, body
, doVts
);
1245 body
= quantifiers::QuantifiersRewriter::preprocess( body
, true );
1246 Trace("inst-debug") << "...preprocess to " << body
<< std::endl
;
1248 //construct the lemma
1249 Trace("inst-assert") << "(assert " << body
<< ")" << std::endl
;
1250 body
= Rewriter::rewrite(body
);
1252 if( d_useModelEe
&& options::instNoModelTrue() ){
1253 Node val_body
= d_model
->getValue( body
);
1254 if( val_body
==d_term_util
->d_true
){
1255 Trace("inst-add-debug") << " --> True in model." << std::endl
;
1256 ++(d_statistics
.d_inst_duplicate_model_true
);
1262 if( rlv_cond
.empty() ){
1263 lem
= NodeManager::currentNM()->mkNode( kind::OR
, q
.negate(), body
);
1265 rlv_cond
.push_back( q
.negate() );
1266 rlv_cond
.push_back( body
);
1267 lem
= NodeManager::currentNM()->mkNode( kind::OR
, rlv_cond
);
1269 lem
= Rewriter::rewrite(lem
);
1271 //check for lemma duplication
1272 if( addLemma( lem
, true, false ) ){
1273 d_total_inst_debug
[q
]++;
1274 d_temp_inst_debug
[q
]++;
1275 d_total_inst_count_debug
++;
1276 if( Trace
.isOn("inst") ){
1277 Trace("inst") << "*** Instantiate " << q
<< " with " << std::endl
;
1278 for( unsigned i
=0; i
<terms
.size(); i
++ ){
1279 if( Trace
.isOn("inst") ){
1280 Trace("inst") << " " << terms
[i
];
1281 if( Trace
.isOn("inst-debug") ){
1282 Trace("inst-debug") << ", type=" << terms
[i
].getType() << ", var_type=" << q
[0][i
].getType();
1284 Trace("inst") << std::endl
;
1288 if( options::instMaxLevel()!=-1 ){
1290 //virtual term substitution/instantiation level features are incompatible
1293 uint64_t maxInstLevel
= 0;
1294 for( unsigned i
=0; i
<terms
.size(); i
++ ){
1295 if( terms
[i
].hasAttribute(InstLevelAttribute()) ){
1296 if( terms
[i
].getAttribute(InstLevelAttribute())>maxInstLevel
){
1297 maxInstLevel
= terms
[i
].getAttribute(InstLevelAttribute());
1301 setInstantiationLevelAttr( orig_body
, q
[1], maxInstLevel
+1 );
1304 if (d_curr_effort_level
> QuantifiersModule::QEFFORT_CONFLICT
1305 && d_curr_effort_level
< QuantifiersModule::QEFFORT_NONE
)
1308 for( unsigned j
=0; j
<d_inst_notify
.size(); j
++ ){
1309 if( !d_inst_notify
[j
]->notifyInstantiation( d_curr_effort_level
, q
, lem
, terms
, body
) ){
1310 Trace("inst-add-debug") << "...we are in conflict." << std::endl
;
1312 Assert( !d_lemmas_waiting
.empty() );
1317 if( options::trackInstLemmas() ){
1319 if( options::incrementalSolving() ){
1320 recorded
= d_c_inst_match_trie
[q
]->recordInstLemma( q
, terms
, lem
);
1322 recorded
= d_inst_match_trie
[q
].recordInstLemma( q
, terms
, lem
);
1324 Trace("inst-add-debug") << "...was recorded : " << recorded
<< std::endl
;
1327 Trace("inst-add-debug") << " --> Success." << std::endl
;
1328 ++(d_statistics
.d_instantiations
);
1331 Trace("inst-add-debug") << " --> Lemma already exists." << std::endl
;
1332 ++(d_statistics
.d_inst_duplicate
);
1337 bool QuantifiersEngine::removeInstantiation( Node q
, Node lem
, std::vector
< Node
>& terms
) {
1338 //lem must occur in d_waiting_lemmas
1339 if( removeLemma( lem
) ){
1340 return removeInstantiationInternal( q
, terms
);
1346 bool QuantifiersEngine::addSplit( Node n
, bool reqPhase
, bool reqPhasePol
){
1347 n
= Rewriter::rewrite( n
);
1348 Node lem
= NodeManager::currentNM()->mkNode( OR
, n
, n
.notNode() );
1349 if( addLemma( lem
) ){
1350 Debug("inst") << "*** Add split " << n
<< std::endl
;
1356 bool QuantifiersEngine::addSplitEquality( Node n1
, Node n2
, bool reqPhase
, bool reqPhasePol
){
1357 //Assert( !areEqual( n1, n2 ) );
1358 //Assert( !areDisequal( n1, n2 ) );
1359 Node fm
= NodeManager::currentNM()->mkNode( EQUAL
, n1
, n2
);
1360 return addSplit( fm
);
1363 bool QuantifiersEngine::addEPRAxiom( TypeNode tn
) {
1365 Assert( !options::incrementalSolving() );
1366 if( d_qepr
->isEPR( tn
) && !d_qepr
->hasEPRAxiom( tn
) ){
1367 Node lem
= d_qepr
->mkEPRAxiom( tn
);
1368 Trace("quant-epr") << "EPR lemma for " << tn
<< " : " << lem
<< std::endl
;
1369 getOutputChannel().lemma( lem
);
1375 void QuantifiersEngine::markRelevant( Node q
) {
1376 d_model
->markRelevant( q
);
1379 void QuantifiersEngine::setConflict() {
1381 d_conflict_c
= true;
1384 bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e
) {
1385 Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter
<< ", " << d_ierCounter_lc
<< std::endl
;
1386 //determine if we should perform check, based on instWhenMode
1387 bool performCheck
= false;
1388 if( options::instWhenMode()==quantifiers::INST_WHEN_FULL
){
1389 performCheck
= ( e
>= Theory::EFFORT_FULL
);
1390 }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY
){
1391 performCheck
= ( e
>= Theory::EFFORT_FULL
) && !getTheoryEngine()->needCheck();
1392 }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL
){
1393 performCheck
= ( ( e
==Theory::EFFORT_FULL
&& d_ierCounter
%d_inst_when_phase
!=0 ) || e
==Theory::EFFORT_LAST_CALL
);
1394 }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL
){
1395 performCheck
= ( ( e
==Theory::EFFORT_FULL
&& !getTheoryEngine()->needCheck() && d_ierCounter
%d_inst_when_phase
!=0 ) || e
==Theory::EFFORT_LAST_CALL
);
1396 }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL
){
1397 performCheck
= ( e
>= Theory::EFFORT_LAST_CALL
);
1399 performCheck
= true;
1401 if( e
==Theory::EFFORT_LAST_CALL
){
1402 //with bounded integers, skip every other last call,
1403 // since matching loops may occur with infinite quantification
1404 if( d_ierCounter_lc
%2==0 && options::fmfBound() ){
1405 performCheck
= false;
1408 return performCheck
;
1411 quantifiers::UserPatMode
QuantifiersEngine::getInstUserPatMode() {
1412 if( options::userPatternsQuant()==quantifiers::USER_PAT_MODE_INTERLEAVE
){
1413 return d_ierCounter
%2==0 ? quantifiers::USER_PAT_MODE_USE
: quantifiers::USER_PAT_MODE_RESORT
;
1415 return options::userPatternsQuant();
1419 void QuantifiersEngine::flushLemmas(){
1420 if( !d_lemmas_waiting
.empty() ){
1421 //filter based on notify classes
1422 if( !d_inst_notify
.empty() ){
1423 unsigned prev_lem_sz
= d_lemmas_waiting
.size();
1424 for( unsigned j
=0; j
<d_inst_notify
.size(); j
++ ){
1425 d_inst_notify
[j
]->filterInstantiations();
1427 if( prev_lem_sz
!=d_lemmas_waiting
.size() ){
1428 Trace("quant-engine") << "...filtered instances : " << d_lemmas_waiting
.size() << " / " << prev_lem_sz
<< std::endl
;
1431 //take default output channel if none is provided
1432 d_hasAddedLemma
= true;
1433 for( unsigned i
=0; i
<d_lemmas_waiting
.size(); i
++ ){
1434 Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting
[i
] << std::endl
;
1435 getOutputChannel().lemma( d_lemmas_waiting
[i
], false, true );
1437 d_lemmas_waiting
.clear();
1439 if( !d_phase_req_waiting
.empty() ){
1440 for( std::map
< Node
, bool >::iterator it
= d_phase_req_waiting
.begin(); it
!= d_phase_req_waiting
.end(); ++it
){
1441 Trace("qe-lemma") << "Require phase : " << it
->first
<< " -> " << it
->second
<< std::endl
;
1442 getOutputChannel().requirePhase( it
->first
, it
->second
);
1444 d_phase_req_waiting
.clear();
1448 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector
< Node
>& active_lemmas
) {
1449 //only if unsat core available
1450 bool isUnsatCoreAvailable
= false;
1451 if( options::proof() ){
1452 isUnsatCoreAvailable
= ProofManager::currentPM()->unsatCoreAvailable();
1454 if( isUnsatCoreAvailable
){
1455 Trace("inst-unsat-core") << "Get instantiations in unsat core..." << std::endl
;
1456 ProofManager::currentPM()->getLemmasInUnsatCore(theory::THEORY_QUANTIFIERS
, active_lemmas
);
1457 if( Trace
.isOn("inst-unsat-core") ){
1458 Trace("inst-unsat-core") << "Quantifiers lemmas in unsat core: " << std::endl
;
1459 for (unsigned i
= 0; i
< active_lemmas
.size(); ++i
) {
1460 Trace("inst-unsat-core") << " " << active_lemmas
[i
] << std::endl
;
1462 Trace("inst-unsat-core") << std::endl
;
1470 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector
< Node
>& active_lemmas
, std::map
< Node
, Node
>& weak_imp
) {
1471 if( getUnsatCoreLemmas( active_lemmas
) ){
1472 for (unsigned i
= 0; i
< active_lemmas
.size(); ++i
) {
1473 Node n
= ProofManager::currentPM()->getWeakestImplicantInUnsatCore(active_lemmas
[i
]);
1474 if( n
!=active_lemmas
[i
] ){
1475 Trace("inst-unsat-core") << " weaken : " << active_lemmas
[i
] << " -> " << n
<< std::endl
;
1477 weak_imp
[active_lemmas
[i
]] = n
;
1485 void QuantifiersEngine::getInstantiationTermVectors( Node q
, std::vector
< std::vector
< Node
> >& tvecs
) {
1486 std::vector
< Node
> lemmas
;
1487 getInstantiations( q
, lemmas
);
1488 std::map
< Node
, Node
> quant
;
1489 std::map
< Node
, std::vector
< Node
> > tvec
;
1490 getExplanationForInstLemmas( lemmas
, quant
, tvec
);
1491 for( std::map
< Node
, std::vector
< Node
> >::iterator it
= tvec
.begin(); it
!= tvec
.end(); ++it
){
1492 tvecs
.push_back( it
->second
);
1496 void QuantifiersEngine::getInstantiationTermVectors( std::map
< Node
, std::vector
< std::vector
< Node
> > >& insts
) {
1497 if( options::incrementalSolving() ){
1498 for( std::map
< Node
, inst::CDInstMatchTrie
* >::iterator it
= d_c_inst_match_trie
.begin(); it
!= d_c_inst_match_trie
.end(); ++it
){
1499 getInstantiationTermVectors( it
->first
, insts
[it
->first
] );
1502 for( std::map
< Node
, inst::InstMatchTrie
>::iterator it
= d_inst_match_trie
.begin(); it
!= d_inst_match_trie
.end(); ++it
){
1503 getInstantiationTermVectors( it
->first
, insts
[it
->first
] );
1508 void QuantifiersEngine::getExplanationForInstLemmas( std::vector
< Node
>& lems
, std::map
< Node
, Node
>& quant
, std::map
< Node
, std::vector
< Node
> >& tvec
) {
1509 if( options::trackInstLemmas() ){
1510 if( options::incrementalSolving() ){
1511 for( std::map
< Node
, inst::CDInstMatchTrie
* >::iterator it
= d_c_inst_match_trie
.begin(); it
!= d_c_inst_match_trie
.end(); ++it
){
1512 it
->second
->getExplanationForInstLemmas( it
->first
, lems
, quant
, tvec
);
1515 for( std::map
< Node
, inst::InstMatchTrie
>::iterator it
= d_inst_match_trie
.begin(); it
!= d_inst_match_trie
.end(); ++it
){
1516 it
->second
.getExplanationForInstLemmas( it
->first
, lems
, quant
, tvec
);
1519 #ifdef CVC4_ASSERTIONS
1520 for( unsigned j
=0; j
<lems
.size(); j
++ ){
1521 Assert( quant
.find( lems
[j
] )!=quant
.end() );
1522 Assert( tvec
.find( lems
[j
] )!=tvec
.end() );
1530 void QuantifiersEngine::printInstantiations( std::ostream
& out
) {
1531 bool useUnsatCore
= false;
1532 std::vector
< Node
> active_lemmas
;
1533 if( options::trackInstLemmas() && getUnsatCoreLemmas( active_lemmas
) ){
1534 useUnsatCore
= true;
1537 bool printed
= false;
1538 // print the skolemizations
1539 if (d_skolemize
->printSkolemization(out
))
1543 // print the instantiations
1544 if( options::incrementalSolving() ){
1545 for( std::map
< Node
, inst::CDInstMatchTrie
* >::iterator it
= d_c_inst_match_trie
.begin(); it
!= d_c_inst_match_trie
.end(); ++it
){
1546 bool firstTime
= true;
1547 it
->second
->print( out
, it
->first
, firstTime
, useUnsatCore
, active_lemmas
);
1549 out
<< ")" << std::endl
;
1551 printed
= printed
|| !firstTime
;
1554 for( std::map
< Node
, inst::InstMatchTrie
>::iterator it
= d_inst_match_trie
.begin(); it
!= d_inst_match_trie
.end(); ++it
){
1555 bool firstTime
= true;
1556 it
->second
.print( out
, it
->first
, firstTime
, useUnsatCore
, active_lemmas
);
1558 out
<< ")" << std::endl
;
1560 printed
= printed
|| !firstTime
;
1564 out
<< "No instantiations" << std::endl
;
1568 void QuantifiersEngine::printSynthSolution( std::ostream
& out
) {
1570 d_ceg_inst
->printSynthSolution( out
);
1572 out
<< "Internal error : module for synth solution not found." << std::endl
;
1576 void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector
< Node
>& qs
) {
1577 if( options::incrementalSolving() ){
1578 for( std::map
< Node
, inst::CDInstMatchTrie
* >::iterator it
= d_c_inst_match_trie
.begin(); it
!= d_c_inst_match_trie
.end(); ++it
){
1579 qs
.push_back( it
->first
);
1582 for( std::map
< Node
, inst::InstMatchTrie
>::iterator it
= d_inst_match_trie
.begin(); it
!= d_inst_match_trie
.end(); ++it
){
1583 qs
.push_back( it
->first
);
1588 void QuantifiersEngine::getInstantiations( std::map
< Node
, std::vector
< Node
> >& insts
) {
1589 bool useUnsatCore
= false;
1590 std::vector
< Node
> active_lemmas
;
1591 if( options::trackInstLemmas() && getUnsatCoreLemmas( active_lemmas
) ){
1592 useUnsatCore
= true;
1595 if( options::incrementalSolving() ){
1596 for( std::map
< Node
, inst::CDInstMatchTrie
* >::iterator it
= d_c_inst_match_trie
.begin(); it
!= d_c_inst_match_trie
.end(); ++it
){
1597 it
->second
->getInstantiations( insts
[it
->first
], it
->first
, this, useUnsatCore
, active_lemmas
);
1600 for( std::map
< Node
, inst::InstMatchTrie
>::iterator it
= d_inst_match_trie
.begin(); it
!= d_inst_match_trie
.end(); ++it
){
1601 it
->second
.getInstantiations( insts
[it
->first
], it
->first
, this, useUnsatCore
, active_lemmas
);
1606 void QuantifiersEngine::getInstantiations( Node q
, std::vector
< Node
>& insts
) {
1607 if( options::incrementalSolving() ){
1608 std::map
< Node
, inst::CDInstMatchTrie
* >::iterator it
= d_c_inst_match_trie
.find( q
);
1609 if( it
!=d_c_inst_match_trie
.end() ){
1610 std::vector
< Node
> active_lemmas
;
1611 it
->second
->getInstantiations( insts
, it
->first
, this, false, active_lemmas
);
1614 std::map
< Node
, inst::InstMatchTrie
>::iterator it
= d_inst_match_trie
.find( q
);
1615 if( it
!=d_inst_match_trie
.end() ){
1616 std::vector
< Node
> active_lemmas
;
1617 it
->second
.getInstantiations( insts
, it
->first
, this, false, active_lemmas
);
1622 Node
QuantifiersEngine::getInstantiatedConjunction( Node q
) {
1623 Assert( q
.getKind()==FORALL
);
1624 std::vector
< Node
> insts
;
1625 getInstantiations( q
, insts
);
1626 if( insts
.empty() ){
1627 return NodeManager::currentNM()->mkConst(true);
1630 if( insts
.size()==1 ){
1633 ret
= NodeManager::currentNM()->mkNode( kind::AND
, insts
);
1635 //have to remove q, TODO: avoid this in a better way
1637 TNode tt
= d_term_util
->d_true
;
1638 ret
= ret
.substitute( tq
, tt
);
1643 QuantifiersEngine::Statistics::Statistics()
1644 : d_time("theory::QuantifiersEngine::time"),
1645 d_qcf_time("theory::QuantifiersEngine::time_qcf"),
1646 d_ematching_time("theory::QuantifiersEngine::time_ematching"),
1647 d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
1648 d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
1649 d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
1650 d_instantiations("QuantifiersEngine::Instantiations_Total", 0),
1651 d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0),
1652 d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0),
1653 d_inst_duplicate_ent("QuantifiersEngine::Duplicate_Inst_Entailed", 0),
1654 d_inst_duplicate_model_true("QuantifiersEngine::Duplicate_Inst_Model_True", 0),
1655 d_triggers("QuantifiersEngine::Triggers", 0),
1656 d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
1657 d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
1658 d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
1659 d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0),
1660 d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0),
1661 d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0),
1662 d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0),
1663 d_instantiations_qcf("QuantifiersEngine::Instantiations_Qcf_Conflict", 0),
1664 d_instantiations_qcf_prop("QuantifiersEngine::Instantiations_Qcf_Prop", 0),
1665 d_instantiations_fmf_exh("QuantifiersEngine::Instantiations_Fmf_Exh", 0),
1666 d_instantiations_fmf_mbqi("QuantifiersEngine::Instantiations_Fmf_Mbqi", 0),
1667 d_instantiations_cbqi("QuantifiersEngine::Instantiations_Cbqi", 0),
1668 d_instantiations_rr("QuantifiersEngine::Instantiations_Rewrite_Rules", 0)
1670 smtStatisticsRegistry()->registerStat(&d_time
);
1671 smtStatisticsRegistry()->registerStat(&d_qcf_time
);
1672 smtStatisticsRegistry()->registerStat(&d_ematching_time
);
1673 smtStatisticsRegistry()->registerStat(&d_num_quant
);
1674 smtStatisticsRegistry()->registerStat(&d_instantiation_rounds
);
1675 smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc
);
1676 smtStatisticsRegistry()->registerStat(&d_instantiations
);
1677 smtStatisticsRegistry()->registerStat(&d_inst_duplicate
);
1678 smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq
);
1679 smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent
);
1680 smtStatisticsRegistry()->registerStat(&d_inst_duplicate_model_true
);
1681 smtStatisticsRegistry()->registerStat(&d_triggers
);
1682 smtStatisticsRegistry()->registerStat(&d_simple_triggers
);
1683 smtStatisticsRegistry()->registerStat(&d_multi_triggers
);
1684 smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations
);
1685 smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv
);
1686 smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns
);
1687 smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen
);
1688 smtStatisticsRegistry()->registerStat(&d_instantiations_guess
);
1689 smtStatisticsRegistry()->registerStat(&d_instantiations_qcf
);
1690 smtStatisticsRegistry()->registerStat(&d_instantiations_qcf_prop
);
1691 smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_exh
);
1692 smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_mbqi
);
1693 smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi
);
1694 smtStatisticsRegistry()->registerStat(&d_instantiations_rr
);
1697 QuantifiersEngine::Statistics::~Statistics(){
1698 smtStatisticsRegistry()->unregisterStat(&d_time
);
1699 smtStatisticsRegistry()->unregisterStat(&d_qcf_time
);
1700 smtStatisticsRegistry()->unregisterStat(&d_ematching_time
);
1701 smtStatisticsRegistry()->unregisterStat(&d_num_quant
);
1702 smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds
);
1703 smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc
);
1704 smtStatisticsRegistry()->unregisterStat(&d_instantiations
);
1705 smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate
);
1706 smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq
);
1707 smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent
);
1708 smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_model_true
);
1709 smtStatisticsRegistry()->unregisterStat(&d_triggers
);
1710 smtStatisticsRegistry()->unregisterStat(&d_simple_triggers
);
1711 smtStatisticsRegistry()->unregisterStat(&d_multi_triggers
);
1712 smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations
);
1713 smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv
);
1714 smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns
);
1715 smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen
);
1716 smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess
);
1717 smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf
);
1718 smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf_prop
);
1719 smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_exh
);
1720 smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_mbqi
);
1721 smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi
);
1722 smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr
);
1725 eq::EqualityEngine
* QuantifiersEngine::getMasterEqualityEngine(){
1726 return d_te
->getMasterEqualityEngine();
1729 eq::EqualityEngine
* QuantifiersEngine::getActiveEqualityEngine() {
1731 return d_model
->getEqualityEngine();
1733 return d_te
->getMasterEqualityEngine();
1737 Node
QuantifiersEngine::getInternalRepresentative( Node a
, Node q
, int index
){
1738 bool prevModelEe
= d_useModelEe
;
1739 d_useModelEe
= false;
1740 Node ret
= d_eq_query
->getInternalRepresentative( a
, q
, index
);
1741 d_useModelEe
= prevModelEe
;
1745 Node
QuantifiersEngine::getTermForType(TypeNode tn
)
1747 if (d_term_enum
->isClosedEnumerableType(tn
))
1749 return d_term_enum
->getEnumerateTerm(tn
, 0);
1753 return d_term_db
->getOrMakeTypeGroundTerm(tn
);
1757 void QuantifiersEngine::debugPrintEqualityEngine( const char * c
) {
1758 eq::EqualityEngine
* ee
= getActiveEqualityEngine();
1759 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( ee
);
1760 std::map
< TypeNode
, int > typ_num
;
1761 while( !eqcs_i
.isFinished() ){
1762 TNode r
= (*eqcs_i
);
1763 TypeNode tr
= r
.getType();
1764 if( typ_num
.find( tr
)==typ_num
.end() ){
1768 bool firstTime
= true;
1769 Trace(c
) << " " << r
;
1770 Trace(c
) << " : { ";
1771 eq::EqClassIterator eqc_i
= eq::EqClassIterator( r
, ee
);
1772 while( !eqc_i
.isFinished() ){
1776 Trace(c
) << std::endl
;
1779 Trace(c
) << " " << n
<< std::endl
;
1783 if( !firstTime
){ Trace(c
) << " "; }
1784 Trace(c
) << "}" << std::endl
;
1787 Trace(c
) << std::endl
;
1788 for( std::map
< TypeNode
, int >::iterator it
= typ_num
.begin(); it
!= typ_num
.end(); ++it
){
1789 Trace(c
) << "# eqc for " << it
->first
<< " : " << it
->second
<< std::endl
;