LFSCPfLambda Class Reference

#include <LFSCUtilProof.h>

Inherits LFSCProof.

Collaboration diagram for LFSCPfLambda:

Public Member Functions
virtual LFSCPfLambda *	AsLFSCPfLambda ()
void	print_pf (std::ostream &s, int ind=0)
LFSCProof *	clone ()
int	getNumChildren ()
LFSCProof *	getChild (int n)
Public Member Functions inherited from LFSCProof
virtual LFSCProofExpr *	AsLFSCProofExpr ()
virtual LFSCLraAdd *	AsLFSCLraAdd ()
virtual LFSCLraSub *	AsLFSCLraSub ()
virtual LFSCLraMulC *	AsLFSCLraMulC ()
virtual LFSCLraAxiom *	AsLFSCLraAxiom ()
virtual LFSCLraContra *	AsLFSCLraContra ()
virtual LFSCLraPoly *	AsLFSCLraPoly ()
virtual LFSCBoolRes *	AsLFSCBoolRes ()
virtual LFSCLem *	AsLFSCLem ()
virtual LFSCClausify *	AsLFSCClausify ()
virtual LFSCAssume *	AsLFSCAssume ()
virtual LFSCProofGeneric *	AsLFSCProofGeneric ()
virtual LFSCPfVar *	AsLFSCPfVar ()
virtual LFSCPfLet *	AsLFSCPfLet ()
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)
virtual void	print_struct (std::ostream &s, int ind=0)
void	setRplProof (LFSCProof *p)
virtual void	fillHoles ()
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 LFSCProof *	Make (LFSCPfVar *v, LFSCProof *bd, LFSCProof *aVal=NULL)
Static Public Member Functions inherited from LFSCProof
static int	make_lambda (LFSCProof *p)
static LFSCProof *	Make_CNF (const Expr &form, const Expr &reason, int pos)
static LFSCProof *	Make_not_not_elim (const Expr &pf, LFSCProof *p)
static LFSCProof *	Make_mimic (const Expr &pf, LFSCProof *p, int numHoles)
static LFSCProof *	Make_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
	LFSCPfLambda (LFSCPfVar *v, LFSCProof *bd, LFSCProof *aVal=NULL)
virtual	~LFSCPfLambda ()
long int	get_length ()

Private Attributes
RefPtr< LFSCPfVar >	pfV
RefPtr< LFSCProof >	body
RefPtr< LFSCProof >	abstVal

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
LFSCProof *	rplProof
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 39 of file LFSCUtilProof.h.

Constructor & Destructor Documentation

LFSCPfLambda::LFSCPfLambda ( LFSCPfVar *  v, LFSCProof *  bd, LFSCProof *  aVal = NULL  )

inlineprivate

Definition at line 46 of file LFSCUtilProof.h.

Referenced by clone(), and Make().

virtual LFSCPfLambda::~LFSCPfLambda ( )

inlineprivatevirtual

Definition at line 48 of file LFSCUtilProof.h.

Member Function Documentation

long int LFSCPfLambda::get_length ( )

inlineprivatevirtual

Reimplemented from LFSCProof.

Definition at line 49 of file LFSCUtilProof.h.

References body, LFSCProof::get_string_length(), and pfV.

virtual LFSCPfLambda* LFSCPfLambda::AsLFSCPfLambda ( )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 51 of file LFSCUtilProof.h.

void LFSCPfLambda::print_pf ( std::ostream &  s, int  ind = 0  )

virtual

Implements LFSCProof.

Definition at line 52 of file LFSCUtilProof.cpp.

References abstVal, body, RefPtr< T >::get(), LFSCProof::lambdaPrintMap, pfV, and LFSCProof::print().

static LFSCProof* LFSCPfLambda::Make ( LFSCPfVar *  v, LFSCProof *  bd, LFSCProof *  aVal = NULL  )

inlinestatic

Definition at line 53 of file LFSCUtilProof.h.

References LFSCPfLambda().

Referenced by LFSCPfLet::LFSCPfLet().

LFSCProof* LFSCPfLambda::clone ( )

inlinevirtual

Implements LFSCProof.

Definition at line 56 of file LFSCUtilProof.h.

References abstVal, body, RefPtr< T >::get(), LFSCPfLambda(), and pfV.

int LFSCPfLambda::getNumChildren ( )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 57 of file LFSCUtilProof.h.

LFSCProof* LFSCPfLambda::getChild ( int  n )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 58 of file LFSCUtilProof.h.

References body, RefPtr< T >::get(), and pfV.

Member Data Documentation

RefPtr< LFSCPfVar > LFSCPfLambda::pfV

private

Definition at line 41 of file LFSCUtilProof.h.

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

RefPtr< LFSCProof > LFSCPfLambda::body

private

Definition at line 42 of file LFSCUtilProof.h.

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

RefPtr< LFSCProof > LFSCPfLambda::abstVal

private

Definition at line 44 of file LFSCUtilProof.h.

Referenced by clone(), and print_pf().

---

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

• LFSCUtilProof.h
• LFSCUtilProof.cpp