#include <LFSCLraProof.h>

Collaboration diagram for LFSCLraAdd:

Public Member Functions
virtual LFSCLraAdd *	AsLFSCLraAdd ()

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 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 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 pf1, LFSCProof pf2, int op1, int op2)

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
	LFSCLraAdd (LFSCProof pf1, LFSCProof pf2, int op1, int op2)

virtual	~LFSCLraAdd ()

long int	get_length ()

Private Attributes
RefPtr< LFSCProof >	d_children [2]

int	d_op1

int	d_op2

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

Constructor & Destructor Documentation

LFSCLraAdd::LFSCLraAdd	(	LFSCProof *	pf1,
		LFSCProof *	pf2,
		int	op1,
		int	op2
	)

inlineprivate

Definition at line 12 of file LFSCLraProof.h.

References d_children.

Referenced by clone(), and Make().

virtual LFSCLraAdd::~LFSCLraAdd ( )

inlineprivatevirtual

Definition at line 18 of file LFSCLraProof.h.

Member Function Documentation

long int LFSCLraAdd::get_length ( )

inlineprivatevirtual

Reimplemented from LFSCProof.

Definition at line 19 of file LFSCLraProof.h.

References d_children, and LFSCProof::get_string_length().

virtual LFSCLraAdd* LFSCLraAdd::AsLFSCLraAdd ( )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 23 of file LFSCLraProof.h.

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

virtual

Implements LFSCProof.

Definition at line 5 of file LFSCLraProof.cpp.

References d_children, d_op1, d_op2, kind_to_str(), and LFSCProof::print().

LFSCProof * LFSCLraAdd::Make	(	LFSCProof *	pf1,
		LFSCProof *	pf2,
		int	op1,
		int	op2
	)

static

Definition at line 17 of file LFSCLraProof.cpp.

References LFSCProof::checkOp(), get_knd_order(), LFSCProof::isTrivial(), and LFSCLraAdd().

Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), TReturn::normalize_to_tf(), and TReturn::normalize_tr().

LFSCProof* LFSCLraAdd::clone ( )

inlinevirtual

Implements LFSCProof.

Definition at line 26 of file LFSCLraProof.h.

References d_children, d_op1, d_op2, and LFSCLraAdd().

int LFSCLraAdd::getNumChildren ( )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 27 of file LFSCLraProof.h.

LFSCProof* LFSCLraAdd::getChild ( int n )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 28 of file LFSCLraProof.h.

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

int LFSCLraAdd::checkOp ( )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 29 of file LFSCLraProof.h.

References d_op1, d_op2, and get_knd_result().

Member Data Documentation

RefPtr< LFSCProof > LFSCLraAdd::d_children[2]

private

Definition at line 9 of file LFSCLraProof.h.

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

int LFSCLraAdd::d_op1

private

Definition at line 10 of file LFSCLraProof.h.

Referenced by checkOp(), clone(), and print_pf().

int LFSCLraAdd::d_op2

private

Definition at line 10 of file LFSCLraProof.h.

Referenced by checkOp(), 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