CVC3  2.4.1
Public Member Functions | Static Public Member Functions | Private Member Functions | Static Private Member Functions | Private Attributes | Friends
LFSCClausify Class Reference

#include <LFSCBoolProof.h>

Inheritance diagram for LFSCClausify:
LFSCProof LFSCObj Obj

List of all members.

Public Member Functions

Static Public Member Functions

Private Member Functions

Static Private Member Functions

Private Attributes

Friends


Constructor & Destructor Documentation

LFSCClausify::LFSCClausify ( int  v,
LFSCProof pf 
) [inline, private]

Definition at line 66 of file LFSCBoolProof.h.

Referenced by Make(), and clone().

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

Definition at line 67 of file LFSCBoolProof.h.


Member Function Documentation

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

Reimplemented from LFSCProof.

Definition at line 68 of file LFSCBoolProof.h.

References d_pf.

LFSCProof * LFSCClausify::Make_i ( const Expr e,
LFSCProof p,
std::vector< Expr > &  exprs,
const Expr end 
) [static, private]

Definition at line 134 of file LFSCBoolProof.cpp.

References CVC3::Expr::getKind(), OR, Make(), LFSCObj::queryM(), and CVC3::abs().

Referenced by Make().

virtual LFSCClausify* LFSCClausify::AsLFSCClausify ( ) [inline, virtual]

Reimplemented from LFSCProof.

Definition at line 72 of file LFSCBoolProof.h.

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

Implements LFSCProof.

Definition at line 114 of file LFSCBoolProof.cpp.

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

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

Reimplemented from LFSCProof.

Definition at line 74 of file LFSCBoolProof.h.

References d_var.

static LFSCProof* LFSCClausify::Make ( int  v,
LFSCProof pf 
) [inline, static]
LFSCProof * LFSCClausify::Make ( const Expr e,
LFSCProof p,
bool  cascadeOr = false 
) [static]
LFSCProof* LFSCClausify::clone ( ) [inline, virtual]

Implements LFSCProof.

Definition at line 80 of file LFSCBoolProof.h.

References LFSCClausify(), d_var, d_pf, and RefPtr::get().

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

Reimplemented from LFSCProof.

Definition at line 81 of file LFSCBoolProof.h.

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

Reimplemented from LFSCProof.

Definition at line 82 of file LFSCBoolProof.h.

References d_pf, and RefPtr::get().

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

Reimplemented from LFSCProof.

Definition at line 83 of file LFSCBoolProof.h.

References d_pf, and d_var.


Friends And Related Function Documentation

friend class LFSCPrinter [friend]

Reimplemented from LFSCProof.

Definition at line 63 of file LFSCBoolProof.h.


Member Data Documentation

int LFSCClausify::d_var [private]

Definition at line 64 of file LFSCBoolProof.h.

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

Definition at line 65 of file LFSCBoolProof.h.

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


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