Inferno  0.2
conjecture.cpp
Go to the documentation of this file.
00001 
00002 #include "search_replace.hpp"
00003 #include "conjecture.hpp"
00004 
00005 Conjecture::Conjecture()
00006 {
00007     failed = false;
00008 }
00009 
00010 Conjecture::~Conjecture()
00011 {
00012     if( !it_names.empty() )
00013     {
00014         TRACE("Conjecture dump step %d; start counts: ", HitCount::instance.GetStep());
00015         for( int i=0; i<it_names.size(); i++ )
00016             TRACE("%d ", start_counts[i]);
00017         TRACE("; inc counts: ", this);
00018         for( int i=0; i<it_names.size(); i++ )
00019             TRACE("%d ", inc_counts[i]);
00020         TRACE("; iterators: ");
00021         for( int i=0; i<it_names.size(); i++ )
00022         {
00023             string s = it_names[i];
00024             for( int i=0; i<s.size(); i++ )
00025                 if( s[i] == '<' )
00026                     break;
00027                 else 
00028                     TRACE("%c", s[i]);
00029             TRACE(" ");
00030         }
00031         TRACE("; %s\n", failed?"FAILED":"SUCCEEDED");
00032     }
00033 }
00034 
00035 void Conjecture::PrepareForDecidedCompare()
00036 {
00037   ASSERT( this );
00038 
00039   TRACE("Decision prepare\n");
00040   decision_index = 0;
00041 }
00042 
00043 
00044 bool Conjecture::Increment()
00045 {   
00046   // If we've run out of choices, we're done.
00047   if( choices.empty() )
00048   {
00049       failed = true;
00050         TRACE("Giving up\n");
00051       return false;
00052   }
00053   else if( choices.back().it != choices.back().end )
00054   {
00055       ResizeCounts();
00056         inc_counts[choices.size()-1]++;
00057 
00058     TRACE("Incrementing choice FROM ")(**choices.back().it)("\n");
00059     ++(choices.back().it); // There are potentially more choices so increment the last decision
00060     }
00061     
00062     if( choices.back().it == choices.back().end )
00063     {
00064         TRACE("Incrementing end count FROM %d\n", choices.back().end_count);
00065         ++choices.back().end_count;
00066         if( choices.back().end_count > choices.back().end_num )
00067         {
00068             choices.resize( choices.size()-1 );
00069             return Increment();  // TODO use a loop?
00070         }
00071     }
00072             
00073     return true;
00074 }
00075 
00076 
00077 ContainerInterface::iterator Conjecture::HandleDecision( ContainerInterface::iterator begin,
00078                                                      ContainerInterface::iterator end,
00079                                                      int en )
00080 {
00081   ASSERT( this );
00082   ASSERT( choices.size() >= decision_index ); // consistency check; as we see more decisions, we should be adding them to the conjecture
00083   Choice c;
00084 
00085   // See if this decision needs to be added to the present Conjecture
00086   if( choices.size() == decision_index ) // this decision missing from conjecture?
00087   {
00088     c.it = begin; // Choose the first option supplied
00089     c.end = end; // Choose the first option supplied
00090     c.end_count = 0;
00091     c.end_num = en;
00092     c.forced = false;
00093     choices.push_back( c ); // append this decision so we will iterate it later
00094         
00095         ResizeCounts();
00096         start_counts[choices.size()-1]++;
00097         TRACE("Decision %d appending begin at %p\n", decision_index, GetChoicePtr() );
00098   }
00099   else // already know about this decision
00100   {
00101     // Adopt the current decision based on Conjecture
00102       c = choices[decision_index]; // Get present decision
00103   }
00104     
00105     decision_index++;
00106     
00107   // Return whatever choice we made
00108     return c.it;
00109 }
00110 
00111 
00112 ContainerInterface::iterator Conjecture::HandleDecision( ContainerInterface::iterator only )
00113 {
00114     ContainerInterface::iterator end = only;
00115     ++end;
00116     return HandleDecision( only, end );
00117 }
00118 
00119 
00120 void Conjecture::ResizeCounts()
00121 {
00122     while( choices.size() > it_names.size() )
00123     {
00124         start_counts.resize( start_counts.size()+1 );
00125         inc_counts.resize( inc_counts.size()+1 );
00126         it_names.resize( it_names.size()+1 );         
00127         it_names[it_names.size()-1] = (string)(choices[it_names.size()-1].it);
00128         start_counts[start_counts.size()-1] = 0;
00129         inc_counts[inc_counts.size()-1] = 0;
00130     }
00131 }
00132