CVC3
2.4.1
|
#include <LFSCUtilProof.h>
LFSCPfLet::LFSCPfLet | ( | LFSCProof * | letPf, |
LFSCPfVar * | pv, | ||
LFSCProof * | body, | ||
bool | isTh, | ||
LFSCProof * | letPfRpl, | ||
LFSCProof * | pvRpl | ||
) | [inline, private] |
Definition at line 105 of file LFSCUtilProof.h.
LFSCPfLet::LFSCPfLet | ( | LFSCProof * | letPf, |
LFSCPfVar * | pv, | ||
LFSCProof * | body, | ||
bool | isTh, | ||
std::vector< int > & | fv | ||
) | [private] |
Definition at line 124 of file LFSCUtilProof.cpp.
References d_letPfRpl, d_pvRpl, Make(), CVC3::abs(), LFSCPfVar::MakeV(), and RefPtr::get().
virtual LFSCPfLet::~LFSCPfLet | ( | ) | [inline, private, virtual] |
Definition at line 110 of file LFSCUtilProof.h.
long int LFSCPfLet::get_length | ( | ) | [inline, private, virtual] |
virtual LFSCPfLet* LFSCPfLet::AsLFSCPfLet | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 115 of file LFSCUtilProof.h.
void LFSCPfLet::print_pf | ( | std::ostream & | s, |
int | ind = 0 |
||
) | [virtual] |
Implements LFSCProof.
Definition at line 153 of file LFSCUtilProof.cpp.
References d_pvRpl, RefPtr::get(), d_pv, d_letPfRpl, d_isTh, std::endl(), LFSCProof::lambdaPrintMap, d_letPf, and d_body.
void LFSCPfLet::print_struct | ( | std::ostream & | s, |
int | ind = 0 |
||
) | [virtual] |
Reimplemented from LFSCProof.
Definition at line 169 of file LFSCUtilProof.cpp.
References d_letPf, d_pv, LFSCProof::lambdaPrintMap, RefPtr::get(), and d_body.
static LFSCProof* LFSCPfLet::Make | ( | LFSCProof * | letPf, |
LFSCPfVar * | pv, | ||
LFSCProof * | body, | ||
bool | isTh, | ||
std::vector< int > & | fv | ||
) | [inline, static] |
Definition at line 118 of file LFSCUtilProof.h.
References LFSCPfLet().
Referenced by LFSCConvert::make_let_proof(), and LFSCPfLet().
LFSCProof* LFSCPfLet::clone | ( | ) | [inline, virtual] |
Implements LFSCProof.
Definition at line 122 of file LFSCUtilProof.h.
References LFSCPfLet(), d_letPf, RefPtr::get(), d_pv, d_body, d_isTh, d_letPfRpl, and d_pvRpl.
RefPtr< LFSCProof > LFSCPfLet::d_letPf [private] |
Definition at line 97 of file LFSCUtilProof.h.
Referenced by print_pf(), print_struct(), get_length(), and clone().
RefPtr< LFSCPfVar > LFSCPfLet::d_pv [private] |
Definition at line 98 of file LFSCUtilProof.h.
Referenced by print_pf(), print_struct(), get_length(), and clone().
RefPtr< LFSCProof > LFSCPfLet::d_body [private] |
Definition at line 99 of file LFSCUtilProof.h.
Referenced by print_pf(), print_struct(), get_length(), and clone().
RefPtr< LFSCProof > LFSCPfLet::d_letPfRpl [private] |
Definition at line 101 of file LFSCUtilProof.h.
Referenced by LFSCPfLet(), print_pf(), and clone().
RefPtr< LFSCProof > LFSCPfLet::d_pvRpl [private] |
Definition at line 103 of file LFSCUtilProof.h.
Referenced by LFSCPfLet(), print_pf(), and clone().
bool LFSCPfLet::d_isTh [private] |
Definition at line 104 of file LFSCUtilProof.h.
Referenced by print_pf(), and clone().