#include <LFSCLraProof.h>

Inheritance diagram for LFSCLraAxiom:

Public Member Functions

virtual LFSCLraAxiom * AsLFSCLraAxiom ()
void print_pf (std::ostream &s, int ind=0)
bool isTrivial ()
LFSCProof * clone ()
int checkOp ()

Static Public Member Functions

static LFSCProof * MakeEq ()
static LFSCProof * Make (Rational r, int op)

Private Member Functions

LFSCLraAxiom (int op)
LFSCLraAxiom (int op, Rational r)
virtual ~LFSCLraAxiom ()
long int get_length ()

Private Attributes

int d_op
Rational d_r

Static Private Attributes

static RefPtr< LFSCProof > eq

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

Rational LFSCLraAxiom::d_r [private]

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: