CVC3  2.4.1
Public Member Functions | Static Public Member Functions | Private Member Functions | Private Attributes | Static Private Attributes
LFSCLraAxiom Class Reference

#include <LFSCLraProof.h>

Inheritance diagram for LFSCLraAxiom:
LFSCProof LFSCObj Obj

List of all members.

Public Member Functions

Static Public Member Functions

Private Member Functions

Private Attributes

Static Private Attributes


Constructor & Destructor Documentation

LFSCLraAxiom::LFSCLraAxiom ( int  op) [inline, private]

Definition at line 40 of file LFSCLraProof.h.

Referenced by MakeEq(), Make(), and clone().

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.


Member Function Documentation

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.

References d_op, and EQ.

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().

static LFSCProof* LFSCLraAxiom::Make ( Rational  r,
int  op 
) [inline, static]

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]

Reimplemented from LFSCProof.

Definition at line 53 of file LFSCLraProof.h.

References d_op.


Member Data Documentation

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().

Definition at line 39 of file LFSCLraProof.h.

Referenced by print_pf(), and clone().


The documentation for this class was generated from the following files: