#include <LFSCLraProof.h>

Inheritance diagram for LFSCLraMulC:

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

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, and LFSCProof::get_string_length().

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(), LFSCProof::print(), 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: