CVC3
Public Member Functions | Static Public Member Functions | Protected Member Functions | Protected Attributes | Static Protected Attributes | Friends

LFSCProof Class Reference

#include <LFSCProof.h>

Inherits LFSCObj.

Inherited by LFSCAssume, LFSCBoolRes, LFSCClausify, LFSCLem, LFSCLraAdd, LFSCLraAxiom, LFSCLraContra, LFSCLraMulC, LFSCLraPoly, LFSCLraSub, LFSCPfLambda, LFSCPfLet, LFSCPfVar, LFSCProofExpr, and LFSCProofGeneric.

Collaboration diagram for LFSCProof:
Collaboration graph
[legend]

List of all members.

Public Member Functions

Static Public Member Functions

Protected Member Functions

Protected Attributes

Static Protected Attributes

Friends

Detailed Description

Definition at line 26 of file LFSCProof.h.

Constructor & Destructor Documentation

LFSCProof::LFSCProof ( ) [protected]

Definition at line 11 of file LFSCProof.cpp.

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

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]

Reimplemented in LFSCBoolRes, LFSCLem, LFSCClausify, LFSCAssume, LFSCLraAdd, LFSCLraAxiom, LFSCLraMulC, LFSCLraSub, LFSCLraPoly, LFSCLraContra, LFSCProofExpr, LFSCPfVar, LFSCPfLambda, LFSCProofGeneric, and LFSCPfLet.

Definition at line 43 of file LFSCProof.h.

Referenced by get_string_length().

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 lambdaCounter, and lambdaMap.

Referenced by LFSCConvert::make_let_proof().

void LFSCProof::print ( std::ostream &  s,
int  ind = 0 
)

Definition at line 23 of file LFSCProof.cpp.

References Obj::indent(), lambdaMap, lambdaPrintMap, print(), print_pf(), Obj::print_warning(), printCounter, and rplProof.

Referenced by print(), and print_structure().

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

Implemented in LFSCBoolRes, LFSCLem, LFSCClausify, LFSCAssume, LFSCLraAdd, LFSCLraAxiom, LFSCLraMulC, LFSCLraSub, LFSCLraPoly, LFSCLraContra, LFSCProofExpr, LFSCPfVar, LFSCPfLambda, LFSCProofGeneric, and LFSCPfLet.

Referenced by print().

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

Reimplemented in LFSCLraAxiom.

Definition at line 72 of file LFSCProof.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCLraSub::Make(), LFSCLraMulC::Make(), LFSCLraAdd::Make(), and LFSCBoolRes::Make().

long int LFSCProof::get_string_length ( ) [inline]

Definition at line 73 of file LFSCProof.h.

References get_length(), get_string_length(), getChild(), getNumChildren(), and strLen.

Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCProofGeneric::get_length(), and get_string_length().

void LFSCProof::print_structure ( std::ostream &  s,
int  ind = 0 
)

Definition at line 43 of file LFSCProof.cpp.

References Obj::indent(), lambdaMap, lambdaPrintMap, print(), print_struct(), Obj::print_warning(), printCounter, and rplProof.

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

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

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 fillHoles(), getChild(), and getNumChildren().

Referenced by fillHoles().

virtual LFSCProof* LFSCProof::clone ( ) [pure virtual]

Implemented in LFSCBoolRes, LFSCLem, LFSCClausify, LFSCAssume, LFSCLraAdd, LFSCLraAxiom, LFSCLraMulC, LFSCLraSub, LFSCLraPoly, LFSCLraContra, LFSCProofExpr, LFSCPfVar, LFSCPfLambda, LFSCProofGeneric, and LFSCPfLet.

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

Reimplemented in LFSCBoolRes, LFSCClausify, LFSCAssume, LFSCLraAdd, LFSCLraMulC, LFSCLraSub, LFSCLraPoly, LFSCLraContra, LFSCPfLambda, and LFSCProofGeneric.

Definition at line 100 of file LFSCProof.h.

Referenced by checkOp(), fillHoles(), and get_string_length().

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

Reimplemented in LFSCBoolRes, LFSCClausify, LFSCAssume, LFSCLraAdd, LFSCLraMulC, LFSCLraSub, LFSCLraPoly, LFSCLraContra, LFSCPfLambda, and LFSCProofGeneric.

Definition at line 101 of file LFSCProof.h.

Referenced by checkOp(), fillHoles(), get_string_length(), and TReturn::normalize_to_tf().

int LFSCProof::checkOp ( ) [virtual]

Reimplemented in LFSCLraAdd, LFSCLraAxiom, LFSCLraMulC, LFSCLraSub, LFSCLraPoly, and LFSCLraContra.

Definition at line 83 of file LFSCProof.cpp.

References checkOp(), chOp, getChild(), and getNumChildren().

Referenced by checkOp(), LFSCLraContra::LFSCLraContra(), LFSCLraMulC::LFSCLraMulC(), LFSCLraPoly::LFSCLraPoly(), LFSCLraSub::LFSCLraSub(), and LFSCLraAdd::Make().

int LFSCProof::getChOp ( ) [inline]

Definition at line 103 of file LFSCProof.h.

References chOp.

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

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

Definition at line 104 of file LFSCProof.h.

References chOp.

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

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

Reimplemented in LFSCBoolRes, LFSCLem, LFSCClausify, and LFSCAssume.

Definition at line 105 of file LFSCProof.h.

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

Definition at line 104 of file LFSCProof.cpp.

References CVC3::abs(), AND, CVC3::Expr::arity(), LFSCObj::cascade_expr(), LFSCObj::d_and_final_s, LFSCObj::d_and_mid_s, LFSCObj::d_iff_s, LFSCObj::d_imp_s, LFSCObj::d_ite_s, LFSCObj::d_or_final_s, LFSCObj::d_or_mid_s, std::endl(), RefPtr< T >::get(), CVC3::Expr::getKind(), LFSCProofGeneric::Make(), LFSCAssume::Make(), LFSCClausify::Make(), LFSCPfVar::Make(), Make_and_elim(), LFSCProofGeneric::MakeStr(), NOT, Obj::print_error(), and LFSCObj::queryM().

Referenced by LFSCConvert::cvc3_to_lfsc().

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]

Definition at line 397 of file LFSCProof.cpp.

References CVC3::Expr::arity(), LFSCObj::cascade_expr(), LFSCProofGeneric::Make(), and Obj::print_error().

Referenced by LFSCConvert::cvc3_to_lfsc(), and Make_CNF().

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 get_proof_counter(), and LFSCProof().

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

Definition at line 29 of file LFSCProof.h.

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

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

Definition at line 30 of file LFSCProof.h.

Referenced by print(), LFSCPfLet::print_pf(), LFSCPfLambda::print_pf(), LFSCPfLet::print_struct(), and print_structure().

int LFSCProof::printCounter [protected]

Definition at line 31 of file LFSCProof.h.

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

LFSCProof* LFSCProof::rplProof [protected]

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 get_string_length(), and LFSCProof().

int LFSCProof::chOp [protected]

Definition at line 35 of file LFSCProof.h.

Referenced by checkOp(), getChOp(), LFSCProof(), 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:
Generated on Thu Sep 1 2011 19:35:09 for CVC3 by  doxygen 1.7.3