#include <LFSCBoolProof.h>

Collaboration diagram for LFSCBoolRes:

Public Member Functions
virtual LFSCBoolRes *	AsLFSCBoolRes ()

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 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)

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 (LFSCProof pf1, LFSCProof pf2, int v, bool col)

static LFSCProof *	Make (LFSCProof p1, LFSCProof p2, const Expr &res, const Expr &pf, bool cascadeOr=false)

static LFSCProof *	MakeC (LFSCProof *p, const Expr &res)

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
	LFSCBoolRes (LFSCProof pf1, LFSCProof pf2, int v, bool col)

virtual	~LFSCBoolRes ()

long int	get_length ()

Private Attributes
RefPtr< LFSCProof >	d_children [2]

int	d_var

bool	d_col

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

Constructor & Destructor Documentation

LFSCBoolRes::LFSCBoolRes	(	LFSCProof *	pf1,
		LFSCProof *	pf2,
		int	v,
		bool	col
	)

inlineprivate

Definition at line 12 of file LFSCBoolProof.h.

References d_children.

Referenced by clone(), and Make().

virtual LFSCBoolRes::~LFSCBoolRes ( )

inlineprivatevirtual

Definition at line 17 of file LFSCBoolProof.h.

Member Function Documentation

long int LFSCBoolRes::get_length ( )

inlineprivatevirtual

Reimplemented from LFSCProof.

Definition at line 18 of file LFSCBoolProof.h.

References d_children, and LFSCProof::get_string_length().

virtual LFSCBoolRes* LFSCBoolRes::AsLFSCBoolRes ( )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 22 of file LFSCBoolProof.h.

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

virtual

Implements LFSCProof.

Definition at line 7 of file LFSCBoolProof.cpp.

References CVC3::abs(), d_children, d_col, d_var, and LFSCProof::print().

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

virtual

Reimplemented from LFSCProof.

Definition at line 24 of file LFSCBoolProof.cpp.

References d_children, d_var, and LFSCProof::print_structure().

LFSCProof * LFSCBoolRes::Make	(	LFSCProof *	pf1,
		LFSCProof *	pf2,
		int	v,
		bool	col
	)

static

Definition at line 32 of file LFSCBoolProof.cpp.

References LFSCProof::isTrivial(), and LFSCBoolRes().

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

LFSCProof * LFSCBoolRes::Make	(	LFSCProof *	p1,
		LFSCProof *	p2,
		const Expr &	res,
		const Expr &	pf,
		bool	cascadeOr = `false`
	)

static

Definition at line 66 of file LFSCBoolProof.cpp.

References LFSCObj::cascade_expr(), CVC3::Expr::getKind(), CVC3::Expr::isNot(), Make(), MakeC(), OR, Obj::print_error(), and LFSCObj::queryM().

LFSCProof * LFSCBoolRes::MakeC	(	LFSCProof *	p,
		const Expr &	res
	)

static

Definition at line 93 of file LFSCBoolProof.cpp.

References CVC3::abs(), CVC3::Expr::isOr(), LFSCProofGeneric::Make(), and LFSCObj::queryM().

Referenced by Make().

LFSCProof* LFSCBoolRes::clone ( )

inlinevirtual

Implements LFSCProof.

Definition at line 32 of file LFSCBoolProof.h.

References d_children, d_col, d_var, and LFSCBoolRes().

int LFSCBoolRes::getNumChildren ( )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 33 of file LFSCBoolProof.h.

LFSCProof* LFSCBoolRes::getChild ( int n )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 34 of file LFSCBoolProof.h.

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

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

virtual

Reimplemented from LFSCProof.

Definition at line 41 of file LFSCBoolProof.cpp.

References LFSCProof::checkBoolRes(), d_children, d_var, and Obj::print_error().

Member Data Documentation

RefPtr< LFSCProof > LFSCBoolRes::d_children[2]

private

Definition at line 9 of file LFSCBoolProof.h.

Referenced by checkBoolRes(), clone(), get_length(), getChild(), LFSCBoolRes(), print_pf(), and print_struct().

int LFSCBoolRes::d_var

private

Definition at line 10 of file LFSCBoolProof.h.

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

bool LFSCBoolRes::d_col

private

Definition at line 11 of file LFSCBoolProof.h.

Referenced by clone(), and print_pf().

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

Public Member Functions

Static Public Member Functions

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation