src/theory/quantifiers/conjecture_generator.cpp

   1 /*********************                                                        */
   2 /*! \file conjecture_generator.cpp
   3  ** \verbatim
   4  ** Original author: Andrew Reynolds
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   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 conjecture generator class
  13  **
  14  **/
  15
  16 #include "theory/quantifiers/conjecture_generator.h"
  17 #include "theory/theory_engine.h"
  18 #include "theory/quantifiers/options.h"
  19 #include "theory/quantifiers/term_database.h"
  20 #include "theory/quantifiers/trigger.h"
  21 #include "theory/quantifiers/first_order_model.h"
  22
  23 using namespace CVC4;
  24 using namespace CVC4::kind;
  25 using namespace CVC4::theory;
  26 using namespace CVC4::theory::quantifiers;
  27 using namespace std;
  28
  29 namespace CVC4 {
  30
  31 struct sortConjectureScore {
  32   std::vector< int > d_scores;
  33   bool operator() (unsigned i, unsigned j) { return d_scores[i]>d_scores[j]; }
  34 };
  35
  36
  37 void OpArgIndex::addTerm( ConjectureGenerator * s, TNode n, unsigned index ){
  38   if( index==n.getNumChildren() ){
  39     Assert( n.hasOperator() );
  40     if( std::find( d_ops.begin(), d_ops.end(), n.getOperator() )==d_ops.end() ){
  41       d_ops.push_back( n.getOperator() );
  42       d_op_terms.push_back( n );
  43     }
  44   }else{
  45     d_child[s->getTermDatabase()->d_arg_reps[n][index]].addTerm( s, n, index+1 );
  46   }
  47 }
  48
  49 Node OpArgIndex::getGroundTerm( ConjectureGenerator * s, std::vector< TNode >& args ) {
  50   if( d_ops.empty() ){
  51     for( std::map< TNode, OpArgIndex >::iterator it = d_child.begin(); it != d_child.end(); ++it ){
  52       std::map< TNode, Node >::iterator itf = s->d_ground_eqc_map.find( it->first );
  53       if( itf!=s->d_ground_eqc_map.end() ){
  54         args.push_back( itf->second );
  55         Node n = it->second.getGroundTerm( s, args );
  56         args.pop_back();
  57         if( !n.isNull() ){
  58           return n;
  59         }
  60       }
  61     }
  62     return Node::null();
  63   }else{
  64     std::vector< TNode > args2;
  65     args2.push_back( d_ops[0] );
  66     args2.insert( args2.end(), args.begin(), args.end() );
  67     return NodeManager::currentNM()->mkNode( d_op_terms[0].getKind(), args2 );
  68   }
  69 }
  70
  71 void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& terms ) {
  72   terms.insert( terms.end(), d_op_terms.begin(), d_op_terms.end() );
  73   for( std::map< TNode, OpArgIndex >::iterator it = d_child.begin(); it != d_child.end(); ++it ){
  74     if( s->isGroundEqc( it->first ) ){
  75       it->second.getGroundTerms( s, terms );
  76     }
  77   }
  78 }
  79
  80
  81
  82 ConjectureGenerator::ConjectureGenerator( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ),
  83 d_notify( *this ),
  84 d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee"),
  85 d_ee_conjectures( c ){
  86   d_fullEffortCount = 0;
  87   d_uequalityEngine.addFunctionKind( kind::APPLY_UF );
  88   d_uequalityEngine.addFunctionKind( kind::APPLY_CONSTRUCTOR );
  89
  90 }
  91
  92 void ConjectureGenerator::eqNotifyNewClass( TNode t ){
  93   Trace("thm-ee-debug") << "UEE : new equivalence class " << t << std::endl;
  94   d_upendingAdds.push_back( t );
  95 }
  96
  97 void ConjectureGenerator::eqNotifyPreMerge(TNode t1, TNode t2) {
  98   //get maintained representatives
  99   TNode rt1 = t1;
 100   TNode rt2 = t2;
 101   std::map< Node, EqcInfo* >::iterator it1 = d_eqc_info.find( t1 );
 102   if( it1!=d_eqc_info.end() && !it1->second->d_rep.get().isNull() ){
 103     rt1 = it1->second->d_rep.get();
 104   }
 105   std::map< Node, EqcInfo* >::iterator it2 = d_eqc_info.find( t2 );
 106   if( it2!=d_eqc_info.end() && !it2->second->d_rep.get().isNull() ){
 107     rt2 = it2->second->d_rep.get();
 108   }
 109   Trace("thm-ee-debug") << "UEE : equality holds : " << t1 << " == " << t2 << std::endl;
 110   Trace("thm-ee-debug") << "      ureps : " << rt1 << " == " << rt2 << std::endl;
 111   Trace("thm-ee-debug") << "      relevant : " << d_pattern_is_relevant[rt1] << " " << d_pattern_is_relevant[rt2] << std::endl;
 112   Trace("thm-ee-debug") << "      normal : " << d_pattern_is_normal[rt1] << " " << d_pattern_is_normal[rt2] << std::endl;
 113   Trace("thm-ee-debug") << "      size :   " << d_pattern_fun_sum[rt1] << " " << d_pattern_fun_sum[rt2] << std::endl;
 114
 115   if( isUniversalLessThan( rt2, rt1 ) ){
 116     EqcInfo * ei;
 117     if( it1==d_eqc_info.end() ){
 118       ei = getOrMakeEqcInfo( t1, true );
 119     }else{
 120       ei = it1->second;
 121     }
 122     ei->d_rep = t2;
 123   }
 124 }
 125
 126 void ConjectureGenerator::eqNotifyPostMerge(TNode t1, TNode t2) {
 127
 128 }
 129
 130 void ConjectureGenerator::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
 131   Trace("thm-ee-debug") << "UEE : disequality holds : " << t1 << " != " << t2 << std::endl;
 132
 133 }
 134
 135
 136 ConjectureGenerator::EqcInfo::EqcInfo( context::Context* c ) : d_rep( c, Node::null() ){
 137
 138 }
 139
 140 ConjectureGenerator::EqcInfo* ConjectureGenerator::getOrMakeEqcInfo( TNode n, bool doMake ) {
 141   //Assert( getUniversalRepresentative( n )==n );
 142   std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n );
 143   if( eqc_i!=d_eqc_info.end() ){
 144     return eqc_i->second;
 145   }else if( doMake ){
 146     EqcInfo* ei = new EqcInfo( d_quantEngine->getSatContext() );
 147     d_eqc_info[n] = ei;
 148     return ei;
 149   }else{
 150     return NULL;
 151   }
 152 }
 153
 154 void ConjectureGenerator::setUniversalRelevant( TNode n ) {
 155   //add pattern information
 156   registerPattern( n, n.getType() );
 157   d_urelevant_terms[n] = true;
 158   for( unsigned i=0; i<n.getNumChildren(); i++ ){
 159     setUniversalRelevant( n[i] );
 160   }
 161 }
 162
 163 bool ConjectureGenerator::isUniversalLessThan( TNode rt1, TNode rt2 ) {
 164   //prefer the one that is (normal, smaller) lexographically
 165   Assert( d_pattern_is_relevant.find( rt1 )!=d_pattern_is_relevant.end() );
 166   Assert( d_pattern_is_relevant.find( rt2 )!=d_pattern_is_relevant.end() );
 167   Assert( d_pattern_is_normal.find( rt1 )!=d_pattern_is_normal.end() );
 168   Assert( d_pattern_is_normal.find( rt2 )!=d_pattern_is_normal.end() );
 169   Assert( d_pattern_fun_sum.find( rt1 )!=d_pattern_fun_sum.end() );
 170   Assert( d_pattern_fun_sum.find( rt2 )!=d_pattern_fun_sum.end() );
 171
 172   if( d_pattern_is_relevant[rt1] && !d_pattern_is_relevant[rt2] ){
 173     Trace("thm-ee-debug") << "UEE : LT due to relevant." << std::endl;
 174     return true;
 175   }else if( d_pattern_is_relevant[rt1]==d_pattern_is_relevant[rt2] ){
 176     if( d_pattern_is_normal[rt1] && !d_pattern_is_normal[rt2] ){
 177       Trace("thm-ee-debug") << "UEE : LT due to normal." << std::endl;
 178       return true;
 179     }else if( d_pattern_is_normal[rt1]==d_pattern_is_normal[rt2] ){
 180       if( d_pattern_fun_sum[rt1]<d_pattern_fun_sum[rt2] ){
 181         Trace("thm-ee-debug") << "UEE : LT due to size." << std::endl;
 182         //decide which representative to use : based on size of the term
 183         return true;
 184       }else if( d_pattern_fun_sum[rt1]==d_pattern_fun_sum[rt2] ){
 185         //same size : tie goes to term that has already been reported
 186         return isReportedCanon( rt1 ) && !isReportedCanon( rt2 );
 187       }
 188     }
 189   }
 190   return false;
 191 }
 192
 193
 194 bool ConjectureGenerator::isReportedCanon( TNode n ) {
 195   return std::find( d_ue_canon.begin(), d_ue_canon.end(), n )==d_ue_canon.end();
 196 }
 197
 198 void ConjectureGenerator::markReportedCanon( TNode n ) {
 199   if( !isReportedCanon( n ) ){
 200     d_ue_canon.push_back( n );
 201   }
 202 }
 203
 204 bool ConjectureGenerator::areUniversalEqual( TNode n1, TNode n2 ) {
 205   return n1==n2 || ( d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areEqual( n1, n2 ) );
 206 }
 207
 208 bool ConjectureGenerator::areUniversalDisequal( TNode n1, TNode n2 ) {
 209   return n1!=n2 && d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areDisequal( n1, n2, false );
 210 }
 211
 212 TNode ConjectureGenerator::getUniversalRepresentative( TNode n, bool add ) {
 213   if( add ){
 214     if( d_urelevant_terms.find( n )==d_urelevant_terms.end() ){
 215       setUniversalRelevant( n );
 216       //add term to universal equality engine
 217       d_uequalityEngine.addTerm( n );
 218       // addding this term to equality engine will lead to a set of new terms (the new subterms of n)
 219       // now, do instantiation-based merging for each of these terms
 220       Trace("thm-ee-debug") << "Merge equivalence classes based on instantiations of terms..." << std::endl;
 221       //merge all pending equalities
 222       while( !d_upendingAdds.empty() ){
 223         Trace("sg-pending") << "Add " << d_upendingAdds.size() << " pending terms..." << std::endl;
 224         std::vector< Node > pending;
 225         pending.insert( pending.end(), d_upendingAdds.begin(), d_upendingAdds.end() );
 226         d_upendingAdds.clear();
 227         for( unsigned i=0; i<pending.size(); i++ ){
 228           Node t = pending[i];
 229           TypeNode tn = t.getType();
 230           Trace("thm-ee-add") << "UEE : Add universal term " << t << std::endl;
 231           std::vector< Node > eq_terms;
 232           //if occurs modulo equality at ground level, it is equivalent to representative of ground equality engine
 233           TNode gt = getTermDatabase()->evaluateTerm( t );
 234           if( !gt.isNull() && gt!=t ){
 235             eq_terms.push_back( gt );
 236           }
 237           //get all equivalent terms based on theorem database
 238           d_thm_index.getEquivalentTerms( t, eq_terms );
 239           if( !eq_terms.empty() ){
 240             Trace("thm-ee-add") << "UEE : Based on ground EE/theorem DB, it is equivalent to " << eq_terms.size() << " terms : " << std::endl;
 241             //add equivalent terms as equalities to universal engine
 242             for( unsigned i=0; i<eq_terms.size(); i++ ){
 243               Trace("thm-ee-add") << "  " << eq_terms[i] << std::endl;
 244               bool assertEq = false;
 245               if( d_urelevant_terms.find( eq_terms[i] )!=d_urelevant_terms.end() ){
 246                 assertEq = true;
 247               }else{
 248                 Assert( eq_terms[i].getType()==tn );
 249                 registerPattern( eq_terms[i], tn );
 250                 if( isUniversalLessThan( eq_terms[i], t ) || ( options::conjectureUeeIntro() && d_pattern_fun_sum[t]>=d_pattern_fun_sum[eq_terms[i]] ) ){
 251                   setUniversalRelevant( eq_terms[i] );
 252                   assertEq = true;
 253                 }
 254               }
 255               if( assertEq ){
 256                 Node exp;
 257                 d_uequalityEngine.assertEquality( t.eqNode( eq_terms[i] ), true, exp );
 258               }else{
 259                 Trace("thm-ee-no-add") << "Do not add : " << t << " == " << eq_terms[i] << std::endl;
 260               }
 261             }
 262           }else{
 263             Trace("thm-ee-add") << "UEE : No equivalent terms." << std::endl;
 264           }
 265         }
 266       }
 267     }
 268   }
 269
 270   if( d_uequalityEngine.hasTerm( n ) ){
 271     Node r = d_uequalityEngine.getRepresentative( n );
 272     EqcInfo * ei = getOrMakeEqcInfo( r );
 273     if( ei && !ei->d_rep.get().isNull() ){
 274       return ei->d_rep.get();
 275     }else{
 276       return r;
 277     }
 278   }else{
 279     return n;
 280   }
 281 }
 282
 283 Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) {
 284   Assert( !tn.isNull() );
 285   while( d_free_var[tn].size()<=i ){
 286     std::stringstream oss;
 287     oss << tn;
 288     std::stringstream os;
 289     os << oss.str()[0] << i;
 290     Node x = NodeManager::currentNM()->mkBoundVar( os.str().c_str(), tn );
 291     d_free_var_num[x] = d_free_var[tn].size();
 292     d_free_var[tn].push_back( x );
 293   }
 294   return d_free_var[tn][i];
 295 }
 296
 297
 298
 299 Node ConjectureGenerator::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs ) {
 300   if( n.getKind()==BOUND_VARIABLE ){
 301     std::map< TNode, TNode >::iterator it = subs.find( n );
 302     if( it==subs.end() ){
 303       TypeNode tn = n.getType();
 304       //allocate variable
 305       unsigned vn = var_count[tn];
 306       var_count[tn]++;
 307       subs[n] = getFreeVar( tn, vn );
 308       return subs[n];
 309     }else{
 310       return it->second;
 311     }
 312   }else{
 313     std::vector< Node > children;
 314     if( n.getKind()!=EQUAL ){
 315       if( n.hasOperator() ){
 316         TNode op = n.getOperator();
 317         if( !d_tge.isRelevantFunc( op ) ){
 318           return Node::null();
 319         }
 320         children.push_back( op );
 321       }else{
 322         return Node::null();
 323       }
 324     }
 325     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 326       Node cn = getCanonicalTerm( n[i], var_count, subs );
 327       if( cn.isNull() ){
 328         return Node::null();
 329       }else{
 330         children.push_back( cn );
 331       }
 332     }
 333     return NodeManager::currentNM()->mkNode( n.getKind(), children );
 334   }
 335 }
 336
 337 bool ConjectureGenerator::isHandledTerm( TNode n ){
 338   return !n.getAttribute(NoMatchAttribute()) && inst::Trigger::isAtomicTrigger( n ) && ( n.getKind()!=APPLY_UF || n.getOperator().getKind()!=SKOLEM );
 339 }
 340
 341 Node ConjectureGenerator::getGroundEqc( TNode r ) {
 342   std::map< TNode, Node >::iterator it = d_ground_eqc_map.find( r );
 343   return it!=d_ground_eqc_map.end() ? it->second : Node::null();
 344 }
 345
 346 bool ConjectureGenerator::isGroundEqc( TNode r ) {
 347   return d_ground_eqc_map.find( r )!=d_ground_eqc_map.end();
 348 }
 349
 350 bool ConjectureGenerator::isGroundTerm( TNode n ) {
 351   return std::find( d_ground_terms.begin(), d_ground_terms.end(), n )!=d_ground_terms.end();
 352 }
 353
 354 bool ConjectureGenerator::needsCheck( Theory::Effort e ) {
 355   return e==Theory::EFFORT_FULL;
 356 }
 357
 358 bool ConjectureGenerator::hasEnumeratedUf( Node n ) {
 359   if( options::conjectureGenGtEnum()>0 ){
 360     std::map< Node, bool >::iterator it = d_uf_enum.find( n.getOperator() );
 361     if( it==d_uf_enum.end() ){
 362       d_uf_enum[n.getOperator()] = true;
 363       std::vector< Node > lem;
 364       getEnumeratePredUfTerm( n, options::conjectureGenGtEnum(), lem );
 365       if( !lem.empty() ){
 366         for( unsigned j=0; j<lem.size(); j++ ){
 367           d_quantEngine->addLemma( lem[j], false );
 368           d_hasAddedLemma = true;
 369         }
 370         return false;
 371       }
 372     }
 373   }
 374   return true;
 375 }
 376
 377 void ConjectureGenerator::reset_round( Theory::Effort e ) {
 378
 379 }
 380
 381 void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
 382   if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
 383     d_fullEffortCount++;
 384     if( d_fullEffortCount%optFullCheckFrequency()==0 ){
 385       d_hasAddedLemma = false;
 386       d_tge.d_cg = this;
 387       double clSet = 0;
 388       if( Trace.isOn("sg-engine") ){
 389         clSet = double(clock())/double(CLOCKS_PER_SEC);
 390         Trace("sg-engine") << "---Conjecture Engine Round, effort = " << e << "---" << std::endl;
 391       }
 392       eq::EqualityEngine * ee = getEqualityEngine();
 393
 394       Trace("sg-proc") << "Get eq classes..." << std::endl;
 395       d_op_arg_index.clear();
 396       d_ground_eqc_map.clear();
 397       d_bool_eqc[0] = Node::null();
 398       d_bool_eqc[1] = Node::null();
 399       std::vector< TNode > eqcs;
 400       d_em.clear();
 401       eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
 402       while( !eqcs_i.isFinished() ){
 403         TNode r = (*eqcs_i);
 404         eqcs.push_back( r );
 405         if( r.getType().isBoolean() ){
 406           if( areEqual( r, getTermDatabase()->d_true ) ){
 407             d_ground_eqc_map[r] = getTermDatabase()->d_true;
 408             d_bool_eqc[0] = r;
 409           }else if( areEqual( r, getTermDatabase()->d_false ) ){
 410             d_ground_eqc_map[r] = getTermDatabase()->d_false;
 411             d_bool_eqc[1] = r;
 412           }
 413         }
 414         d_em[r] = eqcs.size();
 415         eq::EqClassIterator ieqc_i = eq::EqClassIterator( r, ee );
 416         while( !ieqc_i.isFinished() ){
 417           TNode n = (*ieqc_i);
 418           if( isHandledTerm( n ) ){
 419             d_op_arg_index[r].addTerm( this, n );
 420           }
 421           ++ieqc_i;
 422         }
 423         ++eqcs_i;
 424       }
 425       Assert( !d_bool_eqc[0].isNull() );
 426       Assert( !d_bool_eqc[1].isNull() );
 427       d_urelevant_terms.clear();
 428       Trace("sg-proc") << "...done get eq classes" << std::endl;
 429
 430       Trace("sg-proc") << "Determine ground EQC..." << std::endl;
 431       bool success;
 432       do{
 433         success = false;
 434         for( unsigned i=0; i<eqcs.size(); i++ ){
 435           TNode r = eqcs[i];
 436           if( d_ground_eqc_map.find( r )==d_ground_eqc_map.end() ){
 437             std::vector< TNode > args;
 438             Trace("sg-pat-debug") << "******* Get ground term for " << r << std::endl;
 439             Node n;
 440             if( getTermDatabase()->isInductionTerm( r ) ){
 441               n = d_op_arg_index[r].getGroundTerm( this, args );
 442             }else{
 443               n = r;
 444             }
 445             if( !n.isNull() ){
 446               Trace("sg-pat") << "Ground term for eqc " << r << " : " << std::endl;
 447               Trace("sg-pat") << "   " << n << std::endl;
 448               d_ground_eqc_map[r] = n;
 449               success = true;
 450             }else{
 451               Trace("sg-pat-debug") << "...could not find ground term." << std::endl;
 452             }
 453           }
 454         }
 455       }while( success );
 456       //also get ground terms
 457       d_ground_terms.clear();
 458       for( unsigned i=0; i<eqcs.size(); i++ ){
 459         TNode r = eqcs[i];
 460         d_op_arg_index[r].getGroundTerms( this, d_ground_terms );
 461       }
 462       Trace("sg-proc") << "...done determine ground EQC" << std::endl;
 463
 464       //debug printing
 465       if( Trace.isOn("sg-gen-eqc") ){
 466         for( unsigned i=0; i<eqcs.size(); i++ ){
 467           TNode r = eqcs[i];
 468           //print out members
 469           bool firstTime = true;
 470           bool isFalse = areEqual( r, getTermDatabase()->d_false );
 471           eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
 472           while( !eqc_i.isFinished() ){
 473             TNode n = (*eqc_i);
 474             if( !n.getAttribute(NoMatchAttribute()) && ( n.getKind()!=EQUAL || isFalse ) ){
 475               if( firstTime ){
 476                 Trace("sg-gen-eqc") << "e" << d_em[r] << " : { " << std::endl;
 477                 firstTime = false;
 478               }
 479               if( n.hasOperator() ){
 480                 Trace("sg-gen-eqc") << "   (" << n.getOperator();
 481                 getTermDatabase()->computeArgReps( n );
 482                 for( unsigned i=0; i<getTermDatabase()->d_arg_reps[n].size(); i++ ){
 483                   Trace("sg-gen-eqc") << " e" << d_em[getTermDatabase()->d_arg_reps[n][i]];
 484                 }
 485                 Trace("sg-gen-eqc") << ") :: " << n << std::endl;
 486               }else{
 487                 Trace("sg-gen-eqc") << "   " << n << std::endl;
 488               }
 489             }
 490             ++eqc_i;
 491           }
 492           if( !firstTime ){
 493             Trace("sg-gen-eqc") << "}" << std::endl;
 494             //print out ground term
 495             std::map< TNode, Node >::iterator it = d_ground_eqc_map.find( r );
 496             if( it!=d_ground_eqc_map.end() ){
 497               Trace("sg-gen-eqc") << "- Ground term : " << it->second << std::endl;
 498             }
 499           }
 500         }
 501       }
 502
 503       Trace("sg-proc") << "Compute relevant eqc..." << std::endl;
 504       d_tge.d_relevant_eqc[0].clear();
 505       d_tge.d_relevant_eqc[1].clear();
 506       for( unsigned i=0; i<eqcs.size(); i++ ){
 507         TNode r = eqcs[i];
 508         std::map< TNode, Node >::iterator it = d_ground_eqc_map.find( r );
 509         unsigned index = 1;
 510         if( it==d_ground_eqc_map.end() ){
 511           index = 0;
 512         }
 513         //based on unproven conjectures? TODO
 514         d_tge.d_relevant_eqc[index].push_back( r );
 515       }
 516       Trace("sg-gen-tg-debug") << "Initial relevant eqc : ";
 517       for( unsigned i=0; i<d_tge.d_relevant_eqc[0].size(); i++ ){
 518         Trace("sg-gen-tg-debug") << "e" << d_em[d_tge.d_relevant_eqc[0][i]] << " ";
 519       }
 520       Trace("sg-gen-tg-debug") << std::endl;
 521       Trace("sg-proc") << "...done compute relevant eqc" << std::endl;
 522
 523
 524       Trace("sg-proc") << "Collect signature information..." << std::endl;
 525       d_tge.collectSignatureInformation();
 526       if( d_hasAddedLemma ){
 527         Trace("sg-proc") << "...added enumeration lemmas." << std::endl;
 528       }
 529       Trace("sg-proc") << "...done collect signature information" << std::endl;
 530
 531
 532
 533       Trace("sg-proc") << "Build theorem index..." << std::endl;
 534       d_ue_canon.clear();
 535       d_thm_index.clear();
 536       std::vector< Node > provenConj;
 537       quantifiers::FirstOrderModel* m = d_quantEngine->getModel();
 538       for( int i=0; i<m->getNumAssertedQuantifiers(); i++ ){
 539         Node q = m->getAssertedQuantifier( i );
 540         Trace("thm-db-debug") << "Is " << q << " a relevant theorem?" << std::endl;
 541         Node conjEq;
 542         if( q[1].getKind()==EQUAL ){
 543           bool isSubsume = false;
 544           bool inEe = false;
 545           for( unsigned r=0; r<2; r++ ){
 546             TNode nl = q[1][r==0 ? 0 : 1];
 547             TNode nr = q[1][r==0 ? 1 : 0];
 548             Node eq = nl.eqNode( nr );
 549             if( r==1 || std::find( d_conjectures.begin(), d_conjectures.end(), q )==d_conjectures.end() ){
 550               //must make it canonical
 551               std::map< TypeNode, unsigned > var_count;
 552               std::map< TNode, TNode > subs;
 553               Trace("sg-proc-debug") << "get canonical " << eq << std::endl;
 554               eq = getCanonicalTerm( eq, var_count, subs );
 555             }
 556             if( !eq.isNull() ){
 557               if( r==0 ){
 558                 inEe = d_ee_conjectures.find( q[1] )!=d_ee_conjectures.end();
 559                 if( !inEe ){
 560                   //add to universal equality engine
 561                   Node nl = getUniversalRepresentative( eq[0], true );
 562                   Node nr = getUniversalRepresentative( eq[1], true );
 563                   if( areUniversalEqual( nl, nr ) ){
 564                     isSubsume = true;
 565                     //set inactive (will be ignored by other modules)
 566                     d_quantEngine->getModel()->setQuantifierActive( q, false );
 567                   }else{
 568                     Node exp;
 569                     d_ee_conjectures[q[1]] = true;
 570                     d_uequalityEngine.assertEquality( nl.eqNode( nr ), true, exp );
 571                   }
 572                 }
 573                 Trace("sg-conjecture") << "*** CONJECTURE : currently proven" << (isSubsume ? " and subsumed" : "");
 574                 Trace("sg-conjecture") << " : " << q[1] << std::endl;
 575                 provenConj.push_back( q );
 576               }
 577               if( !isSubsume ){
 578                 Trace("thm-db-debug") << "Adding theorem to database " << eq[0] << " == " << eq[1] << std::endl;
 579                 d_thm_index.addTheorem( eq[0], eq[1] );
 580               }else{
 581                 break;
 582               }
 583             }else{
 584               break;
 585             }
 586           }
 587         }
 588       }
 589       //examine status of other conjectures
 590       for( unsigned i=0; i<d_conjectures.size(); i++ ){
 591         Node q = d_conjectures[i];
 592         if( std::find( provenConj.begin(), provenConj.end(), q )==provenConj.end() ){
 593           //check each skolem variable
 594           bool disproven = true;
 595           //std::vector< Node > sk;
 596           //getTermDatabase()->getSkolemConstants( q, sk, true );
 597           Trace("sg-conjecture") << "    CONJECTURE : ";
 598           std::vector< Node > ce;
 599           for( unsigned j=0; j<getTermDatabase()->d_skolem_constants[q].size(); j++ ){
 600             TNode k = getTermDatabase()->d_skolem_constants[q][j];
 601             TNode rk = getRepresentative( k );
 602             std::map< TNode, Node >::iterator git = d_ground_eqc_map.find( rk );
 603             //check if it is a ground term
 604             if( git==d_ground_eqc_map.end() ){
 605               Trace("sg-conjecture") << "ACTIVE : " << q;
 606               if( Trace.isOn("sg-gen-eqc") ){
 607                 Trace("sg-conjecture") << " { ";
 608                 for( unsigned k=0; k<getTermDatabase()->d_skolem_constants[q].size(); k++ ){ Trace("sg-conjecture") << getTermDatabase()->d_skolem_constants[q][k] << ( j==k ? "*" : "" ) << " "; }
 609                 Trace("sg-conjecture") << "}";
 610               }
 611               Trace("sg-conjecture") << std::endl;
 612               disproven = false;
 613               break;
 614             }else{
 615               ce.push_back( git->second );
 616             }
 617           }
 618           if( disproven ){
 619             Trace("sg-conjecture") << "disproven : " << q << " : ";
 620             for( unsigned i=0; i<ce.size(); i++ ){
 621               Trace("sg-conjecture") << q[0][i] << " -> " << ce[i] << " ";
 622             }
 623             Trace("sg-conjecture") << std::endl;
 624           }
 625         }
 626       }
 627       Trace("thm-db") << "Theorem database is : " << std::endl;
 628       d_thm_index.debugPrint( "thm-db" );
 629       Trace("thm-db") << std::endl;
 630       Trace("sg-proc") << "...done build theorem index" << std::endl;
 631
 632
 633       //clear patterns
 634       d_patterns.clear();
 635       d_pattern_var_id.clear();
 636       d_pattern_var_duplicate.clear();
 637       d_pattern_is_normal.clear();
 638       d_pattern_is_relevant.clear();
 639       d_pattern_fun_id.clear();
 640       d_pattern_fun_sum.clear();
 641       d_rel_patterns.clear();
 642       d_rel_pattern_var_sum.clear();
 643       d_rel_pattern_typ_index.clear();
 644       d_rel_pattern_subs_index.clear();
 645
 646       unsigned rel_term_count = 0;
 647       std::map< TypeNode, unsigned > rt_var_max;
 648       std::vector< TypeNode > rt_types;
 649       std::map< TypeNode, std::map< int, std::vector< Node > > > conj_lhs;
 650       unsigned addedLemmas = 0;
 651       for( unsigned depth=1; depth<=3; depth++ ){
 652         Trace("sg-proc") << "Generate relevant LHS at depth " << depth << "..." << std::endl;
 653         Trace("sg-rel-term") << "Relevant terms of depth " << depth << " : " << std::endl;
 654         //set up environment
 655         d_tge.d_var_id.clear();
 656         d_tge.d_var_limit.clear();
 657         d_tge.reset( depth, true, TypeNode::null() );
 658         while( d_tge.getNextTerm() ){
 659           //construct term
 660           Node nn = d_tge.getTerm();
 661           if( !options::conjectureFilterCanonical() || considerTermCanon( nn, true ) ){
 662             rel_term_count++;
 663             Trace("sg-rel-term") << "*** Relevant term : ";
 664             d_tge.debugPrint( "sg-rel-term", "sg-rel-term-debug2" );
 665             Trace("sg-rel-term") << std::endl;
 666
 667             for( unsigned r=0; r<2; r++ ){
 668               Trace("sg-rel-term-debug") << "...from equivalence classes (" << r << ") : ";
 669               int index = d_tge.d_ccand_eqc[r].size()-1;
 670               for( unsigned j=0; j<d_tge.d_ccand_eqc[r][index].size(); j++ ){
 671                 Trace("sg-rel-term-debug") << "e" << d_em[d_tge.d_ccand_eqc[r][index][j]] << " ";
 672               }
 673               Trace("sg-rel-term-debug") << std::endl;
 674             }
 675             TypeNode tnn = nn.getType();
 676             Trace("sg-gen-tg-debug") << "...term is " << nn << std::endl;
 677             conj_lhs[tnn][depth].push_back( nn );
 678
 679             //add information about pattern
 680             Trace("sg-gen-tg-debug") << "Collect pattern information..." << std::endl;
 681             Assert( std::find( d_rel_patterns[tnn].begin(), d_rel_patterns[tnn].end(), nn )==d_rel_patterns[tnn].end() );
 682             d_rel_patterns[tnn].push_back( nn );
 683             //build information concerning the variables in this pattern
 684             unsigned sum = 0;
 685             std::map< TypeNode, unsigned > typ_to_subs_index;
 686             std::vector< TNode > gsubs_vars;
 687             for( std::map< TypeNode, unsigned >::iterator it = d_tge.d_var_id.begin(); it != d_tge.d_var_id.end(); ++it ){
 688               if( it->second>0 ){
 689                 typ_to_subs_index[it->first] = sum;
 690                 sum += it->second;
 691                 for( unsigned i=0; i<it->second; i++ ){
 692                   gsubs_vars.push_back( getFreeVar( it->first, i ) );
 693                 }
 694               }
 695             }
 696             d_rel_pattern_var_sum[nn] = sum;
 697             //register the pattern
 698             registerPattern( nn, tnn );
 699             Assert( d_pattern_is_normal[nn] );
 700             Trace("sg-gen-tg-debug") << "...done collect pattern information" << std::endl;
 701
 702             //record information about types
 703             Trace("sg-gen-tg-debug") << "Collect type information..." << std::endl;
 704             PatternTypIndex * pti = &d_rel_pattern_typ_index;
 705             for( std::map< TypeNode, unsigned >::iterator it = d_tge.d_var_id.begin(); it != d_tge.d_var_id.end(); ++it ){
 706               pti = &pti->d_children[it->first][it->second];
 707               //record maximum
 708               if( rt_var_max.find( it->first )==rt_var_max.end() || it->second>rt_var_max[it->first] ){
 709                 rt_var_max[it->first] = it->second;
 710               }
 711             }
 712             if( std::find( rt_types.begin(), rt_types.end(), tnn )==rt_types.end() ){
 713               rt_types.push_back( tnn );
 714             }
 715             pti->d_terms.push_back( nn );
 716             Trace("sg-gen-tg-debug") << "...done collect type information" << std::endl;
 717
 718             Trace("sg-gen-tg-debug") << "Build substitutions for ground EQC..." << std::endl;
 719             std::vector< TNode > gsubs_terms;
 720             gsubs_terms.resize( gsubs_vars.size() );
 721             int index = d_tge.d_ccand_eqc[1].size()-1;
 722             for( unsigned j=0; j<d_tge.d_ccand_eqc[1][index].size(); j++ ){
 723               TNode r = d_tge.d_ccand_eqc[1][index][j];
 724               Trace("sg-rel-term-debug") << "  Matches for e" << d_em[r] << ", which is ground term " << d_ground_eqc_map[r] << ":" << std::endl;
 725               std::map< TypeNode, std::map< unsigned, TNode > > subs;
 726               std::map< TNode, bool > rev_subs;
 727               //only get ground terms
 728               unsigned mode = 2;
 729               d_tge.resetMatching( r, mode );
 730               while( d_tge.getNextMatch( r, subs, rev_subs ) ){
 731                 //we will be building substitutions
 732                 bool firstTime = true;
 733                 for( std::map< TypeNode, std::map< unsigned, TNode > >::iterator it = subs.begin(); it != subs.end(); ++it ){
 734                   unsigned tindex = typ_to_subs_index[it->first];
 735                   for( std::map< unsigned, TNode >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
 736                     if( !firstTime ){
 737                       Trace("sg-rel-term-debug") << ", ";
 738                     }else{
 739                       firstTime = false;
 740                       Trace("sg-rel-term-debug") << "    ";
 741                     }
 742                     Trace("sg-rel-term-debug") << it->first << ":x" << it2->first << " -> " << it2->second;
 743                     Assert( tindex+it2->first<gsubs_terms.size() );
 744                     gsubs_terms[tindex+it2->first] = it2->second;
 745                   }
 746                 }
 747                 Trace("sg-rel-term-debug") << std::endl;
 748                 d_rel_pattern_subs_index[nn].addSubstitution( r, gsubs_vars, gsubs_terms );
 749               }
 750             }
 751             Trace("sg-gen-tg-debug") << "...done build substitutions for ground EQC" << std::endl;
 752           }else{
 753             Trace("sg-gen-tg-debug") << "> not canonical : " << nn << std::endl;
 754           }
 755         }
 756         Trace("sg-proc") << "...done generate terms at depth " << depth << std::endl;
 757         Trace("sg-stats") << "--------> Total LHS of depth " << depth << " : " << rel_term_count << std::endl;
 758         //Trace("conjecture-count") << "Total LHS of depth " << depth << " : " << conj_lhs[depth].size() << std::endl;
 759
 760         /* test...
 761         for( unsigned i=0; i<rt_types.size(); i++ ){
 762           Trace("sg-term-enum") << "Term enumeration for " << rt_types[i] << " : " << std::endl;
 763           Trace("sg-term-enum") << "Ground term : " << rt_types[i].mkGroundTerm() << std::endl;
 764           for( unsigned j=0; j<150; j++ ){
 765             Trace("sg-term-enum") << "  " << getEnumerateTerm( rt_types[i], j ) << std::endl;
 766           }
 767         }
 768         */
 769
 770         //consider types from relevant terms
 771         for( unsigned rdepth=0; rdepth<=depth; rdepth++ ){
 772           //set up environment
 773           d_tge.d_var_id.clear();
 774           d_tge.d_var_limit.clear();
 775           for( std::map< TypeNode, unsigned >::iterator it = rt_var_max.begin(); it != rt_var_max.end(); ++it ){
 776             d_tge.d_var_id[ it->first ] = it->second;
 777             d_tge.d_var_limit[ it->first ] = it->second;
 778           }
 779           std::random_shuffle( rt_types.begin(), rt_types.end() );
 780           std::map< TypeNode, std::vector< Node > > conj_rhs;
 781           for( unsigned i=0; i<rt_types.size(); i++ ){
 782
 783             Trace("sg-proc") << "Generate relevant RHS terms of type " << rt_types[i] << " at depth " << rdepth << "..." << std::endl;
 784             d_tge.reset( rdepth, false, rt_types[i] );
 785
 786             while( d_tge.getNextTerm() ){
 787               Node rhs = d_tge.getTerm();
 788               if( considerTermCanon( rhs, false ) ){
 789                 Trace("sg-rel-prop") << "Relevant RHS : " << rhs << std::endl;
 790                 //register pattern
 791                 Assert( rhs.getType()==rt_types[i] );
 792                 registerPattern( rhs, rt_types[i] );
 793                 if( rdepth<depth ){
 794                   //consider against all LHS at depth
 795                   for( unsigned j=0; j<conj_lhs[rt_types[i]][depth].size(); j++ ){
 796                     processCandidateConjecture( conj_lhs[rt_types[i]][depth][j], rhs, depth, rdepth );
 797                   }
 798                 }else{
 799                   conj_rhs[rt_types[i]].push_back( rhs );
 800                 }
 801               }
 802             }
 803           }
 804           flushWaitingConjectures( addedLemmas, depth, rdepth );
 805           //consider against all LHS up to depth
 806           if( rdepth==depth ){
 807             for( unsigned lhs_depth = 1; lhs_depth<=depth; lhs_depth++ ){
 808               if( (int)addedLemmas<options::conjectureGenPerRound() ){
 809                 Trace("sg-proc") << "Consider conjectures at depth (" << lhs_depth << ", " << rdepth << ")..." << std::endl;
 810                 for( std::map< TypeNode, std::vector< Node > >::iterator it = conj_rhs.begin(); it != conj_rhs.end(); ++it ){
 811                   for( unsigned j=0; j<it->second.size(); j++ ){
 812                     for( unsigned k=0; k<conj_lhs[it->first][lhs_depth].size(); k++ ){
 813                       processCandidateConjecture( conj_lhs[it->first][lhs_depth][k], it->second[j], lhs_depth, rdepth );
 814                     }
 815                   }
 816                 }
 817                 flushWaitingConjectures( addedLemmas, lhs_depth, depth );
 818               }
 819             }
 820           }
 821           if( (int)addedLemmas>=options::conjectureGenPerRound() ){
 822             break;
 823           }
 824         }
 825         if( (int)addedLemmas>=options::conjectureGenPerRound() ){
 826           break;
 827         }
 828       }
 829
 830       if( Trace.isOn("thm-ee") ){
 831         Trace("thm-ee") << "Universal equality engine is : " << std::endl;
 832         eq::EqClassesIterator ueqcs_i = eq::EqClassesIterator( &d_uequalityEngine );
 833         while( !ueqcs_i.isFinished() ){
 834           TNode r = (*ueqcs_i);
 835           bool firstTime = true;
 836           TNode rr = getUniversalRepresentative( r );
 837           Trace("thm-ee") << "  " << rr;
 838           Trace("thm-ee") << " : { ";
 839           eq::EqClassIterator ueqc_i = eq::EqClassIterator( r, &d_uequalityEngine );
 840           while( !ueqc_i.isFinished() ){
 841             TNode n = (*ueqc_i);
 842             if( rr!=n ){
 843               if( firstTime ){
 844                 Trace("thm-ee") << std::endl;
 845                 firstTime = false;
 846               }
 847               Trace("thm-ee") << "    " << n << std::endl;
 848             }
 849             ++ueqc_i;
 850           }
 851           if( !firstTime ){ Trace("thm-ee") << "  "; }
 852           Trace("thm-ee") << "}" << std::endl;
 853           ++ueqcs_i;
 854         }
 855         Trace("thm-ee") << std::endl;
 856       }
 857       if( Trace.isOn("sg-engine") ){
 858         double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
 859         Trace("sg-engine") << "Finished conjecture generator, time = " << (clSet2-clSet) << std::endl;
 860       }
 861     }
 862   }
 863 }
 864
 865 unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth ) {
 866   if( !d_waiting_conjectures_lhs.empty() ){
 867     Trace("sg-proc") << "Generated " << d_waiting_conjectures_lhs.size() << " conjectures at depth " << ldepth << "/" << rdepth << "." << std::endl;
 868     if( !optStatsOnly() && (int)addedLemmas<options::conjectureGenPerRound() ){
 869       std::vector< unsigned > indices;
 870       for( unsigned i=0; i<d_waiting_conjectures_lhs.size(); i++ ){
 871         indices.push_back( i );
 872       }
 873       bool doSort = false;
 874       if( doSort ){
 875         //sort them based on score
 876         sortConjectureScore scs;
 877         scs.d_scores.insert( scs.d_scores.begin(), d_waiting_conjectures_score.begin(), d_waiting_conjectures_score.end() );
 878         std::sort( indices.begin(), indices.end(), scs );
 879       }
 880       if( doSort && d_waiting_conjectures_score[indices[0]]<optFilterScoreThreshold() ){
 881         //do splitting on demand (TODO)
 882
 883       }else{
 884         for( unsigned i=0; i<indices.size(); i++ ){
 885           //if( d_waiting_conjectures_score[indices[i]]<optFilterScoreThreshold() ){
 886           if( d_waiting_conjectures_score[indices[i]]>=optFilterScoreThreshold() ){
 887             //we have determined a relevant subgoal
 888             Node lhs = d_waiting_conjectures_lhs[indices[i]];
 889             Node rhs = d_waiting_conjectures_rhs[indices[i]];
 890             if( options::conjectureFilterCanonical() && ( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ) ){
 891               //skip
 892             }else{
 893               Trace("sg-engine") << "*** Consider conjecture : " << lhs << " == " << rhs << std::endl;
 894               Trace("sg-engine-debug") << "      score : " << d_waiting_conjectures_score[indices[i]] << std::endl;
 895               std::vector< Node > bvs;
 896               for( std::map< TypeNode, unsigned >::iterator it = d_pattern_var_id[lhs].begin(); it != d_pattern_var_id[lhs].end(); ++it ){
 897                 for( unsigned i=0; i<=it->second; i++ ){
 898                   bvs.push_back( getFreeVar( it->first, i ) );
 899                 }
 900               }
 901               Node rsg;
 902               if( !bvs.empty() ){
 903                 Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );
 904                 rsg = NodeManager::currentNM()->mkNode( FORALL, bvl, lhs.eqNode( rhs ) );
 905               }else{
 906                 rsg = lhs.eqNode( rhs );
 907               }
 908               rsg = Rewriter::rewrite( rsg );
 909               d_conjectures.push_back( rsg );
 910               d_eq_conjectures[lhs].push_back( rhs );
 911               d_eq_conjectures[rhs].push_back( lhs );
 912
 913               Node lem = NodeManager::currentNM()->mkNode( OR, rsg.negate(), rsg );
 914               d_quantEngine->addLemma( lem, false );
 915               d_quantEngine->addRequirePhase( rsg, false );
 916               addedLemmas++;
 917               if( (int)addedLemmas>=options::conjectureGenPerRound() ){
 918                 break;
 919               }
 920             }
 921           }else{
 922             if( doSort ){
 923               break;
 924             }
 925           }
 926         }
 927       }
 928       Trace("sg-proc") << "...have now added " << addedLemmas << " conjecture lemmas." << std::endl;
 929     }
 930     d_waiting_conjectures_lhs.clear();
 931     d_waiting_conjectures_rhs.clear();
 932     d_waiting_conjectures_score.clear();
 933     d_waiting_conjectures.clear();
 934   }
 935   return addedLemmas;
 936 }
 937
 938 void ConjectureGenerator::registerQuantifier( Node q ) {
 939
 940 }
 941
 942 void ConjectureGenerator::assertNode( Node n ) {
 943
 944 }
 945
 946 bool ConjectureGenerator::considerTermCanon( Node ln, bool genRelevant ){
 947   if( !ln.isNull() ){
 948     //do not consider if it is non-canonical, and either:
 949     //  (1) we are not generating relevant terms, or
 950     //  (2) its canonical form is a generalization.
 951     TNode lnr = getUniversalRepresentative( ln, true );
 952     if( lnr==ln ){
 953       markReportedCanon( ln );
 954     }else if( !genRelevant || isGeneralization( lnr, ln ) ){
 955       Trace("sg-gen-consider-term") << "Do not consider term, " << ln << " is not canonical representation (which is " << lnr << ")." << std::endl;
 956       return false;
 957     }
 958   }
 959   Trace("sg-gen-tg-debug") << "Will consider term canon " << ln << std::endl;
 960   Trace("sg-gen-consider-term-debug") << std::endl;
 961   return true;
 962 }
 963
 964 unsigned ConjectureGenerator::collectFunctions( TNode opat, TNode pat, std::map< TNode, unsigned >& funcs,
 965                                              std::map< TypeNode, unsigned >& mnvn, std::map< TypeNode, unsigned >& mxvn ){
 966   if( pat.hasOperator() ){
 967     funcs[pat.getOperator()]++;
 968     if( !d_tge.isRelevantFunc( pat.getOperator() ) ){
 969       d_pattern_is_relevant[opat] = false;
 970     }
 971     unsigned sum = 1;
 972     for( unsigned i=0; i<pat.getNumChildren(); i++ ){
 973       sum += collectFunctions( opat, pat[i], funcs, mnvn, mxvn );
 974     }
 975     return sum;
 976   }else{
 977     Assert( pat.getNumChildren()==0 );
 978     funcs[pat]++;
 979     //for variables
 980     if( pat.getKind()==BOUND_VARIABLE ){
 981       if( funcs[pat]>1 ){
 982         //duplicate variable
 983         d_pattern_var_duplicate[opat]++;
 984       }else{
 985         //check for max/min
 986         TypeNode tn = pat.getType();
 987         unsigned vn = d_free_var_num[pat];
 988         std::map< TypeNode, unsigned >::iterator it = mnvn.find( tn );
 989         if( it!=mnvn.end() ){
 990           if( vn<it->second ){
 991             d_pattern_is_normal[opat] = false;
 992             mnvn[tn] = vn;
 993           }else if( vn>mxvn[tn] ){
 994             if( vn!=mxvn[tn]+1 ){
 995               d_pattern_is_normal[opat] = false;
 996             }
 997             mxvn[tn] = vn;
 998           }
 999         }else{
1000           //first variable of this type
1001           mnvn[tn] = vn;
1002           mxvn[tn] = vn;
1003         }
1004       }
1005     }else{
1006       d_pattern_is_relevant[opat] = false;
1007     }
1008     return 1;
1009   }
1010 }
1011
1012 void ConjectureGenerator::registerPattern( Node pat, TypeNode tpat ) {
1013   if( std::find( d_patterns[tpat].begin(), d_patterns[tpat].end(), pat )==d_patterns[tpat].end() ){
1014     d_patterns[TypeNode::null()].push_back( pat );
1015     d_patterns[tpat].push_back( pat );
1016
1017     Assert( d_pattern_fun_id.find( pat )==d_pattern_fun_id.end() );
1018     Assert( d_pattern_var_id.find( pat )==d_pattern_var_id.end() );
1019
1020     //collect functions
1021     std::map< TypeNode, unsigned > mnvn;
1022     d_pattern_fun_sum[pat] = collectFunctions( pat, pat, d_pattern_fun_id[pat], mnvn, d_pattern_var_id[pat] );
1023     if( d_pattern_is_normal.find( pat )==d_pattern_is_normal.end() ){
1024       d_pattern_is_normal[pat] = true;
1025     }
1026     if( d_pattern_is_relevant.find( pat )==d_pattern_is_relevant.end() ){
1027       d_pattern_is_relevant[pat] = true;
1028     }
1029   }
1030 }
1031
1032 bool ConjectureGenerator::isGeneralization( TNode patg, TNode pat, std::map< TNode, TNode >& subs ) {
1033   if( patg.getKind()==BOUND_VARIABLE ){
1034     std::map< TNode, TNode >::iterator it = subs.find( patg );
1035     if( it!=subs.end() ){
1036       return it->second==pat;
1037     }else{
1038       subs[patg] = pat;
1039       return true;
1040     }
1041   }else{
1042     Assert( patg.hasOperator() );
1043     if( !pat.hasOperator() || patg.getOperator()!=pat.getOperator() ){
1044       return false;
1045     }else{
1046       Assert( patg.getNumChildren()==pat.getNumChildren() );
1047       for( unsigned i=0; i<patg.getNumChildren(); i++ ){
1048         if( !isGeneralization( patg[i], pat[i], subs ) ){
1049           return false;
1050         }
1051       }
1052       return true;
1053     }
1054   }
1055 }
1056
1057 int ConjectureGenerator::calculateGeneralizationDepth( TNode n, std::vector< TNode >& fv ) {
1058   if( n.getKind()==BOUND_VARIABLE ){
1059     if( std::find( fv.begin(), fv.end(), n )==fv.end() ){
1060       fv.push_back( n );
1061       return 0;
1062     }else{
1063       return 1;
1064     }
1065   }else{
1066     int depth = 1;
1067     for( unsigned i=0; i<n.getNumChildren(); i++ ){
1068       depth += calculateGeneralizationDepth( n[i], fv );
1069     }
1070     return depth;
1071   }
1072 }
1073
1074 Node ConjectureGenerator::getPredicateForType( TypeNode tn ) {
1075   std::map< TypeNode, Node >::iterator it = d_typ_pred.find( tn );
1076   if( it==d_typ_pred.end() ){
1077     TypeNode op_tn = NodeManager::currentNM()->mkFunctionType( tn, NodeManager::currentNM()->booleanType() );
1078     Node op = NodeManager::currentNM()->mkSkolem( "PE", op_tn, "was created by conjecture ground term enumerator." );
1079     d_typ_pred[tn] = op;
1080     return op;
1081   }else{
1082     return it->second;
1083   }
1084 }
1085
1086 void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms ) {
1087   if( n.getNumChildren()>0 ){
1088     std::vector< int > vec;
1089     for( unsigned i=0; i<n.getNumChildren(); i++ ){
1090       vec.push_back( 0 );
1091     }
1092     vec.pop_back();
1093     int size_limit = 0;
1094     int vec_sum = -1;
1095     unsigned index = 0;
1096     unsigned last_size = terms.size();
1097     while( terms.size()<num ){
1098       bool success = true;
1099       if( vec_sum==-1 ){
1100         vec_sum = 0;
1101         vec.push_back( size_limit );
1102       }else{
1103         //see if we can iterate current
1104         if( vec_sum<size_limit && !getTermDatabase()->getEnumerateTerm( n[index].getType(), vec[index]+1 ).isNull() ){
1105           vec[index]++;
1106           vec_sum++;
1107           vec.push_back( size_limit - vec_sum );
1108         }else{
1109           vec_sum -= vec[index];
1110           vec[index] = 0;
1111           index++;
1112           if( index==n.getNumChildren() ){
1113             success = false;
1114           }
1115         }
1116       }
1117       if( success ){
1118         if( vec.size()==n.getNumChildren() ){
1119           Node lc = getTermDatabase()->getEnumerateTerm( n[vec.size()-1].getType(), vec[vec.size()-1] );
1120           if( !lc.isNull() ){
1121             for( unsigned i=0; i<vec.size(); i++ ){
1122               Trace("sg-gt-enum-debug") << vec[i] << " ";
1123             }
1124             Trace("sg-gt-enum-debug") << " / " << size_limit << std::endl;
1125             for( unsigned i=0; i<n.getNumChildren(); i++ ){
1126               Trace("sg-gt-enum-debug") << n[i].getType() << " ";
1127             }
1128             Trace("sg-gt-enum-debug") << std::endl;
1129             std::vector< Node > children;
1130             children.push_back( n.getOperator() );
1131             for( unsigned i=0; i<(vec.size()-1); i++ ){
1132               Node nn = getTermDatabase()->getEnumerateTerm( n[i].getType(), vec[i] );
1133               Assert( !nn.isNull() );
1134               Assert( nn.getType()==n[i].getType() );
1135               children.push_back( nn );
1136             }
1137             children.push_back( lc );
1138             Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
1139             Trace("sg-gt-enum") << "Ground term enumerate : " << n << std::endl;
1140             terms.push_back( n );
1141           }
1142           vec.pop_back();
1143           index = 0;
1144         }
1145       }else{
1146         if( terms.size()>last_size ){
1147           last_size = terms.size();
1148           size_limit++;
1149           for( unsigned i=0; i<vec.size(); i++ ){
1150             vec[i] = 0;
1151           }
1152           vec_sum = -1;
1153         }
1154       }
1155     }
1156   }else{
1157     terms.push_back( n );
1158   }
1159 }
1160
1161 void ConjectureGenerator::getEnumeratePredUfTerm( Node n, unsigned num, std::vector< Node >& terms ) {
1162   std::vector< Node > uf_terms;
1163   getEnumerateUfTerm( n, num, uf_terms );
1164   Node p = getPredicateForType( n.getType() );
1165   for( unsigned i=0; i<uf_terms.size(); i++ ){
1166     terms.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, p, uf_terms[i] ) );
1167   }
1168 }
1169
1170 void ConjectureGenerator::processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth ) {
1171   int score = considerCandidateConjecture( lhs, rhs );
1172   if( score>0 ){
1173     Trace("sg-conjecture") << "* Candidate conjecture : " << lhs << " == " << rhs << std::endl;
1174     Trace("sg-conjecture-debug") << "     LHS, RHS generalization depth : " << lhs_depth << ", " << rhs_depth << std::endl;
1175     Trace("sg-conjecture-debug") << "     confirmed = " << d_subs_confirmCount << ", #witnesses range = " << d_subs_confirmWitnessRange.size() << "." << std::endl;
1176     Trace("sg-conjecture-debug") << "     #witnesses for ";
1177     bool firstTime = true;
1178     for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){
1179       if( !firstTime ){
1180         Trace("sg-conjecture-debug") << ", ";
1181       }
1182       Trace("sg-conjecture-debug") << it->first << " : " << it->second.size();
1183       //if( it->second.size()==1 ){
1184       //  Trace("sg-conjecture-debug") << " (" << it->second[0] << ")";
1185       //}
1186       Trace("sg-conjecture-debug2") << " (";
1187       for( unsigned j=0; j<it->second.size(); j++ ){
1188         if( j>0 ){ Trace("sg-conjecture-debug2") << " "; }
1189         Trace("sg-conjecture-debug2") << d_ground_eqc_map[it->second[j]];
1190       }
1191       Trace("sg-conjecture-debug2") << ")";
1192       firstTime = false;
1193     }
1194     Trace("sg-conjecture-debug") << std::endl;
1195     Trace("sg-conjecture-debug") << "     unknown = " << d_subs_unkCount << std::endl;
1196     //Assert( getUniversalRepresentative( rhs )==rhs );
1197     //Assert( getUniversalRepresentative( lhs )==lhs );
1198     d_waiting_conjectures_lhs.push_back( lhs );
1199     d_waiting_conjectures_rhs.push_back( rhs );
1200     d_waiting_conjectures_score.push_back( score );
1201     d_waiting_conjectures[lhs].push_back( rhs );
1202     d_waiting_conjectures[rhs].push_back( lhs );
1203   }
1204 }
1205
1206 int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {
1207   Assert( lhs.getType()==rhs.getType() );
1208
1209   Trace("sg-cconj-debug") << "Consider candidate conjecture : " << lhs << " == " << rhs << "?" << std::endl;
1210   if( lhs==rhs ){
1211     Trace("sg-cconj-debug") << "  -> trivial." << std::endl;
1212     return -1;
1213   }else{
1214     if( lhs.getKind()==APPLY_CONSTRUCTOR && rhs.getKind()==APPLY_CONSTRUCTOR ){
1215       Trace("sg-cconj-debug") << "  -> irrelevant by syntactic analysis." << std::endl;
1216       return -1;
1217     }
1218     //variables of LHS must subsume variables of RHS
1219     for( std::map< TypeNode, unsigned >::iterator it = d_pattern_var_id[rhs].begin(); it != d_pattern_var_id[rhs].end(); ++it ){
1220       std::map< TypeNode, unsigned >::iterator itl = d_pattern_var_id[lhs].find( it->first );
1221       if( itl!=d_pattern_var_id[lhs].end() ){
1222         if( itl->second<it->second ){
1223           Trace("sg-cconj-debug") << "  -> variables of sort " << it->first << " are not subsumed." << std::endl;
1224           return -1;
1225         }else{
1226           Trace("sg-cconj-debug2") << "  variables of sort " << it->first << " are : " << itl->second << " vs " << it->second << std::endl;
1227         }
1228       }else{
1229         Trace("sg-cconj-debug") << "  -> has no variables of sort " << it->first << "." << std::endl;
1230         return -1;
1231       }
1232     }
1233
1234     //currently active conjecture?
1235     std::map< Node, std::vector< Node > >::iterator iteq = d_eq_conjectures.find( lhs );
1236     if( iteq!=d_eq_conjectures.end() ){
1237       if( std::find( iteq->second.begin(), iteq->second.end(), rhs )!=iteq->second.end() ){
1238         Trace("sg-cconj-debug") << "  -> this conjecture is already active." << std::endl;
1239         return -1;
1240       }
1241     }
1242     //current a waiting conjecture?
1243     std::map< Node, std::vector< Node > >::iterator itw = d_waiting_conjectures.find( lhs );
1244     if( itw!=d_waiting_conjectures.end() ){
1245       if( std::find( itw->second.begin(), itw->second.end(), rhs )!=itw->second.end() ){
1246         Trace("sg-cconj-debug") << "  -> already are considering this conjecture." << std::endl;
1247         return -1;
1248       }
1249     }
1250     //check if canonical representation (should be, but for efficiency this is not guarenteed)
1251     //if( options::conjectureFilterCanonical() && ( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ) ){
1252     //  Trace("sg-cconj") << "  -> after processing, not canonical." << std::endl;
1253     //  return -1;
1254     //}
1255
1256     int score;
1257     bool scoreSet = false;
1258
1259     Trace("sg-cconj") << "Consider possible candidate conjecture : " << lhs << " == " << rhs << "?" << std::endl;
1260     //find witness for counterexample, if possible
1261     if( options::conjectureFilterModel() ){
1262       Assert( d_rel_pattern_var_sum.find( lhs )!=d_rel_pattern_var_sum.end() );
1263       Trace("sg-cconj-debug") << "Notify substitutions over " << d_rel_pattern_var_sum[lhs] << " variables." << std::endl;
1264       std::map< TNode, TNode > subs;
1265       d_subs_confirmCount = 0;
1266       d_subs_confirmWitnessRange.clear();
1267       d_subs_confirmWitnessDomain.clear();
1268       d_subs_unkCount = 0;
1269       if( !d_rel_pattern_subs_index[lhs].notifySubstitutions( this, subs, rhs, d_rel_pattern_var_sum[lhs] ) ){
1270         Trace("sg-cconj") << "  -> found witness that falsifies the conjecture." << std::endl;
1271         return -1;
1272       }
1273       //score is the minimum number of distinct substitutions for a variable
1274       for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){
1275         int num = (int)it->second.size();
1276         if( !scoreSet || num<score ){
1277           score = num;
1278           scoreSet = true;
1279         }
1280       }
1281       if( !scoreSet ){
1282         score = 0;
1283       }
1284       Trace("sg-cconj") << "     confirmed = " << d_subs_confirmCount << ", #witnesses range = " << d_subs_confirmWitnessRange.size() << "." << std::endl;
1285       for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){
1286         Trace("sg-cconj") << "     #witnesses for " << it->first << " : " << it->second.size() << std::endl;
1287       }
1288     }else{
1289       score = 0;
1290     }
1291
1292     Trace("sg-cconj") << "  -> SUCCESS." << std::endl;
1293     Trace("sg-cconj") << "     score : " << score << std::endl;
1294
1295     return score;
1296   }
1297 }
1298
1299 bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode >& subs, TNode rhs ) {
1300   if( Trace.isOn("sg-cconj-debug") ){
1301     Trace("sg-cconj-debug") << "Ground eqc for LHS : " << glhs << ", based on substituion: " << std::endl;
1302     for( std::map< TNode, TNode >::iterator it = subs.begin(); it != subs.end(); ++it ){
1303       Assert( getRepresentative( it->second )==it->second );
1304       Trace("sg-cconj-debug") << "  " << it->first << " -> " << it->second << std::endl;
1305     }
1306   }
1307   Trace("sg-cconj-debug") << "Evaluate RHS : : " << rhs << std::endl;
1308   //get the representative of rhs with substitution subs
1309   TNode grhs = getTermDatabase()->evaluateTerm( rhs, subs, true );
1310   Trace("sg-cconj-debug") << "...done evaluating term, got : " << grhs << std::endl;
1311   if( !grhs.isNull() ){
1312     if( glhs!=grhs ){
1313       Trace("sg-cconj-debug") << "Ground eqc for RHS : " << grhs << std::endl;
1314       //check based on ground terms
1315       std::map< TNode, Node >::iterator itl = d_ground_eqc_map.find( glhs );
1316       if( itl!=d_ground_eqc_map.end() ){
1317         std::map< TNode, Node >::iterator itr = d_ground_eqc_map.find( grhs );
1318         if( itr!=d_ground_eqc_map.end() ){
1319           Trace("sg-cconj-debug") << "We have ground terms " << itl->second << " and " << itr->second << "." << std::endl;
1320           if( itl->second.isConst() && itr->second.isConst() ){
1321             Trace("sg-cconj-debug") << "...disequal constants." << std::endl;
1322             Trace("sg-cconj-witness") << "  Witness of falsification : " << itl->second << " != " << itr->second << ", substutition is : " << std::endl;
1323             for( std::map< TNode, TNode >::iterator it = subs.begin(); it != subs.end(); ++it ){
1324               Trace("sg-cconj-witness") << "    " << it->first << " -> " << it->second << std::endl;
1325             }
1326             return false;
1327           }
1328         }
1329       }
1330     }
1331     Trace("sg-cconj-debug") << "RHS is identical." << std::endl;
1332     bool isGroundSubs = true;
1333     for( std::map< TNode, TNode >::iterator it = subs.begin(); it != subs.end(); ++it ){
1334       std::map< TNode, Node >::iterator git = d_ground_eqc_map.find( it->second );
1335       if( git==d_ground_eqc_map.end() ){
1336         isGroundSubs = false;
1337         break;
1338       }
1339     }
1340     if( isGroundSubs ){
1341       if( glhs==grhs ){
1342         Trace("sg-cconj-witness") << "  Witnessed " << glhs << " == " << grhs << ", substutition is : " << std::endl;
1343         for( std::map< TNode, TNode >::iterator it = subs.begin(); it != subs.end(); ++it ){
1344           Trace("sg-cconj-witness") << "    " << it->first << " -> " << it->second << std::endl;
1345           if( std::find( d_subs_confirmWitnessDomain[it->first].begin(), d_subs_confirmWitnessDomain[it->first].end(), it->second )==d_subs_confirmWitnessDomain[it->first].end() ){
1346             d_subs_confirmWitnessDomain[it->first].push_back( it->second );
1347           }
1348         }
1349         d_subs_confirmCount++;
1350         if( std::find( d_subs_confirmWitnessRange.begin(), d_subs_confirmWitnessRange.end(), glhs )==d_subs_confirmWitnessRange.end() ){
1351           d_subs_confirmWitnessRange.push_back( glhs );
1352         }
1353       }else{
1354         if( optFilterUnknown() ){
1355           Trace("sg-cconj-debug") << "...ground substitution giving terms that are neither equal nor disequal." << std::endl;
1356           return false;
1357         }
1358       }
1359     }
1360   }else{
1361     Trace("sg-cconj-debug") << "(could not ground eqc for RHS)." << std::endl;
1362   }
1363   return true;
1364 }
1365
1366
1367
1368
1369
1370
1371 void TermGenerator::reset( TermGenEnv * s, TypeNode tn ) {
1372   Assert( d_children.empty() );
1373   d_typ = tn;
1374   d_status = 0;
1375   d_status_num = 0;
1376   d_children.clear();
1377   Trace("sg-gen-tg-debug2") << "...add to context " << this << std::endl;
1378   d_id = s->d_tg_id;
1379   s->changeContext( true );
1380 }
1381
1382 bool TermGenerator::getNextTerm( TermGenEnv * s, unsigned depth ) {
1383   if( Trace.isOn("sg-gen-tg-debug2") ){
1384     Trace("sg-gen-tg-debug2") << this << " getNextTerm depth " << depth << " : status = " << d_status << ", num = " << d_status_num;
1385     if( d_status==5 ){
1386       TNode f = s->getTgFunc( d_typ, d_status_num );
1387       Trace("sg-gen-tg-debug2") << ", f = " << f;
1388       Trace("sg-gen-tg-debug2") << ", #args = " << s->d_func_args[f].size();
1389       Trace("sg-gen-tg-debug2") << ", childNum = " << d_status_child_num;
1390       Trace("sg-gen-tg-debug2") << ", #children = " << d_children.size();
1391     }
1392     Trace("sg-gen-tg-debug2") << std::endl;
1393   }
1394
1395   if( d_status==0 ){
1396     d_status++;
1397     if( !d_typ.isNull() ){
1398       if( s->allowVar( d_typ ) ){
1399         //allocate variable
1400         d_status_num = s->d_var_id[d_typ];
1401         s->addVar( d_typ );
1402         Trace("sg-gen-tg-debug2") << this << " ...return unique var #" << d_status_num << std::endl;
1403         return s->considerCurrentTerm() ? true : getNextTerm( s, depth );
1404       }else{
1405         //check allocating new variable
1406         d_status++;
1407         d_status_num = -1;
1408         if( s->d_gen_relevant_terms ){
1409           s->d_tg_gdepth++;
1410         }
1411         return getNextTerm( s, depth );
1412       }
1413     }else{
1414       d_status = 4;
1415       d_status_num = -1;
1416       return getNextTerm( s, depth );
1417     }
1418   }else if( d_status==2 ){
1419     //cleanup previous information
1420     //if( d_status_num>=0 ){
1421     //  s->d_var_eq_tg[d_status_num].pop_back();
1422     //}
1423     //check if there is another variable
1424     if( (d_status_num+1)<(int)s->getNumTgVars( d_typ ) ){
1425       d_status_num++;
1426       //we have equated two variables
1427       //s->d_var_eq_tg[d_status_num].push_back( d_id );
1428       Trace("sg-gen-tg-debug2") << this << "...consider other var #" << d_status_num << std::endl;
1429       return s->considerCurrentTerm() ? true : getNextTerm( s, depth );
1430     }else{
1431       if( s->d_gen_relevant_terms ){
1432         s->d_tg_gdepth--;
1433       }
1434       d_status++;
1435       return getNextTerm( s, depth );
1436     }
1437   }else if( d_status==4 ){
1438     d_status++;
1439     if( depth>0 && (d_status_num+1)<(int)s->getNumTgFuncs( d_typ ) ){
1440       d_status_num++;
1441       d_status_child_num = 0;
1442       Trace("sg-gen-tg-debug2") << this << "...consider function " << s->getTgFunc( d_typ, d_status_num ) << std::endl;
1443       s->d_tg_gdepth++;
1444       if( !s->considerCurrentTerm() ){
1445         s->d_tg_gdepth--;
1446         //don't consider this function
1447         d_status--;
1448       }else{
1449         //we have decided on a function application
1450       }
1451       return getNextTerm( s, depth );
1452     }else{
1453       //do not choose function applications at depth 0
1454       d_status++;
1455       return getNextTerm( s, depth );
1456     }
1457   }else if( d_status==5 ){
1458     //iterating over arguments
1459     TNode f = s->getTgFunc( d_typ, d_status_num );
1460     if( d_status_child_num<0 ){
1461       //no more arguments
1462       s->d_tg_gdepth--;
1463       d_status--;
1464       return getNextTerm( s, depth );
1465     }else if( d_status_child_num==(int)s->d_func_args[f].size() ){
1466       d_status_child_num--;
1467       return s->considerCurrentTermCanon( d_id ) ? true : getNextTerm( s, depth );
1468       //return true;
1469     }else{
1470       Assert( d_status_child_num<(int)s->d_func_args[f].size() );
1471       if( d_status_child_num==(int)d_children.size() ){
1472         d_children.push_back( s->d_tg_id );
1473         Assert( s->d_tg_alloc.find( s->d_tg_id )==s->d_tg_alloc.end() );
1474         s->d_tg_alloc[d_children[d_status_child_num]].reset( s, s->d_func_args[f][d_status_child_num] );
1475         return getNextTerm( s, depth );
1476       }else{
1477         Assert( d_status_child_num+1==(int)d_children.size() );
1478         if( s->d_tg_alloc[d_children[d_status_child_num]].getNextTerm( s, depth-1 ) ){
1479           d_status_child_num++;
1480           return getNextTerm( s, depth );
1481         }else{
1482           d_children.pop_back();
1483           d_status_child_num--;
1484           return getNextTerm( s, depth );
1485         }
1486       }
1487     }
1488   }else if( d_status==1 || d_status==3 ){
1489     if( d_status==1 ){
1490       s->removeVar( d_typ );
1491       Assert( d_status_num==(int)s->d_var_id[d_typ] );
1492       //check if there is only one feasible equivalence class.  if so, don't make pattern any more specific.
1493       //unsigned i = s->d_ccand_eqc[0].size()-1;
1494       //if( s->d_ccand_eqc[0][i].size()==1 && s->d_ccand_eqc[1][i].empty() ){
1495       //  d_status = 6;
1496       //  return getNextTerm( s, depth );
1497       //}
1498       s->d_tg_gdepth++;
1499     }
1500     d_status++;
1501     d_status_num = -1;
1502     return getNextTerm( s, depth );
1503   }else{
1504     //clean up
1505     Assert( d_children.empty() );
1506     Trace("sg-gen-tg-debug2") << "...remove from context " << this << std::endl;
1507     s->changeContext( false );
1508     Assert( d_id==s->d_tg_id );
1509     return false;
1510   }
1511 }
1512
1513 void TermGenerator::resetMatching( TermGenEnv * s, TNode eqc, unsigned mode ) {
1514   d_match_status = 0;
1515   d_match_status_child_num = 0;
1516   d_match_children.clear();
1517   d_match_children_end.clear();
1518   d_match_mode = mode;
1519   //if this term generalizes, it must generalize a non-ground term
1520   //if( (d_match_mode & ( 1 << 2 ))!=0 && s->isGroundEqc( eqc ) && d_status==5 ){
1521   //  d_match_status = -1;
1522   //}
1523 }
1524
1525 bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs ) {
1526   if( d_match_status<0 ){
1527     return false;
1528   }
1529   if( Trace.isOn("sg-gen-tg-match") ){
1530     Trace("sg-gen-tg-match") << "Matching ";
1531     debugPrint( s, "sg-gen-tg-match", "sg-gen-tg-match" );
1532     Trace("sg-gen-tg-match") << " with eqc e" << s->d_cg->d_em[eqc] << "..." << std::endl;
1533     Trace("sg-gen-tg-match") << "   mstatus = " << d_match_status;
1534     if( d_status==5 ){
1535       TNode f = s->getTgFunc( d_typ, d_status_num );
1536       Trace("sg-gen-tg-debug2") << ", f = " << f;
1537       Trace("sg-gen-tg-debug2") << ", #args = " << s->d_func_args[f].size();
1538       Trace("sg-gen-tg-debug2") << ", mchildNum = " << d_match_status_child_num;
1539       Trace("sg-gen-tg-debug2") << ", #mchildren = " << d_match_children.size();
1540     }
1541     Trace("sg-gen-tg-debug2") << ", current substitution : {";
1542     for( std::map< TypeNode, std::map< unsigned, TNode > >::iterator itt = subs.begin(); itt != subs.end(); ++itt ){
1543       for( std::map< unsigned, TNode >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
1544         Trace("sg-gen-tg-debug2")  << " " << it->first << " -> e" << s->d_cg->d_em[it->second];
1545       }
1546     }
1547     Trace("sg-gen-tg-debug2") << " } " << std::endl;
1548   }
1549   if( d_status==1 ){
1550     //a variable
1551     if( d_match_status==0 ){
1552       d_match_status++;
1553       if( (d_match_mode & ( 1 << 1 ))!=0 ){
1554         //only ground terms
1555         if( !s->isGroundEqc( eqc ) ){
1556           return false;
1557         }
1558       }else if( (d_match_mode & ( 1 << 2 ))!=0 ){
1559         //only non-ground terms
1560         //if( s->isGroundEqc( eqc ) ){
1561         //  return false;
1562         //}
1563       }
1564       //store the match : restricted if match_mode.0 = 1
1565       if( (d_match_mode & ( 1 << 0 ))!=0 ){
1566         std::map< TNode, bool >::iterator it = rev_subs.find( eqc );
1567         if( it==rev_subs.end() ){
1568           rev_subs[eqc] = true;
1569         }else{
1570           return false;
1571         }
1572       }
1573       Assert( subs[d_typ].find( d_status_num )==subs[d_typ].end() );
1574       subs[d_typ][d_status_num] = eqc;
1575       return true;
1576     }else{
1577       //clean up
1578       subs[d_typ].erase( d_status_num );
1579       if( (d_match_mode & ( 1 << 0 ))!=0 ){
1580         rev_subs.erase( eqc );
1581       }
1582       return false;
1583     }
1584   }else if( d_status==2 ){
1585     if( d_match_status==0 ){
1586       d_match_status++;
1587       Assert( d_status_num<(int)s->getNumTgVars( d_typ ) );
1588       std::map< unsigned, TNode >::iterator it = subs[d_typ].find( d_status_num );
1589       Assert( it!=subs[d_typ].end() );
1590       return it->second==eqc;
1591     }else{
1592       return false;
1593     }
1594   }else if( d_status==5 ){
1595     //Assert( d_match_children.size()<=d_children.size() );
1596     //enumerating over f-applications in eqc
1597     if( d_match_status_child_num<0 ){
1598       return false;
1599     }else if( d_match_status==0 ){
1600       //set up next binding
1601       if( d_match_status_child_num==(int)d_match_children.size() ){
1602         if( d_match_status_child_num==0 ){
1603           //initial binding
1604           TNode f = s->getTgFunc( d_typ, d_status_num );
1605           std::map< TNode, TermArgTrie >::iterator it = s->getTermDatabase()->d_func_map_eqc_trie[f].d_data.find( eqc );
1606           if( it!=s->getTermDatabase()->d_func_map_eqc_trie[f].d_data.end() ){
1607             d_match_children.push_back( it->second.d_data.begin() );
1608             d_match_children_end.push_back( it->second.d_data.end() );
1609           }else{
1610             d_match_status++;
1611             d_match_status_child_num--;
1612             return getNextMatch( s, eqc, subs, rev_subs );
1613           }
1614         }else{
1615           d_match_children.push_back( d_match_children[d_match_status_child_num-1]->second.d_data.begin() );
1616           d_match_children_end.push_back( d_match_children[d_match_status_child_num-1]->second.d_data.end() );
1617         }
1618       }
1619       d_match_status++;
1620       Assert( d_match_status_child_num+1==(int)d_match_children.size() );
1621       if( d_match_children[d_match_status_child_num]==d_match_children_end[d_match_status_child_num] ){
1622         //no more arguments to bind
1623         d_match_children.pop_back();
1624         d_match_children_end.pop_back();
1625         d_match_status_child_num--;
1626         return getNextMatch( s, eqc, subs, rev_subs );
1627       }else{
1628         if( d_match_status_child_num==(int)d_children.size() ){
1629           //successfully matched all children
1630           d_match_children.pop_back();
1631           d_match_children_end.pop_back();
1632           d_match_status_child_num--;
1633           return true;//return d_match_children[d_match_status]!=d_match_children_end[d_match_status];
1634         }else{
1635           //do next binding
1636           s->d_tg_alloc[d_children[d_match_status_child_num]].resetMatching( s, d_match_children[d_match_status_child_num]->first, d_match_mode );
1637           return getNextMatch( s, eqc, subs, rev_subs );
1638         }
1639       }
1640     }else{
1641       Assert( d_match_status==1 );
1642       Assert( d_match_status_child_num+1==(int)d_match_children.size() );
1643       Assert( d_match_children[d_match_status_child_num]!=d_match_children_end[d_match_status_child_num] );
1644       d_match_status--;
1645       if( s->d_tg_alloc[d_children[d_match_status_child_num]].getNextMatch( s, d_match_children[d_match_status_child_num]->first, subs, rev_subs ) ){
1646         d_match_status_child_num++;
1647         return getNextMatch( s, eqc, subs, rev_subs );
1648       }else{
1649         //iterate
1650         d_match_children[d_match_status_child_num]++;
1651         return getNextMatch( s, eqc, subs, rev_subs );
1652       }
1653     }
1654   }
1655   Assert( false );
1656   return false;
1657 }
1658
1659 unsigned TermGenerator::getDepth( TermGenEnv * s ) {
1660   if( d_status==5 ){
1661     unsigned maxd = 0;
1662     for( unsigned i=0; i<d_children.size(); i++ ){
1663       unsigned d = s->d_tg_alloc[d_children[i]].getDepth( s );
1664       if( d>maxd ){
1665         maxd = d;
1666       }
1667     }
1668     return 1+maxd;
1669   }else{
1670     return 0;
1671   }
1672 }
1673
1674 unsigned TermGenerator::calculateGeneralizationDepth( TermGenEnv * s, std::map< TypeNode, std::vector< int > >& fvs ) {
1675   if( d_status==5 ){
1676     unsigned sum = 1;
1677     for( unsigned i=0; i<d_children.size(); i++ ){
1678       sum += s->d_tg_alloc[d_children[i]].calculateGeneralizationDepth( s, fvs );
1679     }
1680     return sum;
1681   }else{
1682     Assert( d_status==2 || d_status==1 );
1683     std::map< TypeNode, std::vector< int > >::iterator it = fvs.find( d_typ );
1684     if( it!=fvs.end() ){
1685       if( std::find( it->second.begin(), it->second.end(), d_status_num )!=it->second.end() ){
1686         return 1;
1687       }
1688     }
1689     fvs[d_typ].push_back( d_status_num );
1690     return 0;
1691   }
1692 }
1693
1694 unsigned TermGenerator::getGeneralizationDepth( TermGenEnv * s ) {
1695   //if( s->d_gen_relevant_terms ){
1696   //  return s->d_tg_gdepth;
1697   //}else{
1698     std::map< TypeNode, std::vector< int > > fvs;
1699     return calculateGeneralizationDepth( s, fvs );
1700   //}
1701 }
1702
1703 Node TermGenerator::getTerm( TermGenEnv * s ) {
1704   if( d_status==1 || d_status==2 ){
1705     Assert( !d_typ.isNull() );
1706     return s->getFreeVar( d_typ, d_status_num );
1707   }else if( d_status==5 ){
1708     Node f = s->getTgFunc( d_typ, d_status_num );
1709     if( d_children.size()==s->d_func_args[f].size() ){
1710       std::vector< Node > children;
1711       children.push_back( f );
1712       for( unsigned i=0; i<d_children.size(); i++ ){
1713         Node nc = s->d_tg_alloc[d_children[i]].getTerm( s );
1714         if( nc.isNull() ){
1715           return Node::null();
1716         }else{
1717           //Assert( nc.getType()==s->d_func_args[f][i] );
1718           children.push_back( nc );
1719         }
1720       }
1721       return NodeManager::currentNM()->mkNode( s->d_func_kind[f], children );
1722     }
1723   }else{
1724     Assert( false );
1725   }
1726   return Node::null();
1727 }
1728
1729 void TermGenerator::debugPrint( TermGenEnv * s, const char * c, const char * cd ) {
1730   Trace(cd) << "[*" << d_id << "," << d_status << "]:";
1731   if( d_status==1 || d_status==2 ){
1732     Trace(c) << s->getFreeVar( d_typ, d_status_num );
1733   }else if( d_status==5 ){
1734     TNode f = s->getTgFunc( d_typ, d_status_num );
1735     Trace(c) << "(" << f;
1736     for( unsigned i=0; i<d_children.size(); i++ ){
1737       Trace(c) << " ";
1738        s->d_tg_alloc[d_children[i]].debugPrint( s, c, cd );
1739     }
1740     if( d_children.size()<s->d_func_args[f].size() ){
1741       Trace(c) << " ...";
1742     }
1743     Trace(c) << ")";
1744   }else{
1745     Trace(c) << "???";
1746   }
1747 }
1748
1749 void TermGenEnv::collectSignatureInformation() {
1750   d_typ_tg_funcs.clear();
1751   d_funcs.clear();
1752   d_func_kind.clear();
1753   d_func_args.clear();
1754   TypeNode tnull;
1755   for( std::map< Node, TermArgTrie >::iterator it = getTermDatabase()->d_func_map_trie.begin(); it != getTermDatabase()->d_func_map_trie.end(); ++it ){
1756     if( !getTermDatabase()->d_op_map[it->first].empty() ){
1757       Node nn = getTermDatabase()->d_op_map[it->first][0];
1758       if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){
1759         bool do_enum = true;
1760         //check if we have enumerated ground terms
1761         if( nn.getKind()==APPLY_UF ){
1762           if( !d_cg->hasEnumeratedUf( nn ) ){
1763             do_enum = false;
1764           }
1765         }
1766         if( do_enum ){
1767           d_funcs.push_back( it->first );
1768           for( unsigned i=0; i<nn.getNumChildren(); i++ ){
1769             d_func_args[it->first].push_back( nn[i].getType() );
1770           }
1771           d_func_kind[it->first] = nn.getKind();
1772           d_typ_tg_funcs[tnull].push_back( it->first );
1773           d_typ_tg_funcs[nn.getType()].push_back( it->first );
1774           Trace("sg-rel-sig") << "Will enumerate function applications of : " << it->first << ", #args = " << d_func_args[it->first].size() << ", kind = " << nn.getKind() << std::endl;
1775           getTermDatabase()->computeUfEqcTerms( it->first );
1776         }
1777       }
1778     }
1779   }
1780   //shuffle functions
1781   for( std::map< TypeNode, std::vector< TNode > >::iterator it = d_typ_tg_funcs.begin(); it != d_typ_tg_funcs.end(); ++it ){
1782     std::random_shuffle( it->second.begin(), it->second.end() );
1783     if( it->first.isNull() ){
1784       Trace("sg-gen-tg-debug") << "In this order : ";
1785       for( unsigned i=0; i<it->second.size(); i++ ){
1786         Trace("sg-gen-tg-debug") << it->second[i] << " ";
1787       }
1788       Trace("sg-gen-tg-debug") << std::endl;
1789     }
1790   }
1791 }
1792
1793 void TermGenEnv::reset( unsigned depth, bool genRelevant, TypeNode tn ) {
1794   Assert( d_tg_alloc.empty() );
1795   d_tg_alloc.clear();
1796
1797   if( genRelevant ){
1798     for( unsigned i=0; i<2; i++ ){
1799       d_ccand_eqc[i].clear();
1800       d_ccand_eqc[i].push_back( d_relevant_eqc[i] );
1801     }
1802   }
1803
1804   d_tg_id = 0;
1805   d_tg_gdepth = 0;
1806   d_tg_gdepth_limit = depth;
1807   d_gen_relevant_terms = genRelevant;
1808   d_tg_alloc[0].reset( this, tn );
1809 }
1810
1811 bool TermGenEnv::getNextTerm() {
1812   if( d_tg_alloc[0].getNextTerm( this, d_tg_gdepth_limit ) ){
1813     Assert( (int)d_tg_alloc[0].getGeneralizationDepth( this )<=d_tg_gdepth_limit );
1814     if( (int)d_tg_alloc[0].getGeneralizationDepth( this )!=d_tg_gdepth_limit ){
1815       return getNextTerm();
1816     }else{
1817       return true;
1818     }
1819   }else{
1820     return false;
1821   }
1822 }
1823
1824 //reset matching
1825 void TermGenEnv::resetMatching( TNode eqc, unsigned mode ) {
1826   d_tg_alloc[0].resetMatching( this, eqc, mode );
1827 }
1828
1829 //get next match
1830 bool TermGenEnv::getNextMatch( TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs ) {
1831   return d_tg_alloc[0].getNextMatch( this, eqc, subs, rev_subs );
1832 }
1833
1834 //get term
1835 Node TermGenEnv::getTerm() {
1836   return d_tg_alloc[0].getTerm( this );
1837 }
1838
1839 void TermGenEnv::debugPrint( const char * c, const char * cd ) {
1840   d_tg_alloc[0].debugPrint( this, c, cd );
1841 }
1842
1843 unsigned TermGenEnv::getNumTgVars( TypeNode tn ) {
1844   return d_var_id[tn];
1845 }
1846
1847 bool TermGenEnv::allowVar( TypeNode tn ) {
1848   std::map< TypeNode, unsigned >::iterator it = d_var_limit.find( tn );
1849   if( it==d_var_limit.end() ){
1850     return true;
1851   }else{
1852     return d_var_id[tn]<it->second;
1853   }
1854 }
1855
1856 void TermGenEnv::addVar( TypeNode tn ) {
1857   d_var_id[tn]++;
1858 }
1859
1860 void TermGenEnv::removeVar( TypeNode tn ) {
1861   d_var_id[tn]--;
1862   //d_var_eq_tg.pop_back();
1863   //d_var_tg.pop_back();
1864 }
1865
1866 unsigned TermGenEnv::getNumTgFuncs( TypeNode tn ) {
1867   return d_typ_tg_funcs[tn].size();
1868 }
1869
1870 TNode TermGenEnv::getTgFunc( TypeNode tn, unsigned i ) {
1871   return d_typ_tg_funcs[tn][i];
1872 }
1873
1874 Node TermGenEnv::getFreeVar( TypeNode tn, unsigned i ) {
1875   return d_cg->getFreeVar( tn, i );
1876 }
1877
1878 bool TermGenEnv::considerCurrentTerm() {
1879   Assert( !d_tg_alloc.empty() );
1880
1881   //if generalization depth is too large, don't consider it
1882   unsigned i = d_tg_alloc.size();
1883   Trace("sg-gen-tg-debug") << "Consider term ";
1884   d_tg_alloc[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );
1885   Trace("sg-gen-tg-debug") << "?  curr term size = " << d_tg_alloc.size() << ", last status = " << d_tg_alloc[i-1].d_status;
1886   Trace("sg-gen-tg-debug") << std::endl;
1887
1888   if( d_tg_gdepth_limit>=0 && d_tg_alloc[0].getGeneralizationDepth( this )>(unsigned)d_tg_gdepth_limit ){
1889     Trace("sg-gen-consider-term") << "-> generalization depth of ";
1890     d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-tg-debug" );
1891     Trace("sg-gen-consider-term") << " is too high " << d_tg_gdepth << " " << d_tg_alloc[0].getGeneralizationDepth( this ) << ", do not consider." << std::endl;
1892     return false;
1893   }
1894
1895   //----optimizations
1896   /*
1897   if( d_tg_alloc[i-1].d_status==1 ){
1898   }else if( d_tg_alloc[i-1].d_status==2 ){
1899   }else if( d_tg_alloc[i-1].d_status==5 ){
1900   }else{
1901     Trace("sg-gen-tg-debug") << "Bad tg: " << &d_tg_alloc[i-1] << std::endl;
1902     Assert( false );
1903   }
1904   */
1905   //if equated two variables, first check if context-independent TODO
1906   //----end optimizations
1907
1908
1909   //check based on which candidate equivalence classes match
1910   if( d_gen_relevant_terms ){
1911     Trace("sg-gen-tg-debug") << "Filter based on relevant ground EQC";
1912     Trace("sg-gen-tg-debug") << ", #eqc to try = " << d_ccand_eqc[0][i-1].size() << "/" << d_ccand_eqc[1][i-1].size() << std::endl;
1913
1914     Assert( d_ccand_eqc[0].size()>=2 );
1915     Assert( d_ccand_eqc[0].size()==d_ccand_eqc[1].size() );
1916     Assert( d_ccand_eqc[0].size()==d_tg_id+1 );
1917     Assert( d_tg_id==d_tg_alloc.size() );
1918     for( unsigned r=0; r<2; r++ ){
1919       d_ccand_eqc[r][i].clear();
1920     }
1921
1922     //re-check feasibility of EQC
1923     for( unsigned r=0; r<2; r++ ){
1924       for( unsigned j=0; j<d_ccand_eqc[r][i-1].size(); j++ ){
1925         std::map< TypeNode, std::map< unsigned, TNode > > subs;
1926         std::map< TNode, bool > rev_subs;
1927         unsigned mode;
1928         if( r==0 ){
1929           mode = d_cg->optReqDistinctVarPatterns() ? ( 1 << 0 ) : 0;
1930           mode = mode | (1 << 2 );
1931         }else{
1932           mode =  1 << 1;
1933         }
1934         d_tg_alloc[0].resetMatching( this, d_ccand_eqc[r][i-1][j], mode );
1935         if( d_tg_alloc[0].getNextMatch( this, d_ccand_eqc[r][i-1][j], subs, rev_subs ) ){
1936           d_ccand_eqc[r][i].push_back( d_ccand_eqc[r][i-1][j] );
1937         }
1938       }
1939     }
1940     for( unsigned r=0; r<2; r++ ){
1941       Trace("sg-gen-tg-debug") << "Current eqc of type " << r << " : ";
1942       for( unsigned j=0; j<d_ccand_eqc[r][i].size(); j++ ){
1943         Trace("sg-gen-tg-debug") << "e" << d_cg->d_em[d_ccand_eqc[r][i][j]] << " ";
1944       }
1945       Trace("sg-gen-tg-debug") << std::endl;
1946     }
1947     if( options::conjectureFilterActiveTerms() && d_ccand_eqc[0][i].empty() ){
1948       Trace("sg-gen-consider-term") << "Do not consider term of form ";
1949       d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" );
1950       Trace("sg-gen-consider-term") << " since no relevant EQC matches it." << std::endl;
1951       return false;
1952     }
1953     if( options::conjectureFilterModel() && d_ccand_eqc[1][i].empty() ){
1954       Trace("sg-gen-consider-term") << "Do not consider term of form ";
1955       d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" );
1956       Trace("sg-gen-consider-term") << " since no ground EQC matches it." << std::endl;
1957       return false;
1958     }
1959   }
1960   Trace("sg-gen-tg-debug") << "Will consider term ";
1961   d_tg_alloc[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );
1962   Trace("sg-gen-tg-debug") << std::endl;
1963   Trace("sg-gen-consider-term-debug") << std::endl;
1964   return true;
1965 }
1966
1967 void TermGenEnv::changeContext( bool add ) {
1968   if( add ){
1969     for( unsigned r=0; r<2; r++ ){
1970       d_ccand_eqc[r].push_back( std::vector< TNode >() );
1971     }
1972     d_tg_id++;
1973   }else{
1974     for( unsigned r=0; r<2; r++ ){
1975       d_ccand_eqc[r].pop_back();
1976     }
1977     d_tg_id--;
1978     Assert( d_tg_alloc.find( d_tg_id )!=d_tg_alloc.end() );
1979     d_tg_alloc.erase( d_tg_id );
1980   }
1981 }
1982
1983 bool TermGenEnv::considerCurrentTermCanon( unsigned tg_id ){
1984   Assert( tg_id<d_tg_alloc.size() );
1985   if( options::conjectureFilterCanonical() ){
1986     //check based on a canonicity of the term (if there is one)
1987     Trace("sg-gen-tg-debug") << "Consider term canon ";
1988     d_tg_alloc[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );
1989     Trace("sg-gen-tg-debug") << ", tg is [" << tg_id << "]..." << std::endl;
1990
1991     Node ln = d_tg_alloc[tg_id].getTerm( this );
1992     Trace("sg-gen-tg-debug") << "Term is " << ln << std::endl;
1993     return d_cg->considerTermCanon( ln, d_gen_relevant_terms );
1994   }
1995   return true;
1996 }
1997
1998 bool TermGenEnv::isRelevantFunc( Node f ) {
1999   return std::find( d_funcs.begin(), d_funcs.end(), f )!=d_funcs.end();
2000 }
2001 TermDb * TermGenEnv::getTermDatabase() {
2002   return d_cg->getTermDatabase();
2003 }
2004 Node TermGenEnv::getGroundEqc( TNode r ) {
2005   return d_cg->getGroundEqc( r );
2006 }
2007 bool TermGenEnv::isGroundEqc( TNode r ){
2008   return d_cg->isGroundEqc( r );
2009 }
2010 bool TermGenEnv::isGroundTerm( TNode n ){
2011   return d_cg->isGroundTerm( n );
2012 }
2013
2014
2015 void SubstitutionIndex::addSubstitution( TNode eqc, std::vector< TNode >& vars, std::vector< TNode >& terms, unsigned i ) {
2016   if( i==vars.size() ){
2017     d_var = eqc;
2018   }else{
2019     Assert( d_var.isNull() || d_var==vars[i] );
2020     d_var = vars[i];
2021     d_children[terms[i]].addSubstitution( eqc, vars, terms, i+1 );
2022   }
2023 }
2024
2025 bool SubstitutionIndex::notifySubstitutions( ConjectureGenerator * s, std::map< TNode, TNode >& subs, TNode rhs, unsigned numVars, unsigned i ) {
2026   if( i==numVars ){
2027     Assert( d_children.empty() );
2028     return s->notifySubstitution( d_var, subs, rhs );
2029   }else{
2030     Assert( i==0 || !d_children.empty() );
2031     for( std::map< TNode, SubstitutionIndex >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
2032       Trace("sg-cconj-debug2") << "Try " << d_var << " -> " << it->first << " (" << i << "/" << numVars << ")" << std::endl;
2033       subs[d_var] = it->first;
2034       if( !it->second.notifySubstitutions( s, subs, rhs, numVars, i+1 ) ){
2035         return false;
2036       }
2037     }
2038     return true;
2039   }
2040 }
2041
2042
2043 void TheoremIndex::addTheorem( std::vector< TNode >& lhs_v, std::vector< unsigned >& lhs_arg, TNode rhs ){
2044   if( lhs_v.empty() ){
2045     if( std::find( d_terms.begin(), d_terms.end(), rhs )==d_terms.end() ){
2046       d_terms.push_back( rhs );
2047     }
2048   }else{
2049     unsigned index = lhs_v.size()-1;
2050     if( lhs_arg[index]==lhs_v[index].getNumChildren() ){
2051       lhs_v.pop_back();
2052       lhs_arg.pop_back();
2053       addTheorem( lhs_v, lhs_arg, rhs );
2054     }else{
2055       lhs_arg[index]++;
2056       addTheoremNode( lhs_v[index][lhs_arg[index]-1], lhs_v, lhs_arg, rhs );
2057     }
2058   }
2059 }
2060
2061 void TheoremIndex::addTheoremNode( TNode curr, std::vector< TNode >& lhs_v, std::vector< unsigned >& lhs_arg, TNode rhs ){
2062   Trace("thm-db-debug") << "Adding conjecture for subterm " << curr << "..." << std::endl;
2063   if( curr.hasOperator() ){
2064     lhs_v.push_back( curr );
2065     lhs_arg.push_back( 0 );
2066     d_children[curr.getOperator()].addTheorem( lhs_v, lhs_arg, rhs );
2067   }else{
2068     Assert( curr.getKind()==kind::BOUND_VARIABLE );
2069     TypeNode tn = curr.getType();
2070     Assert( d_var[tn].isNull() || d_var[tn]==curr );
2071     d_var[tn] = curr;
2072     d_children[curr].addTheorem( lhs_v, lhs_arg, rhs );
2073   }
2074 }
2075
2076 void TheoremIndex::getEquivalentTerms( std::vector< TNode >& n_v, std::vector< unsigned >& n_arg,
2077                                        std::map< TNode, TNode >& smap, std::vector< TNode >& vars, std::vector< TNode >& subs,
2078                                        std::vector< Node >& terms ) {
2079   Trace("thm-db-debug") << "Get equivalent terms " << n_v.size() << " " << n_arg.size() << std::endl;
2080   if( n_v.empty() ){
2081     Trace("thm-db-debug") << "Number of terms : " << d_terms.size() << std::endl;
2082     //apply substutitions to RHS's
2083     for( unsigned i=0; i<d_terms.size(); i++ ){
2084       Node n = d_terms[i].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
2085       terms.push_back( n );
2086     }
2087   }else{
2088     unsigned index = n_v.size()-1;
2089     if( n_arg[index]==n_v[index].getNumChildren() ){
2090       n_v.pop_back();
2091       n_arg.pop_back();
2092       getEquivalentTerms( n_v, n_arg, smap, vars, subs, terms );
2093     }else{
2094       n_arg[index]++;
2095       getEquivalentTermsNode( n_v[index][n_arg[index]-1], n_v, n_arg, smap, vars, subs, terms );
2096     }
2097   }
2098 }
2099
2100 void TheoremIndex::getEquivalentTermsNode( Node curr, std::vector< TNode >& n_v, std::vector< unsigned >& n_arg,
2101                                            std::map< TNode, TNode >& smap, std::vector< TNode >& vars, std::vector< TNode >& subs,
2102                                            std::vector< Node >& terms ) {
2103   Trace("thm-db-debug") << "Get equivalent based on subterm " << curr << "..." << std::endl;
2104   if( curr.hasOperator() ){
2105     Trace("thm-db-debug") << "Check based on operator..." << std::endl;
2106     std::map< TNode, TheoremIndex >::iterator it = d_children.find( curr.getOperator() );
2107     if( it!=d_children.end() ){
2108       n_v.push_back( curr );
2109       n_arg.push_back( 0 );
2110       it->second.getEquivalentTerms( n_v, n_arg, smap, vars, subs, terms );
2111     }
2112     Trace("thm-db-debug") << "...done check based on operator" << std::endl;
2113   }
2114   TypeNode tn = curr.getType();
2115   std::map< TypeNode, TNode >::iterator itt = d_var.find( tn );
2116   if( itt!=d_var.end() ){
2117     Trace("thm-db-debug") << "Check for substitution with " << itt->second << "..." << std::endl;
2118     Assert( curr.getType()==itt->second.getType() );
2119     //add to substitution if possible
2120     bool success = false;
2121     std::map< TNode, TNode >::iterator it = smap.find( itt->second );
2122     if( it==smap.end() ){
2123       smap[itt->second] = curr;
2124       vars.push_back( itt->second );
2125       subs.push_back( curr );
2126       success = true;
2127     }else if( it->second==curr ){
2128       success = true;
2129     }else{
2130       //also check modulo equality (in universal equality engine)
2131     }
2132     Trace("thm-db-debug") << "...check for substitution with " << itt->second << ", success = " << success << "." << std::endl;
2133     if( success ){
2134       d_children[itt->second].getEquivalentTerms( n_v, n_arg, smap, vars, subs, terms );
2135     }
2136   }
2137 }
2138
2139 void TheoremIndex::debugPrint( const char * c, unsigned ind ) {
2140   for( std::map< TNode, TheoremIndex >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
2141     for( unsigned i=0; i<ind; i++ ){ Trace(c) << "  "; }
2142     Trace(c) << it->first << std::endl;
2143     it->second.debugPrint( c, ind+1 );
2144   }
2145   if( !d_terms.empty() ){
2146     for( unsigned i=0; i<ind; i++ ){ Trace(c) << "  "; }
2147     Trace(c) << "{";
2148     for( unsigned i=0; i<d_terms.size(); i++ ){
2149       Trace(c) << " " << d_terms[i];
2150     }
2151     Trace(c) << " }" << std::endl;
2152   }
2153   //if( !d_var.isNull() ){
2154   //  for( unsigned i=0; i<ind; i++ ){ Trace(c) << "  "; }
2155   //  Trace(c) << "var:" << d_var << std::endl;
2156   //}
2157 }
2158
2159 bool ConjectureGenerator::optReqDistinctVarPatterns() { return false; }
2160 bool ConjectureGenerator::optFilterUnknown() { return true; }  //may change
2161 int ConjectureGenerator::optFilterScoreThreshold() { return 1; }
2162 unsigned ConjectureGenerator::optFullCheckFrequency() { return 1; }
2163
2164 bool ConjectureGenerator::optStatsOnly() { return false; }
2165
2166 }