LFSCPfVar Class Reference

#include <LFSCUtilProof.h>

Inherits LFSCProof.

Collaboration diagram for LFSCPfVar:

Public Member Functions
virtual LFSCPfVar *	AsLFSCPfVar ()
void	print_pf (std::ostream &s, int ind=0)
void	print_struct (std::ostream &s, int ind=0)
LFSCProof *	clone ()
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 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)
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 (const char *c, int v)
static LFSCProof *	MakeV (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
	LFSCPfVar (string nm)
virtual	~LFSCPfVar ()
long int	get_length ()

Private Attributes
string	name

Static Private Attributes
static std::map< int, RefPtr < LFSCProof > >	vMap

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 23 of file LFSCUtilProof.h.

Constructor & Destructor Documentation

LFSCPfVar::LFSCPfVar ( string  nm )

inlineprivate

Definition at line 27 of file LFSCUtilProof.h.

Referenced by clone(), and Make().

virtual LFSCPfVar::~LFSCPfVar ( )

inlineprivatevirtual

Definition at line 28 of file LFSCUtilProof.h.

Member Function Documentation

long int LFSCPfVar::get_length ( )

inlineprivatevirtual

Reimplemented from LFSCProof.

Definition at line 29 of file LFSCUtilProof.h.

References name.

virtual LFSCPfVar* LFSCPfVar::AsLFSCPfVar ( )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 31 of file LFSCUtilProof.h.

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

inlinevirtual

Implements LFSCProof.

Definition at line 32 of file LFSCUtilProof.h.

References name.

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

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 33 of file LFSCUtilProof.h.

References name.

LFSCProof * LFSCPfVar::Make ( const char *  c, int  v  )

static

Definition at line 33 of file LFSCUtilProof.cpp.

References LFSCPfVar().

Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCPfLet::LFSCPfLet(), LFSCProof::Make_CNF(), LFSCConvert::make_let_proof(), LFSCConvert::make_trusted(), MakeV(), TReturn::normalize_to_tf(), and TReturn::normalize_tr().

LFSCProof * LFSCPfVar::MakeV ( int  v )

static

Definition at line 40 of file LFSCUtilProof.cpp.

References RefPtr< T >::get(), Make(), and vMap.

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

LFSCProof* LFSCPfVar::clone ( )

inlinevirtual

Implements LFSCProof.

Definition at line 36 of file LFSCUtilProof.h.

References LFSCPfVar(), and name.

Member Data Documentation

std::map< int, RefPtr< LFSCProof > > LFSCPfVar::vMap

staticprivate

Definition at line 25 of file LFSCUtilProof.h.

Referenced by MakeV().

string LFSCPfVar::name

private

Definition at line 26 of file LFSCUtilProof.h.

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

---

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

• LFSCUtilProof.h
• LFSCUtilProof.cpp