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

#include <LFSCBoolProof.h>

Inheritance diagram for LFSCBoolRes:
LFSCProof LFSCObj Obj

List of all members.

Public Member Functions

Static Public Member Functions

Private Member Functions

Private Attributes


Constructor & Destructor Documentation

LFSCBoolRes::LFSCBoolRes ( LFSCProof pf1,
LFSCProof pf2,
int  v,
bool  col 
) [inline, private]

Definition at line 12 of file LFSCBoolProof.h.

References d_children.

Referenced by Make(), and clone().

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

Definition at line 17 of file LFSCBoolProof.h.


Member Function Documentation

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

Reimplemented from LFSCProof.

Definition at line 18 of file LFSCBoolProof.h.

References d_children.

virtual LFSCBoolRes* LFSCBoolRes::AsLFSCBoolRes ( ) [inline, virtual]

Reimplemented from LFSCProof.

Definition at line 22 of file LFSCBoolProof.h.

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

Implements LFSCProof.

Definition at line 7 of file LFSCBoolProof.cpp.

References d_col, CVC3::abs(), d_var, and d_children.

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

Reimplemented from LFSCProof.

Definition at line 24 of file LFSCBoolProof.cpp.

References d_var, and d_children.

LFSCProof * LFSCBoolRes::Make ( LFSCProof pf1,
LFSCProof pf2,
int  v,
bool  col 
) [static]

Definition at line 32 of file LFSCBoolProof.cpp.

References LFSCProof::isTrivial(), and LFSCBoolRes().

Referenced by Make(), MakeC(), and LFSCConvert::cvc3_to_lfsc().

LFSCProof * LFSCBoolRes::Make ( LFSCProof p1,
LFSCProof p2,
const Expr res,
const Expr pf,
bool  cascadeOr = false 
) [static]
LFSCProof * LFSCBoolRes::MakeC ( LFSCProof p,
const Expr res 
) [static]

Definition at line 93 of file LFSCBoolProof.cpp.

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

Referenced by Make().

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

Implements LFSCProof.

Definition at line 32 of file LFSCBoolProof.h.

References LFSCBoolRes(), d_children, d_var, and d_col.

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

Reimplemented from LFSCProof.

Definition at line 33 of file LFSCBoolProof.h.

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

Reimplemented from LFSCProof.

Definition at line 34 of file LFSCBoolProof.h.

References d_children, and RefPtr::get().

int LFSCBoolRes::checkBoolRes ( std::vector< int > &  clause) [virtual]

Reimplemented from LFSCProof.

Definition at line 41 of file LFSCBoolProof.cpp.

References d_children, d_var, and Obj::print_error().


Member Data Documentation

int LFSCBoolRes::d_var [private]

Definition at line 10 of file LFSCBoolProof.h.

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

bool LFSCBoolRes::d_col [private]

Definition at line 11 of file LFSCBoolProof.h.

Referenced by print_pf(), and clone().


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