src/theory/quantifiers/model_builder.cpp

   1 /*********************                                                        */
   2 /*! \file model_builder.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Implementation of model builder class
  13  **/
  14
  15 #include "theory/quantifiers/model_builder.h"
  16
  17 #include "options/quantifiers_options.h"
  18 #include "theory/quantifiers/first_order_model.h"
  19 #include "theory/quantifiers/instantiate.h"
  20 #include "theory/quantifiers/model_engine.h"
  21 #include "theory/quantifiers/quantifiers_attributes.h"
  22 #include "theory/quantifiers/term_database.h"
  23 #include "theory/quantifiers/term_util.h"
  24 #include "theory/quantifiers/trigger.h"
  25 #include "theory/theory_engine.h"
  26 #include "theory/uf/equality_engine.h"
  27 #include "theory/uf/theory_uf.h"
  28 #include "theory/uf/theory_uf_model.h"
  29 #include "theory/uf/theory_uf_strong_solver.h"
  30
  31 using namespace std;
  32 using namespace CVC4;
  33 using namespace CVC4::kind;
  34 using namespace CVC4::context;
  35 using namespace CVC4::theory;
  36 using namespace CVC4::theory::quantifiers;
  37
  38 QModelBuilder::QModelBuilder(context::Context* c, QuantifiersEngine* qe)
  39     : TheoryEngineModelBuilder(qe->getTheoryEngine()),
  40       d_qe(qe),
  41       d_addedLemmas(0),
  42       d_triedLemmas(0) {}
  43
  44 bool QModelBuilder::optUseModel() {
  45   return options::mbqiMode()!=MBQI_NONE || options::fmfBound();
  46 }
  47
  48 bool QModelBuilder::preProcessBuildModel(TheoryModel* m) {
  49   return preProcessBuildModelStd( m );
  50 }
  51
  52 bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) {
  53   d_addedLemmas = 0;
  54   d_triedLemmas = 0;
  55   if( options::fmfEmptySorts() || options::fmfFunWellDefinedRelevant() ){
  56     FirstOrderModel * fm = (FirstOrderModel*)m;
  57     //traverse equality engine
  58     std::map< TypeNode, bool > eqc_usort;
  59     eq::EqClassesIterator eqcs_i =
  60         eq::EqClassesIterator(fm->getEqualityEngine());
  61     while( !eqcs_i.isFinished() ){
  62       TypeNode tr = (*eqcs_i).getType();
  63       eqc_usort[tr] = true;
  64       ++eqcs_i;
  65     }
  66     //look at quantified formulas
  67     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
  68       Node q = fm->getAssertedQuantifier( i, true );
  69       if( fm->isQuantifierActive( q ) ){
  70         //check if any of these quantified formulas can be set inactive
  71         if( options::fmfEmptySorts() ){
  72           for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
  73             TypeNode tn = q[0][i].getType();
  74             //we are allowed to assume the type is empty
  75             if( tn.isSort() && eqc_usort.find( tn )==eqc_usort.end() ){
  76               Trace("model-engine-debug") << "Empty domain quantified formula : " << q << std::endl;
  77               fm->setQuantifierActive( q, false );
  78             }
  79           }
  80         }else if( options::fmfFunWellDefinedRelevant() ){
  81           if( q[0].getNumChildren()==1 ){
  82             TypeNode tn = q[0][0].getType();
  83             if( tn.getAttribute(AbsTypeFunDefAttribute()) ){
  84               //Trace("model-engine-debug2") << "...possible irrelevant function def : " << q << ", #rr = " << d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn ) << std::endl;
  85               //we are allowed to assume the introduced type is empty
  86               if( eqc_usort.find( tn )==eqc_usort.end() ){
  87                 Trace("model-engine-debug") << "Irrelevant function definition : " << q << std::endl;
  88                 fm->setQuantifierActive( q, false );
  89               }
  90             }
  91           }
  92         }
  93       }
  94     }
  95   }
  96   return true;
  97 }
  98
  99 void QModelBuilder::debugModel( TheoryModel* m ){
 100   //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
 101   if( Trace.isOn("quant-check-model") ){
 102     FirstOrderModel* fm = (FirstOrderModel*)m;
 103     Trace("quant-check-model") << "Testing quantifier instantiations..." << std::endl;
 104     int tests = 0;
 105     int bad = 0;
 106     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
 107       Node f = fm->getAssertedQuantifier( i );
 108       std::vector< Node > vars;
 109       for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
 110         vars.push_back( f[0][j] );
 111       }
 112       QRepBoundExt qrbe(d_qe);
 113       RepSetIterator riter(d_qe->getModel()->getRepSet(), &qrbe);
 114       if( riter.setQuantifier( f ) ){
 115         while( !riter.isFinished() ){
 116           tests++;
 117           std::vector< Node > terms;
 118           for (unsigned k = 0; k < riter.getNumTerms(); k++)
 119           {
 120             terms.push_back( riter.getCurrentTerm( k ) );
 121           }
 122           Node n = d_qe->getInstantiate()->getInstantiation(f, vars, terms);
 123           Node val = fm->getValue( n );
 124           if (val != d_qe->getTermUtil()->d_true)
 125           {
 126             Trace("quant-check-model") << "*******  Instantiation " << n << " for " << std::endl;
 127             Trace("quant-check-model") << "         " << f << std::endl;
 128             Trace("quant-check-model") << "         Evaluates to " << val << std::endl;
 129             bad++;
 130           }
 131           riter.increment();
 132         }
 133         Trace("quant-check-model") << "Tested " << tests << " instantiations";
 134         if( bad>0 ){
 135           Trace("quant-check-model") << ", " << bad << " failed" << std::endl;
 136         }
 137         Trace("quant-check-model") << "." << std::endl;
 138       }else{
 139         if( riter.isIncomplete() ){
 140           Trace("quant-check-model") << "Warning: Could not test quantifier " << f << std::endl;
 141         }
 142       }
 143     }
 144   }
 145 }
 146
 147 bool TermArgBasisTrie::addTerm(FirstOrderModel* fm, Node n, unsigned argIndex)
 148 {
 149   if (argIndex < n.getNumChildren())
 150   {
 151     Node r;
 152     if( n[ argIndex ].getAttribute(ModelBasisAttribute()) ){
 153       r = n[ argIndex ];
 154     }else{
 155       r = fm->getRepresentative( n[ argIndex ] );
 156     }
 157     std::map< Node, TermArgBasisTrie >::iterator it = d_data.find( r );
 158     if( it==d_data.end() ){
 159       d_data[r].addTerm(fm, n, argIndex + 1);
 160       return true;
 161     }else{
 162       return it->second.addTerm(fm, n, argIndex + 1);
 163     }
 164   }else{
 165     return false;
 166   }
 167 }
 168
 169 QModelBuilderIG::QModelBuilderIG(context::Context* c, QuantifiersEngine* qe)
 170     : QModelBuilder(c, qe),
 171       d_basisNoMatch(c),
 172       d_didInstGen(false),
 173       d_numQuantSat(0),
 174       d_numQuantInstGen(0),
 175       d_numQuantNoInstGen(0),
 176       d_numQuantNoSelForm(0),
 177       d_instGenMatches(0) {}
 178
 179 /*
 180 Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) {
 181   return n;
 182 }
 183 */
 184
 185 bool QModelBuilderIG::processBuildModel( TheoryModel* m ) {
 186   FirstOrderModel* f = (FirstOrderModel*)m;
 187   FirstOrderModelIG* fm = f->asFirstOrderModelIG();
 188   Trace("model-engine-debug") << "Process build model " << optUseModel() << std::endl;
 189   d_didInstGen = false;
 190   //reset the internal information
 191   reset( fm );
 192   //only construct first order model if optUseModel() is true
 193   if( optUseModel() ){
 194     Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl;
 195     //check if any quantifiers are un-initialized
 196     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
 197       Node q = fm->getAssertedQuantifier( i );
 198       if( d_qe->getModel()->isQuantifierActive( q ) ){
 199         int lems = initializeQuantifier(q, q, f);
 200         d_statistics.d_init_inst_gen_lemmas += lems;
 201         d_addedLemmas += lems;
 202         if( d_qe->inConflict() ){
 203           break;
 204         }
 205       }
 206     }
 207     if( d_addedLemmas>0 ){
 208       Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas << std::endl;
 209       return false;
 210     }else{
 211       Assert( !d_qe->inConflict() );
 212       //initialize model
 213       fm->initialize();
 214       //analyze the functions
 215       Trace("model-engine-debug") << "Analyzing model..." << std::endl;
 216       analyzeModel( fm );
 217       //analyze the quantifiers
 218       Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl;
 219       d_uf_prefs.clear();
 220       for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
 221         Node q = fm->getAssertedQuantifier( i );
 222         analyzeQuantifier( fm, q );
 223       }
 224
 225       //if applicable, find exceptions to model via inst-gen
 226       if( options::fmfInstGen() ){
 227         d_didInstGen = true;
 228         d_instGenMatches = 0;
 229         d_numQuantSat = 0;
 230         d_numQuantInstGen = 0;
 231         d_numQuantNoInstGen = 0;
 232         d_numQuantNoSelForm = 0;
 233         //now, see if we know that any exceptions via InstGen exist
 234         Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl;
 235         for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
 236           Node f = fm->getAssertedQuantifier( i );
 237           if( d_qe->getModel()->isQuantifierActive( f ) ){
 238             int lems = doInstGen( fm, f );
 239             d_statistics.d_inst_gen_lemmas += lems;
 240             d_addedLemmas += lems;
 241             //temporary
 242             if( lems>0 ){
 243               d_numQuantInstGen++;
 244             }else if( hasInstGen( f ) ){
 245               d_numQuantNoInstGen++;
 246             }else{
 247               d_numQuantNoSelForm++;
 248             }
 249             if( d_qe->inConflict() || ( options::fmfInstGenOneQuantPerRound() && lems>0 ) ){
 250               break;
 251             }
 252           }else{
 253             d_numQuantSat++;
 254           }
 255         }
 256         Trace("model-engine-debug") << "Quantifiers sat/ig/n-ig/null " << d_numQuantSat << " / " << d_numQuantInstGen << " / ";
 257         Trace("model-engine-debug") << d_numQuantNoInstGen << " / " << d_numQuantNoSelForm << std::endl;
 258         Trace("model-engine-debug") << "Inst-gen # matches examined = " << d_instGenMatches << std::endl;
 259         if( Trace.isOn("model-engine") ){
 260           if( d_addedLemmas>0 ){
 261             Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
 262           }else{
 263             Trace("model-engine") << "No InstGen lemmas..." << std::endl;
 264           }
 265         }
 266       }
 267       //construct the model if necessary
 268       if( d_addedLemmas==0 ){
 269         //if no immediate exceptions, build the model
 270         //  this model will be an approximation that will need to be tested via exhaustive instantiation
 271         Trace("model-engine-debug") << "Building model..." << std::endl;
 272         //build model for UF
 273         for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
 274           Trace("model-engine-debug-uf") << "Building model for " << it->first << "..." << std::endl;
 275           constructModelUf( fm, it->first );
 276         }
 277         Trace("model-engine-debug") << "Done building models." << std::endl;
 278       }else{
 279         return false;
 280       }
 281     }
 282   }
 283   //update models
 284   for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
 285     it->second.update( fm );
 286     Trace("model-func") << "QModelBuilder: Make function value from tree " << it->first << std::endl;
 287     //construct function values
 288     Node f_def = it->second.getFunctionValue( "$x" );
 289     fm->assignFunctionDefinition( it->first, f_def );
 290   }
 291   Assert( d_addedLemmas==0 );
 292   return TheoryEngineModelBuilder::processBuildModel( m );
 293 }
 294
 295 int QModelBuilderIG::initializeQuantifier(Node f, Node fp, FirstOrderModel* fm)
 296 {
 297   if( d_quant_basis_match_added.find( f )==d_quant_basis_match_added.end() ){
 298     //create the basis match if necessary
 299     if( d_quant_basis_match.find( f )==d_quant_basis_match.end() ){
 300       Trace("inst-fmf-init") << "Initialize " << f << std::endl;
 301       //add the model basis instantiation
 302       // This will help produce the necessary information for model completion.
 303       // We do this by extending distinguish ground assertions (those
 304       //   containing terms with "model basis" attribute) to hold for all cases.
 305
 306       ////first, check if any variables are required to be equal
 307       //for( std::map< Node, bool >::iterator it = d_quantEngine->d_phase_reqs[f].begin();
 308       //    it != d_quantEngine->d_phase_reqs[f].end(); ++it ){
 309       //  Node n = it->first;
 310       //  if( n.getKind()==EQUAL && n[0].getKind()==INST_CONSTANT && n[1].getKind()==INST_CONSTANT ){
 311       //    Notice() << "Unhandled phase req: " << n << std::endl;
 312       //  }
 313       //}
 314       d_quant_basis_match[f] = InstMatch( f );
 315       for (unsigned j = 0; j < f[0].getNumChildren(); j++)
 316       {
 317         Node t = fm->getModelBasisTerm(f[0][j].getType());
 318         //calculate the basis match for f
 319         d_quant_basis_match[f].setValue( j, t );
 320       }
 321       ++(d_statistics.d_num_quants_init);
 322     }
 323     //try to add it
 324     Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl;
 325     //add model basis instantiation
 326     if (d_qe->getInstantiate()->addInstantiation(fp, d_quant_basis_match[f]))
 327     {
 328       d_quant_basis_match_added[f] = true;
 329       return 1;
 330     }else{
 331       //shouldn't happen usually, but will occur if x != y is a required literal for f.
 332       //Notice() << "No model basis for " << f << std::endl;
 333       d_quant_basis_match_added[f] = false;
 334     }
 335   }
 336   return 0;
 337 }
 338
 339 void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){
 340   FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
 341   d_uf_model_constructed.clear();
 342   //determine if any functions are constant
 343   for( std::map< Node, uf::UfModelTree >::iterator it = fmig->d_uf_model_tree.begin(); it != fmig->d_uf_model_tree.end(); ++it ){
 344     Node op = it->first;
 345     TermArgBasisTrie tabt;
 346     std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op );
 347     if( itut!=fmig->d_uf_terms.end() ){
 348       for( size_t i=0; i<itut->second.size(); i++ ){
 349         Node n = fmig->d_uf_terms[op][i];
 350         //for calculating if op is constant
 351         Node v = fmig->getRepresentative( n );
 352         if( i==0 ){
 353           d_uf_prefs[op].d_const_val = v;
 354         }else if( v!=d_uf_prefs[op].d_const_val ){
 355           d_uf_prefs[op].d_const_val = Node::null();
 356           break;
 357         }
 358         //for calculating terms that we don't need to consider
 359         //if( d_qe->getTermDatabase()->isTermActive( n ) || n.getAttribute(ModelBasisArgAttribute())!=0 ){
 360         if( d_basisNoMatch.find( n )==d_basisNoMatch.end() ){
 361           //need to consider if it is not congruent modulo model basis
 362           if( !tabt.addTerm( fmig, n ) ){
 363             d_basisNoMatch[n] = true;
 364           }
 365         }
 366       }
 367     }
 368     if( !d_uf_prefs[op].d_const_val.isNull() ){
 369       fmig->d_uf_model_gen[op].setDefaultValue( d_uf_prefs[op].d_const_val );
 370       fmig->d_uf_model_gen[op].makeModel( fmig, it->second );
 371       Debug("fmf-model-cons") << "Function " << op << " is the constant function ";
 372       fmig->printRepresentativeDebug( "fmf-model-cons", d_uf_prefs[op].d_const_val );
 373       Debug("fmf-model-cons") << std::endl;
 374       d_uf_model_constructed[op] = true;
 375     }else{
 376       d_uf_model_constructed[op] = false;
 377     }
 378   }
 379 }
 380
 381 bool QModelBuilderIG::hasConstantDefinition( Node n ){
 382   Node lit = n.getKind()==NOT ? n[0] : n;
 383   if( lit.getKind()==APPLY_UF ){
 384     Node op = lit.getOperator();
 385     if( !d_uf_prefs[op].d_const_val.isNull() ){
 386       return true;
 387     }
 388   }
 389   return false;
 390 }
 391
 392 QModelBuilderIG::Statistics::Statistics():
 393   d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0),
 394   d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", 0),
 395   d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0 ),
 396   d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0 ),
 397   d_eval_formulas("QModelBuilderIG::Eval_Formulas", 0 ),
 398   d_eval_uf_terms("QModelBuilderIG::Eval_Uf_Terms", 0 ),
 399   d_eval_lits("QModelBuilderIG::Eval_Lits", 0 ),
 400   d_eval_lits_unknown("QModelBuilderIG::Eval_Lits_Unknown", 0 )
 401 {
 402   smtStatisticsRegistry()->registerStat(&d_num_quants_init);
 403   smtStatisticsRegistry()->registerStat(&d_num_partial_quants_init);
 404   smtStatisticsRegistry()->registerStat(&d_init_inst_gen_lemmas);
 405   smtStatisticsRegistry()->registerStat(&d_inst_gen_lemmas);
 406   smtStatisticsRegistry()->registerStat(&d_eval_formulas);
 407   smtStatisticsRegistry()->registerStat(&d_eval_uf_terms);
 408   smtStatisticsRegistry()->registerStat(&d_eval_lits);
 409   smtStatisticsRegistry()->registerStat(&d_eval_lits_unknown);
 410 }
 411
 412 QModelBuilderIG::Statistics::~Statistics(){
 413   smtStatisticsRegistry()->unregisterStat(&d_num_quants_init);
 414   smtStatisticsRegistry()->unregisterStat(&d_num_partial_quants_init);
 415   smtStatisticsRegistry()->unregisterStat(&d_init_inst_gen_lemmas);
 416   smtStatisticsRegistry()->unregisterStat(&d_inst_gen_lemmas);
 417   smtStatisticsRegistry()->unregisterStat(&d_eval_formulas);
 418   smtStatisticsRegistry()->unregisterStat(&d_eval_uf_terms);
 419   smtStatisticsRegistry()->unregisterStat(&d_eval_lits);
 420   smtStatisticsRegistry()->unregisterStat(&d_eval_lits_unknown);
 421 }
 422
 423 //do exhaustive instantiation
 424 int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
 425   if( optUseModel() ){
 426     QRepBoundExt qrbe(d_qe);
 427     RepSetIterator riter(d_qe->getModel()->getRepSet(), &qrbe);
 428     if( riter.setQuantifier( f ) ){
 429       FirstOrderModelIG * fmig = (FirstOrderModelIG*)d_qe->getModel();
 430       Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
 431       fmig->resetEvaluate();
 432       Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
 433       EqualityQuery* qy = d_qe->getEqualityQuery();
 434       Instantiate* inst = d_qe->getInstantiate();
 435       TermUtil* util = d_qe->getTermUtil();
 436       while( !riter.isFinished() && ( d_addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
 437         d_triedLemmas++;
 438         if( Debug.isOn("inst-fmf-ei-debug") ){
 439           for( int i=0; i<(int)riter.d_index.size(); i++ ){
 440             Debug("inst-fmf-ei-debug") << i << " : " << riter.d_index[i] << " : " << riter.getCurrentTerm( i ) << std::endl;
 441           }
 442         }
 443         int eval = 0;
 444         int depIndex;
 445         //see if instantiation is already true in current model
 446         if( Debug.isOn("fmf-model-eval") ){
 447           Debug("fmf-model-eval") << "Evaluating ";
 448           riter.debugPrintSmall("fmf-model-eval");
 449           Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
 450         }
 451         //if evaluate(...)==1, then the instantiation is already true in the model
 452         //  depIndex is the index of the least significant variable that this evaluation relies upon
 453         depIndex = riter.getNumTerms()-1;
 454         Debug("fmf-model-eval") << "We will evaluate "
 455                                 << util->getInstConstantBody(f) << std::endl;
 456         eval = fmig->evaluate(util->getInstConstantBody(f), depIndex, &riter);
 457         if( eval==1 ){
 458           Debug("fmf-model-eval") << "  Returned success with depIndex = " << depIndex << std::endl;
 459         }else{
 460           Debug("fmf-model-eval") << "  Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
 461         }
 462         if( eval==1 ){
 463           //instantiation is already true -> skip
 464           riter.incrementAtIndex(depIndex);
 465         }else{
 466           //instantiation was not shown to be true, construct the match
 467           InstMatch m( f );
 468           for (unsigned i = 0; i < riter.getNumTerms(); i++)
 469           {
 470             m.set(qy, i, riter.getCurrentTerm(i));
 471           }
 472           Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
 473           //add as instantiation
 474           if (inst->addInstantiation(f, m, true))
 475           {
 476             d_addedLemmas++;
 477             if( d_qe->inConflict() ){
 478               break;
 479             }
 480             //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
 481             if( eval==-1 ){
 482               riter.incrementAtIndex(depIndex);
 483             }else{
 484               riter.increment();
 485             }
 486           }else{
 487             Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
 488             riter.increment();
 489           }
 490         }
 491       }
 492       //print debugging information
 493       if( fmig ){
 494         d_statistics.d_eval_formulas += fmig->d_eval_formulas;
 495         d_statistics.d_eval_uf_terms += fmig->d_eval_uf_terms;
 496         d_statistics.d_eval_lits += fmig->d_eval_lits;
 497         d_statistics.d_eval_lits_unknown += fmig->d_eval_lits_unknown;
 498       }
 499       Trace("inst-fmf-ei") << "For " << f << ", finished: " << std::endl;
 500       Trace("inst-fmf-ei") << "   Inst Tried: " << d_triedLemmas << std::endl;
 501       Trace("inst-fmf-ei") << "   Inst Added: " << d_addedLemmas << std::endl;
 502       if( d_addedLemmas>1000 ){
 503         Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
 504         Trace("model-engine-warn") << "   Inst Tried: " << d_triedLemmas << std::endl;
 505         Trace("model-engine-warn") << "   Inst Added: " << d_addedLemmas << std::endl;
 506         Trace("model-engine-warn") << std::endl;
 507       }
 508     }
 509     //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
 510     return riter.isIncomplete() ? -1 : 1;
 511   }else{
 512     return 0;
 513   }
 514 }
 515
 516
 517
 518 void QModelBuilderDefault::reset( FirstOrderModel* fm ){
 519   d_quant_selection_lit.clear();
 520   d_quant_selection_lit_candidates.clear();
 521   d_quant_selection_lit_terms.clear();
 522   d_term_selection_lit.clear();
 523   d_op_selection_terms.clear();
 524 }
 525
 526
 527 int QModelBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms ) {
 528   /*
 529   size_t maxChildren = 0;
 530   for( size_t i=0; i<uf_terms.size(); i++ ){
 531     if( uf_terms[i].getNumChildren()>maxChildren ){
 532       maxChildren = uf_terms[i].getNumChildren();
 533     }
 534   }
 535   //TODO: look at how many entries they have?
 536   return (int)maxChildren;
 537   */
 538   return 0;
 539 }
 540
 541 void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){
 542   if( d_qe->getModel()->isQuantifierActive( f ) ){
 543     FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
 544     Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl;
 545     //the pro/con preferences for this quantifier
 546     std::vector< Node > pro_con[2];
 547     //the terms in the selection literal we choose
 548     std::vector< Node > selectionLitTerms;
 549     Trace("inst-gen-debug-quant") << "Inst-gen analyze " << f << std::endl;
 550     //for each asserted quantifier f,
 551     // - determine selection literals
 552     // - check which function/predicates have good and bad definitions for satisfying f
 553     if( d_phase_reqs.find( f )==d_phase_reqs.end() ){
 554       d_phase_reqs[f].initialize( d_qe->getTermUtil()->getInstConstantBody( f ), true );
 555     }
 556     int selectLitScore = -1;
 557     for( std::map< Node, bool >::iterator it = d_phase_reqs[f].d_phase_reqs.begin(); it != d_phase_reqs[f].d_phase_reqs.end(); ++it ){
 558       //the literal n is phase-required for quantifier f
 559       Node n = it->first;
 560       Node gn = fm->getModelBasis(f, n);
 561       Debug("fmf-model-req") << "   Req: " << n << " -> " << it->second << std::endl;
 562       bool value;
 563       //if the corresponding ground abstraction literal has a SAT value
 564       if( d_qe->getValuation().hasSatValue( gn, value ) ){
 565         //collect the non-ground uf terms that this literal contains
 566         //  and compute if all of the symbols in this literal have
 567         //  constant definitions.
 568         bool isConst = true;
 569         std::vector< Node > uf_terms;
 570         if( TermUtil::hasInstConstAttr(n) ){
 571           isConst = false;
 572           if( gn.getKind()==APPLY_UF ){
 573             uf_terms.push_back( gn );
 574             isConst = hasConstantDefinition( gn );
 575           }else if( gn.getKind()==EQUAL ){
 576             isConst = true;
 577             for( int j=0; j<2; j++ ){
 578               if( TermUtil::hasInstConstAttr(n[j]) ){
 579                 if( n[j].getKind()==APPLY_UF &&
 580                     fmig->d_uf_model_tree.find( gn[j].getOperator() )!=fmig->d_uf_model_tree.end() ){
 581                   uf_terms.push_back( gn[j] );
 582                   isConst = isConst && hasConstantDefinition( gn[j] );
 583                 }else{
 584                   isConst = false;
 585                 }
 586               }
 587             }
 588           }
 589         }
 590         //check if the value in the SAT solver matches the preference according to the quantifier
 591         int pref = 0;
 592         if( value!=it->second ){
 593           //we have a possible selection literal
 594           bool selectLit = d_quant_selection_lit[f].isNull();
 595           bool selectLitConstraints = true;
 596           //it is a constantly defined selection literal : the quantifier is sat
 597           if( isConst ){
 598             selectLit = selectLit || d_qe->getModel()->isQuantifierActive( f );
 599             d_qe->getModel()->setQuantifierActive( f, false );
 600             //check if choosing this literal would add any additional constraints to default definitions
 601             selectLitConstraints = false;
 602             for( int j=0; j<(int)uf_terms.size(); j++ ){
 603               Node op = uf_terms[j].getOperator();
 604               if( d_uf_prefs[op].d_reconsiderModel ){
 605                 selectLitConstraints = true;
 606               }
 607             }
 608             if( !selectLitConstraints ){
 609               selectLit = true;
 610             }
 611           }
 612           //also check if it is naturally a better literal
 613           if( !selectLit ){
 614             int score = getSelectionScore( uf_terms );
 615             //Trace("inst-gen-debug") << "Check " << score << " < " << selectLitScore << std::endl;
 616             selectLit = score<selectLitScore;
 617           }
 618           //see if we wish to choose this as a selection literal
 619           d_quant_selection_lit_candidates[f].push_back( value ? n : n.notNode() );
 620           if( selectLit ){
 621             selectLitScore = getSelectionScore( uf_terms );
 622             Trace("inst-gen-debug") << "Choose selection literal " << gn << std::endl;
 623             Trace("inst-gen-debug") << "  flags: " << isConst << " " << selectLitConstraints << " " << selectLitScore << std::endl;
 624             d_quant_selection_lit[f] = value ? n : n.notNode();
 625             selectionLitTerms.clear();
 626             selectionLitTerms.insert( selectionLitTerms.begin(), uf_terms.begin(), uf_terms.end() );
 627             if( !selectLitConstraints ){
 628               break;
 629             }
 630           }
 631           pref = 1;
 632         }else{
 633           pref = -1;
 634         }
 635         //if we are not yet SAT, so we will add to preferences
 636         if( d_qe->getModel()->isQuantifierActive( f ) ){
 637           Debug("fmf-model-prefs") << "  It is " << ( pref==1 ? "pro" : "con" );
 638           Debug("fmf-model-prefs") << " the definition of " << n << std::endl;
 639           for( int j=0; j<(int)uf_terms.size(); j++ ){
 640             pro_con[ pref==1 ? 0 : 1 ].push_back( uf_terms[j] );
 641           }
 642         }
 643       }
 644     }
 645     //process information about selection literal for f
 646     if( !d_quant_selection_lit[f].isNull() ){
 647       d_quant_selection_lit_terms[f].insert( d_quant_selection_lit_terms[f].begin(), selectionLitTerms.begin(), selectionLitTerms.end() );
 648       for( int i=0; i<(int)selectionLitTerms.size(); i++ ){
 649         d_term_selection_lit[ selectionLitTerms[i] ] = d_quant_selection_lit[f];
 650         d_op_selection_terms[ selectionLitTerms[i].getOperator() ].push_back( selectionLitTerms[i] );
 651       }
 652     }else{
 653       Trace("inst-gen-warn") << "WARNING: " << f << " has no selection literals" << std::endl;
 654     }
 655     //process information about requirements and preferences of quantifier f
 656     if( !d_qe->getModel()->isQuantifierActive( f ) ){
 657       Debug("fmf-model-prefs") << "  * Constant SAT due to definition of ops: ";
 658       for( int i=0; i<(int)selectionLitTerms.size(); i++ ){
 659         Debug("fmf-model-prefs") << selectionLitTerms[i] << " ";
 660         d_uf_prefs[ selectionLitTerms[i].getOperator() ].d_reconsiderModel = false;
 661       }
 662       Debug("fmf-model-prefs") << std::endl;
 663     }else{
 664       //note quantifier's value preferences to models
 665       for( int k=0; k<2; k++ ){
 666         for( int j=0; j<(int)pro_con[k].size(); j++ ){
 667           Node op = pro_con[k][j].getOperator();
 668           Node r = fmig->getRepresentative( pro_con[k][j] );
 669           d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 );
 670         }
 671       }
 672     }
 673   }
 674 }
 675
 676 int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){
 677   int addedLemmas = 0;
 678   //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model.
 679   //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms,
 680   //  effectively acting as partial instantiations instead of pointwise instantiations.
 681   if( !d_quant_selection_lit[f].isNull() ){
 682     Trace("inst-gen") << "Do Inst-Gen for " << f << std::endl;
 683     for( size_t i=0; i<d_quant_selection_lit_candidates[f].size(); i++ ){
 684       bool phase = d_quant_selection_lit_candidates[f][i].getKind()!=NOT;
 685       Node lit = d_quant_selection_lit_candidates[f][i].getKind()==NOT ? d_quant_selection_lit_candidates[f][i][0] : d_quant_selection_lit_candidates[f][i];
 686       Assert( TermUtil::hasInstConstAttr(lit) );
 687       std::vector< Node > tr_terms;
 688       if( lit.getKind()==APPLY_UF ){
 689         //only match predicates that are contrary to this one, use literal matching
 690         Node eq = NodeManager::currentNM()->mkNode(
 691             EQUAL, lit, NodeManager::currentNM()->mkConst(!phase));
 692         tr_terms.push_back( eq );
 693       }else if( lit.getKind()==EQUAL ){
 694         //collect trigger terms
 695         for( int j=0; j<2; j++ ){
 696           if( TermUtil::hasInstConstAttr(lit[j]) ){
 697             if( lit[j].getKind()==APPLY_UF ){
 698               tr_terms.push_back( lit[j] );
 699             }else{
 700               tr_terms.clear();
 701               break;
 702             }
 703           }
 704         }
 705         if( tr_terms.size()==1 && !phase ){
 706           //equality between a function and a ground term, use literal matching
 707           tr_terms.clear();
 708           tr_terms.push_back( lit );
 709         }
 710       }
 711       //if applicable, try to add exceptions here
 712       if( !tr_terms.empty() ){
 713         //make a trigger for these terms, add instantiations
 714         inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms, true, inst::Trigger::TR_MAKE_NEW );
 715         //Notice() << "Trigger = " << (*tr) << std::endl;
 716         tr->resetInstantiationRound();
 717         tr->reset( Node::null() );
 718         //d_qe->d_optInstMakeRepresentative = false;
 719         //d_qe->d_optMatchIgnoreModelBasis = true;
 720         addedLemmas += tr->addInstantiations( d_quant_basis_match[f] );
 721       }
 722     }
 723   }
 724   return addedLemmas;
 725 }
 726
 727 void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
 728   FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
 729   if( optReconsiderFuncConstants() ){
 730     //reconsider constant functions that weren't necessary
 731     if( d_uf_model_constructed[op] ){
 732       if( d_uf_prefs[op].d_reconsiderModel ){
 733         //if we are allowed to reconsider default value, then see if the default value can be improved
 734         Node v = d_uf_prefs[op].d_const_val;
 735         if( d_uf_prefs[op].d_value_pro_con[0][v].empty() ){
 736           Debug("fmf-model-cons-debug") << "Consider changing the default value for " << op << std::endl;
 737           fmig->d_uf_model_tree[op].clear();
 738           fmig->d_uf_model_gen[op].clear();
 739           d_uf_model_constructed[op] = false;
 740         }
 741       }
 742     }
 743   }
 744   if( !d_uf_model_constructed[op] ){
 745     //construct the model for the uninterpretted function/predicate
 746     bool setDefaultVal = true;
 747     Node defaultTerm = fmig->getModelBasisOpTerm(op);
 748     Trace("fmf-model-cons") << "Construct model for " << op << "..." << std::endl;
 749     //set the values in the model
 750     std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op );
 751     if( itut!=fmig->d_uf_terms.end() ){
 752       for( size_t i=0; i<itut->second.size(); i++ ){
 753         Node n = itut->second[i];
 754         // only consider unique up to congruence (in model equality engine)?
 755         Node v = fmig->getRepresentative( n );
 756         Trace("fmf-model-cons") << "Set term " << n << " : "
 757                                 << fmig->getRepSet()->getIndexFor(v) << " " << v
 758                                 << std::endl;
 759         //if this assertion did not help the model, just consider it ground
 760         //set n = v in the model tree
 761         //set it as ground value
 762         fmig->d_uf_model_gen[op].setValue( fm, n, v );
 763         if( fmig->d_uf_model_gen[op].optUsePartialDefaults() ){
 764           //also set as default value if necessary
 765           if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())!=0 ){
 766             Trace("fmf-model-cons") << "  Set as default." << std::endl;
 767             fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
 768             if( n==defaultTerm ){
 769               //incidentally already set, we will not need to find a default value
 770               setDefaultVal = false;
 771             }
 772           }
 773         }else{
 774           if( n==defaultTerm ){
 775             fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
 776             //incidentally already set, we will not need to find a default value
 777             setDefaultVal = false;
 778           }
 779         }
 780       }
 781     }
 782     //set the overall default value if not set already  (is this necessary??)
 783     if( setDefaultVal ){
 784       Trace("fmf-model-cons") << "  Choose default value..." << std::endl;
 785       //chose defaultVal based on heuristic, currently the best ratio of "pro" responses
 786       Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm );
 787       if( defaultVal.isNull() ){
 788         if (!fmig->getRepSet()->hasType(defaultTerm.getType()))
 789         {
 790           Node mbt = fmig->getModelBasisTerm(defaultTerm.getType());
 791           fmig->getRepSetPtr()->d_type_reps[defaultTerm.getType()].push_back(
 792               mbt);
 793         }
 794         defaultVal =
 795             fmig->getRepSet()->getRepresentative(defaultTerm.getType(), 0);
 796       }
 797       Assert( !defaultVal.isNull() );
 798       Trace("fmf-model-cons")
 799           << "Set default term : " << fmig->getRepSet()->getIndexFor(defaultVal)
 800           << std::endl;
 801       fmig->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false );
 802     }
 803     Debug("fmf-model-cons") << "  Making model...";
 804     fmig->d_uf_model_gen[op].makeModel( fm, fmig->d_uf_model_tree[op] );
 805     d_uf_model_constructed[op] = true;
 806     Debug("fmf-model-cons") << "  Finished constructing model for " << op << "." << std::endl;
 807   }
 808 }