LFSCLraSub Class Reference

#include <LFSCLraProof.h>

Inherits LFSCProof.

Collaboration diagram for LFSCLraSub:

List of all members.

Public Member Functions

• virtual LFSCLraSub * AsLFSCLraSub ()
• 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 *pf1, LFSCProof *pf2, int op1, int op2)

Private Member Functions

• LFSCLraSub (LFSCProof *pf1, LFSCProof *pf2, int op1, int op2)
• virtual ~LFSCLraSub ()
• long int get_length ()

Private Attributes

• RefPtr< LFSCProof > d_children [2]
• int d_op1
• int d_op2

---

Detailed Description

Definition at line 84 of file LFSCLraProof.h.

---

Constructor & Destructor Documentation

LFSCLraSub::LFSCLraSub	(	LFSCProof *	pf1,
		LFSCProof *	pf2,
		int	op1,
		int	op2
	)		[inline, private]

Definition at line 88 of file LFSCLraProof.h.

References LFSCProof::checkOp(), d_children, d_op1, and d_op2.

Referenced by clone(), and Make().

virtual LFSCLraSub::~LFSCLraSub

(

)

[inline, private, virtual]

Definition at line 96 of file LFSCLraProof.h.

---

Member Function Documentation

long int LFSCLraSub::get_length

(

)

[inline, private, virtual]

Reimplemented from LFSCProof.

Definition at line 97 of file LFSCLraProof.h.

References d_children.

virtual LFSCLraSub* LFSCLraSub::AsLFSCLraSub

(

)

[inline, virtual]

Reimplemented from LFSCProof.

Definition at line 101 of file LFSCLraProof.h.

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

Implements LFSCProof.

Definition at line 81 of file LFSCLraProof.cpp.

References d_children, d_op1, d_op2, and kind_to_str().

LFSCProof * LFSCLraSub::Make	(	LFSCProof *	pf1,
		LFSCProof *	pf2,
		int	op1,
		int	op2
	)		[static]

Definition at line 89 of file LFSCLraProof.cpp.

References LFSCProof::isTrivial(), and LFSCLraSub().

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

LFSCProof* LFSCLraSub::clone

(

)

[inline, virtual]

Implements LFSCProof.

Definition at line 104 of file LFSCLraProof.h.

References d_children, d_op1, d_op2, and LFSCLraSub().

int LFSCLraSub::getNumChildren

(

)

[inline, virtual]

Reimplemented from LFSCProof.

Definition at line 105 of file LFSCLraProof.h.

LFSCProof* LFSCLraSub::getChild

(

int

n

)

[inline, virtual]

Reimplemented from LFSCProof.

Definition at line 106 of file LFSCLraProof.h.

References d_children, and RefPtr< T >::get().

int LFSCLraSub::checkOp

(

)

[inline, virtual]

Reimplemented from LFSCProof.

Definition at line 107 of file LFSCLraProof.h.

References d_op1, d_op2, and get_knd_result().

---

Member Data Documentation

RefPtr< LFSCProof > LFSCLraSub::d_children[2] [private]

Definition at line 86 of file LFSCLraProof.h.

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

int LFSCLraSub::d_op1 [private]

Definition at line 87 of file LFSCLraProof.h.

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

int LFSCLraSub::d_op2 [private]

Definition at line 87 of file LFSCLraProof.h.

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

---

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

• LFSCLraProof.h
• LFSCLraProof.cpp