CVC3
2.4.1
|
#include <LFSCUtilProof.h>
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.
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(), LFSCConvert::make_let_proof(), LFSCConvert::make_trusted(), LFSCProof::Make_CNF(), MakeV(), TReturn::normalize_tr(), and TReturn::normalize_to_tf().
LFSCProof * LFSCPfVar::MakeV | ( | int | v | ) | [static] |
Definition at line 40 of file LFSCUtilProof.cpp.
References vMap, RefPtr::get(), and Make().
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.
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 get_length(), print_pf(), print_struct(), and clone().