#include <LFSCUtilProof.h>
Inherits LFSCProof.
Public Member Functions
- virtual LFSCPfLet * AsLFSCPfLet ()
- void print_pf (std::ostream &s, int ind=0)
- void print_struct (std::ostream &s, int ind=0)
- LFSCProof * clone ()
Static Public Member Functions
- static LFSCProof * Make (LFSCProof *letPf, LFSCPfVar *pv, LFSCProof *body, bool isTh, std::vector< int > &fv)
Private Member Functions
- LFSCPfLet (LFSCProof *letPf, LFSCPfVar *pv, LFSCProof *body, bool isTh, LFSCProof *letPfRpl, LFSCProof *pvRpl)
- LFSCPfLet (LFSCProof *letPf, LFSCPfVar *pv, LFSCProof *body, bool isTh, std::vector< int > &fv)
- virtual ~LFSCPfLet ()
- long int get_length ()
Private Attributes
- RefPtr< LFSCProof > d_letPf
- RefPtr< LFSCPfVar > d_pv
- RefPtr< LFSCProof > d_body
- RefPtr< LFSCProof > d_letPfRpl
- RefPtr< LFSCProof > d_pvRpl
- bool d_isTh
Detailed Description
Definition at line 95 of file LFSCUtilProof.h.
Constructor & Destructor Documentation
| 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 CVC3::abs(), d_letPfRpl, d_pvRpl, RefPtr< T >::get(), Make(), and LFSCPfVar::MakeV().
| virtual LFSCPfLet::~LFSCPfLet | ( | ) | [inline, private, virtual] |
Definition at line 110 of file LFSCUtilProof.h.
Member Function Documentation
| 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_body, d_isTh, d_letPf, d_letPfRpl, d_pv, d_pvRpl, std::endl(), RefPtr< T >::get(), and LFSCProof::lambdaPrintMap.
| void LFSCPfLet::print_struct | ( | std::ostream & | s, |
| int | ind = 0 |
||
| ) | [virtual] |
Reimplemented from LFSCProof.
Definition at line 169 of file LFSCUtilProof.cpp.
References d_body, d_letPf, d_pv, RefPtr< T >::get(), and LFSCProof::lambdaPrintMap.
| 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 LFSCPfLet(), and LFSCConvert::make_let_proof().
| LFSCProof* LFSCPfLet::clone | ( | ) | [inline, virtual] |
Implements LFSCProof.
Definition at line 122 of file LFSCUtilProof.h.
References d_body, d_isTh, d_letPf, d_letPfRpl, d_pv, d_pvRpl, RefPtr< T >::get(), and LFSCPfLet().
Member Data Documentation
RefPtr< LFSCProof > LFSCPfLet::d_letPf [private] |
Definition at line 97 of file LFSCUtilProof.h.
Referenced by clone(), get_length(), print_pf(), and print_struct().
RefPtr< LFSCPfVar > LFSCPfLet::d_pv [private] |
Definition at line 98 of file LFSCUtilProof.h.
Referenced by clone(), get_length(), print_pf(), and print_struct().
RefPtr< LFSCProof > LFSCPfLet::d_body [private] |
Definition at line 99 of file LFSCUtilProof.h.
Referenced by clone(), get_length(), print_pf(), and print_struct().
RefPtr< LFSCProof > LFSCPfLet::d_letPfRpl [private] |
Definition at line 101 of file LFSCUtilProof.h.
Referenced by clone(), LFSCPfLet(), and print_pf().
RefPtr< LFSCProof > LFSCPfLet::d_pvRpl [private] |
Definition at line 103 of file LFSCUtilProof.h.
Referenced by clone(), LFSCPfLet(), and print_pf().
bool LFSCPfLet::d_isTh [private] |
Definition at line 104 of file LFSCUtilProof.h.
Referenced by clone(), and print_pf().
The documentation for this class was generated from the following files:
