LFSCLem Class Reference

#include <LFSCBoolProof.h>

Inherits LFSCProof.

Collaboration diagram for LFSCLem:

Public Member Functions
virtual LFSCLem *	AsLFSCLem ()
void	print_pf (std::ostream &s, int ind=0)
void	print_struct (std::ostream &s, int ind=0)
bool	IsTrivial ()
LFSCProof *	clone ()
int	checkBoolRes (std::vector< int > &clause)
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 LFSCClausify *	AsLFSCClausify ()
virtual LFSCAssume *	AsLFSCAssume ()
virtual LFSCProofGeneric *	AsLFSCProofGeneric ()
virtual LFSCPfVar *	AsLFSCPfVar ()
virtual LFSCPfLambda *	AsLFSCPfLambda ()
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)
void	setRplProof (LFSCProof *p)
virtual void	fillHoles ()
virtual int	getNumChildren ()
virtual LFSCProof *	getChild (int n)
virtual int	checkOp ()
int	getChOp ()
void	setChOp (int c)
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 (int v)
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
	LFSCLem (int v)
virtual	~LFSCLem ()
long int	get_length ()

Private Attributes
int	d_var

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 38 of file LFSCBoolProof.h.

Constructor & Destructor Documentation

LFSCLem::LFSCLem ( int  v )

inlineprivate

Definition at line 42 of file LFSCBoolProof.h.

Referenced by clone(), and Make().

virtual LFSCLem::~LFSCLem ( )

inlineprivatevirtual

Definition at line 44 of file LFSCBoolProof.h.

Member Function Documentation

long int LFSCLem::get_length ( )

inlineprivatevirtual

Reimplemented from LFSCProof.

Definition at line 45 of file LFSCBoolProof.h.

virtual LFSCLem* LFSCLem::AsLFSCLem ( )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 47 of file LFSCBoolProof.h.

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

inlinevirtual

Implements LFSCProof.

Definition at line 48 of file LFSCBoolProof.h.

References CVC3::abs(), and d_var.

void LFSCLem::print_struct ( std::ostream &  s, int  ind = 0  )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 49 of file LFSCBoolProof.h.

References d_var.

static LFSCProof* LFSCLem::Make ( int  v )

inlinestatic

Definition at line 50 of file LFSCBoolProof.h.

References LFSCLem().

Referenced by LFSCConvert::cvc3_to_lfsc().

bool LFSCLem::IsTrivial ( )

inline

Definition at line 51 of file LFSCBoolProof.h.

LFSCProof* LFSCLem::clone ( )

inlinevirtual

Implements LFSCProof.

Definition at line 52 of file LFSCBoolProof.h.

References d_var, and LFSCLem().

int LFSCLem::checkBoolRes ( std::vector< int > &  clause )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 53 of file LFSCBoolProof.h.

References d_var.

Member Data Documentation

int LFSCLem::d_var

private

Definition at line 41 of file LFSCBoolProof.h.

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

---

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

• LFSCBoolProof.h