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

#include <LFSCUtilProof.h>

Inheritance diagram for LFSCProofExpr:
LFSCProof LFSCObj Obj

List of all members.

Public Member Functions

Static Public Member Functions

Private Member Functions

Private Attributes


Constructor & Destructor Documentation

LFSCProofExpr::LFSCProofExpr ( const Expr e,
bool  isH = false 
) [private]

Definition at line 23 of file LFSCUtilProof.cpp.

References d_e, LFSCObj::cascade_expr(), initialize(), and isHole.

Referenced by Make(), and clone().

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

Definition at line 12 of file LFSCUtilProof.h.


Member Function Documentation

void LFSCProofExpr::initialize ( ) [private]

Reimplemented from Obj.

Definition at line 7 of file LFSCUtilProof.cpp.

References LFSCObj::printer, LFSCPrinter::set_print_expr(), and d_e.

Referenced by LFSCProofExpr().

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

Reimplemented from LFSCProof.

Definition at line 13 of file LFSCUtilProof.h.

virtual LFSCProofExpr* LFSCProofExpr::AsLFSCProofExpr ( ) [inline, virtual]

Reimplemented from LFSCProof.

Definition at line 15 of file LFSCUtilProof.h.

void LFSCProofExpr::print_pf ( std::ostream s,
int  ind 
) [virtual]

Implements LFSCProof.

Definition at line 11 of file LFSCUtilProof.cpp.

References isHole, LFSCObj::printer, LFSCPrinter::print_expr(), and d_e.

static LFSCProof* LFSCProofExpr::Make ( const Expr e,
bool  isH = false 
) [inline, static]
LFSCProof* LFSCProofExpr::clone ( ) [inline, virtual]

Implements LFSCProof.

Definition at line 18 of file LFSCUtilProof.h.

References LFSCProofExpr(), d_e, and isHole.

void LFSCProofExpr::fillHoles ( ) [inline, virtual]

Reimplemented from LFSCProof.

Definition at line 20 of file LFSCUtilProof.h.

References isHole.


Member Data Documentation

bool LFSCProofExpr::isHole [private]

Definition at line 8 of file LFSCUtilProof.h.

Referenced by print_pf(), LFSCProofExpr(), clone(), and fillHoles().

Definition at line 9 of file LFSCUtilProof.h.

Referenced by initialize(), print_pf(), LFSCProofExpr(), and clone().


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