CVC3  2.4.1
Public Member Functions | Static Public Member Functions | Protected Member Functions | Protected Attributes | Static Protected Attributes | Friends
LFSCProof Class Reference

#include <LFSCProof.h>

Inheritance diagram for LFSCProof:
LFSCObj Obj LFSCAssume LFSCBoolRes LFSCClausify LFSCLem LFSCLraAdd LFSCLraAxiom LFSCLraContra LFSCLraMulC LFSCLraPoly LFSCLraSub LFSCPfLambda LFSCPfLet LFSCPfVar LFSCProofExpr LFSCProofGeneric

List of all members.

Public Member Functions

Static Public Member Functions

Protected Member Functions

Protected Attributes

Static Protected Attributes

Friends


Constructor & Destructor Documentation

LFSCProof::LFSCProof ( ) [protected]

Definition at line 11 of file LFSCProof.cpp.

References pf_counter, printCounter, strLen, rplProof, chOp, brComputed, assumeVar, and assumeVarUsed.

virtual LFSCProof::~LFSCProof ( ) [inline, protected, virtual]

Definition at line 44 of file LFSCProof.h.


Member Function Documentation

virtual long int LFSCProof::get_length ( ) [inline, protected, virtual]
virtual LFSCProofExpr* LFSCProof::AsLFSCProofExpr ( ) [inline, virtual]

Reimplemented in LFSCProofExpr.

Definition at line 46 of file LFSCProof.h.

virtual LFSCLraAdd* LFSCProof::AsLFSCLraAdd ( ) [inline, virtual]

Reimplemented in LFSCLraAdd.

Definition at line 47 of file LFSCProof.h.

virtual LFSCLraSub* LFSCProof::AsLFSCLraSub ( ) [inline, virtual]

Reimplemented in LFSCLraSub.

Definition at line 48 of file LFSCProof.h.

virtual LFSCLraMulC* LFSCProof::AsLFSCLraMulC ( ) [inline, virtual]

Reimplemented in LFSCLraMulC.

Definition at line 49 of file LFSCProof.h.

Referenced by LFSCLraMulC::Make().

virtual LFSCLraAxiom* LFSCProof::AsLFSCLraAxiom ( ) [inline, virtual]

Reimplemented in LFSCLraAxiom.

Definition at line 50 of file LFSCProof.h.

virtual LFSCLraContra* LFSCProof::AsLFSCLraContra ( ) [inline, virtual]

Reimplemented in LFSCLraContra.

Definition at line 51 of file LFSCProof.h.

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

Reimplemented in LFSCLraPoly.

Definition at line 52 of file LFSCProof.h.

Referenced by TReturn::normalize_to_tf().

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

Reimplemented in LFSCBoolRes.

Definition at line 53 of file LFSCProof.h.

virtual LFSCLem* LFSCProof::AsLFSCLem ( ) [inline, virtual]

Reimplemented in LFSCLem.

Definition at line 54 of file LFSCProof.h.

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

Reimplemented in LFSCClausify.

Definition at line 55 of file LFSCProof.h.

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

Reimplemented in LFSCAssume.

Definition at line 56 of file LFSCProof.h.

virtual LFSCProofGeneric* LFSCProof::AsLFSCProofGeneric ( ) [inline, virtual]

Reimplemented in LFSCProofGeneric.

Definition at line 57 of file LFSCProof.h.

virtual LFSCPfVar* LFSCProof::AsLFSCPfVar ( ) [inline, virtual]

Reimplemented in LFSCPfVar.

Definition at line 58 of file LFSCProof.h.

virtual LFSCPfLambda* LFSCProof::AsLFSCPfLambda ( ) [inline, virtual]

Reimplemented in LFSCPfLambda.

Definition at line 59 of file LFSCProof.h.

virtual LFSCPfLet* LFSCProof::AsLFSCPfLet ( ) [inline, virtual]

Reimplemented in LFSCPfLet.

Definition at line 60 of file LFSCProof.h.

virtual bool LFSCProof::isLraMulC ( ) [inline, virtual]

Reimplemented in LFSCLraMulC.

Definition at line 62 of file LFSCProof.h.

static int LFSCProof::make_lambda ( LFSCProof p) [inline, static]

Definition at line 63 of file LFSCProof.h.

References lambdaMap, and lambdaCounter.

Referenced by LFSCConvert::make_let_proof().

