Collaboration diagram for LFSCAssume:

Public Member Functions
virtual LFSCAssume *	AsLFSCAssume ()

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

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

LFSCProof *	clone ()

int	getNumChildren ()

LFSCProof *	getChild (int n)

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 LFSCLem *	AsLFSCLem ()

virtual LFSCClausify *	AsLFSCClausify ()

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	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, LFSCProof *pf, bool assm=true, int type=3)

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
	LFSCAssume (int v, LFSCProof *pf, bool assm, int type)

virtual	~LFSCAssume ()

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