72 for(
int a=0; a<(int)
d_str.size(); a++ ){
74 sum +=
d_str[a].length();
75 if( a<(
int)
d_pf.size() )
82 for(
int a=0; a<(int)
d_str.size(); a++ ){
84 if( a<(
int)
d_pf.size() ){
85 d_pf[a]->print( s,
d_pf.size()<3 ? ind+1 : 0 );
92 vector< RefPtr< LFSCProof > > d_pfs;
93 d_pfs.push_back( sub_pf );
94 vector< string > d_strs;
95 d_strs.push_back( str_pre );
96 d_strs.push_back( str_post );
102 vector< RefPtr< LFSCProof > > d_pfs;
103 d_pfs.push_back( sub_pf1 );
104 d_pfs.push_back( sub_pf2 );
105 vector< string > d_strs;
106 string str_empty(
" ");
107 d_strs.push_back( str_pre );
108 d_strs.push_back( str_empty );
109 d_strs.push_back( str_post );
115 vector< RefPtr< LFSCProof > > d_pfs;
116 vector< string > d_strs;
118 d_strs.push_back( str );
125 bool isTh, std::vector< int >& fv ) :
LFSCProof(), d_letPf( letPf ),
126 d_pv( pv ),d_body( body ),d_isTh( isTh ){
129 #ifndef IGNORE_LETPF_VARS
131 for(
int a=0; a<(int)fv.size(); a++ ){
132 ostringstream os1, os2;
134 os1 <<
"(impl_intro _ _ ";
143 for(
int a=(
int)fv.size()-1; a>=0; a-- ){
144 ostringstream os1, os2;
145 os1 <<
"(impl_elim _ _ ";
158 s <<
"(" << (
d_isTh ?
"th_let_pf _ " :
"satlem _ _ _ " );
void print_structure(std::ostream &s, int ind=0)
RefPtr< LFSCProof > d_body
Data structure of expressions in CVC3.
LFSCProofExpr(const Expr &e, bool isH=false)
static Expr cascade_expr(const Expr &e)
void print_pf(std::ostream &s, int ind)
long int get_string_length()
void print_expr(const Expr &expr, std::ostream &s)
LFSCProofGeneric(vector< RefPtr< LFSCProof > > &d_pfs, vector< string > &d_strs, bool db_str=false)
static LFSCProof * Make(const char *c, int v)
static LFSCPrinter * printer
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
static LFSCProof * MakeV(int v)
RefPtr< LFSCProof > abstVal
LFSCPfLet(LFSCProof *letPf, LFSCPfVar *pv, LFSCProof *body, bool isTh, LFSCProof *letPfRpl, LFSCProof *pvRpl)
static std::map< LFSCProof *, LFSCProof * > lambdaPrintMap
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)
RefPtr< LFSCProof > d_letPfRpl
RefPtr< LFSCProof > d_pvRpl
static LFSCProof * Make(LFSCPfVar *v, LFSCProof *bd, LFSCProof *aVal=NULL)
void set_print_expr(const Expr &expr)
vector< RefPtr< LFSCProof > > d_pf
void print(std::ostream &s, int ind=0)
void print_pf(std::ostream &s, int ind=0)