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

#include <LFSCLraProof.h>

Inheritance diagram for LFSCLraPoly:
LFSCProof LFSCObj Obj

List of all members.

Public Member Functions

Static Public Member Functions

Private Member Functions

Private Attributes


Constructor & Destructor Documentation

LFSCLraPoly::LFSCLraPoly ( LFSCProof pf,
int  var,
int  op 
) [inline, private]

Definition at line 116 of file LFSCLraProof.h.

References d_op, and LFSCProof::checkOp().

Referenced by Make(), and clone().

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

Definition at line 122 of file LFSCLraProof.h.


Member Function Documentation

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

Reimplemented from LFSCProof.

Definition at line 123 of file LFSCLraProof.h.

References d_pf.

virtual LFSCLraPoly* LFSCLraPoly::AsLFSCLraPoly ( ) [inline, virtual]

Reimplemented from LFSCProof.

Definition at line 125 of file LFSCLraProof.h.

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

Implements LFSCProof.

Definition at line 101 of file LFSCLraProof.cpp.

References d_var, kind_to_str(), get_normalized(), d_op, get_not(), CVC3::abs(), and d_pf.

static LFSCProof* LFSCLraPoly::Make ( LFSCProof pf,
int  var,
int  op 
) [inline, static]
LFSCProof * LFSCLraPoly::Make ( const Expr e,
LFSCProof p 
) [static]
LFSCProof* LFSCLraPoly::clone ( ) [inline, virtual]

Implements LFSCProof.

Definition at line 131 of file LFSCLraProof.h.

References LFSCLraPoly(), d_pf, RefPtr::get(), d_var, and d_op.

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

Reimplemented from LFSCProof.

Definition at line 132 of file LFSCLraProof.h.

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

Reimplemented from LFSCProof.

Definition at line 133 of file LFSCLraProof.h.

References d_pf, and RefPtr::get().

int LFSCLraPoly::checkOp ( ) [inline, virtual]

Reimplemented from LFSCProof.

Definition at line 134 of file LFSCLraProof.h.

References get_normalized(), d_op, and d_var.


Member Data Documentation

Definition at line 113 of file LFSCLraProof.h.

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

int LFSCLraPoly::d_var [private]

Definition at line 114 of file LFSCLraProof.h.

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

int LFSCLraPoly::d_op [private]

Definition at line 115 of file LFSCLraProof.h.

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


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