LFSCProofGeneric Class Reference

#include <LFSCUtilProof.h>

Inherits LFSCProof.

Collaboration diagram for LFSCProofGeneric:

Public Member Functions
virtual LFSCProofGeneric *	AsLFSCProofGeneric ()
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 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)
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 (vector< RefPtr< LFSCProof > > &d_pfs, std::vector< string > &d_strs, bool db_str=false)
static LFSCProof *	Make (string str_pre, LFSCProof *sub_pf, string str_post, bool db_str=false)
static LFSCProof *	Make (string str_pre, LFSCProof *sub_pf1, LFSCProof *sub_pf2, string str_post, bool db_str=false)
static LFSCProof *	MakeStr (const char *c, bool db_str=false)
static LFSCProof *	MakeUnk ()
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
	LFSCProofGeneric (vector< RefPtr< LFSCProof > > &d_pfs, vector< string > &d_strs, bool db_str=false)
virtual	~LFSCProofGeneric ()
long int	get_length ()

Private Attributes
vector< RefPtr< LFSCProof > >	d_pf
vector< string >	d_str
bool	debug_str

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

Constructor & Destructor Documentation

LFSCProofGeneric::LFSCProofGeneric ( vector< RefPtr< LFSCProof > > &  d_pfs, vector< string > &  d_strs, bool  db_str = false  )

inlineprivate

Definition at line 67 of file LFSCUtilProof.h.

References d_pf, d_str, and debug_str.

Referenced by clone(), Make(), and MakeStr().

virtual LFSCProofGeneric::~LFSCProofGeneric ( )

inlineprivatevirtual

Definition at line 74 of file LFSCUtilProof.h.

Member Function Documentation

long int LFSCProofGeneric::get_length ( )

privatevirtual

Reimplemented from LFSCProof.

Definition at line 70 of file LFSCUtilProof.cpp.

References d_pf, d_str, debug_str, and LFSCProof::get_string_length().

virtual LFSCProofGeneric* LFSCProofGeneric::AsLFSCProofGeneric ( )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 77 of file LFSCUtilProof.h.

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

virtual

Implements LFSCProof.

Definition at line 81 of file LFSCUtilProof.cpp.

References d_pf, and d_str.

static LFSCProof* LFSCProofGeneric::Make ( vector< RefPtr< LFSCProof > > &  d_pfs, std::vector< string > &  d_strs, bool  db_str = false  )

inlinestatic

Definition at line 80 of file LFSCUtilProof.h.

References LFSCProofGeneric().

Referenced by LFSCConvert::convert(), LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), LFSCPfLet::LFSCPfLet(), LFSCProof::Make_and_elim(), LFSCProof::Make_CNF(), LFSCClausify::Make_i(), LFSCProof::Make_mimic(), LFSCProof::Make_not_not_elim(), LFSCBoolRes::MakeC(), and TReturn::normalize_tr().

LFSCProof * LFSCProofGeneric::Make ( string  str_pre, LFSCProof *  sub_pf, string  str_post, bool  db_str = false  )

static

Definition at line 90 of file LFSCUtilProof.cpp.

References LFSCProofGeneric().

LFSCProof * LFSCProofGeneric::Make ( string  str_pre, LFSCProof *  sub_pf1, LFSCProof *  sub_pf2, string  str_post, bool  db_str = false  )

static

Definition at line 100 of file LFSCUtilProof.cpp.

References LFSCProofGeneric().

LFSCProof * LFSCProofGeneric::MakeStr ( const char *  c, bool  db_str = false  )

static

Definition at line 113 of file LFSCUtilProof.cpp.

References LFSCProofGeneric().

Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCProof::Make_CNF(), LFSCConvert::make_trusted(), MakeUnk(), and TReturn::normalize_tr().

static LFSCProof* LFSCProofGeneric::MakeUnk ( )

inlinestatic

Definition at line 88 of file LFSCUtilProof.h.

References MakeStr().

Referenced by LFSCConvert::cvc3_to_lfsc().

LFSCProof* LFSCProofGeneric::clone ( )

inlinevirtual

Implements LFSCProof.

Definition at line 89 of file LFSCUtilProof.h.

References d_pf, d_str, debug_str, and LFSCProofGeneric().

int LFSCProofGeneric::getNumChildren ( )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 90 of file LFSCUtilProof.h.

References d_pf.

LFSCProof* LFSCProofGeneric::getChild ( int  n )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 91 of file LFSCUtilProof.h.

References d_pf.

Member Data Documentation

vector< RefPtr< LFSCProof > > LFSCProofGeneric::d_pf

private

Definition at line 63 of file LFSCUtilProof.h.

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

vector< string > LFSCProofGeneric::d_str

private

Definition at line 64 of file LFSCUtilProof.h.

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

bool LFSCProofGeneric::debug_str

private

Definition at line 65 of file LFSCUtilProof.h.

Referenced by clone(), get_length(), and LFSCProofGeneric().

---

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

• LFSCUtilProof.h
• LFSCUtilProof.cpp