LFSCLraAdd Class Reference

#include <LFSCLraProof.h>

Inherits LFSCProof.

Collaboration diagram for LFSCLraAdd:

List of all members.

Public Member Functions

• virtual LFSCLraAdd * AsLFSCLraAdd ()
• 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

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

Private Attributes

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

---

Detailed Description

Definition at line 7 of file LFSCLraProof.h.

---

Constructor & Destructor Documentation

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

Definition at line 12 of file LFSCLraProof.h.

References d_children.

Referenced by clone(), and Make().

virtual LFSCLraAdd::~LFSCLraAdd

(

)

[inline, private, virtual]

Definition at line 18 of file LFSCLraProof.h.

---

Member Function Documentation

long int LFSCLraAdd::get_length

(

)

[inline, private, virtual]

Reimplemented from LFSCProof.

Definition at line 19 of file LFSCLraProof.h.

References d_children.

virtual LFSCLraAdd* LFSCLraAdd::AsLFSCLraAdd

(

)

[inline, virtual]

Reimplemented from LFSCProof.

Definition at line 23 of file LFSCLraProof.h.

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

Implements LFSCProof.

Definition at line 5 of file LFSCLraProof.cpp.

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

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

Definition at line 17 of file LFSCLraProof.cpp.

References LFSCProof::checkOp(), get_knd_order(), LFSCProof::isTrivial(), and LFSCLraAdd().

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

LFSCProof* LFSCLraAdd::clone

(

)

[inline, virtual]

Implements LFSCProof.

Definition at line 26 of file LFSCLraProof.h.

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

int LFSCLraAdd::getNumChildren

(

)

[inline, virtual]

Reimplemented from LFSCProof.

Definition at line 27 of file LFSCLraProof.h.

LFSCProof* LFSCLraAdd::getChild

(

int

n

)

[inline, virtual]

Reimplemented from LFSCProof.

Definition at line 28 of file LFSCLraProof.h.

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

int LFSCLraAdd::checkOp

(

)

[inline, virtual]

Reimplemented from LFSCProof.

Definition at line 29 of file LFSCLraProof.h.

References d_op1, d_op2, and get_knd_result().

---

Member Data Documentation

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

Definition at line 9 of file LFSCLraProof.h.

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

int LFSCLraAdd::d_op1 [private]

Definition at line 10 of file LFSCLraProof.h.

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

int LFSCLraAdd::d_op2 [private]

Definition at line 10 of file LFSCLraProof.h.

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

---

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

• LFSCLraProof.h
• LFSCLraProof.cpp