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 = 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] );
 177         needsCheck = true;
 178       }
 179     }
 180   }
 181   if( needsCheck ){
 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() << " ";
 186     }
 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;
 190
 191     if( !getMasterEqualityEngine()->consistent() ){
 192       Trace("quant-engine") << "Master equality engine not consistent, return." << std::endl;
 193       return;
 194     }
 195     Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
 196     //reset relevant information
 197     d_conflict = false;
 198     d_hasAddedLemma = false;
 199
 200     //flush previous lemmas (for instance, if was interupted)
 201     flushLemmas();
 202     if( d_hasAddedLemma ){
 203       return;
 204     }
 205
 206     d_term_db->reset( e );
 207     d_eq_query->reset();
 208     if( d_rel_dom ){
 209       d_rel_dom->reset();
 210     }
 211     d_model->reset_round();
 212     for( int i=0; i<(int)d_modules.size(); i++ ){
 213       d_modules[i]->reset_round( e );
 214     }
 215     Trace("quant-engine-debug") << "Done resetting all modules." << std::endl;
 216
 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() ){
 221         return;
 222       }
 223       ++(d_statistics.d_instantiation_rounds_lc);
 224     }else if( e==Theory::EFFORT_FULL ){
 225       ++(d_statistics.d_instantiation_rounds);
 226     }
 227
 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 );
 233       }
 234       //flush all current lemmas
 235       flushLemmas();
 236       //if we have added one, stop
 237       if( d_hasAddedLemma ){
 238         break;
 239       }
 240     }
 241     Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
 242
 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;
 248       }
 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;
 252         }
 253       }
 254     }else{
 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;
 259         }
 260       }
 261     }
 262     Trace("quant-engine") << "Finished quantifiers engine check." << std::endl;
 263   }else{
 264     if( e==Theory::EFFORT_LAST_CALL && options::produceModels() ){
 265       needsBuildModel = true;
 266     }
 267   }
 268
 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;
 273   }
 274 }
 275
 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)";
 281     }
 282     Trace("quant") << " : " << f << std::endl;
 283     d_quants.push_back( f );
 284
 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
 290     if( d_quant_rel ){
 291       d_quant_rel->registerQuantifier( f );
 292     }
 293     //register with each module
 294     for( int i=0; i<(int)d_modules.size(); i++ ){
 295       d_modules[i]->registerQuantifier( f );
 296     }
 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 );
 303     }
 304   }
 305 }
 306
 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 );
 311   }
 312 }
 313
 314 void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
 315   if( !pol ){
 316     //do skolemization
 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();
 321       Node lem = nb;
 322       if( Trace.isOn("quantifiers-sk") ){
 323         Node slem = Rewriter::rewrite( lem );
 324         Trace("quantifiers-sk") << "Skolemize lemma : " << slem << std::endl;
 325       }
 326       getOutputChannel().lemma( lem, false, true );
 327       d_skolemized[f] = true;
 328     }
 329   }
 330   //assert to modules TODO : handle !pol
 331   if( 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 );
 338     }
 339   }
 340 }
 341
 342 void QuantifiersEngine::propagate( Theory::Effort level ){
 343   CodeTimer codeTimer(d_time);
 344
 345   for( int i=0; i<(int)d_modules.size(); i++ ){
 346     d_modules[i]->propagate( level );
 347   }
 348 }
 349
 350 Node QuantifiersEngine::getNextDecisionRequest(){
 351   for( int i=0; i<(int)d_modules.size(); i++ ){
 352     Node n = d_modules[i]->getNextDecisionRequest();
 353     if( !n.isNull() ){
 354       return n;
 355     }
 356   }
 357   return Node::null();
 358 }
 359
 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() ){
 365     flushLemmas();
 366   }
 367   //added contains also the Node that just have been asserted in this branch
 368   if( d_quant_rel ){
 369     for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
 370       if( !withinQuant ){
 371         d_quant_rel->setRelevance( i->getOperator(), 0 );
 372       }
 373     }
 374   }
 375 }
 376
 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++ ){
 379     Node n = m.get( i );
 380     if( !n.isNull() ){
 381       vars.push_back( f[0][i] );
 382       terms.push_back( n );
 383     }
 384   }
 385 }
 386
 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;
 392   //make the lemma
 393   NodeBuilder<> nb(kind::OR);
 394   nb << f.notNode() << body;
 395   Node lem = nb;
 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;
 405     }
 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;
 412           }
 413           Unreachable("Bad instantiation");
 414         }
 415       }
 416     }
 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());
 423           }
 424         }
 425       }
 426       setInstantiationLevelAttr( body, f[1], maxInstLevel+1 );
 427     }
 428     Trace("inst-debug") << "*** Lemma is " << lem << std::endl;
 429     ++(d_statistics.d_instantiations);
 430     return true;
 431   }else{
 432     ++(d_statistics.d_inst_duplicate);
 433     return false;
 434   }
 435 }
 436
 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;
 446     }
 447     Assert( n.getNumChildren()==qn.getNumChildren() );
 448     for( int i=0; i<(int)n.getNumChildren(); i++ ){
 449       setInstantiationLevelAttr( n[i], qn[i], level );
 450     }
 451   }
 452 }
 453
 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;
 459   }
 460   for( int i=0; i<(int)n.getNumChildren(); i++ ){
 461     setInstantiationLevelAttr( n[i], level );
 462   }
 463 }
 464
 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());
 470     }
 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;
 474       return false;
 475     }
 476   }else{
 477     if( options::instLevelInputOnly() ){
 478       Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl;
 479       return false;
 480     }
 481   }
 482   return true;
 483 }
 484
 485
 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())];
 490   }else{
 491     //if( !quantifiers::TermDb::hasInstConstAttr( n ) ){
 492       //Debug("check-inst") << "No inst const attr : " << n << std::endl;
 493       //return n;
 494     //}else{
 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() );
 499     }
 500     bool changed = false;
 501     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 502       Node c = getSubstitute( n[i], terms );
 503       cc.push_back( c );
 504       changed = changed || c!=n[i];
 505     }
 506     if( changed ){
 507       Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cc );
 508       return ret;
 509     }else{
 510       return n;
 511     }
 512   }
 513 }
 514
 515
 516 Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
 517   Node body;
 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] );
 526       }
 527     }
 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;
 532   }else{
 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() );
 538       if( body!=body2 ){
 539         Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl;
 540       }
 541     }
 542   }
 543   return body;
 544 }
 545
 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 );
 551 }
 552
 553 Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& terms ) {
 554   return getInstantiation( f, d_term_db->d_inst_constants[f], terms );
 555 }
 556
 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 ) ){
 561         return true;
 562       }
 563     }
 564   }else{
 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 ) ){
 567         return true;
 568       }
 569     }
 570   }
 571   //also check model engine (it may contain instantiations internally)
 572   if( d_model_engine->getModelBuilder()->existsInstantiation( f, m, modEq, modInst ) ){
 573     return true;
 574   }
 575   return false;
 576 }
 577
 578 bool QuantifiersEngine::addLemma( Node lem, bool doCache ){
 579   if( 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;
 587       return true;
 588     }else{
 589       Debug("inst-engine-debug") << "Duplicate." << std::endl;
 590       return false;
 591     }
 592   }else{
 593     d_lemmas_waiting.push_back( lem );
 594     return true;
 595   }
 596 }
 597
 598 void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
 599   d_phase_req_waiting[lit] = req;
 600 }
 601
 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();
 605
 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 );
 610     if( val.isNull() ){
 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;
 614     }
 615     terms.push_back( val );
 616   }
 617   return addInstantiation( f, terms, mkRep, modEq, modInst );
 618 }
 619
 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
 627     if( mkRep ){
 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] << ")";
 631     }
 632   }
 633   Trace("inst-add-debug") << std::endl;
 634
 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 ) ){
 639         return false;
 640       }
 641     }
 642   }
 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];
 648     }
 649     if( d_term_db->isEntailed( f[1], subs, false, true ) ){
 650       Trace("inst-add-debug") << " -> Currently entailed." << std::endl;
 651       return false;
 652     }
 653   }
 654
 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() ){
 662       imt = it->second;
 663     }else{
 664       imt = new CDInstMatchTrie( getUserContext() );
 665       d_c_inst_match_trie[f] = imt;
 666     }
 667     alreadyExists = !imt->addInstMatch( this, f, terms, getUserContext(), modEq, modInst );
 668   }else{
 669     Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
 670     alreadyExists = !d_inst_match_trie[f].addInstMatch( this, f, terms, modEq, modInst );
 671   }
 672   if( alreadyExists ){
 673     Trace("inst-add-debug") << " -> Already exists." << std::endl;
 674     ++(d_statistics.d_inst_duplicate_eq);
 675     return false;
 676   }
 677
 678
 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 );
 682   //report the result
 683   if( addedInst ){
 684     Trace("inst-add-debug") << " -> Success." << std::endl;
 685     return true;
 686   }else{
 687     Trace("inst-add-debug") << " -> Lemma already exists." << std::endl;
 688     return false;
 689   }
 690 }
 691
 692
 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;
 698     return true;
 699   }
 700   return false;
 701 }
 702
 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 );
 709 }
 710
 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 );
 717     }
 718     d_lemmas_waiting.clear();
 719   }
 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 );
 723     }
 724     d_phase_req_waiting.clear();
 725   }
 726 }
 727
 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) );
 737         nodeChanged = true;
 738       }
 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 );
 742       //}
 743       if( nodeChanged ){
 744         Debug("literal-matching") << "  Make " << prev << " -> " << nodes[i] << std::endl;
 745         ++(d_statistics.d_lit_phase_req);
 746       }else{
 747         ++(d_statistics.d_lit_phase_nreq);
 748       }
 749     }
 750   }else{
 751     d_statistics.d_lit_phase_nreq += (int)nodes.size();
 752   }
 753 }
 754
 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;
 758     out << "  ( ";
 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];
 762     }
 763     out << " )" << std::endl;
 764     out << std::endl;
 765   }
 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 );
 770     }
 771   }else{
 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 );
 775       out << std::endl;
 776     }
 777   }
 778 }
 779
 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)
 793 {
 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);
 806 }
 807
 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);
 821 }
 822
 823 eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
 824   return ((quantifiers::TheoryQuantifiers*)getTheoryEngine()->theoryOf( THEORY_QUANTIFIERS ))->getMasterEqualityEngine();
 825 }
 826
 827 void EqualityQueryQuantifiersEngine::reset(){
 828   d_int_rep.clear();
 829   d_reset_count++;
 830 }
 831
 832 bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){
 833   return getEngine()->hasTerm( a );
 834 }
 835
 836 Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){
 837   eq::EqualityEngine* ee = getEngine();
 838   if( ee->hasTerm( a ) ){
 839     return ee->getRepresentative( a );
 840   }else{
 841     return a;
 842   }
 843 }
 844
 845 bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
 846   if( a==b ){
 847     return true;
 848   }else{
 849     eq::EqualityEngine* ee = getEngine();
 850     if( d_liberal ){
 851       return true;//!areDisequal( a, b );
 852     }else{
 853       if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
 854         if( ee->areEqual( a, b ) ){
 855           return true;
 856         }
 857       }
 858       return false;
 859     }
 860   }
 861 }
 862
 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 ) ){
 867       return true;
 868     }
 869   }
 870   return false;
 871 }
 872
 873 Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){
 874   Node r = getRepresentative( a );
 875   if( !options::internalReps() ){
 876     return r;
 877   }else{
 878     if( d_int_rep.find( r )==d_int_rep.end() ){
 879       //find best selection for representative
 880       Node r_best;
 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;
 885       //}
 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];
 892       }
 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 ) ) ){
 900             r_best = eqc[i];
 901             r_best_score = score;
 902           }
 903         }
 904       }
 905       if( r_best.isNull() ){
 906         if( !f.isNull() ){
 907           Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index );
 908           r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
 909         }else{
 910           r_best = a;
 911         }
 912       }
 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;
 918       }
 919       Trace("internal-rep-select") << "...Choose " << r_best << std::endl;
 920       d_int_rep[r] = r_best;
 921       if( r_best!=a ){
 922         Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl;
 923         Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
 924       }
 925       return r_best;
 926     }else{
 927       return d_int_rep[r];
 928     }
 929   }
 930 }
 931
 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 );
 938       }
 939     }
 940   }
 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;
 944   }
 945   //store representatives for newly created terms
 946   std::map< Node, Node > temp_rep_map;
 947
 948   bool success;
 949   do {
 950     success = false;
 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() );
 962               r = temp_rep_map[r];
 963             }
 964             if( r==ni ){
 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];
 968               changed = false;
 969               success = true;
 970               break;
 971             }else{
 972               Node ir = d_int_rep[r];
 973               cc.push_back( ir );
 974               if( ni[j]!=ir ){
 975                 changed = true;
 976               }
 977             }
 978           }else{
 979             changed = false;
 980             break;
 981           }
 982         }
 983         if( changed ){
 984           Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc );
 985           Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl;
 986           success = true;
 987           d_int_rep[it->first] = n;
 988           temp_rep_map[n] = it->first;
 989         }
 990       }
 991     }
 992   }while( success );
 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;
 996   }
 997 }
 998
 999 eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
