CVC3  2.4.1
Public Member Functions | Static Public Member Functions | Private Member Functions | Private Attributes
LFSCPfLambda Class Reference

#include <LFSCUtilProof.h>

Inheritance diagram for LFSCPfLambda:
LFSCProof LFSCObj Obj

List of all members.

Public Member Functions

Static Public Member Functions

Private Member Functions

Private Attributes


Constructor & Destructor Documentation

LFSCPfLambda::LFSCPfLambda ( LFSCPfVar v,
LFSCProof bd,
LFSCProof aVal = NULL 
) [inline, private]

Definition at line 46 of file LFSCUtilProof.h.

Referenced by Make(), and clone().

virtual LFSCPfLambda::~LFSCPfLambda ( ) [inline, private, virtual]

Definition at line 48 of file LFSCUtilProof.h.


Member Function Documentation

long int LFSCPfLambda::get_length ( ) [inline, private, virtual]

Reimplemented from LFSCProof.

Definition at line 49 of file LFSCUtilProof.h.

References pfV, and body.

virtual LFSCPfLambda* LFSCPfLambda::AsLFSCPfLambda ( ) [inline, virtual]

Reimplemented from LFSCProof.

Definition at line 51 of file LFSCUtilProof.h.

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

Implements LFSCProof.

Definition at line 52 of file LFSCUtilProof.cpp.

References abstVal, RefPtr::get(), LFSCProof::lambdaPrintMap, pfV, and body.

static LFSCProof* LFSCPfLambda::Make ( LFSCPfVar v,
LFSCProof bd,
LFSCProof aVal = NULL 
) [inline, static]

Definition at line 53 of file LFSCUtilProof.h.

References LFSCPfLambda().

LFSCProof* LFSCPfLambda::clone ( ) [inline, virtual]

Implements LFSCProof.

Definition at line 56 of file LFSCUtilProof.h.

References LFSCPfLambda(), pfV, RefPtr::get(), body, and abstVal.

int LFSCPfLambda::getNumChildren ( ) [inline, virtual]

Reimplemented from LFSCProof.

Definition at line 57 of file LFSCUtilProof.h.

LFSCProof* LFSCPfLambda::getChild ( int  n) [inline, virtual]

Reimplemented from LFSCProof.

Definition at line 58 of file LFSCUtilProof.h.

References pfV, RefPtr::get(), and body.


Member Data Documentation

Definition at line 41 of file LFSCUtilProof.h.

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

Definition at line 42 of file LFSCUtilProof.h.

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

Definition at line 44 of file LFSCUtilProof.h.

Referenced by print_pf(), and clone().


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