LFSCLraContra Class Reference

#include <LFSCLraProof.h>

Inherits LFSCProof.

Collaboration diagram for LFSCLraContra:

List of all members.

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

---

Detailed Description

Definition at line 140 of file LFSCLraProof.h.

---

Constructor & Destructor Documentation

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

Definition at line 145 of file LFSCLraProof.h.

References LFSCProof::checkOp(), and d_op.

Referenced by clone(), and Make().

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 d_op, d_pf, and kind_to_str().

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_to_tf(), and TReturn::normalize_tr().

LFSCProof* LFSCLraContra::clone

(

)

[inline, virtual]

Implements LFSCProof.

Definition at line 162 of file LFSCLraProof.h.

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

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< T >::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 clone(), get_length(), getChild(), and print_pf().

int LFSCLraContra::d_op [private]

Definition at line 144 of file LFSCLraProof.h.

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

---

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

• LFSCLraProof.h