CVC3
Public Member Functions | Static Public Member Functions | Private Member Functions | Private Attributes | List of all members
LFSCPfLet Class Reference

#include <LFSCUtilProof.h>

Inherits LFSCProof.

Collaboration diagram for LFSCPfLet:
Collaboration graph

Public Member Functions

virtual LFSCPfLetAsLFSCPfLet ()
 
void print_pf (std::ostream &s, int ind=0)
 
void print_struct (std::ostream &s, int ind=0)
 
LFSCProofclone ()
 
- Public Member Functions inherited from LFSCProof
virtual LFSCProofExprAsLFSCProofExpr ()
 
virtual LFSCLraAddAsLFSCLraAdd ()
 
virtual LFSCLraSubAsLFSCLraSub ()
 
virtual LFSCLraMulCAsLFSCLraMulC ()
 
virtual LFSCLraAxiomAsLFSCLraAxiom ()
 
virtual LFSCLraContraAsLFSCLraContra ()
 
virtual LFSCLraPolyAsLFSCLraPoly ()
 
virtual LFSCBoolResAsLFSCBoolRes ()
 
virtual LFSCLemAsLFSCLem ()
 
virtual LFSCClausifyAsLFSCClausify ()
 
virtual LFSCAssumeAsLFSCAssume ()
 
virtual LFSCProofGenericAsLFSCProofGeneric ()
 
virtual LFSCPfVarAsLFSCPfVar ()
 
virtual LFSCPfLambdaAsLFSCPfLambda ()
 
virtual bool isLraMulC ()
 
void print (std::ostream &s, int ind=0)
 
virtual bool isTrivial ()
 
long int get_string_length ()
 
void print_structure (std::ostream &s, int ind=0)
 
void setRplProof (LFSCProof *p)
 
virtual void fillHoles ()
 
virtual int getNumChildren ()
 
virtual LFSCProofgetChild (int n)
 
virtual int checkOp ()
 
int getChOp ()
 
void setChOp (int c)
 
virtual int checkBoolRes (std::vector< int > &clause)
 
- Public Member Functions inherited from LFSCObj
 LFSCObj ()
 
- Public Member Functions inherited from Obj
 Obj ()
 
virtual ~Obj ()
 
int GetRefCount ()
 get ref count
 
void Ref ()
 reference
 
void Unref ()
 unreference
 

Static Public Member Functions

static LFSCProofMake (LFSCProof *letPf, LFSCPfVar *pv, LFSCProof *body, bool isTh, std::vector< int > &fv)
 
- Static Public Member Functions inherited from LFSCProof
static int make_lambda (LFSCProof *p)
 
static LFSCProofMake_CNF (const Expr &form, const Expr &reason, int pos)
 
static LFSCProofMake_not_not_elim (const Expr &pf, LFSCProof *p)
 
static LFSCProofMake_mimic (const Expr &pf, LFSCProof *p, int numHoles)
 
static LFSCProofMake_and_elim (const Expr &form, LFSCProof *p, int n, const Expr &expected)
 
static int get_proof_counter ()
 
- Static Public Member Functions inherited from LFSCObj
static void initialize (const Expr &pf_expr, int lfscm)
 
- Static Public Member Functions inherited from Obj
static void print_error (const char *c, std::ostream &s)
 
static void print_warning (const char *c)
 
static void initialize ()
 

Private Member Functions

 LFSCPfLet (LFSCProof *letPf, LFSCPfVar *pv, LFSCProof *body, bool isTh, LFSCProof *letPfRpl, LFSCProof *pvRpl)
 
 LFSCPfLet (LFSCProof *letPf, LFSCPfVar *pv, LFSCProof *body, bool isTh, std::vector< int > &fv)
 
virtual ~LFSCPfLet ()
 
long int get_length ()
 

Private Attributes

RefPtr< LFSCProofd_letPf
 
RefPtr< LFSCPfVard_pv
 
RefPtr< LFSCProofd_body
 
RefPtr< LFSCProofd_letPfRpl
 
RefPtr< LFSCProofd_pvRpl
 
bool d_isTh
 

Additional Inherited Members

- Protected Member Functions inherited from LFSCProof
 LFSCProof ()
 
virtual ~LFSCProof ()
 
- Static Protected Member Functions inherited from LFSCObj
static int getNumNodes (const Expr &pf, bool recount=false)
 
static Expr cascade_expr (const Expr &e)
 
static void define_skolem_vars (const Expr &e)
 
