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;
47 pfV( v ), body( bd ), abstVal( aVal ){}
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 );
107 d_letPf( letPf ),d_pv( pv ),d_body( body ),d_letPfRpl( letPfRpl ),d_pvRpl( pvRpl ),d_isTh( isTh ){}
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 );
virtual LFSCProofExpr * AsLFSCProofExpr()
RefPtr< LFSCProof > d_body
Data structure of expressions in CVC3.
LFSCProofExpr(const Expr &e, bool isH=false)
static LFSCProof * Make(LFSCProof *letPf, LFSCPfVar *pv, LFSCProof *body, bool isTh, std::vector< int > &fv)
LFSCProof * getChild(int n)
static LFSCProof * MakeUnk()
void print_pf(std::ostream &s, int ind)
long int get_string_length()
LFSCPfLambda(LFSCPfVar *v, LFSCProof *bd, LFSCProof *aVal=NULL)
LFSCProof * getChild(int n)
static LFSCProof * Make(const Expr &e, bool isH=false)
virtual LFSCProofGeneric * AsLFSCProofGeneric()
LFSCProofGeneric(vector< RefPtr< LFSCProof > > &d_pfs, vector< string > &d_strs, bool db_str=false)
static LFSCProof * Make(const char *c, int v)
void print_pf(std::ostream &s, int ind=0)
static LFSCProof * MakeV(int v)
RefPtr< LFSCProof > abstVal
LFSCPfLet(LFSCProof *letPf, LFSCPfVar *pv, LFSCProof *body, bool isTh, LFSCProof *letPfRpl, LFSCProof *pvRpl)
static std::map< int, RefPtr< LFSCProof > > vMap
static LFSCProof * Make(vector< RefPtr< LFSCProof > > &d_pfs, std::vector< string > &d_strs, bool db_str=false)
void print_pf(std::ostream &s, int ind=0)
void print_struct(std::ostream &s, int ind=0)
RefPtr< LFSCProof > d_letPf
static LFSCProof * MakeStr(const char *c, bool db_str=false)
void print_pf(std::ostream &s, int ind=0)
virtual ~LFSCProofGeneric()
RefPtr< LFSCProof > d_letPfRpl
RefPtr< LFSCProof > d_pvRpl
void print_struct(std::ostream &s, int ind=0)
static LFSCProof * Make(LFSCPfVar *v, LFSCProof *bd, LFSCProof *aVal=NULL)
vector< RefPtr< LFSCProof > > d_pf
void print_pf(std::ostream &s, int ind=0)
virtual LFSCPfVar * AsLFSCPfVar()
virtual LFSCPfLambda * AsLFSCPfLambda()
virtual LFSCPfLet * AsLFSCPfLet()