CVC3
2.4.1
|
#include <LFSCLraProof.h>
LFSCLraContra::LFSCLraContra | ( | LFSCProof * | pf, |
int | op | ||
) | [inline, private] |
Definition at line 145 of file LFSCLraProof.h.
References d_op, and LFSCProof::checkOp().
virtual LFSCLraContra::~LFSCLraContra | ( | ) | [inline, private, virtual] |
Definition at line 150 of file LFSCLraProof.h.
long int LFSCLraContra::get_length | ( | ) | [inline, private, virtual] |
virtual LFSCLraContra* LFSCLraContra::AsLFSCLraContra | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 153 of file LFSCLraProof.h.
void LFSCLraContra::print_pf | ( | std::ostream & | s, |
int | ind = 0 |
||
) | [inline, virtual] |
Implements LFSCProof.
Definition at line 154 of file LFSCLraProof.h.
References kind_to_str(), d_op, and d_pf.
Definition at line 159 of file LFSCLraProof.h.
References LFSCLraContra().
Referenced by LFSCConvert::cvc3_to_lfsc(), TReturn::normalize_tr(), and TReturn::normalize_to_tf().
LFSCProof* LFSCLraContra::clone | ( | ) | [inline, virtual] |
Implements LFSCProof.
Definition at line 162 of file LFSCLraProof.h.
References LFSCLraContra(), d_pf, RefPtr::get(), and d_op.
int LFSCLraContra::getNumChildren | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 163 of file LFSCLraProof.h.
LFSCProof* LFSCLraContra::getChild | ( | int | n | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 164 of file LFSCLraProof.h.
References d_pf, and RefPtr::get().
int LFSCLraContra::checkOp | ( | ) | [inline, virtual] |
RefPtr< LFSCProof > LFSCLraContra::d_pf [private] |
Definition at line 143 of file LFSCLraProof.h.
Referenced by get_length(), print_pf(), clone(), and getChild().
int LFSCLraContra::d_op [private] |
Definition at line 144 of file LFSCLraProof.h.
Referenced by LFSCLraContra(), print_pf(), clone(), and checkOp().