static bool isVar (const Expr &e)
 
static void collect_vars (const Expr &e, bool readPred=true)
 
static Expr queryElimNotNot (const Expr &expr)
 
static Expr queryAtomic (const Expr &expr, bool getBase=false)
 
static int queryM (const Expr &expr, bool add=true, bool trusted=false)
 
static int queryMt (const Expr &expr)
 
static int queryT (const Expr &e)
 
static bool getY (const Expr &e, Expr &pe, bool doIff=true, bool doLogic=true)
 
static bool isFormula (const Expr &e)
 
static bool can_pnorm (const Expr &e)
 
static bool what_is_proven (const Expr &pf, Expr &pe)
 
- Protected Attributes inherited from LFSCProof
int printCounter
 
LFSCProofrplProof
 
long int strLen
 
int chOp
 
int assumeVar
 
int assumeVarUsed
 
std::vector< int > br
 
bool brComputed
 
- Static Protected Attributes inherited from LFSCProof
static int pf_counter = 0
 
static std::map< LFSCProof *, int > lambdaMap
 
static std::map< LFSCProof
*, LFSCProof * > 
lambdaPrintMap
 
static int lambdaCounter = 1
 

Detailed Description

Definition at line 95 of file LFSCUtilProof.h.

Constructor & Destructor Documentation

LFSCPfLet::LFSCPfLet ( LFSCProof letPf,
LFSCPfVar pv,
LFSCProof body,
bool  isTh,
LFSCProof letPfRpl,
LFSCProof pvRpl 
)
inlineprivate

Definition at line 105 of file LFSCUtilProof.h.

Referenced by clone(), and Make().

LFSCPfLet::LFSCPfLet ( LFSCProof letPf,
LFSCPfVar pv,
LFSCProof body,
bool  isTh,
std::vector< int > &  fv 
)
private
virtual LFSCPfLet::~LFSCPfLet ( )
inlineprivatevirtual

Definition at line 110 of file LFSCUtilProof.h.

Member Function Documentation

long int LFSCPfLet::get_length ( )
inlineprivatevirtual

Reimplemented from LFSCProof.

Definition at line 111 of file LFSCUtilProof.h.

References d_body, d_letPf, d_pv, and LFSCProof::get_string_length().

virtual LFSCPfLet* LFSCPfLet::AsLFSCPfLet ( )
inlinevirtual

Reimplemented from LFSCProof.

Definition at line 115 of file LFSCUtilProof.h.

void LFSCPfLet::print_pf ( std::ostream &  s,
int  ind = 0 
)
virtual
void LFSCPfLet::print_struct ( std::ostream &  s,
int  ind = 0 
)
virtual

Reimplemented from LFSCProof.

Definition at line 169 of file LFSCUtilProof.cpp.

References d_body, d_letPf, d_pv, RefPtr< T >::get(), LFSCProof::lambdaPrintMap, and LFSCProof::print_structure().

static LFSCProof* LFSCPfLet::Make ( LFSCProof letPf,
LFSCPfVar pv,
LFSCProof body,
bool  isTh,
std::vector< int > &  fv 
)
inlinestatic

Definition at line 118 of file LFSCUtilProof.h.

References LFSCPfLet().

Referenced by LFSCConvert::make_let_proof().

LFSCProof* LFSCPfLet::clone ( )
inlinevirtual

Implements LFSCProof.

Definition at line 122 of file LFSCUtilProof.h.

References d_body, d_isTh, d_letPf, d_letPfRpl, d_pv, d_pvRpl, RefPtr< T >::get(), and LFSCPfLet().

Member Data Documentation

RefPtr< LFSCProof > LFSCPfLet::d_letPf
private

Definition at line 97 of file LFSCUtilProof.h.

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

RefPtr< LFSCPfVar > LFSCPfLet::d_pv
private

Definition at line 98 of file LFSCUtilProof.h.

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

RefPtr< LFSCProof > LFSCPfLet::d_body
private

Definition at line 99 of file LFSCUtilProof.h.

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

RefPtr< LFSCProof > LFSCPfLet::d_letPfRpl
private

Definition at line 101 of file LFSCUtilProof.h.

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

RefPtr< LFSCProof > LFSCPfLet::d_pvRpl
private

Definition at line 103 of file LFSCUtilProof.h.

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

bool LFSCPfLet::d_isTh
private

Definition at line 104 of file LFSCUtilProof.h.

Referenced by clone(), and print_pf().


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