#include <LFSCBoolProof.h>

Collaboration diagram for LFSCClausify:

Public Member Functions
virtual LFSCClausify *	AsLFSCClausify ()

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

static LFSCProof *	Make (const Expr &e, LFSCProof *p, bool cascadeOr=false)

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
	LFSCClausify (int v, LFSCProof *pf)

virtual	~LFSCClausify ()

long int	get_length ()

Static Private Member Functions
static LFSCProof *	Make_i (const Expr &e, LFSCProof *p, std::vector< Expr > &exprs, const Expr &end)

Private Attributes
int	d_var

RefPtr< LFSCProof >	d_pf

Friends
class	LFSCPrinter

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

Constructor & Destructor Documentation

LFSCClausify::LFSCClausify	(	int	v,
		LFSCProof *	pf
	)

inlineprivate

Definition at line 66 of file LFSCBoolProof.h.

Referenced by clone(), and Make().

virtual LFSCClausify::~LFSCClausify ( )

inlineprivatevirtual

Definition at line 67 of file LFSCBoolProof.h.

Member Function Documentation

long int LFSCClausify::get_length ( )

inlineprivatevirtual

Reimplemented from LFSCProof.

Definition at line 68 of file LFSCBoolProof.h.

References d_pf, and LFSCProof::get_string_length().

LFSCProof * LFSCClausify::Make_i	(	const Expr &	e,
		LFSCProof *	p,
		std::vector< Expr > &	exprs,
		const Expr &	end
	)

staticprivate

Definition at line 134 of file LFSCBoolProof.cpp.

References CVC3::abs(), CVC3::Expr::getKind(), Make(), LFSCProofGeneric::Make(), LFSCAssume::Make(), OR, and LFSCObj::queryM().

Referenced by Make().

virtual LFSCClausify* LFSCClausify::AsLFSCClausify ( )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 72 of file LFSCBoolProof.h.

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

virtual

Implements LFSCProof.

Definition at line 114 of file LFSCBoolProof.cpp.

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

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

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 74 of file LFSCBoolProof.h.

References d_var.

static LFSCProof* LFSCClausify::Make	(	int	v,
		LFSCProof *	pf
	)

inlinestatic

Definition at line 76 of file LFSCBoolProof.h.

References LFSCClausify().

Referenced by LFSCConvert::cvc3_to_lfsc(), Make(), LFSCProof::Make_CNF(), Make_i(), and TReturn::normalize_tr().

LFSCProof * LFSCClausify::Make	(	const Expr &	e,
		LFSCProof *	p,
		bool	cascadeOr = `false`
	)

static

Definition at line 121 of file LFSCBoolProof.cpp.

References CVC3::Expr::arity(), LFSCObj::cascade_expr(), Make(), Make_i(), and LFSCObj::queryM().

LFSCProof* LFSCClausify::clone ( )

inlinevirtual

Implements LFSCProof.

Definition at line 80 of file LFSCBoolProof.h.

References d_pf, d_var, RefPtr< T >::get(), and LFSCClausify().

int LFSCClausify::getNumChildren ( )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 81 of file LFSCBoolProof.h.

LFSCProof* LFSCClausify::getChild ( int n )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 82 of file LFSCBoolProof.h.

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

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

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 83 of file LFSCBoolProof.h.

References LFSCProof::checkBoolRes(), d_pf, and d_var.

Friends And Related Function Documentation

friend class LFSCPrinter

friend

Definition at line 63 of file LFSCBoolProof.h.

Member Data Documentation

int LFSCClausify::d_var

private

Definition at line 64 of file LFSCBoolProof.h.

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

RefPtr< LFSCProof > LFSCClausify::d_pf

private

Definition at line 65 of file LFSCBoolProof.h.

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

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

Public Member Functions

Static Public Member Functions

Private Member Functions

Static Private Member Functions

Private Attributes

Friends

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation

Member Data Documentation