src/theory/quantifiers/conjecture_generator.cpp

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