Public Member Functions

virtual LFSCLraContra * AsLFSCLraContra ()
void print_pf (std::ostream &s, int ind=0)
LFSCProof * clone ()
int getNumChildren ()
LFSCProof * getChild (int n)
int checkOp ()

Static Public Member Functions

static LFSCProof * Make (LFSCProof *pf, int op)

Private Member Functions

LFSCLraContra (LFSCProof *pf, int op)
virtual ~LFSCLraContra ()
long int get_length ()

Private Attributes

RefPtr< LFSCProof > d_pf
int d_op

Constructor & Destructor Documentation

LFSCLraContra::LFSCLraContra	(	LFSCProof *	pf,
		int	op
	)		`[inline, private]`

Definition at line 145 of file LFSCLraProof.h.

References d_op, and LFSCProof::checkOp().

Referenced by Make(), and clone().

virtual LFSCLraContra::~LFSCLraContra ( ) [inline, private, virtual]

Definition at line 150 of file LFSCLraProof.h.

Member Function Documentation

long int LFSCLraContra::get_length ( ) [inline, private, virtual]

Reimplemented from LFSCProof.

Definition at line 151 of file LFSCLraProof.h.

References d_pf.

virtual LFSCLraContra* LFSCLraContra::AsLFSCLraContra ( ) [inline, virtual]

Reimplemented from LFSCProof.

Definition at line 153 of file LFSCLraProof.h.

void LFSCLraContra::print_pf	(	std::ostream &	s,
		int	ind = `0`
	)		`[inline, virtual]`

Implements LFSCProof.

Definition at line 154 of file LFSCLraProof.h.

References kind_to_str(), d_op, and d_pf.

static LFSCProof* LFSCLraContra::Make	(	LFSCProof *	pf,
		int	op
	)		`[inline, static]`

Definition at line 159 of file LFSCLraProof.h.

References LFSCLraContra().

Referenced by LFSCConvert::cvc3_to_lfsc(), TReturn::normalize_tr(), and TReturn::normalize_to_tf().

LFSCProof* LFSCLraContra::clone ( ) [inline, virtual]

Implements LFSCProof.

Definition at line 162 of file LFSCLraProof.h.

References LFSCLraContra(), d_pf, RefPtr::get(), and d_op.

int LFSCLraContra::getNumChildren ( ) [inline, virtual]

Reimplemented from LFSCProof.

Definition at line 163 of file LFSCLraProof.h.

LFSCProof* LFSCLraContra::getChild ( int n ) [inline, virtual]

Reimplemented from LFSCProof.

Definition at line 164 of file LFSCLraProof.h.

References d_pf, and RefPtr::get().

int LFSCLraContra::checkOp ( ) [inline, virtual]

Reimplemented from LFSCProof.

Definition at line 165 of file LFSCLraProof.h.

References d_op.

Member Data Documentation

RefPtr< LFSCProof > LFSCLraContra::d_pf [private]

Definition at line 143 of file LFSCLraProof.h.

Referenced by get_length(), print_pf(), clone(), and getChild().

int LFSCLraContra::d_op [private]

Definition at line 144 of file LFSCLraProof.h.

Referenced by LFSCLraContra(), print_pf(), clone(), and checkOp().

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

LFSCLraProof.h