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