void LFSCProof::print ( std::ostream s,
int  ind = 0 
)
virtual void LFSCProof::print_pf ( std::ostream s,
int  ind = 0 
) [pure virtual]
virtual bool LFSCProof::isTrivial ( ) [inline, virtual]
long int LFSCProof::get_string_length ( ) [inline]
void LFSCProof::print_structure ( std::ostream s,
int  ind = 0 
)
virtual void LFSCProof::print_struct ( std::ostream s,
int  ind = 0 
) [inline, virtual]

Reimplemented in LFSCPfLet, LFSCAssume, LFSCClausify, LFSCLem, LFSCPfVar, and LFSCBoolRes.

Definition at line 86 of file LFSCProof.h.

Referenced by print_structure().

void LFSCProof::setRplProof ( LFSCProof p) [inline]

Definition at line 91 of file LFSCProof.h.

References rplProof.

void LFSCProof::fillHoles ( ) [virtual]

Reimplemented in LFSCProofExpr.

Definition at line 61 of file LFSCProof.cpp.

References getNumChildren(), getChild(), and fillHoles().

Referenced by fillHoles().

virtual LFSCProof* LFSCProof::clone ( ) [pure virtual]
virtual int LFSCProof::getNumChildren ( ) [inline, virtual]
virtual LFSCProof* LFSCProof::getChild ( int  n) [inline, virtual]
int LFSCProof::checkOp ( ) [virtual]
int LFSCProof::getChOp ( ) [inline]

Definition at line 103 of file LFSCProof.h.

References chOp.

Referenced by TReturn::normalize_tr(), and TReturn::normalize_to_tf().

void LFSCProof::setChOp ( int  c) [inline]

Definition at line 104 of file LFSCProof.h.

References chOp.

Referenced by LFSCLraPoly::Make(), TReturn::normalize_tr(), and TReturn::normalize_to_tf().

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

Reimplemented in LFSCAssume, LFSCClausify, LFSCLem, and LFSCBoolRes.

Definition at line 105 of file LFSCProof.h.

LFSCProof * LFSCProof::Make_CNF ( const Expr form,
const Expr reason,
int  pos 
) [static]
LFSCProof * LFSCProof::Make_not_not_elim ( const Expr pf,
LFSCProof p 
) [static]

Definition at line 372 of file LFSCProof.cpp.

References CVC3::Expr::isNot(), and LFSCProofGeneric::Make().

Referenced by LFSCConvert::cvc3_to_lfsc().

LFSCProof * LFSCProof::Make_mimic ( const Expr pf,
LFSCProof p,
int  numHoles 
) [static]

Definition at line 384 of file LFSCProof.cpp.

References LFSCProofGeneric::Make().

Referenced by LFSCConvert::cvc3_to_lfsc().

LFSCProof * LFSCProof::Make_and_elim ( const Expr form,
LFSCProof p,
int  n,
const Expr expected 
) [static]
static int LFSCProof::get_proof_counter ( ) [inline, static]

Definition at line 114 of file LFSCProof.h.

References pf_counter.


Friends And Related Function Documentation

friend class LFSCPrinter [friend]

Reimplemented in LFSCClausify.

Definition at line 97 of file LFSCProof.h.


Member Data Documentation

int LFSCProof::pf_counter = 0 [static, protected]

Definition at line 28 of file LFSCProof.h.

Referenced by LFSCProof(), and get_proof_counter().

std::map< LFSCProof *, int > LFSCProof::lambdaMap [static, protected]

Definition at line 29 of file LFSCProof.h.

Referenced by print(), print_structure(), and make_lambda().

int LFSCProof::printCounter [protected]

Definition at line 31 of file LFSCProof.h.

Referenced by LFSCProof(), print(), and print_structure().

Definition at line 32 of file LFSCProof.h.

Referenced by LFSCProof(), print(), print_structure(), and setRplProof().

int LFSCProof::lambdaCounter = 1 [static, protected]

Definition at line 33 of file LFSCProof.h.

Referenced by make_lambda().

long int LFSCProof::strLen [protected]

Definition at line 34 of file LFSCProof.h.

Referenced by LFSCProof(), and get_string_length().

int LFSCProof::chOp [protected]

Definition at line 35 of file LFSCProof.h.

Referenced by LFSCProof(), checkOp(), getChOp(), and setChOp().

int LFSCProof::assumeVar [protected]

Definition at line 36 of file LFSCProof.h.

Referenced by LFSCProof().

int LFSCProof::assumeVarUsed [protected]

Definition at line 37 of file LFSCProof.h.

Referenced by LFSCProof().

std::vector< int > LFSCProof::br [protected]

Definition at line 39 of file LFSCProof.h.

bool LFSCProof::brComputed [protected]

Definition at line 40 of file LFSCProof.h.

Referenced by LFSCProof().


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