1 #ifndef LFSC_UTIL_PROOF_H_
2 #define LFSC_UTIL_PROOF_H_
16 void print_pf( std::ostream& s,
int ind );
25 static std::map< int, RefPtr< LFSCProof > >
vMap;
52 void print_pf( std::ostream& s,
int ind = 0 );
63 vector< RefPtr< LFSCProof > >
d_pf;
68 for(
int a=0; a<(int)d_pfs.size(); a++ )
69 d_pf.push_back( d_pfs[a].get() );
70 for(
int a=0; a<(int)d_strs.size(); a++ )
71 d_str.push_back( d_strs[a] );
78 void print_pf( std::ostream& s,
int ind = 0 );
109 bool isTh, std::vector< int >& fv );
116 void print_pf( std::ostream& s,
int ind = 0 );
119 bool isTh, std::vector< int >& fv ){
120 return new LFSCPfLet( letPf, pv, body, isTh, fv );