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


Detailed Description

Definition at line 35 of file LFSCLraProof.h.


Constructor & Destructor Documentation

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

Definition at line 40 of file LFSCLraProof.h.

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

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 d_op, d_r, EQ, kind_to_str(), and print_rational().

bool LFSCLraAxiom::isTrivial ( ) [inline, virtual]

Reimplemented from LFSCProof.

Definition at line 49 of file LFSCLraProof.h.

References d_op, and EQ.

Definition at line 37 of file LFSCLraProof.cpp.

References eq, EQ, RefPtr< T >::get(), and LFSCLraAxiom().

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 d_op, d_r, and LFSCLraAxiom().

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 checkOp(), clone(), isTrivial(), and print_pf().

Definition at line 39 of file LFSCLraProof.h.

Referenced by clone(), and print_pf().


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