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-2013  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
  32 using namespace std;
  33 using namespace CVC4;
  34 using namespace CVC4::kind;
  35 using namespace CVC4::context;
  36 using namespace CVC4::theory;
  37 using namespace CVC4::theory::inst;
  38
  39 QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
  40 d_te( te ),
  41 d_quant_rel( false ),
  42 d_lemmas_produced_c(u){
  43   d_eq_query = new EqualityQueryQuantifiersEngine( this );
  44   d_term_db = new quantifiers::TermDb( this );
  45   d_tr_trie = new inst::TriggerTrie;
  46   d_rr_tr_trie = new rrinst::TriggerTrie;
  47   d_eem = new EfficientEMatcher( this );
  48   d_hasAddedLemma = false;
  49
  50   //the model object
  51   if( options::fmfFullModelCheck() ){
  52     d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
  53   }else{
  54     d_model = new quantifiers::FirstOrderModelIG( c, "FirstOrderModelIG" );
  55   }
  56
  57   //add quantifiers modules
  58   if( !options::finiteModelFind() || options::fmfInstEngine() ){
  59     //the instantiation must set incomplete flag unless finite model finding is turned on
  60     d_inst_engine = new quantifiers::InstantiationEngine( this, !options::finiteModelFind() );
  61     d_modules.push_back(  d_inst_engine );
  62   }else{
  63     d_inst_engine = NULL;
  64   }
  65   if( options::finiteModelFind() ){
  66     d_model_engine = new quantifiers::ModelEngine( c, this );
  67     d_modules.push_back( d_model_engine );
  68     if( options::fmfBoundInt() ){
  69       d_bint = new quantifiers::BoundedIntegers( c, this );
  70       d_modules.push_back( d_bint );
  71     }else{
  72       d_bint = NULL;
  73     }
  74   }else{
  75     d_model_engine = NULL;
  76     d_bint = NULL;
  77   }
  78
  79   //options
  80   d_optInstCheckDuplicate = true;
  81   d_optInstMakeRepresentative = true;
  82   d_optInstAddSplits = false;
  83   d_optMatchIgnoreModelBasis = false;
  84   d_optInstLimitActive = false;
  85   d_optInstLimit = 0;
  86   d_total_inst_count_debug = 0;
  87 }
  88
  89 QuantifiersEngine::~QuantifiersEngine(){
  90   delete d_model_engine;
  91   delete d_inst_engine;
  92   delete d_model;
  93   delete d_term_db;
  94   delete d_eq_query;
  95 }
  96
  97 EqualityQuery* QuantifiersEngine::getEqualityQuery() {
  98   return d_eq_query;
  99 }
 100
 101 //Instantiator* QuantifiersEngine::getInstantiator( theory::TheoryId id ){
 102 //  return d_te->theoryOf( id )->getInstantiator();
 103 //}
 104
 105 context::Context* QuantifiersEngine::getSatContext(){
 106   return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext();
 107 }
 108
 109 context::Context* QuantifiersEngine::getUserContext(){
 110   return d_te->theoryOf( THEORY_QUANTIFIERS )->getUserContext();
 111 }
 112
 113 OutputChannel& QuantifiersEngine::getOutputChannel(){
 114   return d_te->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel();
 115 }
 116 /** get default valuation for the quantifiers engine */
 117 Valuation& QuantifiersEngine::getValuation(){
 118   return d_te->theoryOf( THEORY_QUANTIFIERS )->getValuation();
 119 }
 120
 121 void QuantifiersEngine::finishInit(){
 122   for( int i=0; i<(int)d_modules.size(); i++ ){
 123     d_modules[i]->finishInit();
 124   }
 125 }
 126
 127 void QuantifiersEngine::check( Theory::Effort e ){
 128   CodeTimer codeTimer(d_time);
 129   bool needsCheck = e>=Theory::EFFORT_LAST_CALL;  //always need to check at or above last call
 130   for( int i=0; i<(int)d_modules.size(); i++ ){
 131     if( d_modules[i]->needsCheck( e ) ){
 132       needsCheck = true;
 133     }
 134   }
 135   if( needsCheck ){
 136     Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl;
 137     if( !getMasterEqualityEngine()->consistent() ){
 138       Trace("quant-engine") << "Master equality engine not consistent, return." << std::endl;
 139       return;
 140     }
 141     //reset relevant information
 142     d_hasAddedLemma = false;
 143     d_term_db->reset( e );
 144     d_eq_query->reset();
 145     if( e==Theory::EFFORT_LAST_CALL ){
 146       //if effort is last call, try to minimize model first
 147       if( options::finiteModelFind() ){
 148         //first, check if we can minimize the model further
 149         if( !((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){
 150           return;
 151         }
 152       }
 153       ++(d_statistics.d_instantiation_rounds_lc);
 154     }else if( e==Theory::EFFORT_FULL ){
 155       ++(d_statistics.d_instantiation_rounds);
 156     }
 157     for( int i=0; i<(int)d_modules.size(); i++ ){
 158       d_modules[i]->check( e );
 159     }
 160     //build the model if not done so already
 161     //  this happens if no quantifiers are currently asserted and no model-building module is enabled
 162     if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
 163       if( options::produceModels() && !d_model->isModelSet() ){
 164         d_te->getModelBuilder()->buildModel( d_model, true );
 165       }
 166       if( Trace.isOn("inst-per-quant") ){
 167         for( std::map< Node, int >::iterator it = d_total_inst_debug.begin(); it != d_total_inst_debug.end(); ++it ){
 168           Trace("inst-per-quant") << " * " << it->second << " for " << it->first << std::endl;
 169         }
 170       }
 171     }else{
 172       if( Trace.isOn("inst-per-quant-round") ){
 173         for( std::map< Node, int >::iterator it = d_temp_inst_debug.begin(); it != d_temp_inst_debug.end(); ++it ){
 174           Trace("inst-per-quant-round") << " * " << it->second << " for " << it->first << std::endl;
 175           d_temp_inst_debug[it->first] = 0;
 176         }
 177       }
 178     }
 179     Trace("quant-engine") << "Finished quantifiers engine check." << std::endl;
 180   }
 181 }
 182
 183 void QuantifiersEngine::registerQuantifier( Node f ){
 184   if( std::find( d_quants.begin(), d_quants.end(), f )==d_quants.end() ){
 185     d_quants.push_back( f );
 186
 187     ++(d_statistics.d_num_quant);
 188     Assert( f.getKind()==FORALL );
 189     //make instantiation constants for f
 190     d_term_db->makeInstantiationConstantsFor( f );
 191     //register with quantifier relevance
 192     d_quant_rel.registerQuantifier( f );
 193     //register with each module
 194     for( int i=0; i<(int)d_modules.size(); i++ ){
 195       d_modules[i]->registerQuantifier( f );
 196     }
 197     Node ceBody = d_term_db->getInstConstantBody( f );
 198     //generate the phase requirements
 199     d_phase_reqs[f] = new QuantPhaseReq( ceBody, true );
 200     //also register it with the strong solver
 201     if( options::finiteModelFind() ){
 202       ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
 203     }
 204   }
 205 }
 206
 207 void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
 208   for(std::vector<Node>::iterator p = pattern.begin(); p != pattern.end(); ++p){
 209     std::set< Node > added;
 210     getTermDatabase()->addTerm(*p,added);
 211   }
 212 }
 213
 214 void QuantifiersEngine::assertNode( Node f ){
 215   Assert( f.getKind()==FORALL );
 216   d_model->assertQuantifier( f );
 217   for( int i=0; i<(int)d_modules.size(); i++ ){
 218     d_modules[i]->assertNode( f );
 219   }
 220 }
 221
 222 void QuantifiersEngine::propagate( Theory::Effort level ){
 223   CodeTimer codeTimer(d_time);
 224
 225   for( int i=0; i<(int)d_modules.size(); i++ ){
 226     d_modules[i]->propagate( level );
 227   }
 228 }
 229
 230 Node QuantifiersEngine::getNextDecisionRequest(){
 231   for( int i=0; i<(int)d_modules.size(); i++ ){
 232     Node n = d_modules[i]->getNextDecisionRequest();
 233     if( !n.isNull() ){
 234       return n;
 235     }
 236   }
 237   return Node::null();
 238 }
 239
 240 void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){
 241   std::set< Node > added;
 242   getTermDatabase()->addTerm( n, added, withinQuant );
 243   if( options::efficientEMatching() ){
 244     d_eem->newTerms( added );
 245   }
 246   //added contains also the Node that just have been asserted in this branch
 247   for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
 248     if( !withinQuant ){
 249       d_quant_rel.setRelevance( i->getOperator(), 0 );
 250     }
 251   }
 252 }
 253
 254 void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ){
 255   for( size_t i=0; i<d_term_db->d_inst_constants[f].size(); i++ ){
 256     Node n = m.getValue( d_term_db->d_inst_constants[f][i] );
 257     if( !n.isNull() ){
 258       vars.push_back( f[0][i] );
 259       terms.push_back( n );
 260     }
 261   }
 262 }
 263
 264 bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
 265   Assert( f.getKind()==FORALL );
 266   Assert( vars.size()==terms.size() );
 267   Node body = getInstantiation( f, vars, terms );
 268   //make the lemma
 269   NodeBuilder<> nb(kind::OR);
 270   nb << f.notNode() << body;
 271   Node lem = nb;
 272   //check for duplication
 273   if( addLemma( lem ) ){
 274     d_total_inst_debug[f]++;
 275     d_temp_inst_debug[f]++;
 276     d_total_inst_count_debug++;
 277     Trace("inst") << "*** Instantiate " << f << " with " << std::endl;
 278     uint64_t maxInstLevel = 0;
 279     for( int i=0; i<(int)terms.size(); i++ ){
 280       if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){
 281         Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl;
 282         for( int i=0; i<(int)terms.size(); i++ ){
 283           Debug("inst") << "   " << terms[i] << std::endl;
 284         }
 285         Unreachable("Bad instantiation");
 286       }else{
 287         Trace("inst") << "   " << terms[i];
 288         //Debug("inst-engine") << " " << terms[i].getAttribute(InstLevelAttribute());
 289         Trace("inst") << std::endl;
 290         if( terms[i].hasAttribute(InstLevelAttribute()) ){
 291           if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
 292             maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
 293           }
 294         }else{
 295           setInstantiationLevelAttr( terms[i], 0 );
 296         }
 297       }
 298     }
 299     Trace("inst-debug") << "*** Lemma is " << lem << std::endl;
 300     setInstantiationLevelAttr( body, maxInstLevel+1 );
 301     ++(d_statistics.d_instantiations);
 302     d_statistics.d_total_inst_var += (int)terms.size();
 303     d_statistics.d_max_instantiation_level.maxAssign( maxInstLevel+1 );
 304     return true;
 305   }else{
 306     ++(d_statistics.d_inst_duplicate);
 307     return false;
 308   }
 309 }
 310
 311 void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){
 312   if( !n.hasAttribute(InstLevelAttribute()) ){
 313     InstLevelAttribute ila;
 314     n.setAttribute(ila,level);
 315   }
 316   for( int i=0; i<(int)n.getNumChildren(); i++ ){
 317     setInstantiationLevelAttr( n[i], level );
 318   }
 319 }
 320
 321 Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
 322   Node body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
 323   //process partial instantiation if necessary
 324   if( d_term_db->d_vars[f].size()!=vars.size() ){
 325     std::vector< Node > uninst_vars;
 326     //doing a partial instantiation, must add quantifier for all uninstantiated variables
 327     for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
 328       if( std::find( vars.begin(), vars.end(), f[0][i] )==vars.end() ){
 329         uninst_vars.push_back( f[0][i] );
 330       }
 331     }
 332     Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, uninst_vars );
 333     body = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
 334     Trace("partial-inst") << "Partial instantiation : " << f << std::endl;
 335     Trace("partial-inst") << "                      : " << body << std::endl;
 336   }
 337   return body;
 338 }
 339
 340 Node QuantifiersEngine::getInstantiation( Node f, InstMatch& m ){
 341   std::vector< Node > vars;
 342   std::vector< Node > terms;
 343   computeTermVector( f, m, vars, terms );
 344   return getInstantiation( f, vars, terms );
 345 }
 346
 347 bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
 348   if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){
 349     if( d_inst_match_trie[f]->existsInstMatch( this, f, m, modEq, modInst ) ){
 350       return true;
 351     }
 352   }
 353   //also check model engine (it may contain instantiations internally)
 354   if( d_model_engine->getModelBuilder()->existsInstantiation( f, m, modEq, modInst ) ){
 355     return true;
 356   }
 357   return false;
 358 }
 359
 360 bool QuantifiersEngine::addLemma( Node lem ){
 361   Debug("inst-engine-debug") << "Adding lemma : " << lem << std::endl;
 362   lem = Rewriter::rewrite(lem);
 363   if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
 364     //d_curr_out->lemma( lem );
 365     d_lemmas_produced_c[ lem ] = true;
 366     d_lemmas_waiting.push_back( lem );
 367     Debug("inst-engine-debug") << "Added lemma : " << lem << std::endl;
 368     return true;
 369   }else{
 370     Debug("inst-engine-debug") << "Duplicate." << std::endl;
 371     return false;
 372   }
 373 }
 374
 375 bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool modInst, bool mkRep ){
 376   Trace("inst-add-debug") << "Add instantiation: " << m << std::endl;
 377   //make sure there are values for each variable we are instantiating
 378   for( size_t i=0; i<f[0].getNumChildren(); i++ ){
 379     Node ic = d_term_db->getInstantiationConstant( f, i );
 380     Node val = m.getValue( ic );
 381     if( val.isNull() ){
 382       val = d_term_db->getFreeVariableForInstConstant( ic );
 383       Trace("inst-add-debug") << "mkComplete " << val << std::endl;
 384       m.set( ic, val );
 385     }
 386     //make it representative, this is helpful for recognizing duplication
 387     if( mkRep ){
 388       //pick the best possible representative for instantiation, based on past use and simplicity of term
 389       Node r = d_eq_query->getInternalRepresentative( val, f, i );
 390       Trace("inst-add-debug") << "mkRep " << r << " " << val << std::endl;
 391       m.set( ic, r );
 392     }
 393   }
 394   //check for duplication modulo equality
 395   inst::CDInstMatchTrie* imt;
 396   std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_inst_match_trie.find( f );
 397   if( it!=d_inst_match_trie.end() ){
 398     imt = it->second;
 399   }else{
 400     imt = new CDInstMatchTrie( getUserContext() );
 401     d_inst_match_trie[f] = imt;
 402   }
 403   Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
 404   if( !imt->addInstMatch( this, f, m, getUserContext(), modEq, modInst ) ){
 405     Trace("inst-add-debug") << " -> Already exists." << std::endl;
 406     ++(d_statistics.d_inst_duplicate);
 407     return false;
 408   }
 409   Trace("inst-add-debug") << "compute terms" << std::endl;
 410   //compute the vector of terms for the instantiation
 411   std::vector< Node > terms;
 412   for( size_t i=0; i<d_term_db->d_inst_constants[f].size(); i++ ){
 413     Node n = m.getValue( d_term_db->d_inst_constants[f][i] );
 414     Assert( !n.isNull() );
 415     terms.push_back( n );
 416   }
 417   //add the instantiation
 418   bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms );
 419   //report the result
 420   if( addedInst ){
 421     Trace("inst-add") << "Added instantiation for " << f << ": " << std::endl;
 422     Trace("inst-add") << "   " << m << std::endl;
 423     Trace("inst-add-debug") << " -> Success." << std::endl;
 424     return true;
 425   }else{
 426     Trace("inst-add-debug") << " -> Lemma already exists." << std::endl;
 427     return false;
 428   }
 429 }
 430
 431 bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){
 432   n = Rewriter::rewrite( n );
 433   Node lem = NodeManager::currentNM()->mkNode( OR, n, n.notNode() );
 434   if( addLemma( lem ) ){
 435     ++(d_statistics.d_splits);
 436     Debug("inst") << "*** Add split " << n<< std::endl;
 437     //if( reqPhase ){
 438     //  d_curr_out->requirePhase( n, reqPhasePol );
 439     //}
 440     return true;
 441   }
 442   return false;
 443 }
 444
 445 bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool reqPhasePol ){
 446   //Assert( !areEqual( n1, n2 ) );
 447   //Assert( !areDisequal( n1, n2 ) );
 448   Kind knd = n1.getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL;
 449   Node fm = NodeManager::currentNM()->mkNode( knd, n1, n2 );
 450   return addSplit( fm );
 451 }
 452
 453 void QuantifiersEngine::flushLemmas( OutputChannel* out ){
 454   if( !d_lemmas_waiting.empty() ){
 455     //take default output channel if none is provided
 456     d_hasAddedLemma = true;
 457     for( int i=0; i<(int)d_lemmas_waiting.size(); i++ ){
 458       if( out ){
 459         out->lemma( d_lemmas_waiting[i] );
 460       }
 461     }
 462     d_lemmas_waiting.clear();
 463   }
 464 }
 465
 466 void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
 467   if( options::literalMatchMode()!=quantifiers::LITERAL_MATCH_NONE && d_phase_reqs.find( f )!=d_phase_reqs.end() ){
 468     // doing literal-based matching (consider polarity of literals)
 469     for( int i=0; i<(int)nodes.size(); i++ ){
 470       Node prev = nodes[i];
 471       bool nodeChanged = false;
 472       if( d_phase_reqs[f]->isPhaseReq( nodes[i] ) ){
 473         bool preq = d_phase_reqs[f]->getPhaseReq( nodes[i] );
 474         nodes[i] = NodeManager::currentNM()->mkNode( IFF, nodes[i], NodeManager::currentNM()->mkConst<bool>(preq) );
 475         nodeChanged = true;
 476       }
 477       //else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){
 478       //  Node req = qe->getPhaseReqEquality( f, trNodes[i] );
 479       //  trNodes[i] = NodeManager::currentNM()->mkNode( EQUAL, trNodes[i], req );
 480       //}
 481       if( nodeChanged ){
 482         Debug("literal-matching") << "  Make " << prev << " -> " << nodes[i] << std::endl;
 483         ++(d_statistics.d_lit_phase_req);
 484       }else{
 485         ++(d_statistics.d_lit_phase_nreq);
 486       }
 487     }
 488   }else{
 489     d_statistics.d_lit_phase_nreq += (int)nodes.size();
 490   }
 491 }
 492
 493 QuantifiersEngine::Statistics::Statistics():
 494   d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
 495   d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
 496   d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
 497   d_instantiations("QuantifiersEngine::Instantiations_Total", 0),
 498   d_max_instantiation_level("QuantifiersEngine::Max_Instantiation_Level", 0),
 499   d_splits("QuantifiersEngine::Total_Splits", 0),
 500   d_total_inst_var("QuantifiersEngine::Vars_Inst", 0),
 501   d_total_inst_var_unspec("QuantifiersEngine::Vars_Inst_Unspecified", 0),
 502   d_inst_unspec("QuantifiersEngine::Unspecified_Inst", 0),
 503   d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0),
 504   d_lit_phase_req("QuantifiersEngine::lit_phase_req", 0),
 505   d_lit_phase_nreq("QuantifiersEngine::lit_phase_nreq", 0),
 506   d_triggers("QuantifiersEngine::Triggers", 0),
 507   d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
 508   d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
 509   d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
 510   d_term_in_termdb("QuantifiersEngine::Term_in_TermDb", 0),
 511   d_num_mono_candidates("QuantifiersEngine::NumMonoCandidates", 0),
 512   d_num_mono_candidates_new_term("QuantifiersEngine::NumMonoCandidatesNewTerm", 0),
 513   d_num_multi_candidates("QuantifiersEngine::NumMultiCandidates", 0),
 514   d_mono_candidates_cache_hit("QuantifiersEngine::MonoCandidatesCacheHit", 0),
 515   d_mono_candidates_cache_miss("QuantifiersEngine::MonoCandidatesCacheMiss", 0),
 516   d_multi_candidates_cache_hit("QuantifiersEngine::MultiCandidatesCacheHit", 0),
 517   d_multi_candidates_cache_miss("QuantifiersEngine::MultiCandidatesCacheMiss", 0)
 518 {
 519   StatisticsRegistry::registerStat(&d_num_quant);
 520   StatisticsRegistry::registerStat(&d_instantiation_rounds);
 521   StatisticsRegistry::registerStat(&d_instantiation_rounds_lc);
 522   StatisticsRegistry::registerStat(&d_instantiations);
 523   StatisticsRegistry::registerStat(&d_max_instantiation_level);
 524   StatisticsRegistry::registerStat(&d_splits);
 525   StatisticsRegistry::registerStat(&d_total_inst_var);
 526   StatisticsRegistry::registerStat(&d_total_inst_var_unspec);
 527   StatisticsRegistry::registerStat(&d_inst_unspec);
 528   StatisticsRegistry::registerStat(&d_inst_duplicate);
 529   StatisticsRegistry::registerStat(&d_lit_phase_req);
 530   StatisticsRegistry::registerStat(&d_lit_phase_nreq);
 531   StatisticsRegistry::registerStat(&d_triggers);
 532   StatisticsRegistry::registerStat(&d_simple_triggers);
 533   StatisticsRegistry::registerStat(&d_multi_triggers);
 534   StatisticsRegistry::registerStat(&d_multi_trigger_instantiations);
 535   StatisticsRegistry::registerStat(&d_term_in_termdb);
 536   StatisticsRegistry::registerStat(&d_num_mono_candidates);
 537   StatisticsRegistry::registerStat(&d_num_mono_candidates_new_term);
 538   StatisticsRegistry::registerStat(&d_num_multi_candidates);
 539   StatisticsRegistry::registerStat(&d_mono_candidates_cache_hit);
 540   StatisticsRegistry::registerStat(&d_mono_candidates_cache_miss);
 541   StatisticsRegistry::registerStat(&d_multi_candidates_cache_hit);
 542   StatisticsRegistry::registerStat(&d_multi_candidates_cache_miss);
 543 }
 544
 545 QuantifiersEngine::Statistics::~Statistics(){
 546   StatisticsRegistry::unregisterStat(&d_num_quant);
 547   StatisticsRegistry::unregisterStat(&d_instantiation_rounds);
 548   StatisticsRegistry::unregisterStat(&d_instantiation_rounds_lc);
 549   StatisticsRegistry::unregisterStat(&d_instantiations);
 550   StatisticsRegistry::unregisterStat(&d_max_instantiation_level);
 551   StatisticsRegistry::unregisterStat(&d_splits);
 552   StatisticsRegistry::unregisterStat(&d_total_inst_var);
 553   StatisticsRegistry::unregisterStat(&d_total_inst_var_unspec);
 554   StatisticsRegistry::unregisterStat(&d_inst_unspec);
 555   StatisticsRegistry::unregisterStat(&d_inst_duplicate);
 556   StatisticsRegistry::unregisterStat(&d_lit_phase_req);
 557   StatisticsRegistry::unregisterStat(&d_lit_phase_nreq);
 558   StatisticsRegistry::unregisterStat(&d_triggers);
 559   StatisticsRegistry::unregisterStat(&d_simple_triggers);
 560   StatisticsRegistry::unregisterStat(&d_multi_triggers);
 561   StatisticsRegistry::unregisterStat(&d_multi_trigger_instantiations);
 562   StatisticsRegistry::unregisterStat(&d_term_in_termdb);
 563   StatisticsRegistry::unregisterStat(&d_num_mono_candidates);
 564   StatisticsRegistry::unregisterStat(&d_num_mono_candidates_new_term);
 565   StatisticsRegistry::unregisterStat(&d_num_multi_candidates);
 566   StatisticsRegistry::unregisterStat(&d_mono_candidates_cache_hit);
 567   StatisticsRegistry::unregisterStat(&d_mono_candidates_cache_miss);
 568   StatisticsRegistry::unregisterStat(&d_multi_candidates_cache_hit);
 569   StatisticsRegistry::unregisterStat(&d_multi_candidates_cache_miss);
 570 }
 571
 572 eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
 573   return ((quantifiers::TheoryQuantifiers*)getTheoryEngine()->theoryOf( THEORY_QUANTIFIERS ))->getMasterEqualityEngine();
 574 }
 575
 576 void EqualityQueryQuantifiersEngine::reset(){
 577   d_int_rep.clear();
 578   d_reset_count++;
 579 }
 580
 581 bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){
 582   return getEngine()->hasTerm( a );
 583 }
 584
 585 Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){
 586   eq::EqualityEngine* ee = getEngine();
 587   if( ee->hasTerm( a ) ){
 588     return ee->getRepresentative( a );
 589   }
 590   return a;
 591 }
 592
 593 bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
 594   if( a==b ){
 595     return true;
 596   }else{
 597     eq::EqualityEngine* ee = getEngine();
 598     if( d_liberal ){
 599       return true;//!areDisequal( a, b );
 600     }else{
 601       if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
 602         if( ee->areEqual( a, b ) ){
 603           return true;
 604         }
 605       }
 606       return false;
 607     }
 608   }
 609 }
 610
 611 bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
 612   eq::EqualityEngine* ee = getEngine();
 613   if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
 614     if( ee->areDisequal( a, b, false ) ){
 615       return true;
 616     }
 617   }
 618   return false;
 619 }
 620
 621 Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){
 622   Node r = getRepresentative( a );
 623   if( !options::internalReps() ){
 624     return r;
 625   }else{
 626     int sortId = 0;
 627     if( optInternalRepSortInference() ){
 628       sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( f, f[0][index] );
 629     }
 630     if( d_int_rep[sortId].find( r )==d_int_rep[sortId].end() ){
 631       std::vector< Node > eqc;
 632       getEquivalenceClass( r, eqc );
 633       //find best selection for representative
 634       Node r_best;
 635       int r_best_score = -1;
 636       for( size_t i=0; i<eqc.size(); i++ ){
 637         int score = getRepScore( eqc[i], f, index );
 638         if( optInternalRepSortInference() ){
 639           int e_sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( eqc[i]);
 640           if( score>=0 && e_sortId!=sortId ){
 641             score += 100;
 642           }
 643         }
 644         //score prefers earliest use of this term as a representative
 645         if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
 646           r_best = eqc[i];
 647           r_best_score = score;
 648         }
 649       }
 650       //now, make sure that no other member of the class is an instance
 651       if( !optInternalRepSortInference() ){
 652         r_best = getInstance( r_best, eqc );
 653       }
 654       //store that this representative was chosen at this point
 655       if( d_rep_score.find( r_best )==d_rep_score.end() ){
 656         d_rep_score[ r_best ] = d_reset_count;
 657       }
 658       d_int_rep[sortId][r] = r_best;
 659       if( r_best!=a ){
 660         Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl;
 661         Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
 662       }
 663       if( optInternalRepSortInference() ){
 664         int sortIdBest = d_qe->getTheoryEngine()->getSortInference()->getSortId( r_best );
 665         if( sortId!=sortIdBest ){
 666           Trace("sort-inf-rep") << "Choosing representative with bad type " << r_best << " " << sortId << " " << sortIdBest << std::endl;
 667         }
 668       }
 669       return r_best;
 670     }else{
 671       return d_int_rep[sortId][r];
 672     }
 673   }
 674 }
 675
 676 eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
 677   return d_qe->getMasterEqualityEngine();
 678 }
 679
 680 void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
 681   eq::EqualityEngine* ee = getEngine();
 682   if( ee->hasTerm( a ) ){
 683     Node rep = ee->getRepresentative( a );
 684     eq::EqClassIterator eqc_iter( rep, ee );
 685     while( !eqc_iter.isFinished() ){
 686       eqc.push_back( *eqc_iter );
 687       eqc_iter++;
 688     }
 689   }else{
 690     eqc.push_back( a );
 691   }
 692   //a should be in its equivalence class
 693   Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() );
 694 }
 695
 696 //helper functions
 697
 698 Node EqualityQueryQuantifiersEngine::getInstance( Node n, std::vector< Node >& eqc ){
 699   for( size_t i=0; i<n.getNumChildren(); i++ ){
 700     Node nn = getInstance( n[i], eqc );
 701     if( !nn.isNull() ){
 702       return nn;
 703     }
 704   }
 705   if( std::find( eqc.begin(), eqc.end(), n )!=eqc.end() ){
 706     return n;
 707   }else{
 708     return Node::null();
 709   }
 710 }
 711
 712 int getDepth( Node n ){
 713   if( n.getNumChildren()==0 ){
 714     return 0;
 715   }else{
 716     int maxDepth = -1;
 717     for( int i=0; i<(int)n.getNumChildren(); i++ ){
 718       int depth = getDepth( n[i] );
 719       if( depth>maxDepth ){
 720         maxDepth = depth;
 721       }
 722     }
 723     return maxDepth;
 724   }
 725 }
 726
 727 int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index ){
 728   return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];          //initial
 729   //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n );    //term depth
 730 }
 731
 732 bool EqualityQueryQuantifiersEngine::optInternalRepSortInference() {
 733   return false; //shown to be not effective
 734 }