projects / cvc5.git / blob
? search:


eb5dbaef0eb114502a82e8e932eeeb8d2c05d49a
[cvc5.git] / src / theory / quantifiers_engine.cpp
1 /********************* */
2 /*! \file quantifiers_engine.cpp
3 ** \verbatim
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
11 **
12 ** \brief Implementation of quantifiers engine class
13 **/
14
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"
37
38 using namespace std;
39 using namespace CVC4;
40 using namespace CVC4::kind;
41 using namespace CVC4::context;
42 using namespace CVC4::theory;
43 using namespace CVC4::theory::inst;
44
45 QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
46 d_te( 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;
54
55 Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
56
57 //the model object
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" );
66 }else{
67 d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
68 }
69 if( !options::finiteModelFind() ){
70 d_rel_dom = new quantifiers::RelevantDomain( this, d_model );
71 }else{
72 d_rel_dom = NULL;
73 }
74 if( options::relevantTriggers() ){
75 d_quant_rel = new QuantRelevance( false );
76 }else{
77 d_quant_rel = NULL;
78 }
79
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 );
84 }else{
85 d_qcf = NULL;
86 }
87 if( options::conjectureGen() ){
88 d_sg_gen = new quantifiers::ConjectureGenerator( this, c );
89 d_modules.push_back( d_sg_gen );
90 }else{
91 d_sg_gen = NULL;
92 }
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 );
97 }else{
98 d_inst_engine = NULL;
99 }
100 if( options::finiteModelFind() ){
101 if( options::fmfBoundInt() ){
102 d_bint = new quantifiers::BoundedIntegers( c, this );
103 d_modules.push_back( d_bint );
104 }else{
105 d_bint = NULL;
106 }
107 d_model_engine = new quantifiers::ModelEngine( c, this );
108 d_modules.push_back( d_model_engine );
109 }else{
110 d_model_engine = NULL;
111 d_bint = NULL;
112 }
113 if( options::quantRewriteRules() ){
114 d_rr_engine = new quantifiers::RewriteEngine( c, this );
115 d_modules.push_back(d_rr_engine);
116 }else{
117 d_rr_engine = NULL;
118 }
119
120 //options
121 d_total_inst_count_debug = 0;
122 }
123
124 QuantifiersEngine::~QuantifiersEngine(){
125 delete d_rr_engine;
126 delete d_bint;
127 delete d_model_engine;
128 delete d_inst_engine;
129 delete d_qcf;
130 delete d_quant_rel;
131 delete d_rel_dom;
132 delete d_model;
133 delete d_tr_trie;
134 delete d_term_db;
135 delete d_eq_query;
136 for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) {
137 delete (*i).second;
138 }
139 }
140
141 EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() {
142 return d_eq_query;
143 }
144
145 context::Context* QuantifiersEngine::getSatContext(){
146 return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext();
147 }
148
149 context::Context* QuantifiersEngine::getUserContext(){
150 return d_te->theoryOf( THEORY_QUANTIFIERS )->getUserContext();
151 }
152
153 OutputChannel& QuantifiersEngine::getOutputChannel(){
154 return d_te->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel();
155 }
156 /** get default valuation for the quantifiers engine */
157 Valuation& QuantifiersEngine::getValuation(){
158 return d_te->theoryOf( THEORY_QUANTIFIERS )->getValuation();
159 }
160
161 void QuantifiersEngine::finishInit(){
162 for( int i=0; i<(int)d_modules.size(); i++ ){
163 d_modules[i]->finishInit();
164 }
165 }
166
167 void QuantifiersEngine::check( Theory::Effort e ){
168 CodeTimer codeTimer(d_time);
169 bool needsCheck = e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call
170 std::vector< QuantifiersModule* > qm;
171 for( int i=0; i<(int)d_modules.size(); i++ ){
172 if( d_modules[i]->needsCheck( e ) ){
173 qm.push_back( d_modules[i] );
174 needsCheck = true;
175 }
176 }
177 if( needsCheck ){
178 Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl;
179 Trace("quant-engine-debug") << " modules to check : ";
180 for( unsigned i=0; i<qm.size(); i++ ){
181 Trace("quant-engine-debug") << qm[i]->identify() << " ";
182 }
183 Trace("quant-engine-debug") << std::endl;
184 Trace("quant-engine-debug") << " # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl;
185
186 if( !getMasterEqualityEngine()->consistent() ){
187 Trace("quant-engine") << "Master equality engine not consistent, return." << std::endl;
188 return;
189 }
190 Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
191 //reset relevant information
192 d_conflict = false;
193 d_hasAddedLemma = false;
194 d_term_db->reset( e );
195 d_eq_query->reset();
196 if( d_rel_dom ){
197 d_rel_dom->reset();
198 }
199 d_model->reset_round();
200 for( int i=0; i<(int)d_modules.size(); i++ ){
201 d_modules[i]->reset_round( e );
202 }
203 Trace("quant-engine-debug") << "Done resetting all modules." << std::endl;
204
205 if( e==Theory::EFFORT_LAST_CALL ){
206 //if effort is last call, try to minimize model first
207 if( options::finiteModelFind() ){
208 //first, check if we can minimize the model further FIXME: remove?
209 if( !((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){
210 return;
211 }
212 }
213 ++(d_statistics.d_instantiation_rounds_lc);
214 }else if( e==Theory::EFFORT_FULL ){
215 ++(d_statistics.d_instantiation_rounds);
216 }
217
218 Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
219 for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_MODEL; quant_e++ ){
220 for( int i=0; i<(int)qm.size(); i++ ){
221 Trace("quant-engine-debug") << "Check " << d_modules[i]->identify().c_str() << "..." << std::endl;
222 qm[i]->check( e, quant_e );
223 }
224 //flush all current lemmas
225 flushLemmas();
226 //if we have added one, stop
227 if( d_hasAddedLemma ){
228 break;
229 }
230 }
231 Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
232
233 //build the model if not done so already
234 // this happens if no quantifiers are currently asserted and no model-building module is enabled
235 if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
236 if( options::produceModels() && !d_model->isModelSet() ){
237 Trace("quant-engine-debug") << "Build the model..." << std::endl;
238 d_te->getModelBuilder()->buildModel( d_model, true );
239 Trace("quant-engine-debug") << "Done building the model." << std::endl;
240 }
241 if( Trace.isOn("inst-per-quant") ){
242 for( std::map< Node, int >::iterator it = d_total_inst_debug.begin(); it != d_total_inst_debug.end(); ++it ){
243 Trace("inst-per-quant") << " * " << it->second << " for " << it->first << std::endl;
244 }
245 }
246 }else{
247 if( Trace.isOn("inst-per-quant-round") ){
248 for( std::map< Node, int >::iterator it = d_temp_inst_debug.begin(); it != d_temp_inst_debug.end(); ++it ){
249 Trace("inst-per-quant-round") << " * " << it->second << " for " << it->first << std::endl;
250 d_temp_inst_debug[it->first] = 0;
251 }
252 }
253 }
254 Trace("quant-engine") << "Finished quantifiers engine check." << std::endl;
255 }
256 }
257
258 void QuantifiersEngine::registerQuantifier( Node f ){
259 if( std::find( d_quants.begin(), d_quants.end(), f )==d_quants.end() ){
260 Trace("quant") << "QuantifiersEngine : Register quantifier ";
261 if( d_term_db->isRewriteRule( f ) ){
262 Trace("quant") << " (rewrite rule)";
263 }
264 Trace("quant") << " : " << f << std::endl;
265 d_quants.push_back( f );
266
267 ++(d_statistics.d_num_quant);
268 Assert( f.getKind()==FORALL );
269 //make instantiation constants for f
270 d_term_db->makeInstantiationConstantsFor( f );
271 //register with quantifier relevance
272 if( d_quant_rel ){
273 d_quant_rel->registerQuantifier( f );
274 }
275 //register with each module
276 for( int i=0; i<(int)d_modules.size(); i++ ){
277 d_modules[i]->registerQuantifier( f );
278 }
279 Node ceBody = d_term_db->getInstConstantBody( f );
280 //generate the phase requirements
281 d_phase_reqs[f] = new QuantPhaseReq( ceBody, true );
282 //also register it with the strong solver
283 if( options::finiteModelFind() ){
284 ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
285 }
286 }
287 }
288
289 void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
290 for(std::vector<Node>::iterator p = pattern.begin(); p != pattern.end(); ++p){
291 std::set< Node > added;
292 getTermDatabase()->addTerm( *p, added );
293 }
294 }
295
296 void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
297 if( !pol ){
298 //do skolemization
299 if( d_skolemized.find( f )==d_skolemized.end() ){
300 Node body = d_term_db->getSkolemizedBody( f );
301 NodeBuilder<> nb(kind::OR);
302 nb << f << body.notNode();
303 Node lem = nb;
304 if( Trace.isOn("quantifiers-sk") ){
305 Node slem = Rewriter::rewrite( lem );
306 Trace("quantifiers-sk") << "Skolemize lemma : " << slem << std::endl;
307 }
308 getOutputChannel().lemma( lem, false, true );
309 d_skolemized[f] = true;
310 }
311 }
312 //assert to modules TODO : handle !pol
313 if( pol ){
314 //register the quantifier
315 registerQuantifier( f );
316 //assert it to each module
317 d_model->assertQuantifier( f );
318 for( int i=0; i<(int)d_modules.size(); i++ ){
319 d_modules[i]->assertNode( f );
320 }
321 }
322 }
323
324 void QuantifiersEngine::propagate( Theory::Effort level ){
325 CodeTimer codeTimer(d_time);
326
327 for( int i=0; i<(int)d_modules.size(); i++ ){
328 d_modules[i]->propagate( level );
329 }
330 }
331
332 Node QuantifiersEngine::getNextDecisionRequest(){
333 for( int i=0; i<(int)d_modules.size(); i++ ){
334 Node n = d_modules[i]->getNextDecisionRequest();
335 if( !n.isNull() ){
336 return n;
337 }
338 }
339 return Node::null();
340 }
341
342 void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){
343 std::set< Node > added;
344 getTermDatabase()->addTerm( n, added, withinQuant );
345 //maybe have triggered instantiations if we are doing eager instantiation
346 if( options::eagerInstQuant() ){
347 flushLemmas();
348 }
349 //added contains also the Node that just have been asserted in this branch
350 if( d_quant_rel ){
351 for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
352 if( !withinQuant ){
353 d_quant_rel->setRelevance( i->getOperator(), 0 );
354 }
355 }
356 }
357 }
358
359 void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ){
360 for( size_t i=0; i<f[0].getNumChildren(); i++ ){
361 Node n = m.get( i );
362 if( !n.isNull() ){
363 vars.push_back( f[0][i] );
364 terms.push_back( n );
365 }
366 }
367 }
368
369 bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
370 Assert( f.getKind()==FORALL );
371 Assert( vars.size()==terms.size() );
372 Node body = getInstantiation( f, vars, terms );
373 //make the lemma
374 NodeBuilder<> nb(kind::OR);
375 nb << f.notNode() << body;
376 Node lem = nb;
377 //check for duplication
378 if( addLemma( lem ) ){
379 d_total_inst_debug[f]++;
380 d_temp_inst_debug[f]++;
381 d_total_inst_count_debug++;
382 Trace("inst") << "*** Instantiate " << f << " with " << std::endl;
383 for( int i=0; i<(int)terms.size(); i++ ){
384 Trace("inst") << " " << terms[i];
385 Trace("inst") << std::endl;
386 }
387 if( options::cbqi() ){
388 for( int i=0; i<(int)terms.size(); i++ ){
389 if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){
390 Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl;
391 for( int i=0; i<(int)terms.size(); i++ ){
392 Debug("inst") << " " << terms[i] << std::endl;
393 }
394 Unreachable("Bad instantiation");
395 }
396 }
397 }
398 if( options::instMaxLevel()!=-1 ){
399 uint64_t maxInstLevel = 0;
400 for( int i=0; i<(int)terms.size(); i++ ){
401 if( terms[i].hasAttribute(InstLevelAttribute()) ){
402 if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
403 maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
404 }
405 }
406 }
407 setInstantiationLevelAttr( body, f[1], maxInstLevel+1 );
408 }
409 Trace("inst-debug") << "*** Lemma is " << lem << std::endl;
410 ++(d_statistics.d_instantiations);
411 return true;
412 }else{
413 ++(d_statistics.d_inst_duplicate);
414 return false;
415 }
416 }
417
418 void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t level ){
419 Trace("inst-level-debug") << "IL : " << n << " " << qn << " " << level << std::endl;
420 //if not from the vector of terms we instantiatied
421 if( qn.getKind()!=BOUND_VARIABLE && n!=qn ){
422 //if this is a new term, without an instantiation level
423 if( !n.hasAttribute(InstLevelAttribute()) ){
424 InstLevelAttribute ila;
425 n.setAttribute(ila,level);
426 Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl;
427 }
428 Assert( n.getNumChildren()==qn.getNumChildren() );
429 for( int i=0; i<(int)n.getNumChildren(); i++ ){
430 setInstantiationLevelAttr( n[i], qn[i], level );
431 }
432 }
433 }
434
435 void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){
436 InstLevelAttribute ila;
437 n.setAttribute(ila,level);
438 for( int i=0; i<(int)n.getNumChildren(); i++ ){
439 setInstantiationLevelAttr( n[i], level );
440 }
441 }
442
443 Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms ){
444 if( n.getKind()==INST_CONSTANT ){
445 Debug("check-inst") << "Substitute inst constant : " << n << std::endl;
446 return terms[n.getAttribute(InstVarNumAttribute())];
447 }else{
448 //if( !quantifiers::TermDb::hasInstConstAttr( n ) ){
449 //Debug("check-inst") << "No inst const attr : " << n << std::endl;
450 //return n;
451 //}else{
452 //Debug("check-inst") << "Recurse on : " << n << std::endl;
453 std::vector< Node > cc;
454 if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
455 cc.push_back( n.getOperator() );
456 }
457 bool changed = false;
458 for( unsigned i=0; i<n.getNumChildren(); i++ ){
459 Node c = getSubstitute( n[i], terms );
460 cc.push_back( c );
461 changed = changed || c!=n[i];
462 }
463 if( changed ){
464 Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cc );
465 return ret;
466 }else{
467 return n;
468 }
469 }
470 }
471
472
473 Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
474 Node body;
475 //process partial instantiation if necessary
476 if( d_term_db->d_vars[f].size()!=vars.size() ){
477 body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
478 std::vector< Node > uninst_vars;
479 //doing a partial instantiation, must add quantifier for all uninstantiated variables
480 for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
481 if( std::find( vars.begin(), vars.end(), f[0][i] )==vars.end() ){
482 uninst_vars.push_back( f[0][i] );
483 }
484 }
485 Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, uninst_vars );
486 body = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
487 Trace("partial-inst") << "Partial instantiation : " << f << std::endl;
488 Trace("partial-inst") << " : " << body << std::endl;
489 }else{
490 //do optimized version
491 Node icb = d_term_db->getInstConstantBody( f );
492 body = getSubstitute( icb, terms );
493 if( Debug.isOn("check-inst") ){
494 Node body2 = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
495 if( body!=body2 ){
496 Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl;
497 }
498 }
499 }
500 return body;
501 }
502
503 Node QuantifiersEngine::getInstantiation( Node f, InstMatch& m ){
504 std::vector< Node > vars;
505 std::vector< Node > terms;
506 computeTermVector( f, m, vars, terms );
507 return getInstantiation( f, vars, terms );
508 }
509
510 Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& terms ) {
511 return getInstantiation( f, d_term_db->d_inst_constants[f], terms );
512 }
513
514 bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
515 if( options::incrementalSolving() ){
516 if( d_c_inst_match_trie.find( f )!=d_c_inst_match_trie.end() ){
517 if( d_c_inst_match_trie[f]->existsInstMatch( this, f, m, getUserContext(), modEq, modInst ) ){
518 return true;
519 }
520 }
521 }else{
522 if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){
523 if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, modInst ) ){
524 return true;
525 }
526 }
527 }
528 //also check model engine (it may contain instantiations internally)
529 if( d_model_engine->getModelBuilder()->existsInstantiation( f, m, modEq, modInst ) ){
530 return true;
531 }
532 return false;
533 }
534
535 bool QuantifiersEngine::addLemma( Node lem, bool doCache ){
536 if( doCache ){
537 Debug("inst-engine-debug") << "Adding lemma : " << lem << std::endl;
538 lem = Rewriter::rewrite(lem);
539 if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
540 //d_curr_out->lemma( lem, false, true );
541 d_lemmas_produced_c[ lem ] = true;
542 d_lemmas_waiting.push_back( lem );
543 Debug("inst-engine-debug") << "Added lemma : " << lem << std::endl;
544 return true;
545 }else{
546 Debug("inst-engine-debug") << "Duplicate." << std::endl;
547 return false;
548 }
549 }else{
550 d_lemmas_waiting.push_back( lem );
551 return true;
552 }
553 }
554
555 void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
556 d_phase_req_waiting[lit] = req;
557 }
558
559 bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst ){
560 std::vector< Node > terms;
561 //make sure there are values for each variable we are instantiating
562 for( size_t i=0; i<f[0].getNumChildren(); i++ ){
563 Node val = m.get( i );
564 if( val.isNull() ){
565 Node ic = d_term_db->getInstantiationConstant( f, i );
566 val = d_term_db->getFreeVariableForInstConstant( ic );
567 Trace("inst-add-debug") << "mkComplete " << val << std::endl;
568 }
569 terms.push_back( val );
570 }
571 return addInstantiation( f, terms, mkRep, modEq, modInst );
572 }
573
574 bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst ) {
575 Assert( terms.size()==f[0].getNumChildren() );
576 Trace("inst-add-debug") << "Add instantiation: ";
577 for( unsigned i=0; i<terms.size(); i++ ){
578 if( i>0 ) Trace("inst-add-debug") << ", ";
579 Trace("inst-add-debug") << f[0][i] << " -> " << terms[i];
580 //make it representative, this is helpful for recognizing duplication
581 if( mkRep ){
582 //pick the best possible representative for instantiation, based on past use and simplicity of term
583 terms[i] = d_eq_query->getInternalRepresentative( terms[i], f, i );
584 //Trace("inst-add-debug") << " (" << terms[i] << ")";
585 }
586 }
587 Trace("inst-add-debug") << std::endl;
588
589 if( options::instMaxLevel()!=-1 ){
590 for( unsigned i=0; i<terms.size(); i++ ){
591 if( terms[i].hasAttribute(InstLevelAttribute()) ){
592 unsigned ml = options::instMaxLevel();
593 if( f.hasAttribute(QuantInstLevelAttribute()) ){
594 ml = f.getAttribute(QuantInstLevelAttribute());
595 }
596 if( terms[i].getAttribute(InstLevelAttribute())>ml ){
597 Trace("inst-add-debug") << "Term " << terms[i] << " has instantiation level " << terms[i].getAttribute(InstLevelAttribute());
598 Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl;
599 return false;
600 }
601 }else{
602 if( options::instLevelInputOnly() ){
603 Trace("inst-add-debug") << "Term " << terms[i] << " does not have an instantiation level." << std::endl;
604 return false;
605 }
606 }
607 }
608 }
609 //check for entailment
610 if( options::instNoEntail() ){
611 std::map< TNode, TNode > subs;
612 for( unsigned i=0; i<terms.size(); i++ ){
613 subs[f[0][i]] = terms[i];
614 }
615 if( d_term_db->isEntailed( f[1], subs, false, true ) ){
616 Trace("inst-add-debug") << " -> Currently entailed." << std::endl;
617 return false;
618 }
619 }
620
621 //check for duplication
622 bool alreadyExists = false;
623 if( options::incrementalSolving() ){
624 Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << ", modInst = " << modInst << std::endl;
625 inst::CDInstMatchTrie* imt;
626 std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( f );
627 if( it!=d_c_inst_match_trie.end() ){
628 imt = it->second;
629 }else{
630 imt = new CDInstMatchTrie( getUserContext() );
631 d_c_inst_match_trie[f] = imt;
632 }
633 alreadyExists = !imt->addInstMatch( this, f, terms, getUserContext(), modEq, modInst );
634 }else{
635 Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
636 alreadyExists = !d_inst_match_trie[f].addInstMatch( this, f, terms, modEq, modInst );
637 }
638 if( alreadyExists ){
639 Trace("inst-add-debug") << " -> Already exists." << std::endl;
640 ++(d_statistics.d_inst_duplicate_eq);
641 return false;
642 }
643
644
645 //add the instantiation
646 bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms );
647 //report the result
648 if( addedInst ){
649 Trace("inst-add-debug") << " -> Success." << std::endl;
650 return true;
651 }else{
652 Trace("inst-add-debug") << " -> Lemma already exists." << std::endl;
653 return false;
654 }
655 }
656
657
658 bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){
659 n = Rewriter::rewrite( n );
660 Node lem = NodeManager::currentNM()->mkNode( OR, n, n.notNode() );
661 if( addLemma( lem ) ){
662 Debug("inst") << "*** Add split " << n<< std::endl;
663 return true;
664 }
665 return false;
666 }
667
668 bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool reqPhasePol ){
669 //Assert( !areEqual( n1, n2 ) );
670 //Assert( !areDisequal( n1, n2 ) );
671 Kind knd = n1.getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL;
672 Node fm = NodeManager::currentNM()->mkNode( knd, n1, n2 );
673 return addSplit( fm );
674 }
675
676 void QuantifiersEngine::flushLemmas(){
677 if( !d_lemmas_waiting.empty() ){
678 //take default output channel if none is provided
679 d_hasAddedLemma = true;
680 for( int i=0; i<(int)d_lemmas_waiting.size(); i++ ){
681 getOutputChannel().lemma( d_lemmas_waiting[i], false, true );
682 }
683 d_lemmas_waiting.clear();
684 }
685 if( !d_phase_req_waiting.empty() ){
686 for( std::map< Node, bool >::iterator it = d_phase_req_waiting.begin(); it != d_phase_req_waiting.end(); ++it ){
687 getOutputChannel().requirePhase( it->first, it->second );
688 }
689 d_phase_req_waiting.clear();
690 }
691 }
692
693 void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
694 if( options::literalMatchMode()!=quantifiers::LITERAL_MATCH_NONE && d_phase_reqs.find( f )!=d_phase_reqs.end() ){
695 // doing literal-based matching (consider polarity of literals)
696 for( int i=0; i<(int)nodes.size(); i++ ){
697 Node prev = nodes[i];
698 bool nodeChanged = false;
699 if( d_phase_reqs[f]->isPhaseReq( nodes[i] ) ){
700 bool preq = d_phase_reqs[f]->getPhaseReq( nodes[i] );
701 nodes[i] = NodeManager::currentNM()->mkNode( IFF, nodes[i], NodeManager::currentNM()->mkConst<bool>(preq) );
702 nodeChanged = true;
703 }
704 //else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){
705 // Node req = qe->getPhaseReqEquality( f, trNodes[i] );
706 // trNodes[i] = NodeManager::currentNM()->mkNode( EQUAL, trNodes[i], req );
707 //}
708 if( nodeChanged ){
709 Debug("literal-matching") << " Make " << prev << " -> " << nodes[i] << std::endl;
710 ++(d_statistics.d_lit_phase_req);
711 }else{
712 ++(d_statistics.d_lit_phase_nreq);
713 }
714 }
715 }else{
716 d_statistics.d_lit_phase_nreq += (int)nodes.size();
717 }
718 }
719
720 void QuantifiersEngine::printInstantiations( std::ostream& out ) {
721 for( std::map< Node, bool >::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){
722 out << "Skolem constants of " << it->first << " : " << std::endl;
723 out << " ( ";
724 for( unsigned i=0; i<d_term_db->d_skolem_constants[it->first].size(); i++ ){
725 if( i>0 ){ out << ", "; }
726 out << d_term_db->d_skolem_constants[it->first][i];
727 }
728 out << " )" << std::endl;
729 out << std::endl;
730 }
731 if( options::incrementalSolving() ){
732 for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
733 out << "Instantiations of " << it->first << " : " << std::endl;
734 it->second->print( out, it->first );
735 }
736 }else{
737 for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
738 out << "Instantiations of " << it->first << " : " << std::endl;
739 it->second.print( out, it->first );
740 out << std::endl;
741 }
742 }
743 }
744
745 QuantifiersEngine::Statistics::Statistics():
746 d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
747 d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
748 d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
749 d_instantiations("QuantifiersEngine::Instantiations_Total", 0),
750 d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0),
751 d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0),
752 d_lit_phase_req("QuantifiersEngine::lit_phase_req", 0),
753 d_lit_phase_nreq("QuantifiersEngine::lit_phase_nreq", 0),
754 d_triggers("QuantifiersEngine::Triggers", 0),
755 d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
756 d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
757 d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0)
758 {
759 StatisticsRegistry::registerStat(&d_num_quant);
760 StatisticsRegistry::registerStat(&d_instantiation_rounds);
761 StatisticsRegistry::registerStat(&d_instantiation_rounds_lc);
762 StatisticsRegistry::registerStat(&d_instantiations);
763 StatisticsRegistry::registerStat(&d_inst_duplicate);
764 StatisticsRegistry::registerStat(&d_inst_duplicate_eq);
765 StatisticsRegistry::registerStat(&d_lit_phase_req);
766 StatisticsRegistry::registerStat(&d_lit_phase_nreq);
767 StatisticsRegistry::registerStat(&d_triggers);
768 StatisticsRegistry::registerStat(&d_simple_triggers);
769 StatisticsRegistry::registerStat(&d_multi_triggers);
770 StatisticsRegistry::registerStat(&d_multi_trigger_instantiations);
771 }
772
773 QuantifiersEngine::Statistics::~Statistics(){
774 StatisticsRegistry::unregisterStat(&d_num_quant);
775 StatisticsRegistry::unregisterStat(&d_instantiation_rounds);
776 StatisticsRegistry::unregisterStat(&d_instantiation_rounds_lc);
777 StatisticsRegistry::unregisterStat(&d_instantiations);
778 StatisticsRegistry::unregisterStat(&d_inst_duplicate);
779 StatisticsRegistry::unregisterStat(&d_inst_duplicate_eq);
780 StatisticsRegistry::unregisterStat(&d_lit_phase_req);
781 StatisticsRegistry::unregisterStat(&d_lit_phase_nreq);
782 StatisticsRegistry::unregisterStat(&d_triggers);
783 StatisticsRegistry::unregisterStat(&d_simple_triggers);
784 StatisticsRegistry::unregisterStat(&d_multi_triggers);
785 StatisticsRegistry::unregisterStat(&d_multi_trigger_instantiations);
786 }
787
788 eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
789 return ((quantifiers::TheoryQuantifiers*)getTheoryEngine()->theoryOf( THEORY_QUANTIFIERS ))->getMasterEqualityEngine();
790 }
791
792 void EqualityQueryQuantifiersEngine::reset(){
793 d_int_rep.clear();
794 d_reset_count++;
795 }
796
797 bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){
798 return getEngine()->hasTerm( a );
799 }
800
801 Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){
802 eq::EqualityEngine* ee = getEngine();
803 if( ee->hasTerm( a ) ){
804 return ee->getRepresentative( a );
805 }else{
806 return a;
807 }
808 }
809
810 bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
811 if( a==b ){
812 return true;
813 }else{
814 eq::EqualityEngine* ee = getEngine();
815 if( d_liberal ){
816 return true;//!areDisequal( a, b );
817 }else{
818 if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
819 if( ee->areEqual( a, b ) ){
820 return true;
821 }
822 }
823 return false;
824 }
825 }
826 }
827
828 bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
829 eq::EqualityEngine* ee = getEngine();
830 if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
831 if( ee->areDisequal( a, b, false ) ){
832 return true;
833 }
834 }
835 return false;
836 }
837
838 Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){
839 Node r = getRepresentative( a );
840 if( !options::internalReps() ){
841 return r;
842 }else{
843 if( d_int_rep.find( r )==d_int_rep.end() ){
844 //find best selection for representative
845 Node r_best;
846 //if( options::fmfRelevantDomain() && !f.isNull() ){
847 // Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl;
848 // r_best = d_qe->getRelevantDomain()->getRelevantTerm( f, index, r );
849 // Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl;
850 //}
851 std::vector< Node > eqc;
852 getEquivalenceClass( r, eqc );
853 Trace("internal-rep-select") << "Choose representative for equivalence class : { ";
854 for( unsigned i=0; i<eqc.size(); i++ ){
855 if( i>0 ) Trace("internal-rep-select") << ", ";
856 Trace("internal-rep-select") << eqc[i];
857 }
858 Trace("internal-rep-select") << " } " << std::endl;
859 int r_best_score = -1;
860 for( size_t i=0; i<eqc.size(); i++ ){
861 //if cbqi is active, do not choose instantiation constant terms
862 if( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(eqc[i]) ){
863 int score = getRepScore( eqc[i], f, index );
864 //score prefers earliest use of this term as a representative
865 if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
866 r_best = eqc[i];
867 r_best_score = score;
868 }
869 }
870 }
871 if( r_best.isNull() ){
872 if( !f.isNull() ){
873 Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index );
874 r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
875 }else{
876 r_best = a;
877 }
878 }
879 //now, make sure that no other member of the class is an instance
880 r_best = getInstance( r_best, eqc );
881 //store that this representative was chosen at this point
882 if( d_rep_score.find( r_best )==d_rep_score.end() ){
883 d_rep_score[ r_best ] = d_reset_count;
884 }
885 Trace("internal-rep-select") << "...Choose " << r_best << std::endl;
886 d_int_rep[r] = r_best;
887 if( r_best!=a ){
888 Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl;
889 Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
890 }
891 return r_best;
892 }else{
893 return d_int_rep[r];
894 }
895 }
896 }
897
898 void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ) {
899 //make sure internal representatives currently exist
900 for( std::map< TypeNode, std::vector< Node > >::iterator it = reps.begin(); it != reps.end(); ++it ){
901 if( it->first.isSort() ){
902 for( unsigned i=0; i<it->second.size(); i++ ){
903 Node r = getInternalRepresentative( it->second[i], Node::null(), 0 );
904 }
905 }
906 }
907 Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl;
908 for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){
909 Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl;
910 }
911 //store representatives for newly created terms
912 std::map< Node, Node > temp_rep_map;
913
914 bool success;
915 do {
916 success = false;
917 for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){
918 if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){
919 Node ni = it->second;
920 std::vector< Node > cc;
921 cc.push_back( it->second.getOperator() );
922 bool changed = false;
923 for( unsigned j=0; j<ni.getNumChildren(); j++ ){
924 if( ni[j].getType().isSort() ){
925 Node r = getRepresentative( ni[j] );
926 if( d_int_rep.find( r )==d_int_rep.end() ){
927 Assert( temp_rep_map.find( r )!=temp_rep_map.end() );
928 r = temp_rep_map[r];
929 }
930 if( r==ni ){
931 //found sub-term as instance
932 Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl;
933 d_int_rep[it->first] = ni[j];
934 changed = false;
935 success = true;
936 break;
937 }else{
938 Node ir = d_int_rep[r];
939 cc.push_back( ir );
940 if( ni[j]!=ir ){
941 changed = true;
942 }
943 }
944 }else{
945 changed = false;
946 break;
947 }
948 }
949 if( changed ){
950 Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc );
951 Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl;
952 success = true;
953 d_int_rep[it->first] = n;
954 temp_rep_map[n] = it->first;
955 }
956 }
957 }
958 }while( success );
959 Trace("internal-rep-flatten") << "---After flattening : " << std::endl;
960 for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){
961 Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl;
962 }
963 }
964
965 eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
966 return d_qe->getMasterEqualityEngine();
967 }
968
969 void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
970 eq::EqualityEngine* ee = getEngine();
971 if( ee->hasTerm( a ) ){
972 Node rep = ee->getRepresentative( a );
973 eq::EqClassIterator eqc_iter( rep, ee );
974 while( !eqc_iter.isFinished() ){
975 eqc.push_back( *eqc_iter );
976 eqc_iter++;
977 }
978 }else{
979 eqc.push_back( a );
980 }
981 //a should be in its equivalence class
982 Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() );
983 }
984
985 //helper functions
986
987 Node EqualityQueryQuantifiersEngine::getInstance( Node n, std::vector< Node >& eqc ){
988 for( size_t i=0; i<n.getNumChildren(); i++ ){
989 Node nn = getInstance( n[i], eqc );
990 if( !nn.isNull() ){
991 return nn;
992 }
993 }
994 if( std::find( eqc.begin(), eqc.end(), n )!=eqc.end() ){
995 return n;
996 }else{
997 return Node::null();
998 }
999 }
1000
1001 int getDepth( Node n ){
1002 if( n.getNumChildren()==0 ){
1003 return 0;
1004 }else{
1005 int maxDepth = -1;
1006 for( int i=0; i<(int)n.getNumChildren(); i++ ){
1007 int depth = getDepth( n[i] );
1008 if( depth>maxDepth ){
1009 maxDepth = depth;
1010 }
1011 }
1012 return maxDepth;
1013 }
1014 }
1015
1016 int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index ){
1017 return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n]; //initial
1018 //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n ); //term depth
1019 }
1020