CVC3
2.4.1
|
#include <LFSCLraProof.h>
LFSCLraAxiom::LFSCLraAxiom | ( | int | op | ) | [inline, private] |
Definition at line 40 of file LFSCLraProof.h.
LFSCLraAxiom::LFSCLraAxiom | ( | int | op, |
Rational | r | ||
) | [inline, private] |
Definition at line 41 of file LFSCLraProof.h.
virtual LFSCLraAxiom::~LFSCLraAxiom | ( | ) | [inline, private, virtual] |
Definition at line 44 of file LFSCLraProof.h.
long int LFSCLraAxiom::get_length | ( | ) | [inline, private, virtual] |
Reimplemented from LFSCProof.
Definition at line 45 of file LFSCLraProof.h.
virtual LFSCLraAxiom* LFSCLraAxiom::AsLFSCLraAxiom | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 47 of file LFSCLraProof.h.
void LFSCLraAxiom::print_pf | ( | std::ostream & | s, |
int | ind = 0 |
||
) | [virtual] |
Implements LFSCProof.
Definition at line 44 of file LFSCLraProof.cpp.
References kind_to_str(), d_op, EQ, print_rational(), and d_r.
bool LFSCLraAxiom::isTrivial | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 49 of file LFSCLraProof.h.
LFSCProof * LFSCLraAxiom::MakeEq | ( | ) | [static] |
Definition at line 37 of file LFSCLraProof.cpp.
References eq, RefPtr::get(), LFSCLraAxiom(), and EQ.
Referenced by LFSCConvert::cvc3_to_lfsc().
Definition at line 51 of file LFSCLraProof.h.
References LFSCLraAxiom().
LFSCProof* LFSCLraAxiom::clone | ( | ) | [inline, virtual] |
Implements LFSCProof.
Definition at line 52 of file LFSCLraProof.h.
References LFSCLraAxiom(), d_op, and d_r.
int LFSCLraAxiom::checkOp | ( | ) | [inline, virtual] |
RefPtr< LFSCProof > LFSCLraAxiom::eq [static, private] |
Definition at line 37 of file LFSCLraProof.h.
Referenced by MakeEq().
int LFSCLraAxiom::d_op [private] |
Definition at line 38 of file LFSCLraProof.h.
Referenced by print_pf(), isTrivial(), clone(), and checkOp().
Rational LFSCLraAxiom::d_r [private] |
Definition at line 39 of file LFSCLraProof.h.
Referenced by print_pf(), and clone().