LFSCLraMulC Class Reference

#include <LFSCLraProof.h>

Inherits LFSCProof.

Collaboration diagram for LFSCLraMulC:

List of all members.

Public Member Functions

• virtual LFSCLraMulC * AsLFSCLraMulC ()
• bool isLraMulC ()
• 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, Rational r, int op)

Private Member Functions

• LFSCLraMulC (LFSCProof *pf, Rational r, int op)
• virtual ~LFSCLraMulC ()
• long int get_length ()

Private Attributes

• RefPtr< LFSCProof > d_pf
• Rational d_r
• int d_op

---

Detailed Description

Definition at line 58 of file LFSCLraProof.h.

---

Constructor & Destructor Documentation

LFSCLraMulC::LFSCLraMulC	(	LFSCProof *	pf,
		Rational	r,
		int	op
	)		[inline, private]

Definition at line 63 of file LFSCLraProof.h.

References LFSCProof::checkOp(), and d_op.

Referenced by clone(), and Make().

virtual LFSCLraMulC::~LFSCLraMulC

(

)

[inline, private, virtual]

Definition at line 69 of file LFSCLraProof.h.

---

Member Function Documentation

long int LFSCLraMulC::get_length

(

)

[inline, private, virtual]

Reimplemented from LFSCProof.

Definition at line 70 of file LFSCLraProof.h.

References d_pf.

virtual LFSCLraMulC* LFSCLraMulC::AsLFSCLraMulC

(

)

[inline, virtual]

Reimplemented from LFSCProof.

Definition at line 72 of file LFSCLraProof.h.

bool LFSCLraMulC::isLraMulC

(

)

[inline, virtual]

Reimplemented from LFSCProof.

Definition at line 73 of file LFSCLraProof.h.

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

Implements LFSCProof.

Definition at line 56 of file LFSCLraProof.cpp.

References d_op, d_pf, d_r, kind_to_str(), and print_rational().

LFSCProof * LFSCLraMulC::Make	(	LFSCProof *	pf,
		Rational	r,
		int	op
	)		[static]

Definition at line 65 of file LFSCLraProof.cpp.

References LFSCProof::AsLFSCLraMulC(), d_pf, d_r, RefPtr< T >::get(), LFSCProof::isTrivial(), and LFSCLraMulC().

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

LFSCProof* LFSCLraMulC::clone

(

)

[inline, virtual]

Implements LFSCProof.

Definition at line 76 of file LFSCLraProof.h.

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

int LFSCLraMulC::getNumChildren

(

)

[inline, virtual]

Reimplemented from LFSCProof.

Definition at line 77 of file LFSCLraProof.h.

LFSCProof* LFSCLraMulC::getChild

(

int

n

)

[inline, virtual]

Reimplemented from LFSCProof.

Definition at line 78 of file LFSCLraProof.h.

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

int LFSCLraMulC::checkOp

(

)

[inline, virtual]

Reimplemented from LFSCProof.

Definition at line 79 of file LFSCLraProof.h.

References d_op.

---

Member Data Documentation

RefPtr< LFSCProof > LFSCLraMulC::d_pf [private]

Definition at line 60 of file LFSCLraProof.h.

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

Rational LFSCLraMulC::d_r [private]

Definition at line 61 of file LFSCLraProof.h.

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

int LFSCLraMulC::d_op [private]

Definition at line 62 of file LFSCLraProof.h.

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

---

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

• LFSCLraProof.h
• LFSCLraProof.cpp