CVC3
2.4.1
|
#include <LFSCLraProof.h>
Definition at line 12 of file LFSCLraProof.h.
References d_children.
virtual LFSCLraAdd::~LFSCLraAdd | ( | ) | [inline, private, virtual] |
Definition at line 18 of file LFSCLraProof.h.
long int LFSCLraAdd::get_length | ( | ) | [inline, private, virtual] |
virtual LFSCLraAdd* LFSCLraAdd::AsLFSCLraAdd | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 23 of file LFSCLraProof.h.
void LFSCLraAdd::print_pf | ( | std::ostream & | s, |
int | ind = 0 |
||
) | [virtual] |
Implements LFSCProof.
Definition at line 5 of file LFSCLraProof.cpp.
References kind_to_str(), d_op1, d_op2, and d_children.
Definition at line 17 of file LFSCLraProof.cpp.
References LFSCProof::isTrivial(), LFSCProof::checkOp(), get_knd_order(), and LFSCLraAdd().
Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), TReturn::normalize_tr(), and TReturn::normalize_to_tf().
LFSCProof* LFSCLraAdd::clone | ( | ) | [inline, virtual] |
Implements LFSCProof.
Definition at line 26 of file LFSCLraProof.h.
References LFSCLraAdd(), d_children, d_op1, and d_op2.
int LFSCLraAdd::getNumChildren | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 27 of file LFSCLraProof.h.
LFSCProof* LFSCLraAdd::getChild | ( | int | n | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 28 of file LFSCLraProof.h.
References d_children, and RefPtr::get().
int LFSCLraAdd::checkOp | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 29 of file LFSCLraProof.h.
References get_knd_result(), d_op1, and d_op2.
RefPtr< LFSCProof > LFSCLraAdd::d_children[2] [private] |
Definition at line 9 of file LFSCLraProof.h.
Referenced by print_pf(), LFSCLraAdd(), get_length(), clone(), and getChild().
int LFSCLraAdd::d_op1 [private] |
Definition at line 10 of file LFSCLraProof.h.
Referenced by print_pf(), clone(), and checkOp().
int LFSCLraAdd::d_op2 [private] |
Definition at line 10 of file LFSCLraProof.h.
Referenced by print_pf(), clone(), and checkOp().