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