Collaboration diagram for LFSCLraPoly:

Public Member Functions
virtual LFSCLraPoly *	AsLFSCLraPoly ()

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

LFSCProof *	clone ()

int	getNumChildren ()

LFSCProof *	getChild (int n)

int	checkOp ()

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 LFSCBoolRes *	AsLFSCBoolRes ()

virtual LFSCLem *	AsLFSCLem ()

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)

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

void	setRplProof (LFSCProof *p)

virtual void	fillHoles ()

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 (LFSCProof *pf, int var, int op)

static LFSCProof *	Make (const Expr &e, LFSCProof *p)

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
	LFSCLraPoly (LFSCProof *pf, int var, int op)

virtual	~LFSCLraPoly ()

long int	get_length ()

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