CVC3

LFSCUtilProof.h

Go to the documentation of this file.
00001 #ifndef LFSC_UTIL_PROOF_H_
00002 #define LFSC_UTIL_PROOF_H_
00003 
00004 #include "LFSCProof.h"
00005 
00006 class LFSCProofExpr : public LFSCProof
00007 {
00008   bool isHole;
00009   Expr d_e;
00010   LFSCProofExpr( const Expr& e, bool isH = false  );
00011   void initialize();
00012   virtual ~LFSCProofExpr(){}
00013   long int get_length() { return 10; }
00014 public:
00015   virtual LFSCProofExpr* AsLFSCProofExpr(){ return this; }
00016   void print_pf( std::ostream& s, int ind );
00017   static LFSCProof* Make( const Expr& e, bool isH = false ) { return new LFSCProofExpr( e, isH ); }
00018   LFSCProof* clone() { return new LFSCProofExpr( d_e, isHole ); }
00019 
00020   void fillHoles() { isHole = false; }
00021 };
00022 
00023 class LFSCPfVar : public LFSCProof {
00024 private:
00025   static std::map< int, RefPtr< LFSCProof > > vMap;
00026   string name;
00027   LFSCPfVar( string nm ) : LFSCProof(), name( nm ){}
00028   virtual ~LFSCPfVar(){}
00029   long int get_length() { return name.length(); }
00030 public:
00031   virtual LFSCPfVar* AsLFSCPfVar(){ return this; }
00032   void print_pf( std::ostream& s, int ind = 0 ){ s << name; }
00033   void print_struct( std::ostream& s, int ind = 0 ){ s << name; }
00034   static LFSCProof* Make( const char* c, int v );
00035   static LFSCProof* MakeV( int v );
00036   LFSCProof* clone() { return new LFSCPfVar( name ); }
00037 };
00038 
00039 class LFSCPfLambda : public LFSCProof {
00040 private:
00041   RefPtr< LFSCPfVar > pfV;
00042   RefPtr< LFSCProof > body;
00043   //just a placeholder.  This is what the lambda abstracts.
00044   RefPtr< LFSCProof > abstVal;
00045   //constructor
00046   LFSCPfLambda( LFSCPfVar* v, LFSCProof* bd, LFSCProof* aVal = NULL ) : LFSCProof(),
00047     pfV( v ), body( bd ), abstVal( aVal ){}
00048   virtual ~LFSCPfLambda(){}
00049   long int get_length() { return 5 + pfV->get_string_length() + body->get_string_length(); }
00050 public:
00051   virtual LFSCPfLambda* AsLFSCPfLambda(){ return this; }
00052   void print_pf( std::ostream& s, int ind = 0 );
00053   static LFSCProof* Make( LFSCPfVar* v, LFSCProof* bd, LFSCProof* aVal = NULL ){
00054     return new LFSCPfLambda( v, bd, aVal );
00055   }
00056   LFSCProof* clone() { return new LFSCPfLambda( pfV.get(), body.get(), abstVal.get() ); }
00057   int getNumChildren() { return 2; }
00058   LFSCProof* getChild( int n ) { return (n==0) ? (LFSCProof*)pfV.get() : body.get(); }
00059 };
00060 //
00061 class LFSCProofGeneric : public LFSCProof{
00062 private:
00063   vector< RefPtr< LFSCProof > > d_pf;
00064   vector< string > d_str;
00065   bool debug_str;
00066   //Proof in the form "S1.print(P1).S2.print(P2).....print(Pn).S{n+1}"
00067   LFSCProofGeneric( vector< RefPtr< LFSCProof > >& d_pfs, vector< string >& d_strs, bool db_str = false ) : LFSCProof(){
00068     for( int a=0; a<(int)d_pfs.size(); a++ )
00069       d_pf.push_back( d_pfs[a].get() );
00070     for( int a=0; a<(int)d_strs.size(); a++ )
00071       d_str.push_back( d_strs[a] );
00072     debug_str = db_str;
00073   }
00074   virtual ~LFSCProofGeneric(){}
00075   long int get_length();
00076 public:
00077   virtual LFSCProofGeneric* AsLFSCProofGeneric(){ return this; }
00078   void print_pf( std::ostream& s, int ind = 0 );
00079   //Proof in the form "S1.print(P1).S2.print(P2).....print(Pn).S{n+1}"
00080   static LFSCProof* Make( vector< RefPtr< LFSCProof > >& d_pfs, std::vector< string >& d_strs, bool db_str = false ){
00081     return new LFSCProofGeneric( d_pfs, d_strs, db_str );
00082   }
00083   //proof printed in the form "S1.print(P1).S2"
00084   static LFSCProof* Make( string str_pre, LFSCProof* sub_pf, string str_post, bool db_str = false );
00085   //proof printed in the form "S1.print(P1).print(P2).S2"
00086   static LFSCProof* Make( string str_pre, LFSCProof* sub_pf1, LFSCProof* sub_pf2, string str_post, bool db_str = false );
00087   static LFSCProof* MakeStr( const char* c, bool db_str = false );
00088   static LFSCProof* MakeUnk(){ return MakeStr( "unk" ); }
00089   LFSCProof* clone(){ return new LFSCProofGeneric( d_pf, d_str, debug_str ); }
00090   int getNumChildren() { return (int)d_pf.size(); }
00091   LFSCProof* getChild( int n ) { return d_pf[n].get(); }
00092 };
00093 
00094 
00095 class LFSCPfLet : public LFSCProof{
00096 private:
00097   RefPtr< LFSCProof > d_letPf;
00098   RefPtr< LFSCPfVar > d_pv;
00099   RefPtr< LFSCProof > d_body;
00100   //this should be equal to d_letPf, although it could be something else based on fv
00101   RefPtr< LFSCProof > d_letPfRpl;
00102   //this by default is d_pv, although it could be something else based on fv
00103   RefPtr< LFSCProof > d_pvRpl;
00104   bool d_isTh;
00105   LFSCPfLet( LFSCProof* letPf, LFSCPfVar* pv, LFSCProof* body,
00106              bool isTh, LFSCProof* letPfRpl, LFSCProof* pvRpl ) : LFSCProof(),
00107     d_letPf( letPf ),d_pv( pv ),d_body( body ),d_letPfRpl( letPfRpl ),d_pvRpl( pvRpl ),d_isTh( isTh ){}
00108   LFSCPfLet( LFSCProof* letPf, LFSCPfVar* pv, LFSCProof* body,
00109              bool isTh, std::vector< int >& fv );
00110   virtual ~LFSCPfLet(){}
00111   long int get_length() {
00112     return 10 + d_letPf->get_string_length() + d_pv->get_string_length() + d_body->get_string_length();
00113   }
00114 public:
00115   virtual LFSCPfLet* AsLFSCPfLet(){ return this; }
00116   void print_pf( std::ostream& s, int ind = 0 );
00117   void print_struct( std::ostream& s, int ind = 0 );
00118   static LFSCProof* Make( LFSCProof* letPf, LFSCPfVar* pv, LFSCProof* body,
00119                           bool isTh, std::vector< int >& fv ){
00120     return new LFSCPfLet( letPf, pv, body, isTh, fv );
00121   }
00122   LFSCProof* clone() { return new LFSCPfLet( d_letPf.get(), d_pv.get(), d_body.get(),
00123                                              d_isTh, d_letPfRpl.get(), d_pvRpl.get() ); }
00124   //should not be part of the children structure.
00125 };
00126 
00127 
00128 #endif