CVC3

LFSCUtilProof.cpp

Go to the documentation of this file.
00001 #include "LFSCUtilProof.h"
00002 
00003 #include "LFSCPrinter.h"
00004 
00005 //LFSCProofExpr ...
00006 
00007 void LFSCProofExpr::initialize(){
00008   printer->set_print_expr( d_e );
00009 }
00010 
00011 void LFSCProofExpr::print_pf( std::ostream& s, int ind ){
00012   if( isHole )
00013     s << "_";
00014   else{
00015     //HACK (forces unary minus to be printed properly)
00016     //bool prev_cvc3_mimic = cvc3_mimic;
00017     //cvc3_mimic = true;
00018     printer->print_expr( d_e, s );
00019     //cvc3_mimic = prev_cvc3_mimic;
00020   }
00021 }
00022 
00023 LFSCProofExpr::LFSCProofExpr( const Expr& e, bool isH ){
00024   d_e = cascade_expr( e );
00025   initialize();
00026   isHole = isH;
00027 }
00028 
00029 //LFSCPfVar ...
00030 
00031 std::map< int, RefPtr< LFSCProof > > LFSCPfVar::vMap;
00032 
00033 LFSCProof* LFSCPfVar::Make( const char* c, int v )
00034 {
00035   ostringstream os;
00036   os << c << v;
00037   return new LFSCPfVar( os.str() );
00038 }
00039 
00040 LFSCProof* LFSCPfVar::MakeV( int v )
00041 {
00042   RefPtr< LFSCProof > pf = vMap[v];
00043   if( !pf.get() ){
00044     pf = Make( "@v", v );
00045     vMap[v] = pf.get();
00046   }
00047   return pf.get();
00048 }
00049 
00050 //LFSCPfLambda ...
00051 
00052 void LFSCPfLambda::print_pf( std::ostream& s, int ind )
00053 {
00054   if( abstVal.get() ){
00055     lambdaPrintMap[abstVal.get()] = pfV.get();
00056   }
00057   s << "(\\ ";
00058   pfV->print( s );
00059   //s << " _ (: bottom ";
00060   s << " ";
00061   body->print( s );
00062   s << ")";
00063   if( abstVal.get() ){
00064     lambdaPrintMap[abstVal.get()] = NULL;
00065   }
00066 }
00067 
00068 //LFSCProofGeneric ...
00069 
00070 long int LFSCProofGeneric::get_length(){
00071   long int sum = 0;
00072   for( int a=0; a<(int)d_str.size(); a++ ){
00073     if( !debug_str )
00074       sum += d_str[a].length();     
00075     if( a<(int)d_pf.size() )
00076       sum += d_pf[a]->get_string_length();
00077   }
00078   return sum;
00079 }
00080 
00081 void LFSCProofGeneric::print_pf( std::ostream& s, int ind ){
00082   for( int a=0; a<(int)d_str.size(); a++ ){
00083     s << d_str[a];
00084     if( a<(int)d_pf.size() ){
00085       d_pf[a]->print( s, d_pf.size()<3 ? ind+1 : 0 );
00086     }
00087   }
00088 }
00089 
00090 LFSCProof* LFSCProofGeneric::Make( string str_pre, LFSCProof* sub_pf, string str_post, bool db_str )
00091 {
00092   vector< RefPtr< LFSCProof > > d_pfs;
00093   d_pfs.push_back( sub_pf );
00094   vector< string > d_strs;
00095   d_strs.push_back( str_pre );
00096   d_strs.push_back( str_post );
00097   return new LFSCProofGeneric( d_pfs, d_strs, db_str );
00098 }
00099 
00100 LFSCProof* LFSCProofGeneric::Make( string str_pre, LFSCProof* sub_pf1, LFSCProof* sub_pf2, string str_post, bool db_str )
00101 {
00102   vector< RefPtr< LFSCProof > > d_pfs;
00103   d_pfs.push_back( sub_pf1 );
00104   d_pfs.push_back( sub_pf2 );
00105   vector< string > d_strs;
00106   string str_empty(" ");
00107   d_strs.push_back( str_pre );
00108   d_strs.push_back( str_empty );
00109   d_strs.push_back( str_post );
00110   return new LFSCProofGeneric( d_pfs, d_strs, db_str );
00111 }
00112 
00113 LFSCProof* LFSCProofGeneric::MakeStr( const char* c, bool db_str)
00114 {
00115   vector< RefPtr< LFSCProof > > d_pfs;
00116   vector< string > d_strs;
00117   string str( c );
00118   d_strs.push_back( str );
00119   return new LFSCProofGeneric( d_pfs, d_strs, db_str );
00120 }
00121 
00122 //LFSCPfLet
00123 
00124 LFSCPfLet::LFSCPfLet( LFSCProof* letPf, LFSCPfVar* pv, LFSCProof* body,
00125                       bool isTh, std::vector< int >& fv ) : LFSCProof(), d_letPf( letPf ),
00126                                                             d_pv( pv ),d_body( body ),d_isTh( isTh ){
00127   d_letPfRpl = letPf;
00128   d_pvRpl = pv;
00129 #ifndef IGNORE_LETPF_VARS
00130   //modify letPf and rpl based on fv
00131   for(int a=0; a<(int)fv.size(); a++ ){
00132     ostringstream os1, os2;
00133     //if( d_isTh ){
00134       os1 << "(impl_intro _ _ ";
00135       os2 << ")";
00136     //}else{
00137     //}
00138     RefPtr< LFSCProof > pv1 = LFSCPfVar::Make( "@@v", abs( fv[a] ) );
00139     RefPtr< LFSCProof > pv2 = LFSCPfVar::MakeV( abs( fv[a] ) );
00140     d_letPfRpl = LFSCPfLambda::Make( (LFSCPfVar*)pv1.get(), d_letPfRpl.get(), pv2.get() );
00141     d_letPfRpl = LFSCProofGeneric::Make( os1.str(), d_letPfRpl.get(), os2.str() );
00142   }
00143   for( int a=(int)fv.size()-1; a>=0; a-- ){
00144     ostringstream os1, os2;
00145     os1 << "(impl_elim _ _ ";
00146     os2 << ")";
00147     RefPtr< LFSCProof > pv2 = LFSCPfVar::MakeV( abs( fv[a] ) );
00148     d_pvRpl = LFSCProofGeneric::Make( os1.str(), pv2.get(), d_pvRpl.get(), os2.str() );
00149   }
00150 #endif
00151 }
00152 
00153 void LFSCPfLet::print_pf( std::ostream& s, int ind ){
00154   //fill holes if this proof is already abstracted
00155   if( d_pvRpl.get()!=d_pv.get() ){
00156     d_letPfRpl->fillHoles();
00157   }
00158   s << "(" << (d_isTh ? "th_let_pf _ " : "satlem _ _ _ " );
00159   d_letPfRpl->print( s );
00160   s << "(\\ ";
00161   d_pv->print( s );
00162   s << " " << endl;
00163   lambdaPrintMap[d_letPf.get()]=d_pvRpl.get();
00164   d_body->print( s, ind );
00165   lambdaPrintMap[d_letPf.get()]=NULL;
00166   s << "))";
00167 }
00168 
00169 void LFSCPfLet::print_struct( std::ostream& s, int ind ){
00170   s << "(satlem ";
00171   d_letPf->print_structure( s, ind+1 );
00172   s << "(\\ ";
00173   d_pv->print_structure( s );
00174   s << " ";
00175   lambdaPrintMap[d_letPf.get()]=d_pv.get();
00176   d_body->print_structure( s, ind+1 );
00177   lambdaPrintMap[d_letPf.get()]=NULL;
00178   s << ")";
00179 }