1 /********************* */
2 /*! \file quantifiers_engine.cpp
4 ** Original author: Morgan Deters
5 ** Major contributors: Andrew Reynolds
6 ** Minor contributors (to current version): Francois Bobot
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Implementation of quantifiers engine class
15 #include "theory/quantifiers_engine.h"
16 #include "theory/theory_engine.h"
17 #include "theory/uf/theory_uf_strong_solver.h"
18 #include "theory/uf/equality_engine.h"
19 #include "theory/arrays/theory_arrays.h"
20 #include "theory/datatypes/theory_datatypes.h"
21 #include "theory/quantifiers/quantifiers_rewriter.h"
22 #include "theory/quantifiers/options.h"
23 #include "theory/quantifiers/model_engine.h"
24 #include "theory/quantifiers/instantiation_engine.h"
25 #include "theory/quantifiers/first_order_model.h"
26 #include "theory/quantifiers/term_database.h"
27 #include "theory/quantifiers/trigger.h"
28 #include "theory/quantifiers/bounded_integers.h"
29 #include "theory/quantifiers/rewrite_engine.h"
30 #include "theory/quantifiers/quant_conflict_find.h"
31 #include "theory/quantifiers/conjecture_generator.h"
32 #include "theory/quantifiers/ce_guided_instantiation.h"
33 #include "theory/quantifiers/local_theory_ext.h"
34 #include "theory/quantifiers/relevant_domain.h"
35 #include "theory/uf/options.h"
36 #include "theory/uf/theory_uf.h"
37 #include "theory/quantifiers/full_model_check.h"
38 #include "theory/quantifiers/ambqi_builder.h"
42 using namespace CVC4::kind
;
43 using namespace CVC4::context
;
44 using namespace CVC4::theory
;
45 using namespace CVC4::theory::inst
;
48 eq::EqualityEngine
* QuantifiersModule::getEqualityEngine() {
49 return d_quantEngine
->getMasterEqualityEngine();
52 bool QuantifiersModule::areEqual( TNode n1
, TNode n2
) {
53 eq::EqualityEngine
* ee
= getEqualityEngine();
54 return n1
==n2
|| ( ee
->hasTerm( n1
) && ee
->hasTerm( n2
) && ee
->areEqual( n1
, n2
) );
57 bool QuantifiersModule::areDisequal( TNode n1
, TNode n2
) {
58 eq::EqualityEngine
* ee
= getEqualityEngine();
59 return n1
!=n2
&& ee
->hasTerm( n1
) && ee
->hasTerm( n2
) && ee
->areDisequal( n1
, n2
, false );
62 TNode
QuantifiersModule::getRepresentative( TNode n
) {
63 eq::EqualityEngine
* ee
= getEqualityEngine();
64 if( ee
->hasTerm( n
) ){
65 return ee
->getRepresentative( n
);
71 quantifiers::TermDb
* QuantifiersModule::getTermDatabase() {
72 return d_quantEngine
->getTermDatabase();
75 QuantifiersEngine::QuantifiersEngine(context::Context
* c
, context::UserContext
* u
, TheoryEngine
* te
):
77 d_lemmas_produced_c(u
){
78 d_eq_query
= new EqualityQueryQuantifiersEngine( this );
79 d_term_db
= new quantifiers::TermDb( c
, u
, this );
80 d_tr_trie
= new inst::TriggerTrie
;
81 //d_rr_tr_trie = new rrinst::TriggerTrie;
82 //d_eem = new EfficientEMatcher( this );
83 d_hasAddedLemma
= false;
85 bool needsBuilder
= false;
87 Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl
;
90 if( options::mbqiMode()==quantifiers::MBQI_FMC
||
91 options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL
|| options::fmfBoundInt() ||
92 options::mbqiMode()==quantifiers::MBQI_TRUST
){
93 d_model
= new quantifiers::fmcheck::FirstOrderModelFmc( this, c
, "FirstOrderModelFmc" );
94 }else if( options::mbqiMode()==quantifiers::MBQI_ABS
){
95 d_model
= new quantifiers::FirstOrderModelAbs( this, c
, "FirstOrderModelAbs" );
97 d_model
= new quantifiers::FirstOrderModelIG( this, c
, "FirstOrderModelIG" );
99 if( !options::finiteModelFind() ){
100 d_rel_dom
= new quantifiers::RelevantDomain( this, d_model
);
104 if( options::relevantTriggers() ){
105 d_quant_rel
= new QuantRelevance( false );
110 //add quantifiers modules
111 if( options::quantConflictFind() || options::quantRewriteRules() ){
112 d_qcf
= new quantifiers::QuantConflictFind( this, c
);
113 d_modules
.push_back( d_qcf
);
117 if( options::conjectureGen() ){
118 d_sg_gen
= new quantifiers::ConjectureGenerator( this, c
);
119 d_modules
.push_back( d_sg_gen
);
123 if( !options::finiteModelFind() || options::fmfInstEngine() ){
124 //the instantiation must set incomplete flag unless finite model finding is turned on
125 d_inst_engine
= new quantifiers::InstantiationEngine( this, !options::finiteModelFind() );
126 d_modules
.push_back( d_inst_engine
);
128 d_inst_engine
= NULL
;
130 if( options::finiteModelFind() ){
131 if( options::fmfBoundInt() ){
132 d_bint
= new quantifiers::BoundedIntegers( c
, this );
133 d_modules
.push_back( d_bint
);
137 d_model_engine
= new quantifiers::ModelEngine( c
, this );
138 d_modules
.push_back( d_model_engine
);
141 d_model_engine
= NULL
;
144 if( options::quantRewriteRules() ){
145 d_rr_engine
= new quantifiers::RewriteEngine( c
, this );
146 d_modules
.push_back(d_rr_engine
);
150 if( options::ceGuidedInst() ){
151 d_ceg_inst
= new quantifiers::CegInstantiation( this, c
);
152 d_modules
.push_back( d_ceg_inst
);
157 if( options::ltePartialInst() ){
158 d_lte_part_inst
= new quantifiers::LtePartialInst( this, c
);
159 d_modules
.push_back( d_lte_part_inst
);
161 d_lte_part_inst
= NULL
;
165 Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl
;
166 if( options::mbqiMode()==quantifiers::MBQI_FMC
|| options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL
||
167 options::mbqiMode()==quantifiers::MBQI_TRUST
|| options::fmfBoundInt() ){
168 Trace("quant-engine-debug") << "...make fmc builder." << std::endl
;
169 d_builder
= new quantifiers::fmcheck::FullModelChecker( c
, this );
170 }else if( options::mbqiMode()==quantifiers::MBQI_ABS
){
171 Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl
;
172 d_builder
= new quantifiers::AbsMbqiBuilder( c
, this );
174 Trace("quant-engine-debug") << "...make default model builder." << std::endl
;
175 d_builder
= new quantifiers::QModelBuilderDefault( c
, this );
181 d_total_inst_count_debug
= 0;
186 QuantifiersEngine::~QuantifiersEngine(){
190 delete d_model_engine
;
191 delete d_inst_engine
;
201 delete d_lte_part_inst
;
202 for(std::map
< Node
, QuantPhaseReq
* >::iterator i
= d_phase_reqs
.begin(); i
!= d_phase_reqs
.end(); ++i
) {
207 EqualityQueryQuantifiersEngine
* QuantifiersEngine::getEqualityQuery() {
211 context::Context
* QuantifiersEngine::getSatContext(){
212 return d_te
->theoryOf( THEORY_QUANTIFIERS
)->getSatContext();
215 context::Context
* QuantifiersEngine::getUserContext(){
216 return d_te
->theoryOf( THEORY_QUANTIFIERS
)->getUserContext();
219 OutputChannel
& QuantifiersEngine::getOutputChannel(){
220 return d_te
->theoryOf( THEORY_QUANTIFIERS
)->getOutputChannel();
222 /** get default valuation for the quantifiers engine */
223 Valuation
& QuantifiersEngine::getValuation(){
224 return d_te
->theoryOf( THEORY_QUANTIFIERS
)->getValuation();
227 void QuantifiersEngine::finishInit(){
228 for( int i
=0; i
<(int)d_modules
.size(); i
++ ){
229 d_modules
[i
]->finishInit();
233 QuantifiersModule
* QuantifiersEngine::getOwner( Node q
) {
234 std::map
< Node
, QuantifiersModule
* >::iterator it
= d_owner
.find( q
);
235 if( it
==d_owner
.end() ){
242 void QuantifiersEngine::setOwner( Node q
, QuantifiersModule
* m
) {
243 QuantifiersModule
* mo
= getOwner( q
);
246 Trace("quant-warn") << "WARNING: setting owner of " << q
<< " to " << ( m
? m
->identify() : "null" ) << ", but already has owner " << mo
->identify() << "!" << std::endl
;
252 bool QuantifiersEngine::hasOwnership( Node q
, QuantifiersModule
* m
) {
253 QuantifiersModule
* mo
= getOwner( q
);
254 return mo
==m
|| mo
==NULL
;
257 void QuantifiersEngine::check( Theory::Effort e
){
258 CodeTimer
codeTimer(d_time
);
259 if( !getMasterEqualityEngine()->consistent() ){
260 Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl
;
263 if( e
==Theory::EFFORT_FULL
){
265 }else if( e
==Theory::EFFORT_LAST_CALL
){
268 bool needsCheck
= !d_lemmas_waiting
.empty();
269 bool needsModel
= false;
270 bool needsFullModel
= false;
271 std::vector
< QuantifiersModule
* > qm
;
272 if( d_model
->checkNeeded() ){
273 needsCheck
= needsCheck
|| e
>=Theory::EFFORT_LAST_CALL
; //always need to check at or above last call
274 for( int i
=0; i
<(int)d_modules
.size(); i
++ ){
275 if( d_modules
[i
]->needsCheck( e
) ){
276 qm
.push_back( d_modules
[i
] );
278 if( d_modules
[i
]->needsModel( e
) ){
280 if( d_modules
[i
]->needsFullModel( e
) ){
281 needsFullModel
= true;
288 Trace("quant-engine") << "Quantifiers Engine check, level = " << e
<< std::endl
;
289 if( Trace
.isOn("quant-engine-debug") ){
290 Trace("quant-engine-debug") << " modules to check : ";
291 for( unsigned i
=0; i
<qm
.size(); i
++ ){
292 Trace("quant-engine-debug") << qm
[i
]->identify() << " ";
294 Trace("quant-engine-debug") << std::endl
;
295 Trace("quant-engine-debug") << " # quantified formulas = " << d_model
->getNumAssertedQuantifiers() << std::endl
;
296 if( d_model
->getNumToReduceQuantifiers()>0 ){
297 Trace("quant-engine-debug") << " # quantified formulas to reduce = " << d_model
->getNumToReduceQuantifiers() << std::endl
;
299 if( !d_lemmas_waiting
.empty() ){
300 Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting
.size() << std::endl
;
302 Trace("quant-engine-debug") << " Theory engine finished : " << !d_te
->needCheck() << std::endl
;
303 Trace("quant-engine-debug") << "Resetting all modules..." << std::endl
;
305 if( Trace
.isOn("quant-engine-ee") ){
306 Trace("quant-engine-ee") << "Equality engine : " << std::endl
;
307 debugPrintEqualityEngine( "quant-engine-ee" );
310 //reset relevant information
312 d_hasAddedLemma
= false;
314 //flush previous lemmas (for instance, if was interupted), or other lemmas to process
316 if( d_hasAddedLemma
){
320 Trace("quant-engine-debug2") << "Reset term db..." << std::endl
;
321 d_term_db
->reset( e
);
326 d_model
->reset_round();
327 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
328 Trace("quant-engine-debug2") << "Reset " << d_modules
[i
]->identify().c_str() << std::endl
;
329 d_modules
[i
]->reset_round( e
);
331 Trace("quant-engine-debug") << "Done resetting all modules." << std::endl
;
333 if( e
==Theory::EFFORT_LAST_CALL
){
334 //if effort is last call, try to minimize model first FIXME: remove?
335 uf::StrongSolverTheoryUF
* ufss
= ((uf::TheoryUF
*)getTheoryEngine()->theoryOf( THEORY_UF
))->getStrongSolver();
336 if( ufss
&& !ufss
->minimize() ){
339 ++(d_statistics
.d_instantiation_rounds_lc
);
340 }else if( e
==Theory::EFFORT_FULL
){
341 ++(d_statistics
.d_instantiation_rounds
);
344 Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl
;
345 for( unsigned quant_e
= QEFFORT_CONFLICT
; quant_e
<=QEFFORT_MODEL
; quant_e
++ ){
347 //build the model if any module requested it
348 if( quant_e
==QEFFORT_MODEL
&& needsModel
){
349 Assert( d_builder
!=NULL
);
350 Trace("quant-engine-debug") << "Build model, fullModel = " << ( needsFullModel
|| d_builder
->optBuildAtFullModel() ) << "..." << std::endl
;
351 d_builder
->d_addedLemmas
= 0;
352 d_builder
->buildModel( d_model
, needsFullModel
|| d_builder
->optBuildAtFullModel() );
353 //we are done if model building was unsuccessful
354 if( d_builder
->d_addedLemmas
>0 ){
360 for( unsigned i
=0; i
<qm
.size(); i
++ ){
361 Trace("quant-engine-debug") << "Check " << qm
[i
]->identify().c_str() << " at effort " << quant_e
<< "..." << std::endl
;
362 qm
[i
]->check( e
, quant_e
);
365 //flush all current lemmas
367 //if we have added one, stop
368 if( d_hasAddedLemma
){
370 //otherwise, complete the model generation if necessary
371 }else if( quant_e
==QEFFORT_MODEL
&& needsModel
&& options::produceModels() && !needsFullModel
&& !d_builder
->optBuildAtFullModel() ){
372 Trace("quant-engine-debug") << "Build completed model..." << std::endl
;
373 d_builder
->buildModel( d_model
, true );
376 Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl
;
377 if( d_hasAddedLemma
){
379 if( Trace
.isOn("inst-per-quant-round") ){
380 for( std::map
< Node
, int >::iterator it
= d_temp_inst_debug
.begin(); it
!= d_temp_inst_debug
.end(); ++it
){
381 Trace("inst-per-quant-round") << " * " << it
->second
<< " for " << it
->first
<< std::endl
;
382 d_temp_inst_debug
[it
->first
] = 0;
386 Trace("quant-engine") << "Finished quantifiers engine check." << std::endl
;
389 if( e
==Theory::EFFORT_LAST_CALL
&& !d_hasAddedLemma
){
390 if( options::produceModels() && !d_model
->isModelSet() ){
391 //use default model builder when no module built the model
392 Trace("quant-engine-debug") << "Build the model..." << std::endl
;
393 d_te
->getModelBuilder()->buildModel( d_model
, true );
394 Trace("quant-engine-debug") << "Done building the model." << std::endl
;
396 //check other sources of incompleteness
398 if( d_lte_part_inst
&& d_lte_part_inst
->wasInvoked() ){
402 getOutputChannel().setIncomplete();
405 if( Trace
.isOn("inst-per-quant") ){
406 for( std::map
< Node
, int >::iterator it
= d_total_inst_debug
.begin(); it
!= d_total_inst_debug
.end(); ++it
){
407 Trace("inst-per-quant") << " * " << it
->second
<< " for " << it
->first
<< std::endl
;
413 bool QuantifiersEngine::registerQuantifier( Node f
){
414 std::map
< Node
, bool >::iterator it
= d_quants
.find( f
);
415 if( it
==d_quants
.end() ){
416 Trace("quant") << "QuantifiersEngine : Register quantifier ";
417 Trace("quant") << " : " << f
<< std::endl
;
418 ++(d_statistics
.d_num_quant
);
419 Assert( f
.getKind()==FORALL
);
421 //check whether we should apply a reduction
422 bool reduced
= false;
423 if( d_lte_part_inst
&& !f
.getAttribute(LtePartialInstAttribute()) ){
424 Trace("lte-partial-inst") << "LTE: Partially instantiate " << f
<< "?" << std::endl
;
425 if( d_lte_part_inst
->addQuantifier( f
) ){
430 d_model
->assertQuantifier( f
, true );
434 //make instantiation constants for f
435 d_term_db
->makeInstantiationConstantsFor( f
);
436 d_term_db
->computeAttributes( f
);
437 QuantifiersModule
* qm
= getOwner( f
);
439 Trace("quant") << " Owner : " << qm
->identify() << std::endl
;
441 //register with quantifier relevance
443 d_quant_rel
->registerQuantifier( f
);
445 //register with each module
446 for( int i
=0; i
<(int)d_modules
.size(); i
++ ){
447 d_modules
[i
]->registerQuantifier( f
);
449 Node ceBody
= d_term_db
->getInstConstantBody( f
);
450 //generate the phase requirements
451 d_phase_reqs
[f
] = new QuantPhaseReq( ceBody
, true );
452 //also register it with the strong solver
453 if( options::finiteModelFind() ){
454 ((uf::TheoryUF
*)d_te
->theoryOf( THEORY_UF
))->getStrongSolver()->registerQuantifier( f
);
464 void QuantifiersEngine::registerPattern( std::vector
<Node
> & pattern
) {
465 for(std::vector
<Node
>::iterator p
= pattern
.begin(); p
!= pattern
.end(); ++p
){
466 std::set
< Node
> added
;
467 getTermDatabase()->addTerm( *p
, added
);
471 void QuantifiersEngine::assertQuantifier( Node f
, bool pol
){
474 if( d_skolemized
.find( f
)==d_skolemized
.end() ){
475 Node body
= d_term_db
->getSkolemizedBody( f
);
476 NodeBuilder
<> nb(kind::OR
);
477 nb
<< f
<< body
.notNode();
479 if( Trace
.isOn("quantifiers-sk") ){
480 Node slem
= Rewriter::rewrite( lem
);
481 Trace("quantifiers-sk") << "Skolemize lemma : " << slem
<< std::endl
;
483 getOutputChannel().lemma( lem
, false, true );
484 d_skolemized
[f
] = true;
487 //assert to modules TODO : handle !pol
489 //register the quantifier
490 bool nreduced
= registerQuantifier( f
);
491 //assert it to each module
493 d_model
->assertQuantifier( f
);
494 for( int i
=0; i
<(int)d_modules
.size(); i
++ ){
495 d_modules
[i
]->assertNode( f
);
501 void QuantifiersEngine::propagate( Theory::Effort level
){
502 CodeTimer
codeTimer(d_time
);
504 for( int i
=0; i
<(int)d_modules
.size(); i
++ ){
505 d_modules
[i
]->propagate( level
);
509 Node
QuantifiersEngine::getNextDecisionRequest(){
510 for( int i
=0; i
<(int)d_modules
.size(); i
++ ){
511 Node n
= d_modules
[i
]->getNextDecisionRequest();
519 quantifiers::TermDbSygus
* QuantifiersEngine::getTermDatabaseSygus() {
520 return getTermDatabase()->getTermDatabaseSygus();
523 void QuantifiersEngine::addTermToDatabase( Node n
, bool withinQuant
, bool withinInstClosure
){
524 std::set
< Node
> added
;
525 getTermDatabase()->addTerm( n
, added
, withinQuant
, withinInstClosure
);
526 //maybe have triggered instantiations if we are doing eager instantiation
527 if( options::eagerInstQuant() ){
530 //added contains also the Node that just have been asserted in this branch
532 for( std::set
< Node
>::iterator i
=added
.begin(), end
=added
.end(); i
!=end
; i
++ ){
534 d_quant_rel
->setRelevance( i
->getOperator(), 0 );
540 void QuantifiersEngine::computeTermVector( Node f
, InstMatch
& m
, std::vector
< Node
>& vars
, std::vector
< Node
>& terms
){
541 for( size_t i
=0; i
<f
[0].getNumChildren(); i
++ ){
544 vars
.push_back( f
[0][i
] );
545 terms
.push_back( n
);
550 bool QuantifiersEngine::addInstantiation( Node f
, std::vector
< Node
>& vars
, std::vector
< Node
>& terms
){
551 Assert( f
.getKind()==FORALL
);
552 Assert( vars
.size()==terms
.size() );
553 Node body
= getInstantiation( f
, vars
, terms
);
554 Trace("inst-assert") << "(assert " << body
<< ")" << std::endl
;
556 NodeBuilder
<> nb(kind::OR
);
557 nb
<< f
.notNode() << body
;
559 //check for duplication
560 if( addLemma( lem
) ){
561 d_total_inst_debug
[f
]++;
562 d_temp_inst_debug
[f
]++;
563 d_total_inst_count_debug
++;
564 Trace("inst") << "*** Instantiate " << f
<< " with " << std::endl
;
565 for( int i
=0; i
<(int)terms
.size(); i
++ ){
566 Trace("inst") << " " << terms
[i
];
567 Trace("inst") << std::endl
;
568 Assert( terms
[i
].getType().isSubtypeOf( f
[0][i
].getType() ) );
570 if( options::cbqi() && !options::cbqi2() ){
571 for( int i
=0; i
<(int)terms
.size(); i
++ ){
572 if( quantifiers::TermDb::hasInstConstAttr(terms
[i
]) ){
573 Debug("inst")<< "***& Bad Instantiate " << f
<< " with " << std::endl
;
574 for( int i
=0; i
<(int)terms
.size(); i
++ ){
575 Debug("inst") << " " << terms
[i
] << std::endl
;
577 Unreachable("Bad instantiation");
581 if( options::instMaxLevel()!=-1 ){
582 uint64_t maxInstLevel
= 0;
583 for( int i
=0; i
<(int)terms
.size(); i
++ ){
584 if( terms
[i
].hasAttribute(InstLevelAttribute()) ){
585 if( terms
[i
].getAttribute(InstLevelAttribute())>maxInstLevel
){
586 maxInstLevel
= terms
[i
].getAttribute(InstLevelAttribute());
590 setInstantiationLevelAttr( body
, f
[1], maxInstLevel
+1 );
592 ++(d_statistics
.d_instantiations
);
595 ++(d_statistics
.d_inst_duplicate
);
600 void QuantifiersEngine::setInstantiationLevelAttr( Node n
, Node qn
, uint64_t level
){
601 Trace("inst-level-debug2") << "IL : " << n
<< " " << qn
<< " " << level
<< std::endl
;
602 //if not from the vector of terms we instantiatied
603 if( qn
.getKind()!=BOUND_VARIABLE
&& n
!=qn
){
604 //if this is a new term, without an instantiation level
605 if( !n
.hasAttribute(InstLevelAttribute()) ){
606 InstLevelAttribute ila
;
607 n
.setAttribute(ila
,level
);
608 Trace("inst-level-debug") << "Set instantiation level " << n
<< " to " << level
<< std::endl
;
610 Assert( n
.getNumChildren()==qn
.getNumChildren() );
611 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
612 setInstantiationLevelAttr( n
[i
], qn
[i
], level
);
617 void QuantifiersEngine::setInstantiationLevelAttr( Node n
, uint64_t level
){
618 if( !n
.hasAttribute(InstLevelAttribute()) ){
619 InstLevelAttribute ila
;
620 n
.setAttribute(ila
,level
);
621 Trace("inst-level-debug") << "Set instantiation level " << n
<< " to " << level
<< std::endl
;
623 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
624 setInstantiationLevelAttr( n
[i
], level
);
628 Node
QuantifiersEngine::getSubstitute( Node n
, std::vector
< Node
>& terms
){
629 if( n
.getKind()==INST_CONSTANT
){
630 Debug("check-inst") << "Substitute inst constant : " << n
<< std::endl
;
631 return terms
[n
.getAttribute(InstVarNumAttribute())];
633 //if( !quantifiers::TermDb::hasInstConstAttr( n ) ){
634 //Debug("check-inst") << "No inst const attr : " << n << std::endl;
637 //Debug("check-inst") << "Recurse on : " << n << std::endl;
638 std::vector
< Node
> cc
;
639 if( n
.getMetaKind() == kind::metakind::PARAMETERIZED
){
640 cc
.push_back( n
.getOperator() );
642 bool changed
= false;
643 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
644 Node c
= getSubstitute( n
[i
], terms
);
646 changed
= changed
|| c
!=n
[i
];
649 Node ret
= NodeManager::currentNM()->mkNode( n
.getKind(), cc
);
658 Node
QuantifiersEngine::getInstantiation( Node f
, std::vector
< Node
>& vars
, std::vector
< Node
>& terms
){
660 //process partial instantiation if necessary
661 if( d_term_db
->d_vars
[f
].size()!=vars
.size() ){
662 body
= f
[ 1 ].substitute( vars
.begin(), vars
.end(), terms
.begin(), terms
.end() );
663 std::vector
< Node
> uninst_vars
;
664 //doing a partial instantiation, must add quantifier for all uninstantiated variables
665 for( int i
=0; i
<(int)f
[0].getNumChildren(); i
++ ){
666 if( std::find( vars
.begin(), vars
.end(), f
[0][i
] )==vars
.end() ){
667 uninst_vars
.push_back( f
[0][i
] );
670 Node bvl
= NodeManager::currentNM()->mkNode( BOUND_VAR_LIST
, uninst_vars
);
671 body
= NodeManager::currentNM()->mkNode( FORALL
, bvl
, body
);
672 Trace("partial-inst") << "Partial instantiation : " << f
<< std::endl
;
673 Trace("partial-inst") << " : " << body
<< std::endl
;
675 if( options::cbqi() ){
676 body
= f
[ 1 ].substitute( vars
.begin(), vars
.end(), terms
.begin(), terms
.end() );
678 //do optimized version
679 Node icb
= d_term_db
->getInstConstantBody( f
);
680 body
= getSubstitute( icb
, terms
);
681 if( Debug
.isOn("check-inst") ){
682 Node body2
= f
[ 1 ].substitute( vars
.begin(), vars
.end(), terms
.begin(), terms
.end() );
684 Debug("check-inst") << "Substitution is wrong : " << body
<< " " << body2
<< std::endl
;
692 Node
QuantifiersEngine::getInstantiation( Node f
, InstMatch
& m
){
693 std::vector
< Node
> vars
;
694 std::vector
< Node
> terms
;
695 computeTermVector( f
, m
, vars
, terms
);
696 return getInstantiation( f
, vars
, terms
);
699 Node
QuantifiersEngine::getInstantiation( Node f
, std::vector
< Node
>& terms
) {
700 return getInstantiation( f
, d_term_db
->d_inst_constants
[f
], terms
);
704 bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
705 if( options::incrementalSolving() ){
706 if( d_c_inst_match_trie.find( f )!=d_c_inst_match_trie.end() ){
707 if( d_c_inst_match_trie[f]->existsInstMatch( this, f, m, getUserContext(), modEq, modInst ) ){
712 if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){
713 if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, modInst ) ){
718 //also check model builder (it may contain instantiations internally)
719 if( d_builder && d_builder->existsInstantiation( f, m, modEq, modInst ) ){
726 bool QuantifiersEngine::addLemma( Node lem
, bool doCache
){
728 lem
= Rewriter::rewrite(lem
);
729 Trace("inst-add-debug2") << "Adding lemma : " << lem
<< std::endl
;
730 if( d_lemmas_produced_c
.find( lem
)==d_lemmas_produced_c
.end() ){
731 //d_curr_out->lemma( lem, false, true );
732 d_lemmas_produced_c
[ lem
] = true;
733 d_lemmas_waiting
.push_back( lem
);
734 Trace("inst-add-debug2") << "Added lemma : " << lem
<< std::endl
;
737 Trace("inst-add-debug2") << "Duplicate." << std::endl
;
741 d_lemmas_waiting
.push_back( lem
);
746 void QuantifiersEngine::addRequirePhase( Node lit
, bool req
){
747 d_phase_req_waiting
[lit
] = req
;
750 bool QuantifiersEngine::addInstantiation( Node f
, InstMatch
& m
, bool mkRep
, bool modEq
, bool modInst
){
751 std::vector
< Node
> terms
;
752 m
.getTerms( this, f
, terms
);
753 return addInstantiation( f
, terms
, mkRep
, modEq
, modInst
);
756 bool QuantifiersEngine::addInstantiation( Node f
, std::vector
< Node
>& terms
, bool mkRep
, bool modEq
, bool modInst
) {
757 // For resource-limiting (also does a time check).
758 getOutputChannel().safePoint();
760 Assert( terms
.size()==f
[0].getNumChildren() );
761 Trace("inst-add-debug") << "Add instantiation: ";
762 for( unsigned i
=0; i
<terms
.size(); i
++ ){
763 if( i
>0 ) Trace("inst-add-debug") << ", ";
764 Trace("inst-add-debug") << f
[0][i
] << " -> " << terms
[i
];
765 //make it representative, this is helpful for recognizing duplication
767 //pick the best possible representative for instantiation, based on past use and simplicity of term
768 terms
[i
] = d_eq_query
->getInternalRepresentative( terms
[i
], f
, i
);
769 Trace("inst-add-debug2") << " (" << terms
[i
] << ")";
772 Trace("inst-add-debug") << std::endl
;
774 //check based on instantiation level
775 if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
776 for( unsigned i
=0; i
<terms
.size(); i
++ ){
777 if( !d_term_db
->isTermEligibleForInstantiation( terms
[i
], f
, true ) ){
782 //check for entailment
783 if( options::instNoEntail() ){
784 std::map
< TNode
, TNode
> subs
;
785 for( unsigned i
=0; i
<terms
.size(); i
++ ){
786 subs
[f
[0][i
]] = terms
[i
];
788 if( d_term_db
->isEntailed( f
[1], subs
, false, true ) ){
789 Trace("inst-add-debug") << " -> Currently entailed." << std::endl
;
794 //check for duplication
795 bool alreadyExists
= false;
796 if( options::incrementalSolving() ){
797 Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq
<< ", modInst = " << modInst
<< std::endl
;
798 inst::CDInstMatchTrie
* imt
;
799 std::map
< Node
, inst::CDInstMatchTrie
* >::iterator it
= d_c_inst_match_trie
.find( f
);
800 if( it
!=d_c_inst_match_trie
.end() ){
803 imt
= new CDInstMatchTrie( getUserContext() );
804 d_c_inst_match_trie
[f
] = imt
;
806 alreadyExists
= !imt
->addInstMatch( this, f
, terms
, getUserContext(), modEq
, modInst
);
808 Trace("inst-add-debug") << "Adding into inst trie" << std::endl
;
809 alreadyExists
= !d_inst_match_trie
[f
].addInstMatch( this, f
, terms
, modEq
, modInst
);
812 Trace("inst-add-debug") << " -> Already exists." << std::endl
;
813 ++(d_statistics
.d_inst_duplicate_eq
);
818 //add the instantiation
819 Trace("inst-add-debug") << "Constructing instantiation..." << std::endl
;
820 bool addedInst
= addInstantiation( f
, d_term_db
->d_vars
[f
], terms
);
823 Trace("inst-add-debug") << " -> Success." << std::endl
;
826 Trace("inst-add-debug") << " -> Lemma already exists." << std::endl
;
832 bool QuantifiersEngine::addSplit( Node n
, bool reqPhase
, bool reqPhasePol
){
833 n
= Rewriter::rewrite( n
);
834 Node lem
= NodeManager::currentNM()->mkNode( OR
, n
, n
.notNode() );
835 if( addLemma( lem
) ){
836 Debug("inst") << "*** Add split " << n
<< std::endl
;
842 bool QuantifiersEngine::addSplitEquality( Node n1
, Node n2
, bool reqPhase
, bool reqPhasePol
){
843 //Assert( !areEqual( n1, n2 ) );
844 //Assert( !areDisequal( n1, n2 ) );
845 Kind knd
= n1
.getType()==NodeManager::currentNM()->booleanType() ? IFF
: EQUAL
;
846 Node fm
= NodeManager::currentNM()->mkNode( knd
, n1
, n2
);
847 return addSplit( fm
);
850 bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e
) {
851 //determine if we should perform check, based on instWhenMode
852 bool performCheck
= false;
853 if( options::instWhenMode()==quantifiers::INST_WHEN_FULL
){
854 performCheck
= ( e
>= Theory::EFFORT_FULL
);
855 }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY
){
856 performCheck
= ( e
>= Theory::EFFORT_FULL
) && !getTheoryEngine()->needCheck();
857 }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL
){
858 performCheck
= ( ( e
==Theory::EFFORT_FULL
&& d_ierCounter
%2==0 ) || e
==Theory::EFFORT_LAST_CALL
);
859 }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL
){
860 performCheck
= ( e
>= Theory::EFFORT_LAST_CALL
);
864 if( e
==Theory::EFFORT_LAST_CALL
){
865 //with bounded integers, skip every other last call,
866 // since matching loops may occur with infinite quantification
867 if( d_ierCounter_lc
%2==0 && options::fmfBoundInt() ){
868 performCheck
= false;
874 void QuantifiersEngine::flushLemmas(){
875 if( !d_lemmas_waiting
.empty() ){
876 //take default output channel if none is provided
877 d_hasAddedLemma
= true;
878 for( int i
=0; i
<(int)d_lemmas_waiting
.size(); i
++ ){
879 getOutputChannel().lemma( d_lemmas_waiting
[i
], false, true );
881 d_lemmas_waiting
.clear();
883 if( !d_phase_req_waiting
.empty() ){
884 for( std::map
< Node
, bool >::iterator it
= d_phase_req_waiting
.begin(); it
!= d_phase_req_waiting
.end(); ++it
){
885 getOutputChannel().requirePhase( it
->first
, it
->second
);
887 d_phase_req_waiting
.clear();
891 void QuantifiersEngine::getPhaseReqTerms( Node f
, std::vector
< Node
>& nodes
){
892 if( options::literalMatchMode()!=quantifiers::LITERAL_MATCH_NONE
&& d_phase_reqs
.find( f
)!=d_phase_reqs
.end() ){
893 // doing literal-based matching (consider polarity of literals)
894 for( int i
=0; i
<(int)nodes
.size(); i
++ ){
895 Node prev
= nodes
[i
];
896 if( d_phase_reqs
[f
]->isPhaseReq( nodes
[i
] ) ){
897 bool preq
= d_phase_reqs
[f
]->getPhaseReq( nodes
[i
] );
898 nodes
[i
] = NodeManager::currentNM()->mkNode( IFF
, nodes
[i
], NodeManager::currentNM()->mkConst
<bool>(preq
) );
900 //else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){
901 // Node req = qe->getPhaseReqEquality( f, trNodes[i] );
902 // trNodes[i] = NodeManager::currentNM()->mkNode( EQUAL, trNodes[i], req );
908 void QuantifiersEngine::printInstantiations( std::ostream
& out
) {
909 for( std::map
< Node
, bool >::iterator it
= d_skolemized
.begin(); it
!= d_skolemized
.end(); ++it
){
910 out
<< "Skolem constants of " << it
->first
<< " : " << std::endl
;
912 for( unsigned i
=0; i
<d_term_db
->d_skolem_constants
[it
->first
].size(); i
++ ){
913 if( i
>0 ){ out
<< ", "; }
914 out
<< d_term_db
->d_skolem_constants
[it
->first
][i
];
916 out
<< " )" << std::endl
;
919 if( options::incrementalSolving() ){
920 for( std::map
< Node
, inst::CDInstMatchTrie
* >::iterator it
= d_c_inst_match_trie
.begin(); it
!= d_c_inst_match_trie
.end(); ++it
){
921 out
<< "Instantiations of " << it
->first
<< " : " << std::endl
;
922 it
->second
->print( out
, it
->first
);
925 for( std::map
< Node
, inst::InstMatchTrie
>::iterator it
= d_inst_match_trie
.begin(); it
!= d_inst_match_trie
.end(); ++it
){
926 out
<< "Instantiations of " << it
->first
<< " : " << std::endl
;
927 it
->second
.print( out
, it
->first
);
933 void QuantifiersEngine::printSynthSolution( std::ostream
& out
) {
935 d_ceg_inst
->printSynthSolution( out
);
937 out
<< "Internal error : module for synth solution not found." << std::endl
;
941 QuantifiersEngine::Statistics::Statistics():
942 d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
943 d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
944 d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
945 d_instantiations("QuantifiersEngine::Instantiations_Total", 0),
946 d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0),
947 d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0),
948 d_triggers("QuantifiersEngine::Triggers", 0),
949 d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
950 d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
951 d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0)
953 StatisticsRegistry::registerStat(&d_num_quant
);
954 StatisticsRegistry::registerStat(&d_instantiation_rounds
);
955 StatisticsRegistry::registerStat(&d_instantiation_rounds_lc
);
956 StatisticsRegistry::registerStat(&d_instantiations
);
957 StatisticsRegistry::registerStat(&d_inst_duplicate
);
958 StatisticsRegistry::registerStat(&d_inst_duplicate_eq
);
959 StatisticsRegistry::registerStat(&d_triggers
);
960 StatisticsRegistry::registerStat(&d_simple_triggers
);
961 StatisticsRegistry::registerStat(&d_multi_triggers
);
962 StatisticsRegistry::registerStat(&d_multi_trigger_instantiations
);
965 QuantifiersEngine::Statistics::~Statistics(){
966 StatisticsRegistry::unregisterStat(&d_num_quant
);
967 StatisticsRegistry::unregisterStat(&d_instantiation_rounds
);
968 StatisticsRegistry::unregisterStat(&d_instantiation_rounds_lc
);
969 StatisticsRegistry::unregisterStat(&d_instantiations
);
970 StatisticsRegistry::unregisterStat(&d_inst_duplicate
);
971 StatisticsRegistry::unregisterStat(&d_inst_duplicate_eq
);
972 StatisticsRegistry::unregisterStat(&d_triggers
);
973 StatisticsRegistry::unregisterStat(&d_simple_triggers
);
974 StatisticsRegistry::unregisterStat(&d_multi_triggers
);
975 StatisticsRegistry::unregisterStat(&d_multi_trigger_instantiations
);
978 eq::EqualityEngine
* QuantifiersEngine::getMasterEqualityEngine(){
979 return getTheoryEngine()->getMasterEqualityEngine();
982 void QuantifiersEngine::debugPrintEqualityEngine( const char * c
) {
983 eq::EqualityEngine
* ee
= getMasterEqualityEngine();
984 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( ee
);
985 std::map
< TypeNode
, int > typ_num
;
986 while( !eqcs_i
.isFinished() ){
988 TypeNode tr
= r
.getType();
989 if( typ_num
.find( tr
)==typ_num
.end() ){
993 bool firstTime
= true;
994 Trace(c
) << " " << r
;
996 eq::EqClassIterator eqc_i
= eq::EqClassIterator( r
, ee
);
997 while( !eqc_i
.isFinished() ){
1001 Trace(c
) << std::endl
;
1004 Trace(c
) << " " << n
<< std::endl
;
1008 if( !firstTime
){ Trace(c
) << " "; }
1009 Trace(c
) << "}" << std::endl
;
1012 Trace(c
) << std::endl
;
1013 for( std::map
< TypeNode
, int >::iterator it
= typ_num
.begin(); it
!= typ_num
.end(); ++it
){
1014 Trace(c
) << "# eqc for " << it
->first
<< " : " << it
->second
<< std::endl
;
1018 void EqualityQueryQuantifiersEngine::reset(){
1023 bool EqualityQueryQuantifiersEngine::hasTerm( Node a
){
1024 return getEngine()->hasTerm( a
);
1027 Node
EqualityQueryQuantifiersEngine::getRepresentative( Node a
){
1028 eq::EqualityEngine
* ee
= getEngine();
1029 if( ee
->hasTerm( a
) ){
1030 return ee
->getRepresentative( a
);
1036 bool EqualityQueryQuantifiersEngine::areEqual( Node a
, Node b
){
1040 eq::EqualityEngine
* ee
= getEngine();
1042 return true;//!areDisequal( a, b );
1044 if( ee
->hasTerm( a
) && ee
->hasTerm( b
) ){
1045 if( ee
->areEqual( a
, b
) ){
1054 bool EqualityQueryQuantifiersEngine::areDisequal( Node a
, Node b
){
1055 eq::EqualityEngine
* ee
= getEngine();
1056 if( ee
->hasTerm( a
) && ee
->hasTerm( b
) ){
1057 if( ee
->areDisequal( a
, b
, false ) ){
1064 Node
EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a
, Node f
, int index
){
1065 Node r
= getRepresentative( a
);
1066 if( !options::internalReps() ){
1069 if( options::finiteModelFind() ){
1071 //map back from values assigned by model, if any
1072 if( d_qe
->getModel() ){
1073 std::map
< Node
, Node
>::iterator it
= d_qe
->getModel()->d_rep_set
.d_values_to_terms
.find( r
);
1074 if( it
!=d_qe
->getModel()->d_rep_set
.d_values_to_terms
.end() ){
1076 r
= getRepresentative( r
);
1078 if( r
.getType().isSort() ){
1079 Trace("internal-rep-warn") << "No representative for UF constant." << std::endl
;
1086 if( d_int_rep
.find( r
)==d_int_rep
.end() ){
1087 //find best selection for representative
1089 //if( options::fmfRelevantDomain() && !f.isNull() ){
1090 // Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl;
1091 // r_best = d_qe->getRelevantDomain()->getRelevantTerm( f, index, r );
1092 // Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl;
1094 std::vector
< Node
> eqc
;
1095 getEquivalenceClass( r
, eqc
);
1096 Trace("internal-rep-select") << "Choose representative for equivalence class : { ";
1097 for( unsigned i
=0; i
<eqc
.size(); i
++ ){
1098 if( i
>0 ) Trace("internal-rep-select") << ", ";
1099 Trace("internal-rep-select") << eqc
[i
];
1101 Trace("internal-rep-select") << " } " << std::endl
;
1102 int r_best_score
= -1;
1103 for( size_t i
=0; i
<eqc
.size(); i
++ ){
1104 int score
= getRepScore( eqc
[i
], f
, index
);
1106 if( r_best
.isNull() || ( score
>=0 && ( r_best_score
<0 || score
<r_best_score
) ) ){
1108 r_best_score
= score
;
1112 if( r_best
.isNull() ){
1114 Node ic
= d_qe
->getTermDatabase()->getInstantiationConstant( f
, index
);
1115 r_best
= d_qe
->getTermDatabase()->getFreeVariableForInstConstant( ic
);
1120 //now, make sure that no other member of the class is an instance
1121 std::hash_map
<TNode
, Node
, TNodeHashFunction
> cache
;
1122 r_best
= getInstance( r_best
, eqc
, cache
);
1123 //store that this representative was chosen at this point
1124 if( d_rep_score
.find( r_best
)==d_rep_score
.end() ){
1125 d_rep_score
[ r_best
] = d_reset_count
;
1127 Trace("internal-rep-select") << "...Choose " << r_best
<< std::endl
;
1128 d_int_rep
[r
] = r_best
;
1130 Trace("internal-rep-debug") << "rep( " << a
<< " ) = " << r
<< ", " << std::endl
;
1131 Trace("internal-rep-debug") << "int_rep( " << a
<< " ) = " << r_best
<< ", " << std::endl
;
1135 return d_int_rep
[r
];
1140 void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map
< TypeNode
, std::vector
< Node
> >& reps
) {
1141 //make sure internal representatives currently exist
1142 for( std::map
< TypeNode
, std::vector
< Node
> >::iterator it
= reps
.begin(); it
!= reps
.end(); ++it
){
1143 if( it
->first
.isSort() ){
1144 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
1145 Node r
= getInternalRepresentative( it
->second
[i
], Node::null(), 0 );
1149 Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl
;
1150 for( std::map
< Node
, Node
>::iterator it
= d_int_rep
.begin(); it
!= d_int_rep
.end(); ++it
){
1151 Trace("internal-rep-flatten") << it
->first
.getType() << " : irep( " << it
->first
<< " ) = " << it
->second
<< std::endl
;
1153 //store representatives for newly created terms
1154 std::map
< Node
, Node
> temp_rep_map
;
1159 for( std::map
< Node
, Node
>::iterator it
= d_int_rep
.begin(); it
!= d_int_rep
.end(); ++it
){
1160 if( it
->second
.getKind()==APPLY_UF
&& it
->second
.getType().isSort() ){
1161 Node ni
= it
->second
;
1162 std::vector
< Node
> cc
;
1163 cc
.push_back( it
->second
.getOperator() );
1164 bool changed
= false;
1165 for( unsigned j
=0; j
<ni
.getNumChildren(); j
++ ){
1166 if( ni
[j
].getType().isSort() ){
1167 Node r
= getRepresentative( ni
[j
] );
1168 if( d_int_rep
.find( r
)==d_int_rep
.end() ){
1169 Assert( temp_rep_map
.find( r
)!=temp_rep_map
.end() );
1170 r
= temp_rep_map
[r
];
1173 //found sub-term as instance
1174 Trace("internal-rep-flatten-debug") << "...Changed " << it
->second
<< " to subterm " << ni
[j
] << std::endl
;
1175 d_int_rep
[it
->first
] = ni
[j
];
1180 Node ir
= d_int_rep
[r
];
1192 Node n
= NodeManager::currentNM()->mkNode( APPLY_UF
, cc
);
1193 Trace("internal-rep-flatten-debug") << "...Changed " << it
->second
<< " to " << n
<< std::endl
;
1195 d_int_rep
[it
->first
] = n
;
1196 temp_rep_map
[n
] = it
->first
;
1201 Trace("internal-rep-flatten") << "---After flattening : " << std::endl
;
1202 for( std::map
< Node
, Node
>::iterator it
= d_int_rep
.begin(); it
!= d_int_rep
.end(); ++it
){
1203 Trace("internal-rep-flatten") << it
->first
.getType() << " : irep( " << it
->first
<< " ) = " << it
->second
<< std::endl
;
1207 eq::EqualityEngine
* EqualityQueryQuantifiersEngine::getEngine(){
1208 return d_qe
->getMasterEqualityEngine();
1211 void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a
, std::vector
< Node
>& eqc
){
1212 eq::EqualityEngine
* ee
= getEngine();
1213 if( ee
->hasTerm( a
) ){
1214 Node rep
= ee
->getRepresentative( a
);
1215 eq::EqClassIterator
eqc_iter( rep
, ee
);
1216 while( !eqc_iter
.isFinished() ){
1217 eqc
.push_back( *eqc_iter
);
1223 //a should be in its equivalence class
1224 Assert( std::find( eqc
.begin(), eqc
.end(), a
)!=eqc
.end() );
1229 Node
EqualityQueryQuantifiersEngine::getInstance( Node n
, const std::vector
< Node
>& eqc
, std::hash_map
<TNode
, Node
, TNodeHashFunction
>& cache
){
1230 if(cache
.find(n
) != cache
.end()) {
1233 for( size_t i
=0; i
<n
.getNumChildren(); i
++ ){
1234 Node nn
= getInstance( n
[i
], eqc
, cache
);
1236 return cache
[n
] = nn
;
1239 if( std::find( eqc
.begin(), eqc
.end(), n
)!=eqc
.end() ){
1240 return cache
[n
] = n
;
1242 return cache
[n
] = Node::null();
1246 int getDepth( Node n
){
1247 if( n
.getNumChildren()==0 ){
1251 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
1252 int depth
= getDepth( n
[i
] );
1253 if( depth
>maxDepth
){
1261 //smaller the score, the better
1262 int EqualityQueryQuantifiersEngine::getRepScore( Node n
, Node f
, int index
){
1263 if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n
) ){
1265 }else if( options::lteRestrictInstClosure() && ( !d_qe
->getTermDatabase()->isInstClosure( n
) || !d_qe
->getTermDatabase()->hasTermCurrent( n
, false ) ) ){
1267 }else if( options::instMaxLevel()!=-1 ){
1268 //score prefer lowest instantiation level
1269 if( n
.hasAttribute(InstLevelAttribute()) ){
1270 return n
.getAttribute(InstLevelAttribute());
1272 return options::instLevelInputOnly() ? -1 : 0;
1275 //score prefers earliest use of this term as a representative
1276 return d_rep_score
.find( n
)==d_rep_score
.end() ? -1 : d_rep_score
[n
];
1278 //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n ); //term depth