#include <LFSCUtilProof.h>
Inherits LFSCProof.
Public Member Functions
- virtual LFSCPfVar * AsLFSCPfVar ()
- void print_pf (std::ostream &s, int ind=0)
- void print_struct (std::ostream &s, int ind=0)
- LFSCProof * clone ()
Static Public Member Functions
Private Member Functions
- LFSCPfVar (string nm)
- virtual ~LFSCPfVar ()
- long int get_length ()
Private Attributes
- string name
Static Private Attributes
Detailed Description
Definition at line 23 of file LFSCUtilProof.h.
Constructor & Destructor Documentation
| LFSCPfVar::LFSCPfVar | ( | string | nm | ) | [inline, private] |
Definition at line 27 of file LFSCUtilProof.h.
| virtual LFSCPfVar::~LFSCPfVar | ( | ) | [inline, private, virtual] |
Definition at line 28 of file LFSCUtilProof.h.
Member Function Documentation
| long int LFSCPfVar::get_length | ( | ) | [inline, private, virtual] |
| virtual LFSCPfVar* LFSCPfVar::AsLFSCPfVar | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 31 of file LFSCUtilProof.h.
| void LFSCPfVar::print_pf | ( | std::ostream & | s, |
| int | ind = 0 |
||
| ) | [inline, virtual] |
| void LFSCPfVar::print_struct | ( | std::ostream & | s, |
| int | ind = 0 |
||
| ) | [inline, virtual] |
| LFSCProof * LFSCPfVar::Make | ( | const char * | c, |
| int | v | ||
| ) | [static] |
Definition at line 33 of file LFSCUtilProof.cpp.
References LFSCPfVar().
Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCProof::Make_CNF(), LFSCConvert::make_let_proof(), LFSCConvert::make_trusted(), MakeV(), TReturn::normalize_to_tf(), and TReturn::normalize_tr().
| LFSCProof * LFSCPfVar::MakeV | ( | int | v | ) | [static] |
Definition at line 40 of file LFSCUtilProof.cpp.
References RefPtr< T >::get(), Make(), and vMap.
Referenced by LFSCConvert::cvc3_to_lfsc(), and LFSCPfLet::LFSCPfLet().
| LFSCProof* LFSCPfVar::clone | ( | ) | [inline, virtual] |
Implements LFSCProof.
Definition at line 36 of file LFSCUtilProof.h.
References LFSCPfVar(), and name.
Member Data Documentation
std::map< int, RefPtr< LFSCProof > > LFSCPfVar::vMap [static, private] |
Definition at line 25 of file LFSCUtilProof.h.
Referenced by MakeV().
string LFSCPfVar::name [private] |
Definition at line 26 of file LFSCUtilProof.h.
Referenced by clone(), get_length(), print_pf(), and print_struct().
The documentation for this class was generated from the following files:
