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/rewriterules/efficient_e_matching.h"
29 //#include "theory/rewriterules/rr_trigger.h"
30 #include "theory/quantifiers/bounded_integers.h"
31 #include "theory/quantifiers/rewrite_engine.h"
32 #include "theory/quantifiers/quant_conflict_find.h"
33 #include "theory/quantifiers/conjecture_generator.h"
34 #include "theory/quantifiers/relevant_domain.h"
35 #include "theory/uf/options.h"
36 #include "theory/uf/theory_uf.h"
40 using namespace CVC4::kind
;
41 using namespace CVC4::context
;
42 using namespace CVC4::theory
;
43 using namespace CVC4::theory::inst
;
45 QuantifiersEngine::QuantifiersEngine(context::Context
* c
, context::UserContext
* u
, TheoryEngine
* te
):
47 d_lemmas_produced_c(u
){
48 d_eq_query
= new EqualityQueryQuantifiersEngine( this );
49 d_term_db
= new quantifiers::TermDb( c
, u
, this );
50 d_tr_trie
= new inst::TriggerTrie
;
51 //d_rr_tr_trie = new rrinst::TriggerTrie;
52 //d_eem = new EfficientEMatcher( this );
53 d_hasAddedLemma
= false;
55 Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl
;
58 if( options::mbqiMode()==quantifiers::MBQI_FMC
||
59 options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL
|| options::fmfBoundInt() ||
60 options::mbqiMode()==quantifiers::MBQI_TRUST
){
61 d_model
= new quantifiers::fmcheck::FirstOrderModelFmc( this, c
, "FirstOrderModelFmc" );
62 }else if( options::mbqiMode()==quantifiers::MBQI_INTERVAL
){
63 d_model
= new quantifiers::FirstOrderModelQInt( this, c
, "FirstOrderModelQInt" );
64 }else if( options::mbqiMode()==quantifiers::MBQI_ABS
){
65 d_model
= new quantifiers::FirstOrderModelAbs( this, c
, "FirstOrderModelAbs" );
67 d_model
= new quantifiers::FirstOrderModelIG( this, c
, "FirstOrderModelIG" );
69 if( !options::finiteModelFind() ){
70 d_rel_dom
= new quantifiers::RelevantDomain( this, d_model
);
74 if( options::relevantTriggers() ){
75 d_quant_rel
= new QuantRelevance( false );
80 //add quantifiers modules
81 if( options::quantConflictFind() || options::quantRewriteRules() ){
82 d_qcf
= new quantifiers::QuantConflictFind( this, c
);
83 d_modules
.push_back( d_qcf
);
87 if( options::conjectureGen() ){
88 d_sg_gen
= new quantifiers::ConjectureGenerator( this, c
);
89 d_modules
.push_back( d_sg_gen
);
93 if( !options::finiteModelFind() || options::fmfInstEngine() ){
94 //the instantiation must set incomplete flag unless finite model finding is turned on
95 d_inst_engine
= new quantifiers::InstantiationEngine( this, !options::finiteModelFind() );
96 d_modules
.push_back( d_inst_engine
);
100 if( options::finiteModelFind() ){
101 if( options::fmfBoundInt() ){
102 d_bint
= new quantifiers::BoundedIntegers( c
, this );
103 d_modules
.push_back( d_bint
);
107 d_model_engine
= new quantifiers::ModelEngine( c
, this );
108 d_modules
.push_back( d_model_engine
);
110 d_model_engine
= NULL
;
113 if( options::quantRewriteRules() ){
114 d_rr_engine
= new quantifiers::RewriteEngine( c
, this );
115 d_modules
.push_back(d_rr_engine
);
121 d_total_inst_count_debug
= 0;
124 QuantifiersEngine::~QuantifiersEngine(){
127 delete d_model_engine
;
128 delete d_inst_engine
;
136 for(std::map
< Node
, QuantPhaseReq
* >::iterator i
= d_phase_reqs
.begin(); i
!= d_phase_reqs
.end(); ++i
) {
141 EqualityQueryQuantifiersEngine
* QuantifiersEngine::getEqualityQuery() {
145 context::Context
* QuantifiersEngine::getSatContext(){
146 return d_te
->theoryOf( THEORY_QUANTIFIERS
)->getSatContext();
149 context::Context
* QuantifiersEngine::getUserContext(){
150 return d_te
->theoryOf( THEORY_QUANTIFIERS
)->getUserContext();
153 OutputChannel
& QuantifiersEngine::getOutputChannel(){
154 return d_te
->theoryOf( THEORY_QUANTIFIERS
)->getOutputChannel();
156 /** get default valuation for the quantifiers engine */
157 Valuation
& QuantifiersEngine::getValuation(){
158 return d_te
->theoryOf( THEORY_QUANTIFIERS
)->getValuation();
161 void QuantifiersEngine::finishInit(){
162 for( int i
=0; i
<(int)d_modules
.size(); i
++ ){
163 d_modules
[i
]->finishInit();
167 void QuantifiersEngine::check( Theory::Effort e
){
168 CodeTimer
codeTimer(d_time
);
169 bool needsCheck
= false;
170 bool needsBuildModel
= false;
171 std::vector
< QuantifiersModule
* > qm
;
172 if( d_model
->getNumAssertedQuantifiers()>0 ){
173 needsCheck
= e
>=Theory::EFFORT_LAST_CALL
; //always need to check at or above last call
174 for( int i
=0; i
<(int)d_modules
.size(); i
++ ){
175 if( d_modules
[i
]->needsCheck( e
) ){
176 qm
.push_back( d_modules
[i
] );
182 Trace("quant-engine") << "Quantifiers Engine check, level = " << e
<< std::endl
;
183 Trace("quant-engine-debug") << " modules to check : ";
184 for( unsigned i
=0; i
<qm
.size(); i
++ ){
185 Trace("quant-engine-debug") << qm
[i
]->identify() << " ";
187 Trace("quant-engine-debug") << std::endl
;
188 Trace("quant-engine-debug") << " # quantified formulas = " << d_model
->getNumAssertedQuantifiers() << std::endl
;
189 Trace("quant-engine-debug") << " Theory engine finished : " << !d_te
->needCheck() << std::endl
;
191 if( !getMasterEqualityEngine()->consistent() ){
192 Trace("quant-engine") << "Master equality engine not consistent, return." << std::endl
;
195 Trace("quant-engine-debug") << "Resetting all modules..." << std::endl
;
196 //reset relevant information
198 d_hasAddedLemma
= false;
200 //flush previous lemmas (for instance, if was interupted)
202 if( d_hasAddedLemma
){
206 d_term_db
->reset( e
);
211 d_model
->reset_round();
212 for( int i
=0; i
<(int)d_modules
.size(); i
++ ){
213 d_modules
[i
]->reset_round( e
);
215 Trace("quant-engine-debug") << "Done resetting all modules." << std::endl
;
217 if( e
==Theory::EFFORT_LAST_CALL
){
218 //if effort is last call, try to minimize model first FIXME: remove?
219 uf::StrongSolverTheoryUF
* ufss
= ((uf::TheoryUF
*)getTheoryEngine()->theoryOf( THEORY_UF
))->getStrongSolver();
220 if( ufss
&& !ufss
->minimize() ){
223 ++(d_statistics
.d_instantiation_rounds_lc
);
224 }else if( e
==Theory::EFFORT_FULL
){
225 ++(d_statistics
.d_instantiation_rounds
);
228 Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl
;
229 for( unsigned quant_e
= QEFFORT_CONFLICT
; quant_e
<=QEFFORT_MODEL
; quant_e
++ ){
230 for( int i
=0; i
<(int)qm
.size(); i
++ ){
231 Trace("quant-engine-debug") << "Check " << qm
[i
]->identify().c_str() << " at effort " << quant_e
<< "..." << std::endl
;
232 qm
[i
]->check( e
, quant_e
);
234 //flush all current lemmas
236 //if we have added one, stop
237 if( d_hasAddedLemma
){
241 Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl
;
243 //build the model if not done so already
244 // this happens if no quantifiers are currently asserted and no model-building module is enabled
245 if( e
==Theory::EFFORT_LAST_CALL
&& !d_hasAddedLemma
){
246 if( options::produceModels() && !d_model
->isModelSet() ){
247 needsBuildModel
= true;
249 if( Trace
.isOn("inst-per-quant") ){
250 for( std::map
< Node
, int >::iterator it
= d_total_inst_debug
.begin(); it
!= d_total_inst_debug
.end(); ++it
){
251 Trace("inst-per-quant") << " * " << it
->second
<< " for " << it
->first
<< std::endl
;
255 if( Trace
.isOn("inst-per-quant-round") ){
256 for( std::map
< Node
, int >::iterator it
= d_temp_inst_debug
.begin(); it
!= d_temp_inst_debug
.end(); ++it
){
257 Trace("inst-per-quant-round") << " * " << it
->second
<< " for " << it
->first
<< std::endl
;
258 d_temp_inst_debug
[it
->first
] = 0;
262 Trace("quant-engine") << "Finished quantifiers engine check." << std::endl
;
264 if( e
==Theory::EFFORT_LAST_CALL
&& options::produceModels() ){
265 needsBuildModel
= true;
269 if( needsBuildModel
){
270 Trace("quant-engine-debug") << "Build the model..." << std::endl
;
271 d_te
->getModelBuilder()->buildModel( d_model
, true );
272 Trace("quant-engine-debug") << "Done building the model." << std::endl
;
276 void QuantifiersEngine::registerQuantifier( Node f
){
277 if( std::find( d_quants
.begin(), d_quants
.end(), f
)==d_quants
.end() ){
278 Trace("quant") << "QuantifiersEngine : Register quantifier ";
279 if( d_term_db
->isRewriteRule( f
) ){
280 Trace("quant") << " (rewrite rule)";
282 Trace("quant") << " : " << f
<< std::endl
;
283 d_quants
.push_back( f
);
285 ++(d_statistics
.d_num_quant
);
286 Assert( f
.getKind()==FORALL
);
287 //make instantiation constants for f
288 d_term_db
->makeInstantiationConstantsFor( f
);
289 //register with quantifier relevance
291 d_quant_rel
->registerQuantifier( f
);
293 //register with each module
294 for( int i
=0; i
<(int)d_modules
.size(); i
++ ){
295 d_modules
[i
]->registerQuantifier( f
);
297 Node ceBody
= d_term_db
->getInstConstantBody( f
);
298 //generate the phase requirements
299 d_phase_reqs
[f
] = new QuantPhaseReq( ceBody
, true );
300 //also register it with the strong solver
301 if( options::finiteModelFind() ){
302 ((uf::TheoryUF
*)d_te
->theoryOf( THEORY_UF
))->getStrongSolver()->registerQuantifier( f
);
307 void QuantifiersEngine::registerPattern( std::vector
<Node
> & pattern
) {
308 for(std::vector
<Node
>::iterator p
= pattern
.begin(); p
!= pattern
.end(); ++p
){
309 std::set
< Node
> added
;
310 getTermDatabase()->addTerm( *p
, added
);
314 void QuantifiersEngine::assertQuantifier( Node f
, bool pol
){
317 if( d_skolemized
.find( f
)==d_skolemized
.end() ){
318 Node body
= d_term_db
->getSkolemizedBody( f
);
319 NodeBuilder
<> nb(kind::OR
);
320 nb
<< f
<< body
.notNode();
322 if( Trace
.isOn("quantifiers-sk") ){
323 Node slem
= Rewriter::rewrite( lem
);
324 Trace("quantifiers-sk") << "Skolemize lemma : " << slem
<< std::endl
;
326 getOutputChannel().lemma( lem
, false, true );
327 d_skolemized
[f
] = true;
330 //assert to modules TODO : handle !pol
332 //register the quantifier
333 registerQuantifier( f
);
334 //assert it to each module
335 d_model
->assertQuantifier( f
);
336 for( int i
=0; i
<(int)d_modules
.size(); i
++ ){
337 d_modules
[i
]->assertNode( f
);
342 void QuantifiersEngine::propagate( Theory::Effort level
){
343 CodeTimer
codeTimer(d_time
);
345 for( int i
=0; i
<(int)d_modules
.size(); i
++ ){
346 d_modules
[i
]->propagate( level
);
350 Node
QuantifiersEngine::getNextDecisionRequest(){
351 for( int i
=0; i
<(int)d_modules
.size(); i
++ ){
352 Node n
= d_modules
[i
]->getNextDecisionRequest();
360 void QuantifiersEngine::addTermToDatabase( Node n
, bool withinQuant
){
361 std::set
< Node
> added
;
362 getTermDatabase()->addTerm( n
, added
, withinQuant
);
363 //maybe have triggered instantiations if we are doing eager instantiation
364 if( options::eagerInstQuant() ){
367 //added contains also the Node that just have been asserted in this branch
369 for( std::set
< Node
>::iterator i
=added
.begin(), end
=added
.end(); i
!=end
; i
++ ){
371 d_quant_rel
->setRelevance( i
->getOperator(), 0 );
377 void QuantifiersEngine::computeTermVector( Node f
, InstMatch
& m
, std::vector
< Node
>& vars
, std::vector
< Node
>& terms
){
378 for( size_t i
=0; i
<f
[0].getNumChildren(); i
++ ){
381 vars
.push_back( f
[0][i
] );
382 terms
.push_back( n
);
387 bool QuantifiersEngine::addInstantiation( Node f
, std::vector
< Node
>& vars
, std::vector
< Node
>& terms
){
388 Assert( f
.getKind()==FORALL
);
389 Assert( vars
.size()==terms
.size() );
390 Node body
= getInstantiation( f
, vars
, terms
);
391 Trace("inst-assert") << "(assert " << body
<< ")" << std::endl
;
393 NodeBuilder
<> nb(kind::OR
);
394 nb
<< f
.notNode() << body
;
396 //check for duplication
397 if( addLemma( lem
) ){
398 d_total_inst_debug
[f
]++;
399 d_temp_inst_debug
[f
]++;
400 d_total_inst_count_debug
++;
401 Trace("inst") << "*** Instantiate " << f
<< " with " << std::endl
;
402 for( int i
=0; i
<(int)terms
.size(); i
++ ){
403 Trace("inst") << " " << terms
[i
];
404 Trace("inst") << std::endl
;
406 if( options::cbqi() ){
407 for( int i
=0; i
<(int)terms
.size(); i
++ ){
408 if( quantifiers::TermDb::hasInstConstAttr(terms
[i
]) ){
409 Debug("inst")<< "***& Bad Instantiate " << f
<< " with " << std::endl
;
410 for( int i
=0; i
<(int)terms
.size(); i
++ ){
411 Debug("inst") << " " << terms
[i
] << std::endl
;
413 Unreachable("Bad instantiation");
417 if( options::instMaxLevel()!=-1 ){
418 uint64_t maxInstLevel
= 0;
419 for( int i
=0; i
<(int)terms
.size(); i
++ ){
420 if( terms
[i
].hasAttribute(InstLevelAttribute()) ){
421 if( terms
[i
].getAttribute(InstLevelAttribute())>maxInstLevel
){
422 maxInstLevel
= terms
[i
].getAttribute(InstLevelAttribute());
426 setInstantiationLevelAttr( body
, f
[1], maxInstLevel
+1 );
428 Trace("inst-debug") << "*** Lemma is " << lem
<< std::endl
;
429 ++(d_statistics
.d_instantiations
);
432 ++(d_statistics
.d_inst_duplicate
);
437 void QuantifiersEngine::setInstantiationLevelAttr( Node n
, Node qn
, uint64_t level
){
438 Trace("inst-level-debug2") << "IL : " << n
<< " " << qn
<< " " << level
<< std::endl
;
439 //if not from the vector of terms we instantiatied
440 if( qn
.getKind()!=BOUND_VARIABLE
&& n
!=qn
){
441 //if this is a new term, without an instantiation level
442 if( !n
.hasAttribute(InstLevelAttribute()) ){
443 InstLevelAttribute ila
;
444 n
.setAttribute(ila
,level
);
445 Trace("inst-level-debug") << "Set instantiation level " << n
<< " to " << level
<< std::endl
;
447 Assert( n
.getNumChildren()==qn
.getNumChildren() );
448 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
449 setInstantiationLevelAttr( n
[i
], qn
[i
], level
);
454 void QuantifiersEngine::setInstantiationLevelAttr( Node n
, uint64_t level
){
455 if( !n
.hasAttribute(InstLevelAttribute()) ){
456 InstLevelAttribute ila
;
457 n
.setAttribute(ila
,level
);
458 Trace("inst-level-debug") << "Set instantiation level " << n
<< " to " << level
<< std::endl
;
460 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
461 setInstantiationLevelAttr( n
[i
], level
);
465 bool QuantifiersEngine::isTermEligibleForInstantiation( Node n
, Node f
, bool print
) {
466 if( n
.hasAttribute(InstLevelAttribute()) ){
467 unsigned ml
= options::instMaxLevel();
468 if( f
.hasAttribute(QuantInstLevelAttribute()) ){
469 ml
= f
.getAttribute(QuantInstLevelAttribute());
471 if( n
.getAttribute(InstLevelAttribute())>ml
){
472 Trace("inst-add-debug") << "Term " << n
<< " has instantiation level " << n
.getAttribute(InstLevelAttribute());
473 Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml
<< " for this quantified formula." << std::endl
;
477 if( options::instLevelInputOnly() ){
478 Trace("inst-add-debug") << "Term " << n
<< " does not have an instantiation level." << std::endl
;
486 Node
QuantifiersEngine::getSubstitute( Node n
, std::vector
< Node
>& terms
){
487 if( n
.getKind()==INST_CONSTANT
){
488 Debug("check-inst") << "Substitute inst constant : " << n
<< std::endl
;
489 return terms
[n
.getAttribute(InstVarNumAttribute())];
491 //if( !quantifiers::TermDb::hasInstConstAttr( n ) ){
492 //Debug("check-inst") << "No inst const attr : " << n << std::endl;
495 //Debug("check-inst") << "Recurse on : " << n << std::endl;
496 std::vector
< Node
> cc
;
497 if( n
.getMetaKind() == kind::metakind::PARAMETERIZED
){
498 cc
.push_back( n
.getOperator() );
500 bool changed
= false;
501 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
502 Node c
= getSubstitute( n
[i
], terms
);
504 changed
= changed
|| c
!=n
[i
];
507 Node ret
= NodeManager::currentNM()->mkNode( n
.getKind(), cc
);
516 Node
QuantifiersEngine::getInstantiation( Node f
, std::vector
< Node
>& vars
, std::vector
< Node
>& terms
){
518 //process partial instantiation if necessary
519 if( d_term_db
->d_vars
[f
].size()!=vars
.size() ){
520 body
= f
[ 1 ].substitute( vars
.begin(), vars
.end(), terms
.begin(), terms
.end() );
521 std::vector
< Node
> uninst_vars
;
522 //doing a partial instantiation, must add quantifier for all uninstantiated variables
523 for( int i
=0; i
<(int)f
[0].getNumChildren(); i
++ ){
524 if( std::find( vars
.begin(), vars
.end(), f
[0][i
] )==vars
.end() ){
525 uninst_vars
.push_back( f
[0][i
] );
528 Node bvl
= NodeManager::currentNM()->mkNode( BOUND_VAR_LIST
, uninst_vars
);
529 body
= NodeManager::currentNM()->mkNode( FORALL
, bvl
, body
);
530 Trace("partial-inst") << "Partial instantiation : " << f
<< std::endl
;
531 Trace("partial-inst") << " : " << body
<< std::endl
;
533 //do optimized version
534 Node icb
= d_term_db
->getInstConstantBody( f
);
535 body
= getSubstitute( icb
, terms
);
536 if( Debug
.isOn("check-inst") ){
537 Node body2
= f
[ 1 ].substitute( vars
.begin(), vars
.end(), terms
.begin(), terms
.end() );
539 Debug("check-inst") << "Substitution is wrong : " << body
<< " " << body2
<< std::endl
;
546 Node
QuantifiersEngine::getInstantiation( Node f
, InstMatch
& m
){
547 std::vector
< Node
> vars
;
548 std::vector
< Node
> terms
;
549 computeTermVector( f
, m
, vars
, terms
);
550 return getInstantiation( f
, vars
, terms
);
553 Node
QuantifiersEngine::getInstantiation( Node f
, std::vector
< Node
>& terms
) {
554 return getInstantiation( f
, d_term_db
->d_inst_constants
[f
], terms
);
557 bool QuantifiersEngine::existsInstantiation( Node f
, InstMatch
& m
, bool modEq
, bool modInst
){
558 if( options::incrementalSolving() ){
559 if( d_c_inst_match_trie
.find( f
)!=d_c_inst_match_trie
.end() ){
560 if( d_c_inst_match_trie
[f
]->existsInstMatch( this, f
, m
, getUserContext(), modEq
, modInst
) ){
565 if( d_inst_match_trie
.find( f
)!=d_inst_match_trie
.end() ){
566 if( d_inst_match_trie
[f
].existsInstMatch( this, f
, m
, modEq
, modInst
) ){
571 //also check model engine (it may contain instantiations internally)
572 if( d_model_engine
->getModelBuilder()->existsInstantiation( f
, m
, modEq
, modInst
) ){
578 bool QuantifiersEngine::addLemma( Node lem
, bool doCache
){
580 Debug("inst-engine-debug") << "Adding lemma : " << lem
<< std::endl
;
581 lem
= Rewriter::rewrite(lem
);
582 if( d_lemmas_produced_c
.find( lem
)==d_lemmas_produced_c
.end() ){
583 //d_curr_out->lemma( lem, false, true );
584 d_lemmas_produced_c
[ lem
] = true;
585 d_lemmas_waiting
.push_back( lem
);
586 Debug("inst-engine-debug") << "Added lemma : " << lem
<< std::endl
;
589 Debug("inst-engine-debug") << "Duplicate." << std::endl
;
593 d_lemmas_waiting
.push_back( lem
);
598 void QuantifiersEngine::addRequirePhase( Node lit
, bool req
){
599 d_phase_req_waiting
[lit
] = req
;
602 bool QuantifiersEngine::addInstantiation( Node f
, InstMatch
& m
, bool mkRep
, bool modEq
, bool modInst
){
603 // For resource-limiting (also does a time check).
604 getOutputChannel().spendResource();
606 std::vector
< Node
> terms
;
607 //make sure there are values for each variable we are instantiating
608 for( size_t i
=0; i
<f
[0].getNumChildren(); i
++ ){
609 Node val
= m
.get( i
);
611 Node ic
= d_term_db
->getInstantiationConstant( f
, i
);
612 val
= d_term_db
->getFreeVariableForInstConstant( ic
);
613 Trace("inst-add-debug") << "mkComplete " << val
<< std::endl
;
615 terms
.push_back( val
);
617 return addInstantiation( f
, terms
, mkRep
, modEq
, modInst
);
620 bool QuantifiersEngine::addInstantiation( Node f
, std::vector
< Node
>& terms
, bool mkRep
, bool modEq
, bool modInst
) {
621 Assert( terms
.size()==f
[0].getNumChildren() );
622 Trace("inst-add-debug") << "Add instantiation: ";
623 for( unsigned i
=0; i
<terms
.size(); i
++ ){
624 if( i
>0 ) Trace("inst-add-debug") << ", ";
625 Trace("inst-add-debug") << f
[0][i
] << " -> " << terms
[i
];
626 //make it representative, this is helpful for recognizing duplication
628 //pick the best possible representative for instantiation, based on past use and simplicity of term
629 terms
[i
] = d_eq_query
->getInternalRepresentative( terms
[i
], f
, i
);
630 Trace("inst-add-debug2") << " (" << terms
[i
] << ")";
633 Trace("inst-add-debug") << std::endl
;
635 //check based on instantiation level
636 if( options::instMaxLevel()!=-1 ){
637 for( unsigned i
=0; i
<terms
.size(); i
++ ){
638 if( !isTermEligibleForInstantiation( terms
[i
], f
, true ) ){
643 //check for entailment
644 if( options::instNoEntail() ){
645 std::map
< TNode
, TNode
> subs
;
646 for( unsigned i
=0; i
<terms
.size(); i
++ ){
647 subs
[f
[0][i
]] = terms
[i
];
649 if( d_term_db
->isEntailed( f
[1], subs
, false, true ) ){
650 Trace("inst-add-debug") << " -> Currently entailed." << std::endl
;
655 //check for duplication
656 bool alreadyExists
= false;
657 if( options::incrementalSolving() ){
658 Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq
<< ", modInst = " << modInst
<< std::endl
;
659 inst::CDInstMatchTrie
* imt
;
660 std::map
< Node
, inst::CDInstMatchTrie
* >::iterator it
= d_c_inst_match_trie
.find( f
);
661 if( it
!=d_c_inst_match_trie
.end() ){
664 imt
= new CDInstMatchTrie( getUserContext() );
665 d_c_inst_match_trie
[f
] = imt
;
667 alreadyExists
= !imt
->addInstMatch( this, f
, terms
, getUserContext(), modEq
, modInst
);
669 Trace("inst-add-debug") << "Adding into inst trie" << std::endl
;
670 alreadyExists
= !d_inst_match_trie
[f
].addInstMatch( this, f
, terms
, modEq
, modInst
);
673 Trace("inst-add-debug") << " -> Already exists." << std::endl
;
674 ++(d_statistics
.d_inst_duplicate_eq
);
679 //add the instantiation
680 Trace("inst-add-debug") << "Constructing instantiation..." << std::endl
;
681 bool addedInst
= addInstantiation( f
, d_term_db
->d_vars
[f
], terms
);
684 Trace("inst-add-debug") << " -> Success." << std::endl
;
687 Trace("inst-add-debug") << " -> Lemma already exists." << std::endl
;
693 bool QuantifiersEngine::addSplit( Node n
, bool reqPhase
, bool reqPhasePol
){
694 n
= Rewriter::rewrite( n
);
695 Node lem
= NodeManager::currentNM()->mkNode( OR
, n
, n
.notNode() );
696 if( addLemma( lem
) ){
697 Debug("inst") << "*** Add split " << n
<< std::endl
;
703 bool QuantifiersEngine::addSplitEquality( Node n1
, Node n2
, bool reqPhase
, bool reqPhasePol
){
704 //Assert( !areEqual( n1, n2 ) );
705 //Assert( !areDisequal( n1, n2 ) );
706 Kind knd
= n1
.getType()==NodeManager::currentNM()->booleanType() ? IFF
: EQUAL
;
707 Node fm
= NodeManager::currentNM()->mkNode( knd
, n1
, n2
);
708 return addSplit( fm
);
711 void QuantifiersEngine::flushLemmas(){
712 if( !d_lemmas_waiting
.empty() ){
713 //take default output channel if none is provided
714 d_hasAddedLemma
= true;
715 for( int i
=0; i
<(int)d_lemmas_waiting
.size(); i
++ ){
716 getOutputChannel().lemma( d_lemmas_waiting
[i
], false, true );
718 d_lemmas_waiting
.clear();
720 if( !d_phase_req_waiting
.empty() ){
721 for( std::map
< Node
, bool >::iterator it
= d_phase_req_waiting
.begin(); it
!= d_phase_req_waiting
.end(); ++it
){
722 getOutputChannel().requirePhase( it
->first
, it
->second
);
724 d_phase_req_waiting
.clear();
728 void QuantifiersEngine::getPhaseReqTerms( Node f
, std::vector
< Node
>& nodes
){
729 if( options::literalMatchMode()!=quantifiers::LITERAL_MATCH_NONE
&& d_phase_reqs
.find( f
)!=d_phase_reqs
.end() ){
730 // doing literal-based matching (consider polarity of literals)
731 for( int i
=0; i
<(int)nodes
.size(); i
++ ){
732 Node prev
= nodes
[i
];
733 bool nodeChanged
= false;
734 if( d_phase_reqs
[f
]->isPhaseReq( nodes
[i
] ) ){
735 bool preq
= d_phase_reqs
[f
]->getPhaseReq( nodes
[i
] );
736 nodes
[i
] = NodeManager::currentNM()->mkNode( IFF
, nodes
[i
], NodeManager::currentNM()->mkConst
<bool>(preq
) );
739 //else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){
740 // Node req = qe->getPhaseReqEquality( f, trNodes[i] );
741 // trNodes[i] = NodeManager::currentNM()->mkNode( EQUAL, trNodes[i], req );
744 Debug("literal-matching") << " Make " << prev
<< " -> " << nodes
[i
] << std::endl
;
745 ++(d_statistics
.d_lit_phase_req
);
747 ++(d_statistics
.d_lit_phase_nreq
);
751 d_statistics
.d_lit_phase_nreq
+= (int)nodes
.size();
755 void QuantifiersEngine::printInstantiations( std::ostream
& out
) {
756 for( std::map
< Node
, bool >::iterator it
= d_skolemized
.begin(); it
!= d_skolemized
.end(); ++it
){
757 out
<< "Skolem constants of " << it
->first
<< " : " << std::endl
;
759 for( unsigned i
=0; i
<d_term_db
->d_skolem_constants
[it
->first
].size(); i
++ ){
760 if( i
>0 ){ out
<< ", "; }
761 out
<< d_term_db
->d_skolem_constants
[it
->first
][i
];
763 out
<< " )" << std::endl
;
766 if( options::incrementalSolving() ){
767 for( std::map
< Node
, inst::CDInstMatchTrie
* >::iterator it
= d_c_inst_match_trie
.begin(); it
!= d_c_inst_match_trie
.end(); ++it
){
768 out
<< "Instantiations of " << it
->first
<< " : " << std::endl
;
769 it
->second
->print( out
, it
->first
);
772 for( std::map
< Node
, inst::InstMatchTrie
>::iterator it
= d_inst_match_trie
.begin(); it
!= d_inst_match_trie
.end(); ++it
){
773 out
<< "Instantiations of " << it
->first
<< " : " << std::endl
;
774 it
->second
.print( out
, it
->first
);
780 QuantifiersEngine::Statistics::Statistics():
781 d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
782 d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
783 d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
784 d_instantiations("QuantifiersEngine::Instantiations_Total", 0),
785 d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0),
786 d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0),
787 d_lit_phase_req("QuantifiersEngine::lit_phase_req", 0),
788 d_lit_phase_nreq("QuantifiersEngine::lit_phase_nreq", 0),
789 d_triggers("QuantifiersEngine::Triggers", 0),
790 d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
791 d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
792 d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0)
794 StatisticsRegistry::registerStat(&d_num_quant
);
795 StatisticsRegistry::registerStat(&d_instantiation_rounds
);
796 StatisticsRegistry::registerStat(&d_instantiation_rounds_lc
);
797 StatisticsRegistry::registerStat(&d_instantiations
);
798 StatisticsRegistry::registerStat(&d_inst_duplicate
);
799 StatisticsRegistry::registerStat(&d_inst_duplicate_eq
);
800 StatisticsRegistry::registerStat(&d_lit_phase_req
);
801 StatisticsRegistry::registerStat(&d_lit_phase_nreq
);
802 StatisticsRegistry::registerStat(&d_triggers
);
803 StatisticsRegistry::registerStat(&d_simple_triggers
);
804 StatisticsRegistry::registerStat(&d_multi_triggers
);
805 StatisticsRegistry::registerStat(&d_multi_trigger_instantiations
);
808 QuantifiersEngine::Statistics::~Statistics(){
809 StatisticsRegistry::unregisterStat(&d_num_quant
);
810 StatisticsRegistry::unregisterStat(&d_instantiation_rounds
);
811 StatisticsRegistry::unregisterStat(&d_instantiation_rounds_lc
);
812 StatisticsRegistry::unregisterStat(&d_instantiations
);
813 StatisticsRegistry::unregisterStat(&d_inst_duplicate
);
814 StatisticsRegistry::unregisterStat(&d_inst_duplicate_eq
);
815 StatisticsRegistry::unregisterStat(&d_lit_phase_req
);
816 StatisticsRegistry::unregisterStat(&d_lit_phase_nreq
);
817 StatisticsRegistry::unregisterStat(&d_triggers
);
818 StatisticsRegistry::unregisterStat(&d_simple_triggers
);
819 StatisticsRegistry::unregisterStat(&d_multi_triggers
);
820 StatisticsRegistry::unregisterStat(&d_multi_trigger_instantiations
);
823 eq::EqualityEngine
* QuantifiersEngine::getMasterEqualityEngine(){
824 return ((quantifiers::TheoryQuantifiers
*)getTheoryEngine()->theoryOf( THEORY_QUANTIFIERS
))->getMasterEqualityEngine();
827 void EqualityQueryQuantifiersEngine::reset(){
832 bool EqualityQueryQuantifiersEngine::hasTerm( Node a
){
833 return getEngine()->hasTerm( a
);
836 Node
EqualityQueryQuantifiersEngine::getRepresentative( Node a
){
837 eq::EqualityEngine
* ee
= getEngine();
838 if( ee
->hasTerm( a
) ){
839 return ee
->getRepresentative( a
);
845 bool EqualityQueryQuantifiersEngine::areEqual( Node a
, Node b
){
849 eq::EqualityEngine
* ee
= getEngine();
851 return true;//!areDisequal( a, b );
853 if( ee
->hasTerm( a
) && ee
->hasTerm( b
) ){
854 if( ee
->areEqual( a
, b
) ){
863 bool EqualityQueryQuantifiersEngine::areDisequal( Node a
, Node b
){
864 eq::EqualityEngine
* ee
= getEngine();
865 if( ee
->hasTerm( a
) && ee
->hasTerm( b
) ){
866 if( ee
->areDisequal( a
, b
, false ) ){
873 Node
EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a
, Node f
, int index
){
874 Node r
= getRepresentative( a
);
875 if( !options::internalReps() ){
878 if( d_int_rep
.find( r
)==d_int_rep
.end() ){
879 //find best selection for representative
881 //if( options::fmfRelevantDomain() && !f.isNull() ){
882 // Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl;
883 // r_best = d_qe->getRelevantDomain()->getRelevantTerm( f, index, r );
884 // Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl;
886 std::vector
< Node
> eqc
;
887 getEquivalenceClass( r
, eqc
);
888 Trace("internal-rep-select") << "Choose representative for equivalence class : { ";
889 for( unsigned i
=0; i
<eqc
.size(); i
++ ){
890 if( i
>0 ) Trace("internal-rep-select") << ", ";
891 Trace("internal-rep-select") << eqc
[i
];
893 Trace("internal-rep-select") << " } " << std::endl
;
894 int r_best_score
= -1;
895 for( size_t i
=0; i
<eqc
.size(); i
++ ){
896 //if cbqi is active, do not choose instantiation constant terms
897 if( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(eqc
[i
]) ){
898 int score
= getRepScore( eqc
[i
], f
, index
);
899 if( r_best
.isNull() || ( score
>=0 && ( r_best_score
<0 || score
<r_best_score
) ) ){
901 r_best_score
= score
;
905 if( r_best
.isNull() ){
907 Node ic
= d_qe
->getTermDatabase()->getInstantiationConstant( f
, index
);
908 r_best
= d_qe
->getTermDatabase()->getFreeVariableForInstConstant( ic
);
913 //now, make sure that no other member of the class is an instance
914 r_best
= getInstance( r_best
, eqc
);
915 //store that this representative was chosen at this point
916 if( d_rep_score
.find( r_best
)==d_rep_score
.end() ){
917 d_rep_score
[ r_best
] = d_reset_count
;
919 Trace("internal-rep-select") << "...Choose " << r_best
<< std::endl
;
920 d_int_rep
[r
] = r_best
;
922 Trace("internal-rep-debug") << "rep( " << a
<< " ) = " << r
<< ", " << std::endl
;
923 Trace("internal-rep-debug") << "int_rep( " << a
<< " ) = " << r_best
<< ", " << std::endl
;
932 void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map
< TypeNode
, std::vector
< Node
> >& reps
) {
933 //make sure internal representatives currently exist
934 for( std::map
< TypeNode
, std::vector
< Node
> >::iterator it
= reps
.begin(); it
!= reps
.end(); ++it
){
935 if( it
->first
.isSort() ){
936 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
937 Node r
= getInternalRepresentative( it
->second
[i
], Node::null(), 0 );
941 Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl
;
942 for( std::map
< Node
, Node
>::iterator it
= d_int_rep
.begin(); it
!= d_int_rep
.end(); ++it
){
943 Trace("internal-rep-flatten") << it
->first
.getType() << " : irep( " << it
->first
<< " ) = " << it
->second
<< std::endl
;
945 //store representatives for newly created terms
946 std::map
< Node
, Node
> temp_rep_map
;
951 for( std::map
< Node
, Node
>::iterator it
= d_int_rep
.begin(); it
!= d_int_rep
.end(); ++it
){
952 if( it
->second
.getKind()==APPLY_UF
&& it
->second
.getType().isSort() ){
953 Node ni
= it
->second
;
954 std::vector
< Node
> cc
;
955 cc
.push_back( it
->second
.getOperator() );
956 bool changed
= false;
957 for( unsigned j
=0; j
<ni
.getNumChildren(); j
++ ){
958 if( ni
[j
].getType().isSort() ){
959 Node r
= getRepresentative( ni
[j
] );
960 if( d_int_rep
.find( r
)==d_int_rep
.end() ){
961 Assert( temp_rep_map
.find( r
)!=temp_rep_map
.end() );
965 //found sub-term as instance
966 Trace("internal-rep-flatten-debug") << "...Changed " << it
->second
<< " to subterm " << ni
[j
] << std::endl
;
967 d_int_rep
[it
->first
] = ni
[j
];
972 Node ir
= d_int_rep
[r
];
984 Node n
= NodeManager::currentNM()->mkNode( APPLY_UF
, cc
);
985 Trace("internal-rep-flatten-debug") << "...Changed " << it
->second
<< " to " << n
<< std::endl
;
987 d_int_rep
[it
->first
] = n
;
988 temp_rep_map
[n
] = it
->first
;
993 Trace("internal-rep-flatten") << "---After flattening : " << std::endl
;
994 for( std::map
< Node
, Node
>::iterator it
= d_int_rep
.begin(); it
!= d_int_rep
.end(); ++it
){
995 Trace("internal-rep-flatten") << it
->first
.getType() << " : irep( " << it
->first
<< " ) = " << it
->second
<< std::endl
;
999 eq::EqualityEngine
* EqualityQueryQuantifiersEngine::getEngine(){
1000 return d_qe
->getMasterEqualityEngine();
1003 void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a
, std::vector
< Node
>& eqc
){
1004 eq::EqualityEngine
* ee
= getEngine();
1005 if( ee
->hasTerm( a
) ){
1006 Node rep
= ee
->getRepresentative( a
);
1007 eq::EqClassIterator
eqc_iter( rep
, ee
);
1008 while( !eqc_iter
.isFinished() ){
1009 eqc
.push_back( *eqc_iter
);
1015 //a should be in its equivalence class
1016 Assert( std::find( eqc
.begin(), eqc
.end(), a
)!=eqc
.end() );
1021 Node
EqualityQueryQuantifiersEngine::getInstance( Node n
, std::vector
< Node
>& eqc
){
1022 for( size_t i
=0; i
<n
.getNumChildren(); i
++ ){
1023 Node nn
= getInstance( n
[i
], eqc
);
1028 if( std::find( eqc
.begin(), eqc
.end(), n
)!=eqc
.end() ){
1031 return Node::null();
1035 int getDepth( Node n
){
1036 if( n
.getNumChildren()==0 ){
1040 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
1041 int depth
= getDepth( n
[i
] );
1042 if( depth
>maxDepth
){
1050 //smaller the score, the better
1051 int EqualityQueryQuantifiersEngine::getRepScore( Node n
, Node f
, int index
){
1053 if( options::instMaxLevel()!=-1 ){
1054 //score prefer lowest instantiation level
1055 if( n
.hasAttribute(InstLevelAttribute()) ){
1056 s
= n
.getAttribute(InstLevelAttribute());
1058 s
= options::instLevelInputOnly() ? -1 : 0;
1061 //score prefers earliest use of this term as a representative
1062 s
= d_rep_score
.find( n
)==d_rep_score
.end() ? -1 : d_rep_score
[n
];
1065 //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n ); //term depth