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

#include <LFSCBoolProof.h>

Inheritance diagram for LFSCAssume:
LFSCProof LFSCObj Obj

List of all members.

Public Member Functions

Static Public Member Functions

Private Member Functions

Private Attributes


Constructor & Destructor Documentation

LFSCAssume::LFSCAssume ( int  v,
LFSCProof pf,
bool  assm,
int  type 
) [inline, private]

Definition at line 96 of file LFSCBoolProof.h.

Referenced by Make(), and clone().

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

Definition at line 97 of file LFSCBoolProof.h.


Member Function Documentation

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

Reimplemented from LFSCProof.

Definition at line 98 of file LFSCBoolProof.h.

References d_pf.

virtual LFSCAssume* LFSCAssume::AsLFSCAssume ( ) [inline, virtual]

Reimplemented from LFSCProof.

Definition at line 100 of file LFSCBoolProof.h.

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

Implements LFSCProof.

Definition at line 161 of file LFSCBoolProof.cpp.

References d_assm, d_var, d_type, CVC3::abs(), and d_pf.

void LFSCAssume::print_struct ( std::ostream s,
int  ind = 0 
) [virtual]

Reimplemented from LFSCProof.

Definition at line 172 of file LFSCBoolProof.cpp.

References d_assm, d_var, and d_pf.

static LFSCProof* LFSCAssume::Make ( int  v,
LFSCProof pf,
bool  assm = true,
int  type = 3 
) [inline, static]
LFSCProof* LFSCAssume::clone ( ) [inline, virtual]

Implements LFSCProof.

Definition at line 106 of file LFSCBoolProof.h.

References LFSCAssume(), d_var, d_pf, RefPtr::get(), d_assm, and d_type.

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

Reimplemented from LFSCProof.

Definition at line 107 of file LFSCBoolProof.h.

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

Reimplemented from LFSCProof.

Definition at line 108 of file LFSCBoolProof.h.

References d_pf, and RefPtr::get().

int LFSCAssume::checkBoolRes ( std::vector< int > &  clause) [inline, virtual]

Reimplemented from LFSCProof.

Definition at line 110 of file LFSCBoolProof.h.

References d_type, d_pf, and d_var.


Member Data Documentation

int LFSCAssume::d_var [private]

Definition at line 92 of file LFSCBoolProof.h.

Referenced by print_pf(), print_struct(), clone(), and checkBoolRes().

Definition at line 93 of file LFSCBoolProof.h.

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

bool LFSCAssume::d_assm [private]

Definition at line 94 of file LFSCBoolProof.h.

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

int LFSCAssume::d_type [private]

Definition at line 95 of file LFSCBoolProof.h.

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


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