1000   return d_qe->getMasterEqualityEngine();
1001 }
1002
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 );
1010       eqc_iter++;
1011     }
1012   }else{
1013     eqc.push_back( a );
1014   }
1015   //a should be in its equivalence class
1016   Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() );
1017 }
1018
1019 //helper functions
1020
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 );
1024     if( !nn.isNull() ){
1025       return nn;
1026     }
1027   }
1028   if( std::find( eqc.begin(), eqc.end(), n )!=eqc.end() ){
1029     return n;
1030   }else{
1031     return Node::null();
1032   }
1033 }
1034
1035 int getDepth( Node n ){
1036   if( n.getNumChildren()==0 ){
1037     return 0;
1038   }else{
1039     int maxDepth = -1;
1040     for( int i=0; i<(int)n.getNumChildren(); i++ ){
1041       int depth = getDepth( n[i] );
1042       if( depth>maxDepth ){
1043         maxDepth = depth;
1044       }
1045     }
1046     return maxDepth;
1047   }
1048 }
1049
1050 //smaller the score, the better
1051 int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index ){
1052   int s;
1053   if( options::instMaxLevel()!=-1 ){
1054     //score prefer lowest instantiation level
1055     if( n.hasAttribute(InstLevelAttribute()) ){
1056       s = n.getAttribute(InstLevelAttribute());
1057     }else{
1058       s = options::instLevelInputOnly() ? -1 : 0;
1059     }
1060   }else{
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];
1063   }
1064   return s;
1065   //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n );    //term depth
1066 }
1067