CVC3
2.4.1
|
#include <LFSCLraProof.h>
Definition at line 63 of file LFSCLraProof.h.
References d_op, and LFSCProof::checkOp().
virtual LFSCLraMulC::~LFSCLraMulC | ( | ) | [inline, private, virtual] |
Definition at line 69 of file LFSCLraProof.h.
long int LFSCLraMulC::get_length | ( | ) | [inline, private, virtual] |
virtual LFSCLraMulC* LFSCLraMulC::AsLFSCLraMulC | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 72 of file LFSCLraProof.h.
bool LFSCLraMulC::isLraMulC | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 73 of file LFSCLraProof.h.
void LFSCLraMulC::print_pf | ( | std::ostream & | s, |
int | ind = 0 |
||
) | [virtual] |
Implements LFSCProof.
Definition at line 56 of file LFSCLraProof.cpp.
References kind_to_str(), d_op, print_rational(), d_r, and d_pf.
Definition at line 65 of file LFSCLraProof.cpp.
References LFSCProof::isTrivial(), LFSCProof::AsLFSCLraMulC(), d_r, d_pf, RefPtr::get(), and LFSCLraMulC().
Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), and TReturn::normalize_tr().
LFSCProof* LFSCLraMulC::clone | ( | ) | [inline, virtual] |
Implements LFSCProof.
Definition at line 76 of file LFSCLraProof.h.
References LFSCLraMulC(), d_pf, RefPtr::get(), d_r, and d_op.
int LFSCLraMulC::getNumChildren | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 77 of file LFSCLraProof.h.
LFSCProof* LFSCLraMulC::getChild | ( | int | n | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 78 of file LFSCLraProof.h.
References d_pf, and RefPtr::get().
int LFSCLraMulC::checkOp | ( | ) | [inline, virtual] |
RefPtr< LFSCProof > LFSCLraMulC::d_pf [private] |
Definition at line 60 of file LFSCLraProof.h.
Referenced by print_pf(), Make(), get_length(), clone(), and getChild().
Rational LFSCLraMulC::d_r [private] |
Definition at line 61 of file LFSCLraProof.h.
Referenced by print_pf(), Make(), and clone().
int LFSCLraMulC::d_op [private] |
Definition at line 62 of file LFSCLraProof.h.
Referenced by print_pf(), LFSCLraMulC(), clone(), and checkOp().