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/sep/theory_sep.h"
23 #include "theory/quantifiers/alpha_equivalence.h"
24 #include "theory/quantifiers/ambqi_builder.h"
25 #include "theory/quantifiers/bounded_integers.h"
26 #include "theory/quantifiers/ce_guided_instantiation.h"
27 #include "theory/quantifiers/conjecture_generator.h"
28 #include "theory/quantifiers/first_order_model.h"
29 #include "theory/quantifiers/full_model_check.h"
30 #include "theory/quantifiers/fun_def_engine.h"
31 #include "theory/quantifiers/inst_strategy_cbqi.h"
32 #include "theory/quantifiers/inst_strategy_e_matching.h"
33 #include "theory/quantifiers/instantiation_engine.h"
34 #include "theory/quantifiers/local_theory_ext.h"
35 #include "theory/quantifiers/model_engine.h"
36 #include "theory/quantifiers/quant_conflict_find.h"
37 #include "theory/quantifiers/quant_equality_engine.h"
38 #include "theory/quantifiers/quantifiers_rewriter.h"
39 #include "theory/quantifiers/relevant_domain.h"
40 #include "theory/quantifiers/rewrite_engine.h"
41 #include "theory/quantifiers/term_database.h"
42 #include "theory/quantifiers/trigger.h"
43 #include "theory/quantifiers/quant_split.h"
44 #include "theory/quantifiers/anti_skolem.h"
45 #include "theory/quantifiers/equality_infer.h"
46 #include "theory/quantifiers/inst_propagator.h"
47 #include "theory/theory_engine.h"
48 #include "theory/uf/equality_engine.h"
49 #include "theory/uf/theory_uf.h"
50 #include "theory/uf/theory_uf_strong_solver.h"
54 using namespace CVC4::kind
;
55 using namespace CVC4::context
;
56 using namespace CVC4::theory
;
57 using namespace CVC4::theory::inst
;
59 QuantifiersEngine::QuantifiersEngine(context::Context
* c
, context::UserContext
* u
, TheoryEngine
* te
):
61 d_conflict_c(c
, false),
64 d_lemmas_produced_c(u
),
69 //d_ierCounterLastLc(c),
73 d_presolve_cache_wq(u
),
74 d_presolve_cache_wic(u
){
76 d_eq_query
= new EqualityQueryQuantifiersEngine( c
, this );
77 d_util
.push_back( d_eq_query
);
79 d_term_db
= new quantifiers::TermDb( c
, u
, this );
80 d_util
.push_back( d_term_db
);
82 if( options::instPropagate() ){
83 // notice that this option is incompatible with options::qcfAllConflict()
84 d_inst_prop
= new quantifiers::InstPropagator( this );
85 d_util
.push_back( d_inst_prop
);
86 d_inst_notify
.push_back( d_inst_prop
->getInstantiationNotify() );
91 d_tr_trie
= new inst::TriggerTrie
;
92 d_curr_effort_level
= QEFFORT_NONE
;
94 d_hasAddedLemma
= false;
96 //don't add true lemma
97 d_lemmas_produced_c
[d_term_db
->d_true
] = true;
99 Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl
;
100 Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl
;
102 if( options::relevantTriggers() ){
103 d_quant_rel
= new QuantRelevance( false );
108 if( options::quantEpr() ){
109 Assert( !options::incrementalSolving() );
110 d_qepr
= new QuantEPR
;
118 d_inst_engine
= NULL
;
121 d_anti_skolem
= NULL
;
123 d_model_engine
= NULL
;
127 d_lte_part_inst
= NULL
;
128 d_alpha_equiv
= NULL
;
129 d_fun_def_engine
= NULL
;
135 d_total_inst_count_debug
= 0;
136 //allow theory combination to go first, once initially
137 d_ierCounter
= options::instWhenTcFirst() ? 0 : 1;
138 d_ierCounter_c
= d_ierCounter
;
140 d_ierCounterLastLc
= 0;
141 d_inst_when_phase
= 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
144 QuantifiersEngine::~QuantifiersEngine(){
145 for(std::map
< Node
, inst::CDInstMatchTrie
* >::iterator
146 i
= d_c_inst_match_trie
.begin(), iend
= d_c_inst_match_trie
.end();
151 d_c_inst_match_trie
.clear();
153 delete d_alpha_equiv
;
158 delete d_model_engine
;
159 delete d_inst_engine
;
169 delete d_lte_part_inst
;
170 delete d_fun_def_engine
;
175 delete d_anti_skolem
;
179 EqualityQueryQuantifiersEngine
* QuantifiersEngine::getEqualityQuery() {
183 context::Context
* QuantifiersEngine::getSatContext(){
184 return d_te
->theoryOf( THEORY_QUANTIFIERS
)->getSatContext();
187 context::UserContext
* QuantifiersEngine::getUserContext(){
188 return d_te
->theoryOf( THEORY_QUANTIFIERS
)->getUserContext();
191 OutputChannel
& QuantifiersEngine::getOutputChannel(){
192 return d_te
->theoryOf( THEORY_QUANTIFIERS
)->getOutputChannel();
194 /** get default valuation for the quantifiers engine */
195 Valuation
& QuantifiersEngine::getValuation(){
196 return d_te
->theoryOf( THEORY_QUANTIFIERS
)->getValuation();
199 void QuantifiersEngine::finishInit(){
200 context::Context
* c
= getSatContext();
201 Trace("quant-engine-debug") << "QuantifiersEngine : finishInit " << std::endl
;
202 bool needsBuilder
= false;
203 bool needsRelDom
= false;
204 //add quantifiers modules
205 if( options::quantConflictFind() || options::quantRewriteRules() ){
206 d_qcf
= new quantifiers::QuantConflictFind( this, c
);
207 d_modules
.push_back( d_qcf
);
209 if( options::conjectureGen() ){
210 d_sg_gen
= new quantifiers::ConjectureGenerator( this, c
);
211 d_modules
.push_back( d_sg_gen
);
213 if( !options::finiteModelFind() || options::fmfInstEngine() ){
214 d_inst_engine
= new quantifiers::InstantiationEngine( this );
215 d_modules
.push_back( d_inst_engine
);
217 if( options::cbqi() ){
218 d_i_cbqi
= new quantifiers::InstStrategyCegqi( this );
219 d_modules
.push_back( d_i_cbqi
);
220 //if( options::cbqiModel() ){
221 // needsBuilder = true;
224 if( options::ceGuidedInst() ){
225 d_ceg_inst
= new quantifiers::CegInstantiation( this, c
);
226 d_modules
.push_back( d_ceg_inst
);
227 //needsBuilder = true;
229 //finite model finding
230 if( options::finiteModelFind() ){
231 if( options::fmfBound() ){
232 d_bint
= new quantifiers::BoundedIntegers( c
, this );
233 d_modules
.push_back( d_bint
);
235 d_model_engine
= new quantifiers::ModelEngine( c
, this );
236 d_modules
.push_back( d_model_engine
);
237 //finite model finder has special ways of building the model
240 if( options::quantRewriteRules() ){
241 d_rr_engine
= new quantifiers::RewriteEngine( c
, this );
242 d_modules
.push_back(d_rr_engine
);
244 if( options::ltePartialInst() ){
245 d_lte_part_inst
= new quantifiers::LtePartialInst( this, c
);
246 d_modules
.push_back( d_lte_part_inst
);
248 if( options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE
){
249 d_qsplit
= new quantifiers::QuantDSplit( this, c
);
250 d_modules
.push_back( d_qsplit
);
252 if( options::quantAntiSkolem() ){
253 d_anti_skolem
= new quantifiers::QuantAntiSkolem( this );
254 d_modules
.push_back( d_anti_skolem
);
256 if( options::quantAlphaEquiv() ){
257 d_alpha_equiv
= new quantifiers::AlphaEquivalence( this );
259 //if( options::funDefs() ){
260 // d_fun_def_engine = new quantifiers::FunDefEngine( this, c );
261 // d_modules.push_back( d_fun_def_engine );
263 if( options::quantEqualityEngine() ){
264 d_uee
= new quantifiers::QuantEqualityEngine( this, c
);
265 d_modules
.push_back( d_uee
);
267 //full saturation : instantiate from relevant domain, then arbitrary terms
268 if( options::fullSaturateQuant() || options::fullSaturateInterleave() ){
269 d_fs
= new quantifiers::FullSaturation( this );
270 d_modules
.push_back( d_fs
);
275 d_rel_dom
= new quantifiers::RelevantDomain( this );
276 d_util
.push_back( d_rel_dom
);
279 // if we require specialized ways of building the model
281 Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl
;
282 if( options::mbqiMode()==quantifiers::MBQI_FMC
|| options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL
||
283 options::mbqiMode()==quantifiers::MBQI_TRUST
|| options::fmfBound() ){
284 Trace("quant-engine-debug") << "...make fmc builder." << std::endl
;
285 d_model
= new quantifiers::fmcheck::FirstOrderModelFmc( this, c
, "FirstOrderModelFmc" );
286 d_builder
= new quantifiers::fmcheck::FullModelChecker( c
, this );
287 }else if( options::mbqiMode()==quantifiers::MBQI_ABS
){
288 Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl
;
289 d_model
= new quantifiers::FirstOrderModelAbs( this, c
, "FirstOrderModelAbs" );
290 d_builder
= new quantifiers::AbsMbqiBuilder( c
, this );
292 Trace("quant-engine-debug") << "...make default model builder." << std::endl
;
293 d_model
= new quantifiers::FirstOrderModelIG( this, c
, "FirstOrderModelIG" );
294 d_builder
= new quantifiers::QModelBuilderDefault( c
, this );
297 d_model
= new quantifiers::FirstOrderModelIG( this, c
, "FirstOrderModelIG" );
301 QuantifiersModule
* QuantifiersEngine::getOwner( Node q
) {
302 std::map
< Node
, QuantifiersModule
* >::iterator it
= d_owner
.find( q
);
303 if( it
==d_owner
.end() ){
310 void QuantifiersEngine::setOwner( Node q
, QuantifiersModule
* m
, int priority
) {
311 QuantifiersModule
* mo
= getOwner( q
);
314 if( priority
<=d_owner_priority
[q
] ){
315 Trace("quant-warn") << "WARNING: setting owner of " << q
<< " to " << ( m
? m
->identify() : "null" ) << ", but already has owner " << mo
->identify() << " with higher priority!" << std::endl
;
320 d_owner_priority
[q
] = priority
;
324 bool QuantifiersEngine::hasOwnership( Node q
, QuantifiersModule
* m
) {
325 QuantifiersModule
* mo
= getOwner( q
);
326 return mo
==m
|| mo
==NULL
;
329 bool QuantifiersEngine::isFiniteBound( Node q
, Node v
) {
330 if( getBoundedIntegers() && getBoundedIntegers()->isBoundVar( q
, v
) ){
333 TypeNode tn
= v
.getType();
334 if( tn
.isSort() && options::finiteModelFind() ){
336 }else if( getTermDatabase()->mayComplete( tn
) ){
343 void QuantifiersEngine::presolve() {
344 Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl
;
345 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
346 d_modules
[i
]->presolve();
348 d_term_db
->presolve();
350 //add all terms to database
351 if( options::incrementalSolving() ){
352 Trace("quant-engine-proc") << "Add presolve cache " << d_presolve_cache
.size() << std::endl
;
353 for( unsigned i
=0; i
<d_presolve_cache
.size(); i
++ ){
354 addTermToDatabase( d_presolve_cache
[i
], d_presolve_cache_wq
[i
], d_presolve_cache_wic
[i
] );
356 Trace("quant-engine-proc") << "Done add presolve cache " << std::endl
;
360 void QuantifiersEngine::ppNotifyAssertions(
361 const std::vector
<Node
>& assertions
) {
362 Trace("quant-engine-proc")
363 << "ppNotifyAssertions in QE, #assertions = " << assertions
.size()
364 << " check epr = " << (d_qepr
!= NULL
) << std::endl
;
365 if ((options::instLevelInputOnly() && options::instMaxLevel() != -1) ||
367 for (unsigned i
= 0; i
< assertions
.size(); i
++) {
368 if (options::instLevelInputOnly() && options::instMaxLevel() != -1) {
369 setInstantiationLevelAttr(assertions
[i
], 0);
371 if (d_qepr
!= NULL
) {
372 d_qepr
->registerAssertion(assertions
[i
]);
375 if (d_qepr
!= NULL
) {
376 // must handle sources of other new constants e.g. separation logic
378 sep::TheorySep
* theory_sep
=
379 static_cast<sep::TheorySep
*>(getTheoryEngine()->theoryOf(THEORY_SEP
));
380 theory_sep
->initializeBounds();
381 d_qepr
->finishInit();
386 void QuantifiersEngine::check( Theory::Effort e
){
387 CodeTimer
codeTimer(d_statistics
.d_time
);
388 d_useModelEe
= options::quantModelEe() && ( e
>=Theory::EFFORT_LAST_CALL
);
389 // if we want to use the model's equality engine, build the model now
390 if( d_useModelEe
&& !d_model
->isBuilt() ){
391 Trace("quant-engine-debug") << "Build the model." << std::endl
;
392 if( !d_te
->getModelBuilder()->buildModel( d_model
) ){
393 //we are done if model building was unsuccessful
395 if( d_hasAddedLemma
){
396 Trace("quant-engine-debug") << "...failed." << std::endl
;
402 if( !getActiveEqualityEngine()->consistent() ){
403 Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl
;
406 bool needsCheck
= !d_lemmas_waiting
.empty();
407 unsigned needsModelE
= QEFFORT_NONE
;
408 std::vector
< QuantifiersModule
* > qm
;
409 if( d_model
->checkNeeded() ){
410 needsCheck
= needsCheck
|| e
>=Theory::EFFORT_LAST_CALL
; //always need to check at or above last call
411 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
412 if( d_modules
[i
]->needsCheck( e
) ){
413 qm
.push_back( d_modules
[i
] );
415 //can only request model at last call since theory combination can find inconsistencies
416 if( e
>=Theory::EFFORT_LAST_CALL
){
417 unsigned me
= d_modules
[i
]->needsModel( e
);
418 needsModelE
= me
<needsModelE
? me
: needsModelE
;
425 d_hasAddedLemma
= false;
426 bool setIncomplete
= false;
428 Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e
<< ", needsCheck=" << needsCheck
<< std::endl
;
430 //this will fail if a set of instances is marked as a conflict, but is not
431 Assert( !d_conflict_c
.get() );
432 //flush previous lemmas (for instance, if was interupted), or other lemmas to process
434 if( d_hasAddedLemma
){
437 if( !d_recorded_inst
.empty() ){
438 Trace("quant-engine-debug") << "Removing " << d_recorded_inst
.size() << " instantiations..." << std::endl
;
439 //remove explicitly recorded instantiations
440 for( unsigned i
=0; i
<d_recorded_inst
.size(); i
++ ){
441 removeInstantiationInternal( d_recorded_inst
[i
].first
, d_recorded_inst
[i
].second
);
443 d_recorded_inst
.clear();
447 if( Trace
.isOn("quant-engine") ){
448 clSet
= double(clock())/double(CLOCKS_PER_SEC
);
449 Trace("quant-engine") << ">>>>> Quantifiers Engine Round, effort = " << e
<< " <<<<<" << std::endl
;
452 if( Trace
.isOn("quant-engine-debug") ){
453 Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e
<< std::endl
;
454 Trace("quant-engine-debug") << " depth : " << d_ierCounter_c
<< std::endl
;
455 Trace("quant-engine-debug") << " modules to check : ";
456 for( unsigned i
=0; i
<qm
.size(); i
++ ){
457 Trace("quant-engine-debug") << qm
[i
]->identify() << " ";
459 Trace("quant-engine-debug") << std::endl
;
460 Trace("quant-engine-debug") << " # quantified formulas = " << d_model
->getNumAssertedQuantifiers() << std::endl
;
461 if( !d_lemmas_waiting
.empty() ){
462 Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting
.size() << std::endl
;
464 Trace("quant-engine-debug") << " Theory engine finished : " << !d_te
->needCheck() << std::endl
;
465 Trace("quant-engine-debug") << " Needs model effort : " << needsModelE
<< std::endl
;
467 if( Trace
.isOn("quant-engine-ee-pre") ){
468 Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl
;
469 debugPrintEqualityEngine( "quant-engine-ee-pre" );
471 if( Trace
.isOn("quant-engine-assert") ){
472 Trace("quant-engine-assert") << "Assertions : " << std::endl
;
473 getTheoryEngine()->printAssertions("quant-engine-assert");
477 Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl
;
478 for( unsigned i
=0; i
<d_util
.size(); i
++ ){
479 Trace("quant-engine-debug2") << "Reset " << d_util
[i
]->identify().c_str() << "..." << std::endl
;
480 if( !d_util
[i
]->reset( e
) ){
482 if( d_hasAddedLemma
){
485 //should only fail reset if added a lemma
491 if( Trace
.isOn("quant-engine-ee") ){
492 Trace("quant-engine-ee") << "Equality engine : " << std::endl
;
493 debugPrintEqualityEngine( "quant-engine-ee" );
497 Trace("quant-engine-debug") << "Reset model..." << std::endl
;
498 d_model
->reset_round();
501 Trace("quant-engine-debug") << "Resetting all modules..." << std::endl
;
502 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
503 Trace("quant-engine-debug2") << "Reset " << d_modules
[i
]->identify().c_str() << std::endl
;
504 d_modules
[i
]->reset_round( e
);
506 Trace("quant-engine-debug") << "Done resetting all modules." << std::endl
;
507 //reset may have added lemmas
509 if( d_hasAddedLemma
){
513 if( e
==Theory::EFFORT_LAST_CALL
){
514 //if effort is last call, try to minimize model first
515 //uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver();
516 //if( ufss && !ufss->minimize() ){ return; }
517 ++(d_statistics
.d_instantiation_rounds_lc
);
518 }else if( e
==Theory::EFFORT_FULL
){
519 ++(d_statistics
.d_instantiation_rounds
);
521 Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl
;
522 for( unsigned quant_e
= QEFFORT_CONFLICT
; quant_e
<=QEFFORT_LAST_CALL
; quant_e
++ ){
523 d_curr_effort_level
= quant_e
;
524 //build the model if any module requested it
525 if( needsModelE
==quant_e
&& !d_model
->isBuilt() ){
526 // theory engine's model builder is quantifier engine's builder if it has one
527 Assert( !d_builder
|| d_builder
==d_te
->getModelBuilder() );
528 Trace("quant-engine-debug") << "Build model..." << std::endl
;
529 if( !d_te
->getModelBuilder()->buildModel( d_model
) ){
530 //we are done if model building was unsuccessful
531 Trace("quant-engine-debug") << "...added lemmas." << std::endl
;
535 if( !d_hasAddedLemma
){
537 for( unsigned i
=0; i
<qm
.size(); i
++ ){
538 Trace("quant-engine-debug") << "Check " << qm
[i
]->identify().c_str() << " at effort " << quant_e
<< "..." << std::endl
;
539 qm
[i
]->check( e
, quant_e
);
541 Trace("quant-engine-debug") << "...conflict!" << std::endl
;
545 //flush all current lemmas
548 //if we have added one, stop
549 if( d_hasAddedLemma
){
552 Assert( !d_conflict
);
553 if( quant_e
==QEFFORT_CONFLICT
){
554 if( e
==Theory::EFFORT_FULL
){
555 //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase
556 if( d_ierCounterLastLc
!=d_ierCounter_lc
|| !options::instWhenStrictInterleave() || d_ierCounter
%d_inst_when_phase
!=0 ){
557 d_ierCounter
= d_ierCounter
+ 1;
558 d_ierCounterLastLc
= d_ierCounter_lc
;
559 d_ierCounter_c
= d_ierCounter_c
.get() + 1;
561 }else if( e
==Theory::EFFORT_LAST_CALL
){
562 d_ierCounter_lc
= d_ierCounter_lc
+ 1;
564 }else if( quant_e
==QEFFORT_MODEL
){
565 if( e
==Theory::EFFORT_LAST_CALL
){
566 //sources of incompleteness
567 if( !d_recorded_inst
.empty() ){
568 Trace("quant-engine-debug") << "Set incomplete due to recorded instantiations." << std::endl
;
569 setIncomplete
= true;
571 //if we have a chance not to set incomplete
572 if( !setIncomplete
){
573 setIncomplete
= false;
574 //check if we should set the incomplete flag
575 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
576 if( !d_modules
[i
]->checkComplete() ){
577 Trace("quant-engine-debug") << "Set incomplete because " << d_modules
[i
]->identify().c_str() << " was incomplete." << std::endl
;
578 setIncomplete
= true;
582 if( !setIncomplete
){
583 //look at individual quantified formulas, one module must claim completeness for each one
584 for( unsigned i
=0; i
<d_model
->getNumAssertedQuantifiers(); i
++ ){
585 bool hasCompleteM
= false;
586 Node q
= d_model
->getAssertedQuantifier( i
);
587 QuantifiersModule
* qmd
= getOwner( q
);
589 hasCompleteM
= qmd
->checkCompleteFor( q
);
591 for( unsigned j
=0; j
<d_modules
.size(); j
++ ){
592 if( d_modules
[j
]->checkCompleteFor( q
) ){
600 Trace("quant-engine-debug") << "Set incomplete because " << q
<< " was not fully processed." << std::endl
;
601 setIncomplete
= true;
605 Trace("quant-engine-debug2") << "Complete for " << q
<< " due to " << qmd
->identify().c_str() << std::endl
;
610 //if setIncomplete = false, we will answer SAT, otherwise we will run at quant_e QEFFORT_LAST_CALL
611 if( !setIncomplete
){
618 d_curr_effort_level
= QEFFORT_NONE
;
619 Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl
;
620 if( d_hasAddedLemma
){
622 if( Trace
.isOn("inst-per-quant-round") ){
623 for( std::map
< Node
, int >::iterator it
= d_temp_inst_debug
.begin(); it
!= d_temp_inst_debug
.end(); ++it
){
624 Trace("inst-per-quant-round") << " * " << it
->second
<< " for " << it
->first
<< std::endl
;
625 d_temp_inst_debug
[it
->first
] = 0;
629 if( Trace
.isOn("quant-engine") ){
630 double clSet2
= double(clock())/double(CLOCKS_PER_SEC
);
631 Trace("quant-engine") << "Finished quantifiers engine, total time = " << (clSet2
-clSet
);
632 Trace("quant-engine") << ", added lemma = " << d_hasAddedLemma
;
633 Trace("quant-engine") << std::endl
;
636 Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl
;
638 Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl
;
642 if( e
==Theory::EFFORT_LAST_CALL
&& !d_hasAddedLemma
){
643 if( options::produceModels() ){
644 if( d_model
->isBuilt() ){
645 Trace("quant-engine-debug") << "Already built model using model builder, finish..." << std::endl
;
647 //use default model builder when no module built the model
648 Trace("quant-engine-debug") << "Build the default model..." << std::endl
;
649 d_te
->getModelBuilder()->buildModel( d_model
);
650 Trace("quant-engine-debug") << "Done building the model." << std::endl
;
654 Trace("quant-engine") << "Set incomplete flag." << std::endl
;
655 getOutputChannel().setIncomplete();
658 if( Trace
.isOn("inst-per-quant") ){
659 for( std::map
< Node
, int >::iterator it
= d_total_inst_debug
.begin(); it
!= d_total_inst_debug
.end(); ++it
){
660 Trace("inst-per-quant") << " * " << it
->second
<< " for " << it
->first
<< std::endl
;
666 void QuantifiersEngine::notifyCombineTheories() {
667 //if allowing theory combination to happen at most once between instantiation rounds
669 //d_ierCounterLastLc = -1;
672 bool QuantifiersEngine::reduceQuantifier( Node q
) {
673 //TODO: this can be unified with preregistration: AlphaEquivalence takes ownership of reducable quants
674 BoolMap::const_iterator it
= d_quants_red
.find( q
);
675 if( it
==d_quants_red
.end() ){
677 std::map
< Node
, Node
>::iterator itr
= d_quants_red_lem
.find( q
);
678 if( itr
==d_quants_red_lem
.end() ){
680 Trace("quant-engine-red") << "Alpha equivalence " << q
<< "?" << std::endl
;
681 //add equivalence with another quantified formula
682 lem
= d_alpha_equiv
->reduceQuantifier( q
);
684 Trace("quant-engine-red") << "...alpha equivalence success." << std::endl
;
685 ++(d_statistics
.d_red_alpha_equiv
);
688 d_quants_red_lem
[q
] = lem
;
693 getOutputChannel().lemma( lem
);
695 d_quants_red
[q
] = !lem
.isNull();
696 return !lem
.isNull();
702 bool QuantifiersEngine::registerQuantifier( Node f
){
703 std::map
< Node
, bool >::iterator it
= d_quants
.find( f
);
704 if( it
==d_quants
.end() ){
705 Trace("quant") << "QuantifiersEngine : Register quantifier ";
706 Trace("quant") << " : " << f
<< std::endl
;
707 ++(d_statistics
.d_num_quant
);
708 Assert( f
.getKind()==FORALL
);
710 //check whether we should apply a reduction
711 if( reduceQuantifier( f
) ){
712 Trace("quant") << "...reduced." << std::endl
;
716 //make instantiation constants for f
717 d_term_db
->makeInstantiationConstantsFor( f
);
718 d_term_db
->computeAttributes( f
);
719 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
720 Trace("quant-debug") << "pre-register with " << d_modules
[i
]->identify() << "..." << std::endl
;
721 d_modules
[i
]->preRegisterQuantifier( f
);
723 QuantifiersModule
* qm
= getOwner( f
);
725 Trace("quant") << " Owner : " << qm
->identify() << std::endl
;
727 //register with quantifier relevance
729 d_quant_rel
->registerQuantifier( f
);
731 //register with each module
732 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
733 Trace("quant-debug") << "register with " << d_modules
[i
]->identify() << "..." << std::endl
;
734 d_modules
[i
]->registerQuantifier( f
);
737 Node ceBody
= d_term_db
->getInstConstantBody( f
);
738 //also register it with the strong solver
739 //if( options::finiteModelFind() ){
740 // ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
742 Trace("quant-debug") << "...finish." << std::endl
;
753 void QuantifiersEngine::registerPattern( std::vector
<Node
> & pattern
) {
754 for(std::vector
<Node
>::iterator p
= pattern
.begin(); p
!= pattern
.end(); ++p
){
755 std::set
< Node
> added
;
756 getTermDatabase()->addTerm( *p
, added
);
760 void QuantifiersEngine::assertQuantifier( Node f
, bool pol
){
763 if( !reduceQuantifier( f
) ){
765 if( d_skolemized
.find( f
)==d_skolemized
.end() ){
766 Node body
= d_term_db
->getSkolemizedBody( f
);
767 NodeBuilder
<> nb(kind::OR
);
768 nb
<< f
<< body
.notNode();
770 if( Trace
.isOn("quantifiers-sk-debug") ){
771 Node slem
= Rewriter::rewrite( lem
);
772 Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem
<< std::endl
;
774 getOutputChannel().lemma( lem
, false, true );
775 d_skolemized
[f
] = true;
779 //assert to modules TODO : also for !pol?
780 //register the quantifier, assert it to each module
781 if( registerQuantifier( f
) ){
782 d_model
->assertQuantifier( f
);
783 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
784 d_modules
[i
]->assertNode( f
);
786 addTermToDatabase( d_term_db
->getInstConstantBody( f
), true );
791 void QuantifiersEngine::propagate( Theory::Effort level
){
792 CodeTimer
codeTimer(d_statistics
.d_time
);
794 for( int i
=0; i
<(int)d_modules
.size(); i
++ ){
795 d_modules
[i
]->propagate( level
);
799 Node
QuantifiersEngine::getNextDecisionRequest( unsigned& priority
){
800 unsigned min_priority
= 0;
802 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
803 Node n
= d_modules
[i
]->getNextDecisionRequest( priority
);
804 if( !n
.isNull() && ( dec
.isNull() || priority
<min_priority
) ){
806 min_priority
= priority
;
812 quantifiers::TermDbSygus
* QuantifiersEngine::getTermDatabaseSygus() {
813 return getTermDatabase()->getTermDatabaseSygus();
816 void QuantifiersEngine::addTermToDatabase( Node n
, bool withinQuant
, bool withinInstClosure
){
817 if( options::incrementalSolving() ){
818 if( d_presolve_in
.find( n
)==d_presolve_in
.end() ){
819 d_presolve_in
.insert( n
);
820 d_presolve_cache
.push_back( n
);
821 d_presolve_cache_wq
.push_back( withinQuant
);
822 d_presolve_cache_wic
.push_back( withinInstClosure
);
825 //only wait if we are doing incremental solving
826 if( !d_presolve
|| !options::incrementalSolving() ){
827 std::set
< Node
> added
;
828 getTermDatabase()->addTerm( n
, added
, withinQuant
, withinInstClosure
);
830 //added contains also the Node that just have been asserted in this branch
832 for( std::set
< Node
>::iterator i
=added
.begin(), end
=added
.end(); i
!=end
; i
++ ){
834 d_quant_rel
->setRelevance( i
->getOperator(), 0 );
841 void QuantifiersEngine::eqNotifyNewClass(TNode t
) {
842 addTermToDatabase( t
);
843 if( d_eq_query
->getEqualityInference() ){
844 d_eq_query
->getEqualityInference()->eqNotifyNewClass( t
);
848 void QuantifiersEngine::eqNotifyPreMerge(TNode t1
, TNode t2
) {
849 if( d_eq_query
->getEqualityInference() ){
850 d_eq_query
->getEqualityInference()->eqNotifyMerge( t1
, t2
);
854 void QuantifiersEngine::eqNotifyPostMerge(TNode t1
, TNode t2
) {
858 void QuantifiersEngine::eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
) {
860 // d_qcf->assertDisequal( t1, t2 );
864 void QuantifiersEngine::computeTermVector( Node f
, InstMatch
& m
, std::vector
< Node
>& vars
, std::vector
< Node
>& terms
){
865 for( size_t i
=0; i
<f
[0].getNumChildren(); i
++ ){
868 vars
.push_back( f
[0][i
] );
869 terms
.push_back( n
);
875 bool QuantifiersEngine::recordInstantiationInternal( Node q
, std::vector
< Node
>& terms
, bool modEq
, bool addedLem
) {
877 //record the instantiation for deletion later
878 d_recorded_inst
.push_back( std::pair
< Node
, std::vector
< Node
> >( q
, terms
) );
880 if( options::incrementalSolving() ){
881 Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq
<< std::endl
;
882 inst::CDInstMatchTrie
* imt
;
883 std::map
< Node
, inst::CDInstMatchTrie
* >::iterator it
= d_c_inst_match_trie
.find( q
);
884 if( it
!=d_c_inst_match_trie
.end() ){
887 imt
= new CDInstMatchTrie( getUserContext() );
888 d_c_inst_match_trie
[q
] = imt
;
890 return imt
->addInstMatch( this, q
, terms
, getUserContext(), modEq
);
892 Trace("inst-add-debug") << "Adding into inst trie" << std::endl
;
893 return d_inst_match_trie
[q
].addInstMatch( this, q
, terms
, modEq
);
897 bool QuantifiersEngine::removeInstantiationInternal( Node q
, std::vector
< Node
>& terms
) {
898 if( options::incrementalSolving() ){
899 std::map
< Node
, inst::CDInstMatchTrie
* >::iterator it
= d_c_inst_match_trie
.find( q
);
900 if( it
!=d_c_inst_match_trie
.end() ){
901 return it
->second
->removeInstMatch( this, q
, terms
);
906 return d_inst_match_trie
[q
].removeInstMatch( this, q
, terms
);
910 void QuantifiersEngine::setInstantiationLevelAttr( Node n
, Node qn
, uint64_t level
){
911 Trace("inst-level-debug2") << "IL : " << n
<< " " << qn
<< " " << level
<< std::endl
;
912 //if not from the vector of terms we instantiatied
913 if( qn
.getKind()!=BOUND_VARIABLE
&& n
!=qn
){
914 //if this is a new term, without an instantiation level
915 if( !n
.hasAttribute(InstLevelAttribute()) ){
916 InstLevelAttribute ila
;
917 n
.setAttribute(ila
,level
);
918 Trace("inst-level-debug") << "Set instantiation level " << n
<< " to " << level
<< std::endl
;
919 Assert( n
.getNumChildren()==qn
.getNumChildren() );
920 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
921 setInstantiationLevelAttr( n
[i
], qn
[i
], level
);
927 void QuantifiersEngine::setInstantiationLevelAttr( Node n
, uint64_t level
){
928 if( !n
.hasAttribute(InstLevelAttribute()) ){
929 InstLevelAttribute ila
;
930 n
.setAttribute(ila
,level
);
931 Trace("inst-level-debug") << "Set instantiation level " << n
<< " to " << level
<< std::endl
;
932 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
933 setInstantiationLevelAttr( n
[i
], level
);
938 Node
QuantifiersEngine::getSubstitute( Node n
, std::vector
< Node
>& terms
, std::map
< Node
, Node
>& visited
){
939 std::map
< Node
, Node
>::iterator itv
= visited
.find( n
);
940 if( itv
==visited
.end() ){
942 if( n
.getKind()==INST_CONSTANT
){
943 Debug("check-inst") << "Substitute inst constant : " << n
<< std::endl
;
944 ret
= terms
[n
.getAttribute(InstVarNumAttribute())];
946 //if( !quantifiers::TermDb::hasInstConstAttr( n ) ){
947 //Debug("check-inst") << "No inst const attr : " << n << std::endl;
950 //Debug("check-inst") << "Recurse on : " << n << std::endl;
951 std::vector
< Node
> cc
;
952 if( n
.getMetaKind() == kind::metakind::PARAMETERIZED
){
953 cc
.push_back( n
.getOperator() );
955 bool changed
= false;
956 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
957 Node c
= getSubstitute( n
[i
], terms
, visited
);
959 changed
= changed
|| c
!=n
[i
];
962 ret
= NodeManager::currentNM()->mkNode( n
.getKind(), cc
);
973 Node
QuantifiersEngine::getInstantiation( Node q
, std::vector
< Node
>& vars
, std::vector
< Node
>& terms
, bool doVts
){
975 Assert( vars
.size()==terms
.size() );
976 //process partial instantiation if necessary
977 if( q
[0].getNumChildren()!=vars
.size() ){
978 body
= q
[ 1 ].substitute( vars
.begin(), vars
.end(), terms
.begin(), terms
.end() );
979 std::vector
< Node
> uninst_vars
;
980 //doing a partial instantiation, must add quantifier for all uninstantiated variables
981 for( unsigned i
=0; i
<q
[0].getNumChildren(); i
++ ){
982 if( std::find( vars
.begin(), vars
.end(), q
[0][i
] )==vars
.end() ){
983 uninst_vars
.push_back( q
[0][i
] );
986 Trace("partial-inst") << "Partially instantiating with " << vars
.size() << " / " << q
[0].getNumChildren() << " for " << q
<< std::endl
;
987 Assert( !uninst_vars
.empty() );
988 Node bvl
= NodeManager::currentNM()->mkNode( BOUND_VAR_LIST
, uninst_vars
);
989 body
= NodeManager::currentNM()->mkNode( FORALL
, bvl
, body
);
990 Trace("partial-inst") << "Partial instantiation : " << q
<< std::endl
;
991 Trace("partial-inst") << " : " << body
<< std::endl
;
993 if( options::cbqi() ){
994 body
= q
[ 1 ].substitute( vars
.begin(), vars
.end(), terms
.begin(), terms
.end() );
996 //do optimized version
997 Node icb
= d_term_db
->getInstConstantBody( q
);
998 std::map
< Node
, Node
> visited
;
999 body
= getSubstitute( icb
, terms
, visited
);
1000 if( Debug
.isOn("check-inst") ){
1001 Node body2
= q
[ 1 ].substitute( vars
.begin(), vars
.end(), terms
.begin(), terms
.end() );
1003 Debug("check-inst") << "Substitution is wrong : " << body
<< " " << body2
<< std::endl
;
1009 //do virtual term substitution
1010 body
= Rewriter::rewrite( body
);
1011 Trace("quant-vts-debug") << "Rewrite vts symbols in " << body
<< std::endl
;
1012 Node body_r
= d_term_db
->rewriteVtsSymbols( body
);
1013 Trace("quant-vts-debug") << " ...result: " << body_r
<< std::endl
;
1019 Node
QuantifiersEngine::getInstantiation( Node q
, InstMatch
& m
, bool doVts
){
1020 std::vector
< Node
> vars
;
1021 std::vector
< Node
> terms
;
1022 computeTermVector( q
, m
, vars
, terms
);
1023 return getInstantiation( q
, vars
, terms
, doVts
);
1026 Node
QuantifiersEngine::getInstantiation( Node q
, std::vector
< Node
>& terms
, bool doVts
) {
1027 Assert( d_term_db
->d_vars
.find( q
)!=d_term_db
->d_vars
.end() );
1028 return getInstantiation( q
, d_term_db
->d_vars
[q
], terms
, doVts
);
1032 bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq ){
1033 if( options::incrementalSolving() ){
1034 if( d_c_inst_match_trie.find( f )!=d_c_inst_match_trie.end() ){
1035 if( d_c_inst_match_trie[f]->existsInstMatch( this, f, m, getUserContext(), modEq ) ){
1040 if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){
1041 if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq ) ){
1050 bool QuantifiersEngine::addLemma( Node lem
, bool doCache
, bool doRewrite
){
1053 lem
= Rewriter::rewrite(lem
);
1055 Trace("inst-add-debug") << "Adding lemma : " << lem
<< std::endl
;
1056 BoolMap::const_iterator itp
= d_lemmas_produced_c
.find( lem
);
1057 if( itp
==d_lemmas_produced_c
.end() || !(*itp
).second
){
1058 //d_curr_out->lemma( lem, false, true );
1059 d_lemmas_produced_c
[ lem
] = true;
1060 d_lemmas_waiting
.push_back( lem
);
1061 Trace("inst-add-debug") << "Added lemma" << std::endl
;
1064 Trace("inst-add-debug") << "Duplicate." << std::endl
;
1068 //do not need to rewrite, will be rewritten after sending
1069 d_lemmas_waiting
.push_back( lem
);
1074 bool QuantifiersEngine::removeLemma( Node lem
) {
1075 std::vector
< Node
>::iterator it
= std::find( d_lemmas_waiting
.begin(), d_lemmas_waiting
.end(), lem
);
1076 if( it
!=d_lemmas_waiting
.end() ){
1077 d_lemmas_waiting
.erase( it
, it
+ 1 );
1078 d_lemmas_produced_c
[ lem
] = false;
1085 void QuantifiersEngine::addRequirePhase( Node lit
, bool req
){
1086 d_phase_req_waiting
[lit
] = req
;
1089 bool QuantifiersEngine::addInstantiation( Node q
, InstMatch
& m
, bool mkRep
, bool modEq
, bool doVts
){
1090 std::vector
< Node
> terms
;
1091 m
.getTerms( q
, terms
);
1092 return addInstantiation( q
, terms
, mkRep
, modEq
, doVts
);
1095 bool QuantifiersEngine::addInstantiation( Node q
, std::vector
< Node
>& terms
, bool mkRep
, bool modEq
, bool doVts
) {
1096 // For resource-limiting (also does a time check).
1097 getOutputChannel().safePoint(options::quantifierStep());
1098 Assert( !d_conflict
);
1099 Assert( terms
.size()==q
[0].getNumChildren() );
1100 Trace("inst-add-debug") << "For quantified formula " << q
<< ", add instantiation: " << std::endl
;
1101 std::vector
< Node
> rlv_cond
;
1102 for( unsigned i
=0; i
<terms
.size(); i
++ ){
1103 Trace("inst-add-debug") << " " << q
[0][i
];
1104 Trace("inst-add-debug2") << " -> " << terms
[i
];
1105 if( terms
[i
].isNull() ){
1106 terms
[i
] = d_term_db
->getModelBasisTerm( q
[0][i
].getType() );
1109 //pick the best possible representative for instantiation, based on past use and simplicity of term
1110 terms
[i
] = getInternalRepresentative( terms
[i
], q
, i
);
1112 //ensure the type is correct
1113 terms
[i
] = quantifiers::TermDb::ensureType( terms
[i
], q
[0][i
].getType() );
1115 Trace("inst-add-debug") << " -> " << terms
[i
] << std::endl
;
1116 if( terms
[i
].isNull() ){
1117 Trace("inst-add-debug") << " --> Failed to make term vector, due to term/type restrictions." << std::endl
;
1120 //get relevancy conditions
1121 if( options::instRelevantCond() ){
1122 quantifiers::TermDb::getRelevancyCondition( terms
[i
], rlv_cond
);
1125 #ifdef CVC4_ASSERTIONS
1126 bool bad_inst
= false;
1127 if( quantifiers::TermDb::containsUninterpretedConstant( terms
[i
] ) ){
1128 Trace("inst") << "***& inst contains uninterpreted constant : " << terms
[i
] << std::endl
;
1130 }else if( !terms
[i
].getType().isSubtypeOf( q
[0][i
].getType() ) ){
1131 Trace("inst") << "***& inst bad type : " << terms
[i
] << " " << terms
[i
].getType() << "/" << q
[0][i
].getType() << std::endl
;
1133 }else if( options::cbqi() ){
1134 Node icf
= quantifiers::TermDb::getInstConstAttr(terms
[i
]);
1135 if( !icf
.isNull() ){
1137 Trace("inst") << "***& inst contains inst constant attr : " << terms
[i
] << std::endl
;
1139 }else if( quantifiers::TermDb::containsTerms( terms
[i
], d_term_db
->d_inst_constants
[q
] ) ){
1140 Trace("inst") << "***& inst contains inst constants : " << terms
[i
] << std::endl
;
1145 //this assertion is critical to soundness
1147 Trace("inst")<< "***& Bad Instantiate " << q
<< " with " << std::endl
;
1148 for( unsigned j
=0; j
<terms
.size(); j
++ ){
1149 Trace("inst") << " " << terms
[j
] << std::endl
;
1156 //check based on instantiation level
1157 if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
1158 for( unsigned i
=0; i
<terms
.size(); i
++ ){
1159 if( !d_term_db
->isTermEligibleForInstantiation( terms
[i
], q
, true ) ){
1165 //check for positive entailment
1166 if( options::instNoEntail() ){
1167 //TODO: check consistency of equality engine (if not aborting on utility's reset)
1168 std::map
< TNode
, TNode
> subs
;
1169 for( unsigned i
=0; i
<terms
.size(); i
++ ){
1170 subs
[q
[0][i
]] = terms
[i
];
1172 if( d_term_db
->isEntailed( q
[1], subs
, false, true ) ){
1173 Trace("inst-add-debug") << " --> Currently entailed." << std::endl
;
1174 ++(d_statistics
.d_inst_duplicate_ent
);
1177 //Node eval = d_term_db->evaluateTerm( q[1], subs, false, true );
1178 //Trace("inst-add-debug2") << "Instantiation evaluates to : " << std::endl;
1179 //Trace("inst-add-debug2") << " " << eval << std::endl;
1182 //check for term vector duplication
1183 bool alreadyExists
= !recordInstantiationInternal( q
, terms
, modEq
);
1184 if( alreadyExists
){
1185 Trace("inst-add-debug") << " --> Already exists." << std::endl
;
1186 ++(d_statistics
.d_inst_duplicate_eq
);
1190 //construct the instantiation
1191 Trace("inst-add-debug") << "Constructing instantiation..." << std::endl
;
1192 Assert( d_term_db
->d_vars
[q
].size()==terms
.size() );
1193 Node body
= getInstantiation( q
, d_term_db
->d_vars
[q
], terms
, doVts
); //do virtual term substitution
1194 Node orig_body
= body
;
1195 if( options::cbqiNestedQE() && d_i_cbqi
){
1196 body
= d_i_cbqi
->doNestedQE( q
, terms
, body
, doVts
);
1198 body
= quantifiers::QuantifiersRewriter::preprocess( body
, true );
1199 Trace("inst-debug") << "...preprocess to " << body
<< std::endl
;
1201 //construct the lemma
1202 Trace("inst-assert") << "(assert " << body
<< ")" << std::endl
;
1203 body
= Rewriter::rewrite(body
);
1205 if( d_useModelEe
&& options::instNoModelTrue() ){
1206 Node val_body
= d_model
->getValue( body
);
1207 if( val_body
==d_term_db
->d_true
){
1208 Trace("inst-add-debug") << " --> True in model." << std::endl
;
1209 ++(d_statistics
.d_inst_duplicate_model_true
);
1215 if( rlv_cond
.empty() ){
1216 lem
= NodeManager::currentNM()->mkNode( kind::OR
, q
.negate(), body
);
1218 rlv_cond
.push_back( q
.negate() );
1219 rlv_cond
.push_back( body
);
1220 lem
= NodeManager::currentNM()->mkNode( kind::OR
, rlv_cond
);
1222 lem
= Rewriter::rewrite(lem
);
1224 //check for lemma duplication
1225 if( addLemma( lem
, true, false ) ){
1226 d_total_inst_debug
[q
]++;
1227 d_temp_inst_debug
[q
]++;
1228 d_total_inst_count_debug
++;
1229 if( Trace
.isOn("inst") ){
1230 Trace("inst") << "*** Instantiate " << q
<< " with " << std::endl
;
1231 for( unsigned i
=0; i
<terms
.size(); i
++ ){
1232 if( Trace
.isOn("inst") ){
1233 Trace("inst") << " " << terms
[i
];
1234 if( Trace
.isOn("inst-debug") ){
1235 Trace("inst-debug") << ", type=" << terms
[i
].getType() << ", var_type=" << q
[0][i
].getType();
1237 Trace("inst") << std::endl
;
1241 if( options::instMaxLevel()!=-1 ){
1243 //virtual term substitution/instantiation level features are incompatible
1246 uint64_t maxInstLevel
= 0;
1247 for( unsigned i
=0; i
<terms
.size(); i
++ ){
1248 if( terms
[i
].hasAttribute(InstLevelAttribute()) ){
1249 if( terms
[i
].getAttribute(InstLevelAttribute())>maxInstLevel
){
1250 maxInstLevel
= terms
[i
].getAttribute(InstLevelAttribute());
1254 setInstantiationLevelAttr( orig_body
, q
[1], maxInstLevel
+1 );
1257 if( d_curr_effort_level
>QEFFORT_CONFLICT
&& d_curr_effort_level
<QEFFORT_NONE
){
1259 for( unsigned j
=0; j
<d_inst_notify
.size(); j
++ ){
1260 if( !d_inst_notify
[j
]->notifyInstantiation( d_curr_effort_level
, q
, lem
, terms
, body
) ){
1261 Trace("inst-add-debug") << "...we are in conflict." << std::endl
;
1263 Assert( !d_lemmas_waiting
.empty() );
1268 if( options::trackInstLemmas() ){
1270 if( options::incrementalSolving() ){
1271 recorded
= d_c_inst_match_trie
[q
]->recordInstLemma( q
, terms
, lem
);
1273 recorded
= d_inst_match_trie
[q
].recordInstLemma( q
, terms
, lem
);
1275 Trace("inst-add-debug") << "...was recorded : " << recorded
<< std::endl
;
1278 Trace("inst-add-debug") << " --> Success." << std::endl
;
1279 ++(d_statistics
.d_instantiations
);
1282 Trace("inst-add-debug") << " --> Lemma already exists." << std::endl
;
1283 ++(d_statistics
.d_inst_duplicate
);
1288 bool QuantifiersEngine::removeInstantiation( Node q
, Node lem
, std::vector
< Node
>& terms
) {
1289 //lem must occur in d_waiting_lemmas
1290 if( removeLemma( lem
) ){
1291 return removeInstantiationInternal( q
, terms
);
1297 bool QuantifiersEngine::addSplit( Node n
, bool reqPhase
, bool reqPhasePol
){
1298 n
= Rewriter::rewrite( n
);
1299 Node lem
= NodeManager::currentNM()->mkNode( OR
, n
, n
.notNode() );
1300 if( addLemma( lem
) ){
1301 Debug("inst") << "*** Add split " << n
<< std::endl
;
1307 bool QuantifiersEngine::addSplitEquality( Node n1
, Node n2
, bool reqPhase
, bool reqPhasePol
){
1308 //Assert( !areEqual( n1, n2 ) );
1309 //Assert( !areDisequal( n1, n2 ) );
1310 Node fm
= NodeManager::currentNM()->mkNode( EQUAL
, n1
, n2
);
1311 return addSplit( fm
);
1314 bool QuantifiersEngine::addEPRAxiom( TypeNode tn
) {
1316 Assert( !options::incrementalSolving() );
1317 if( d_qepr
->isEPR( tn
) && !d_qepr
->hasEPRAxiom( tn
) ){
1318 Node lem
= d_qepr
->mkEPRAxiom( tn
);
1319 Trace("quant-epr") << "EPR lemma for " << tn
<< " : " << lem
<< std::endl
;
1320 getOutputChannel().lemma( lem
);
1326 void QuantifiersEngine::markRelevant( Node q
) {
1327 d_model
->markRelevant( q
);
1330 void QuantifiersEngine::setConflict() {
1332 d_conflict_c
= true;
1335 bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e
) {
1336 Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter
<< ", " << d_ierCounter_lc
<< std::endl
;
1337 //determine if we should perform check, based on instWhenMode
1338 bool performCheck
= false;
1339 if( options::instWhenMode()==quantifiers::INST_WHEN_FULL
){
1340 performCheck
= ( e
>= Theory::EFFORT_FULL
);
1341 }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY
){
1342 performCheck
= ( e
>= Theory::EFFORT_FULL
) && !getTheoryEngine()->needCheck();
1343 }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL
){
1344 performCheck
= ( ( e
==Theory::EFFORT_FULL
&& d_ierCounter
%d_inst_when_phase
!=0 ) || e
==Theory::EFFORT_LAST_CALL
);
1345 }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL
){
1346 performCheck
= ( ( e
==Theory::EFFORT_FULL
&& !getTheoryEngine()->needCheck() && d_ierCounter
%d_inst_when_phase
!=0 ) || e
==Theory::EFFORT_LAST_CALL
);
1347 }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL
){
1348 performCheck
= ( e
>= Theory::EFFORT_LAST_CALL
);
1350 performCheck
= true;
1352 if( e
==Theory::EFFORT_LAST_CALL
){
1353 //with bounded integers, skip every other last call,
1354 // since matching loops may occur with infinite quantification
1355 if( d_ierCounter_lc
%2==0 && options::fmfBound() ){
1356 performCheck
= false;
1359 return performCheck
;
1362 quantifiers::UserPatMode
QuantifiersEngine::getInstUserPatMode() {
1363 if( options::userPatternsQuant()==quantifiers::USER_PAT_MODE_INTERLEAVE
){
1364 return d_ierCounter
%2==0 ? quantifiers::USER_PAT_MODE_USE
: quantifiers::USER_PAT_MODE_RESORT
;
1366 return options::userPatternsQuant();
1370 void QuantifiersEngine::flushLemmas(){
1371 if( !d_lemmas_waiting
.empty() ){
1372 //filter based on notify classes
1373 if( !d_inst_notify
.empty() ){
1374 unsigned prev_lem_sz
= d_lemmas_waiting
.size();
1375 for( unsigned j
=0; j
<d_inst_notify
.size(); j
++ ){
1376 d_inst_notify
[j
]->filterInstantiations();
1378 if( prev_lem_sz
!=d_lemmas_waiting
.size() ){
1379 Trace("quant-engine") << "...filtered instances : " << d_lemmas_waiting
.size() << " / " << prev_lem_sz
<< std::endl
;
1382 //take default output channel if none is provided
1383 d_hasAddedLemma
= true;
1384 for( unsigned i
=0; i
<d_lemmas_waiting
.size(); i
++ ){
1385 Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting
[i
] << std::endl
;
1386 getOutputChannel().lemma( d_lemmas_waiting
[i
], false, true );
1388 d_lemmas_waiting
.clear();
1390 if( !d_phase_req_waiting
.empty() ){
1391 for( std::map
< Node
, bool >::iterator it
= d_phase_req_waiting
.begin(); it
!= d_phase_req_waiting
.end(); ++it
){
1392 Trace("qe-lemma") << "Require phase : " << it
->first
<< " -> " << it
->second
<< std::endl
;
1393 getOutputChannel().requirePhase( it
->first
, it
->second
);
1395 d_phase_req_waiting
.clear();
1399 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector
< Node
>& active_lemmas
) {
1400 //only if unsat core available
1401 bool isUnsatCoreAvailable
= false;
1402 if( options::proof() ){
1403 isUnsatCoreAvailable
= ProofManager::currentPM()->unsatCoreAvailable();
1405 if( isUnsatCoreAvailable
){
1406 Trace("inst-unsat-core") << "Get instantiations in unsat core..." << std::endl
;
1407 ProofManager::currentPM()->getLemmasInUnsatCore(theory::THEORY_QUANTIFIERS
, active_lemmas
);
1408 if( Trace
.isOn("inst-unsat-core") ){
1409 Trace("inst-unsat-core") << "Quantifiers lemmas in unsat core: " << std::endl
;
1410 for (unsigned i
= 0; i
< active_lemmas
.size(); ++i
) {
1411 Trace("inst-unsat-core") << " " << active_lemmas
[i
] << std::endl
;
1413 Trace("inst-unsat-core") << std::endl
;
1421 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector
< Node
>& active_lemmas
, std::map
< Node
, Node
>& weak_imp
) {
1422 if( getUnsatCoreLemmas( active_lemmas
) ){
1423 for (unsigned i
= 0; i
< active_lemmas
.size(); ++i
) {
1424 Node n
= ProofManager::currentPM()->getWeakestImplicantInUnsatCore(active_lemmas
[i
]);
1425 if( n
!=active_lemmas
[i
] ){
1426 Trace("inst-unsat-core") << " weaken : " << active_lemmas
[i
] << " -> " << n
<< std::endl
;
1428 weak_imp
[active_lemmas
[i
]] = n
;
1436 void QuantifiersEngine::getInstantiationTermVectors( Node q
, std::vector
< std::vector
< Node
> >& tvecs
) {
1437 std::vector
< Node
> lemmas
;
1438 getInstantiations( q
, lemmas
);
1439 std::map
< Node
, Node
> quant
;
1440 std::map
< Node
, std::vector
< Node
> > tvec
;
1441 getExplanationForInstLemmas( lemmas
, quant
, tvec
);
1442 for( std::map
< Node
, std::vector
< Node
> >::iterator it
= tvec
.begin(); it
!= tvec
.end(); ++it
){
1443 tvecs
.push_back( it
->second
);
1447 void QuantifiersEngine::getInstantiationTermVectors( std::map
< Node
, std::vector
< std::vector
< Node
> > >& insts
) {
1448 if( options::incrementalSolving() ){
1449 for( std::map
< Node
, inst::CDInstMatchTrie
* >::iterator it
= d_c_inst_match_trie
.begin(); it
!= d_c_inst_match_trie
.end(); ++it
){
1450 getInstantiationTermVectors( it
->first
, insts
[it
->first
] );
1453 for( std::map
< Node
, inst::InstMatchTrie
>::iterator it
= d_inst_match_trie
.begin(); it
!= d_inst_match_trie
.end(); ++it
){
1454 getInstantiationTermVectors( it
->first
, insts
[it
->first
] );
1459 void QuantifiersEngine::getExplanationForInstLemmas( std::vector
< Node
>& lems
, std::map
< Node
, Node
>& quant
, std::map
< Node
, std::vector
< Node
> >& tvec
) {
1460 if( options::trackInstLemmas() ){
1461 if( options::incrementalSolving() ){
1462 for( std::map
< Node
, inst::CDInstMatchTrie
* >::iterator it
= d_c_inst_match_trie
.begin(); it
!= d_c_inst_match_trie
.end(); ++it
){
1463 it
->second
->getExplanationForInstLemmas( it
->first
, lems
, quant
, tvec
);
1466 for( std::map
< Node
, inst::InstMatchTrie
>::iterator it
= d_inst_match_trie
.begin(); it
!= d_inst_match_trie
.end(); ++it
){
1467 it
->second
.getExplanationForInstLemmas( it
->first
, lems
, quant
, tvec
);
1470 #ifdef CVC4_ASSERTIONS
1471 for( unsigned j
=0; j
<lems
.size(); j
++ ){
1472 Assert( quant
.find( lems
[j
] )!=quant
.end() );
1473 Assert( tvec
.find( lems
[j
] )!=tvec
.end() );
1481 void QuantifiersEngine::printInstantiations( std::ostream
& out
) {
1482 bool useUnsatCore
= false;
1483 std::vector
< Node
> active_lemmas
;
1484 if( options::trackInstLemmas() && getUnsatCoreLemmas( active_lemmas
) ){
1485 useUnsatCore
= true;
1488 bool printed
= false;
1489 for( BoolMap::iterator it
= d_skolemized
.begin(); it
!= d_skolemized
.end(); ++it
){
1490 Node q
= (*it
).first
;
1492 out
<< "(skolem " << q
<< std::endl
;
1494 for( unsigned i
=0; i
<d_term_db
->d_skolem_constants
[q
].size(); i
++ ){
1495 if( i
>0 ){ out
<< " "; }
1496 out
<< d_term_db
->d_skolem_constants
[q
][i
];
1498 out
<< " )" << std::endl
;
1499 out
<< ")" << std::endl
;
1501 if( options::incrementalSolving() ){
1502 for( std::map
< Node
, inst::CDInstMatchTrie
* >::iterator it
= d_c_inst_match_trie
.begin(); it
!= d_c_inst_match_trie
.end(); ++it
){
1503 bool firstTime
= true;
1504 it
->second
->print( out
, it
->first
, firstTime
, useUnsatCore
, active_lemmas
);
1506 out
<< ")" << std::endl
;
1508 printed
= printed
|| !firstTime
;
1511 for( std::map
< Node
, inst::InstMatchTrie
>::iterator it
= d_inst_match_trie
.begin(); it
!= d_inst_match_trie
.end(); ++it
){
1512 bool firstTime
= true;
1513 it
->second
.print( out
, it
->first
, firstTime
, useUnsatCore
, active_lemmas
);
1515 out
<< ")" << std::endl
;
1517 printed
= printed
|| !firstTime
;
1521 out
<< "No instantiations" << std::endl
;
1525 void QuantifiersEngine::printSynthSolution( std::ostream
& out
) {
1527 d_ceg_inst
->printSynthSolution( out
);
1529 out
<< "Internal error : module for synth solution not found." << std::endl
;
1533 void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector
< Node
>& qs
) {
1534 if( options::incrementalSolving() ){
1535 for( std::map
< Node
, inst::CDInstMatchTrie
* >::iterator it
= d_c_inst_match_trie
.begin(); it
!= d_c_inst_match_trie
.end(); ++it
){
1536 qs
.push_back( it
->first
);
1539 for( std::map
< Node
, inst::InstMatchTrie
>::iterator it
= d_inst_match_trie
.begin(); it
!= d_inst_match_trie
.end(); ++it
){
1540 qs
.push_back( it
->first
);
1545 void QuantifiersEngine::getInstantiations( std::map
< Node
, std::vector
< Node
> >& insts
) {
1546 bool useUnsatCore
= false;
1547 std::vector
< Node
> active_lemmas
;
1548 if( options::trackInstLemmas() && getUnsatCoreLemmas( active_lemmas
) ){
1549 useUnsatCore
= true;
1552 if( options::incrementalSolving() ){
1553 for( std::map
< Node
, inst::CDInstMatchTrie
* >::iterator it
= d_c_inst_match_trie
.begin(); it
!= d_c_inst_match_trie
.end(); ++it
){
1554 it
->second
->getInstantiations( insts
[it
->first
], it
->first
, this, useUnsatCore
, active_lemmas
);
1557 for( std::map
< Node
, inst::InstMatchTrie
>::iterator it
= d_inst_match_trie
.begin(); it
!= d_inst_match_trie
.end(); ++it
){
1558 it
->second
.getInstantiations( insts
[it
->first
], it
->first
, this, useUnsatCore
, active_lemmas
);
1563 void QuantifiersEngine::getInstantiations( Node q
, std::vector
< Node
>& insts
) {
1564 if( options::incrementalSolving() ){
1565 std::map
< Node
, inst::CDInstMatchTrie
* >::iterator it
= d_c_inst_match_trie
.find( q
);
1566 if( it
!=d_c_inst_match_trie
.end() ){
1567 std::vector
< Node
> active_lemmas
;
1568 it
->second
->getInstantiations( insts
, it
->first
, this, false, active_lemmas
);
1571 std::map
< Node
, inst::InstMatchTrie
>::iterator it
= d_inst_match_trie
.find( q
);
1572 if( it
!=d_inst_match_trie
.end() ){
1573 std::vector
< Node
> active_lemmas
;
1574 it
->second
.getInstantiations( insts
, it
->first
, this, false, active_lemmas
);
1579 Node
QuantifiersEngine::getInstantiatedConjunction( Node q
) {
1580 Assert( q
.getKind()==FORALL
);
1581 std::vector
< Node
> insts
;
1582 getInstantiations( q
, insts
);
1583 if( insts
.empty() ){
1584 return NodeManager::currentNM()->mkConst(true);
1587 if( insts
.size()==1 ){
1590 ret
= NodeManager::currentNM()->mkNode( kind::AND
, insts
);
1592 //have to remove q, TODO: avoid this in a better way
1594 TNode tt
= d_term_db
->d_true
;
1595 ret
= ret
.substitute( tq
, tt
);
1600 QuantifiersEngine::Statistics::Statistics()
1601 : d_time("theory::QuantifiersEngine::time"),
1602 d_qcf_time("theory::QuantifiersEngine::time_qcf"),
1603 d_ematching_time("theory::QuantifiersEngine::time_ematching"),
1604 d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
1605 d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
1606 d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
1607 d_instantiations("QuantifiersEngine::Instantiations_Total", 0),
1608 d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0),
1609 d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0),
1610 d_inst_duplicate_ent("QuantifiersEngine::Duplicate_Inst_Entailed", 0),
1611 d_inst_duplicate_model_true("QuantifiersEngine::Duplicate_Inst_Model_True", 0),
1612 d_triggers("QuantifiersEngine::Triggers", 0),
1613 d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
1614 d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
1615 d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
1616 d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0),
1617 d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0),
1618 d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0),
1619 d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0),
1620 d_instantiations_qcf("QuantifiersEngine::Instantiations_Qcf_Conflict", 0),
1621 d_instantiations_qcf_prop("QuantifiersEngine::Instantiations_Qcf_Prop", 0),
1622 d_instantiations_fmf_exh("QuantifiersEngine::Instantiations_Fmf_Exh", 0),
1623 d_instantiations_fmf_mbqi("QuantifiersEngine::Instantiations_Fmf_Mbqi", 0),
1624 d_instantiations_cbqi("QuantifiersEngine::Instantiations_Cbqi", 0),
1625 d_instantiations_rr("QuantifiersEngine::Instantiations_Rewrite_Rules", 0)
1627 smtStatisticsRegistry()->registerStat(&d_time
);
1628 smtStatisticsRegistry()->registerStat(&d_qcf_time
);
1629 smtStatisticsRegistry()->registerStat(&d_ematching_time
);
1630 smtStatisticsRegistry()->registerStat(&d_num_quant
);
1631 smtStatisticsRegistry()->registerStat(&d_instantiation_rounds
);
1632 smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc
);
1633 smtStatisticsRegistry()->registerStat(&d_instantiations
);
1634 smtStatisticsRegistry()->registerStat(&d_inst_duplicate
);
1635 smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq
);
1636 smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent
);
1637 smtStatisticsRegistry()->registerStat(&d_inst_duplicate_model_true
);
1638 smtStatisticsRegistry()->registerStat(&d_triggers
);
1639 smtStatisticsRegistry()->registerStat(&d_simple_triggers
);
1640 smtStatisticsRegistry()->registerStat(&d_multi_triggers
);
1641 smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations
);
1642 smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv
);
1643 smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns
);
1644 smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen
);
1645 smtStatisticsRegistry()->registerStat(&d_instantiations_guess
);
1646 smtStatisticsRegistry()->registerStat(&d_instantiations_qcf
);
1647 smtStatisticsRegistry()->registerStat(&d_instantiations_qcf_prop
);
1648 smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_exh
);
1649 smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_mbqi
);
1650 smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi
);
1651 smtStatisticsRegistry()->registerStat(&d_instantiations_rr
);
1654 QuantifiersEngine::Statistics::~Statistics(){
1655 smtStatisticsRegistry()->unregisterStat(&d_time
);
1656 smtStatisticsRegistry()->unregisterStat(&d_qcf_time
);
1657 smtStatisticsRegistry()->unregisterStat(&d_ematching_time
);
1658 smtStatisticsRegistry()->unregisterStat(&d_num_quant
);
1659 smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds
);
1660 smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc
);
1661 smtStatisticsRegistry()->unregisterStat(&d_instantiations
);
1662 smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate
);
1663 smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq
);
1664 smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent
);
1665 smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_model_true
);
1666 smtStatisticsRegistry()->unregisterStat(&d_triggers
);
1667 smtStatisticsRegistry()->unregisterStat(&d_simple_triggers
);
1668 smtStatisticsRegistry()->unregisterStat(&d_multi_triggers
);
1669 smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations
);
1670 smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv
);
1671 smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns
);
1672 smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen
);
1673 smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess
);
1674 smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf
);
1675 smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf_prop
);
1676 smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_exh
);
1677 smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_mbqi
);
1678 smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi
);
1679 smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr
);
1682 eq::EqualityEngine
* QuantifiersEngine::getMasterEqualityEngine(){
1683 return d_te
->getMasterEqualityEngine();
1686 eq::EqualityEngine
* QuantifiersEngine::getActiveEqualityEngine() {
1688 return d_model
->d_equalityEngine
;
1690 return d_te
->getMasterEqualityEngine();
1694 Node
QuantifiersEngine::getInternalRepresentative( Node a
, Node q
, int index
){
1695 bool prevModelEe
= d_useModelEe
;
1696 d_useModelEe
= false;
1697 Node ret
= d_eq_query
->getInternalRepresentative( a
, q
, index
);
1698 d_useModelEe
= prevModelEe
;
1702 void QuantifiersEngine::debugPrintEqualityEngine( const char * c
) {
1703 eq::EqualityEngine
* ee
= getActiveEqualityEngine();
1704 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( ee
);
1705 std::map
< TypeNode
, int > typ_num
;
1706 while( !eqcs_i
.isFinished() ){
1707 TNode r
= (*eqcs_i
);
1708 TypeNode tr
= r
.getType();
1709 if( typ_num
.find( tr
)==typ_num
.end() ){
1713 bool firstTime
= true;
1714 Trace(c
) << " " << r
;
1715 Trace(c
) << " : { ";
1716 eq::EqClassIterator eqc_i
= eq::EqClassIterator( r
, ee
);
1717 while( !eqc_i
.isFinished() ){
1721 Trace(c
) << std::endl
;
1724 Trace(c
) << " " << n
<< std::endl
;
1728 if( !firstTime
){ Trace(c
) << " "; }
1729 Trace(c
) << "}" << std::endl
;
1732 Trace(c
) << std::endl
;
1733 for( std::map
< TypeNode
, int >::iterator it
= typ_num
.begin(); it
!= typ_num
.end(); ++it
){
1734 Trace(c
) << "# eqc for " << it
->first
<< " : " << it
->second
<< std::endl
;
1739 EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( context::Context
* c
, QuantifiersEngine
* qe
) : d_qe( qe
), d_eqi_counter( c
), d_reset_count( 0 ){
1740 if( options::inferArithTriggerEq() ){
1741 d_eq_inference
= new quantifiers::EqualityInference( c
, options::inferArithTriggerEqExp() );
1743 d_eq_inference
= NULL
;
1747 EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){
1748 delete d_eq_inference
;
1751 bool EqualityQueryQuantifiersEngine::reset( Theory::Effort e
){
1754 return processInferences( e
);
1757 bool EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e
) {
1758 if( options::inferArithTriggerEq() ){
1759 eq::EqualityEngine
* ee
= getEngine();
1760 //updated implementation
1761 while( d_eqi_counter
.get()<d_eq_inference
->getNumPendingMerges() ){
1762 Node eq
= d_eq_inference
->getPendingMerge( d_eqi_counter
.get() );
1763 Node eq_exp
= d_eq_inference
->getPendingMergeExplanation( d_eqi_counter
.get() );
1764 Trace("quant-engine-ee-proc") << "processInferences : Infer : " << eq
<< std::endl
;
1765 Trace("quant-engine-ee-proc") << " explanation : " << eq_exp
<< std::endl
;
1766 Assert( ee
->hasTerm( eq
[0] ) );
1767 Assert( ee
->hasTerm( eq
[1] ) );
1768 if( areDisequal( eq
[0], eq
[1] ) ){
1769 Trace("quant-engine-ee-proc") << "processInferences : Conflict : " << eq
<< std::endl
;
1770 if( Trace
.isOn("term-db-lemma") ){
1771 Trace("term-db-lemma") << "Disequal terms, equal by normalization : " << eq
[0] << " " << eq
[1] << "!!!!" << std::endl
;
1772 if( !d_qe
->getTheoryEngine()->needCheck() ){
1773 Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl
;
1774 //this should really never happen (implies arithmetic is incomplete when sharing is enabled)
1777 Trace("term-db-lemma") << " add split on : " << eq
<< std::endl
;
1779 d_qe
->addSplit( eq
);
1782 ee
->assertEquality( eq
, true, eq_exp
);
1783 d_eqi_counter
= d_eqi_counter
.get() + 1;
1786 Assert( ee
->consistent() );
1791 bool EqualityQueryQuantifiersEngine::hasTerm( Node a
){
1792 return getEngine()->hasTerm( a
);
1795 Node
EqualityQueryQuantifiersEngine::getRepresentative( Node a
){
1796 eq::EqualityEngine
* ee
= getEngine();
1797 if( ee
->hasTerm( a
) ){
1798 return ee
->getRepresentative( a
);
1804 bool EqualityQueryQuantifiersEngine::areEqual( Node a
, Node b
){
1808 eq::EqualityEngine
* ee
= getEngine();
1809 if( ee
->hasTerm( a
) && ee
->hasTerm( b
) ){
1810 return ee
->areEqual( a
, b
);
1817 bool EqualityQueryQuantifiersEngine::areDisequal( Node a
, Node b
){
1821 eq::EqualityEngine
* ee
= getEngine();
1822 if( ee
->hasTerm( a
) && ee
->hasTerm( b
) ){
1823 return ee
->areDisequal( a
, b
, false );
1825 return a
.isConst() && b
.isConst();
1830 Node
EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a
, Node f
, int index
){
1831 Assert( f
.isNull() || f
.getKind()==FORALL
);
1832 Node r
= getRepresentative( a
);
1833 if( options::finiteModelFind() ){
1834 if( r
.isConst() && quantifiers::TermDb::containsUninterpretedConstant( r
) ){
1835 //map back from values assigned by model, if any
1836 if( d_qe
->getModel() ){
1837 std::map
< Node
, Node
>::iterator it
= d_qe
->getModel()->d_rep_set
.d_values_to_terms
.find( r
);
1838 if( it
!=d_qe
->getModel()->d_rep_set
.d_values_to_terms
.end() ){
1840 r
= getRepresentative( r
);
1842 if( r
.getType().isSort() ){
1843 Trace("internal-rep-warn") << "No representative for UF constant." << std::endl
;
1844 //should never happen : UF constants should never escape model
1851 if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_EE
){
1854 TypeNode v_tn
= f
.isNull() ? a
.getType() : f
[0][index
].getType();
1855 std::map
< Node
, Node
>::iterator itir
= d_int_rep
[v_tn
].find( r
);
1856 if( itir
==d_int_rep
[v_tn
].end() ){
1857 //find best selection for representative
1859 //if( options::fmfRelevantDomain() && !f.isNull() ){
1860 // Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl;
1861 // r_best = d_qe->getRelevantDomain()->getRelevantTerm( f, index, r );
1862 // Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl;
1864 std::vector
< Node
> eqc
;
1865 getEquivalenceClass( r
, eqc
);
1866 Trace("internal-rep-select") << "Choose representative for equivalence class : { ";
1867 for( unsigned i
=0; i
<eqc
.size(); i
++ ){
1868 if( i
>0 ) Trace("internal-rep-select") << ", ";
1869 Trace("internal-rep-select") << eqc
[i
];
1871 Trace("internal-rep-select") << " }, type = " << v_tn
<< std::endl
;
1872 int r_best_score
= -1;
1873 for( size_t i
=0; i
<eqc
.size(); i
++ ){
1874 int score
= getRepScore( eqc
[i
], f
, index
, v_tn
);
1876 if( r_best
.isNull() || ( score
>=0 && ( r_best_score
<0 || score
<r_best_score
) ) ){
1878 r_best_score
= score
;
1882 if( r_best
.isNull() ){
1883 Trace("internal-rep-warn") << "No valid choice for representative in eqc class." << std::endl
;
1886 //now, make sure that no other member of the class is an instance
1887 std::unordered_map
<TNode
, Node
, TNodeHashFunction
> cache
;
1888 r_best
= getInstance( r_best
, eqc
, cache
);
1889 //store that this representative was chosen at this point
1890 if( d_rep_score
.find( r_best
)==d_rep_score
.end() ){
1891 d_rep_score
[ r_best
] = d_reset_count
;
1893 Trace("internal-rep-select") << "...Choose " << r_best
<< " with score " << r_best_score
<< std::endl
;
1894 Assert( r_best
.getType().isSubtypeOf( v_tn
) );
1895 d_int_rep
[v_tn
][r
] = r_best
;
1897 Trace("internal-rep-debug") << "rep( " << a
<< " ) = " << r
<< ", " << std::endl
;
1898 Trace("internal-rep-debug") << "int_rep( " << a
<< " ) = " << r_best
<< ", " << std::endl
;
1902 return itir
->second
;
1907 void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map
< TypeNode
, std::vector
< Node
> >& reps
) {
1908 //make sure internal representatives currently exist
1909 for( std::map
< TypeNode
, std::vector
< Node
> >::iterator it
= reps
.begin(); it
!= reps
.end(); ++it
){
1910 if( it
->first
.isSort() ){
1911 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
1912 Node r
= getInternalRepresentative( it
->second
[i
], Node::null(), 0 );
1916 Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl
;
1917 for( std::map
< TypeNode
, std::map
< Node
, Node
> >::iterator itt
= d_int_rep
.begin(); itt
!= d_int_rep
.end(); ++itt
){
1918 for( std::map
< Node
, Node
>::iterator it
= itt
->second
.begin(); it
!= itt
->second
.end(); ++it
){
1919 Trace("internal-rep-flatten") << itt
->first
<< " : irep( " << it
->first
<< " ) = " << it
->second
<< std::endl
;
1922 //store representatives for newly created terms
1923 std::map
< Node
, Node
> temp_rep_map
;
1928 for( std::map
< TypeNode
, std::map
< Node
, Node
> >::iterator itt
= d_int_rep
.begin(); itt
!= d_int_rep
.end(); ++itt
){
1929 for( std::map
< Node
, Node
>::iterator it
= itt
->second
.begin(); it
!= itt
->second
.end(); ++it
){
1930 if( it
->second
.getKind()==APPLY_UF
&& it
->second
.getType().isSort() ){
1931 Node ni
= it
->second
;
1932 std::vector
< Node
> cc
;
1933 cc
.push_back( it
->second
.getOperator() );
1934 bool changed
= false;
1935 for( unsigned j
=0; j
<ni
.getNumChildren(); j
++ ){
1936 if( ni
[j
].getType().isSort() ){
1937 Node r
= getRepresentative( ni
[j
] );
1938 if( itt
->second
.find( r
)==itt
->second
.end() ){
1939 Assert( temp_rep_map
.find( r
)!=temp_rep_map
.end() );
1940 r
= temp_rep_map
[r
];
1943 //found sub-term as instance
1944 Trace("internal-rep-flatten-debug") << "...Changed " << it
->second
<< " to subterm " << ni
[j
] << std::endl
;
1945 itt
->second
[it
->first
] = ni
[j
];
1950 Node ir
= itt
->second
[r
];
1962 Node n
= NodeManager::currentNM()->mkNode( APPLY_UF
, cc
);
1963 Trace("internal-rep-flatten-debug") << "...Changed " << it
->second
<< " to " << n
<< std::endl
;
1965 itt
->second
[it
->first
] = n
;
1966 temp_rep_map
[n
] = it
->first
;
1972 Trace("internal-rep-flatten") << "---After flattening : " << std::endl
;
1973 for( std::map
< TypeNode
, std::map
< Node
, Node
> >::iterator itt
= d_int_rep
.begin(); itt
!= d_int_rep
.end(); ++itt
){
1974 for( std::map
< Node
, Node
>::iterator it
= itt
->second
.begin(); it
!= itt
->second
.end(); ++it
){
1975 Trace("internal-rep-flatten") << itt
->first
<< " : irep( " << it
->first
<< " ) = " << it
->second
<< std::endl
;
1980 eq::EqualityEngine
* EqualityQueryQuantifiersEngine::getEngine(){
1981 return d_qe
->getActiveEqualityEngine();
1984 void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a
, std::vector
< Node
>& eqc
){
1985 eq::EqualityEngine
* ee
= getEngine();
1986 if( ee
->hasTerm( a
) ){
1987 Node rep
= ee
->getRepresentative( a
);
1988 eq::EqClassIterator
eqc_iter( rep
, ee
);
1989 while( !eqc_iter
.isFinished() ){
1990 eqc
.push_back( *eqc_iter
);
1996 //a should be in its equivalence class
1997 Assert( std::find( eqc
.begin(), eqc
.end(), a
)!=eqc
.end() );
2000 TNode
EqualityQueryQuantifiersEngine::getCongruentTerm( Node f
, std::vector
< TNode
>& args
) {
2001 return d_qe
->getTermDatabase()->getCongruentTerm( f
, args
);
2006 Node
EqualityQueryQuantifiersEngine::getInstance( Node n
, const std::vector
< Node
>& eqc
, std::unordered_map
<TNode
, Node
, TNodeHashFunction
>& cache
){
2007 if(cache
.find(n
) != cache
.end()) {
2010 for( size_t i
=0; i
<n
.getNumChildren(); i
++ ){
2011 Node nn
= getInstance( n
[i
], eqc
, cache
);
2013 return cache
[n
] = nn
;
2016 if( std::find( eqc
.begin(), eqc
.end(), n
)!=eqc
.end() ){
2017 return cache
[n
] = n
;
2019 return cache
[n
] = Node::null();
2023 //-2 : invalid, -1 : undesired, otherwise : smaller the score, the better
2024 int EqualityQueryQuantifiersEngine::getRepScore( Node n
, Node f
, int index
, TypeNode v_tn
){
2025 if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n
) ){ //reject
2027 }else if( !n
.getType().isSubtypeOf( v_tn
) ){ //reject if incorrect type
2029 }else if( options::lteRestrictInstClosure() && ( !d_qe
->getTermDatabase()->isInstClosure( n
) || !d_qe
->getTermDatabase()->hasTermCurrent( n
, false ) ) ){
2031 }else if( options::instMaxLevel()!=-1 ){
2032 //score prefer lowest instantiation level
2033 if( n
.hasAttribute(InstLevelAttribute()) ){
2034 return n
.getAttribute(InstLevelAttribute());
2036 return options::instLevelInputOnly() ? -1 : 0;
2039 if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_FIRST
){
2040 //score prefers earliest use of this term as a representative
2041 return d_rep_score
.find( n
)==d_rep_score
.end() ? -1 : d_rep_score
[n
];
2043 Assert( options::quantRepMode()==quantifiers::QUANT_REP_MODE_DEPTH
);
2044 return quantifiers::TermDb::getTermDepth( n
);