LFSCLraAxiom Class Reference

#include <LFSCLraProof.h>

Inherits LFSCProof.

Collaboration diagram for LFSCLraAxiom:

Public Member Functions
virtual LFSCLraAxiom *	AsLFSCLraAxiom ()
void	print_pf (std::ostream &s, int ind=0)
bool	isTrivial ()
LFSCProof *	clone ()
int	checkOp ()
Public Member Functions inherited from LFSCProof
virtual LFSCProofExpr *	AsLFSCProofExpr ()
virtual LFSCLraAdd *	AsLFSCLraAdd ()
virtual LFSCLraSub *	AsLFSCLraSub ()
virtual LFSCLraMulC *	AsLFSCLraMulC ()
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)
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 ()
virtual int	getNumChildren ()
virtual LFSCProof *	getChild (int n)
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 *	MakeEq ()
static LFSCProof *	Make (Rational r, int op)
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
	LFSCLraAxiom (int op)
	LFSCLraAxiom (int op, Rational r)
virtual	~LFSCLraAxiom ()
long int	get_length ()

Private Attributes
int	d_op
Rational	d_r

Static Private Attributes
static RefPtr< LFSCProof >	eq

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

Constructor & Destructor Documentation

LFSCLraAxiom::LFSCLraAxiom ( int  op )

inlineprivate

Definition at line 40 of file LFSCLraProof.h.

Referenced by clone(), Make(), and MakeEq().

LFSCLraAxiom::LFSCLraAxiom ( int  op, Rational  r  )

inlineprivate

Definition at line 41 of file LFSCLraProof.h.

virtual LFSCLraAxiom::~LFSCLraAxiom ( )

inlineprivatevirtual

Definition at line 44 of file LFSCLraProof.h.

Member Function Documentation

long int LFSCLraAxiom::get_length ( )

inlineprivatevirtual

Reimplemented from LFSCProof.

Definition at line 45 of file LFSCLraProof.h.

virtual LFSCLraAxiom* LFSCLraAxiom::AsLFSCLraAxiom ( )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 47 of file LFSCLraProof.h.

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

virtual

Implements LFSCProof.

Definition at line 44 of file LFSCLraProof.cpp.

References d_op, d_r, EQ, kind_to_str(), and print_rational().

bool LFSCLraAxiom::isTrivial ( )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 49 of file LFSCLraProof.h.

References d_op, and EQ.

LFSCProof * LFSCLraAxiom::MakeEq ( )

static

Definition at line 37 of file LFSCLraProof.cpp.

References eq, EQ, RefPtr< T >::get(), and LFSCLraAxiom().

Referenced by LFSCConvert::cvc3_to_lfsc().

static LFSCProof* LFSCLraAxiom::Make ( Rational  r, int  op  )

inlinestatic

Definition at line 51 of file LFSCLraProof.h.

References LFSCLraAxiom().

LFSCProof* LFSCLraAxiom::clone ( )

inlinevirtual

Implements LFSCProof.

Definition at line 52 of file LFSCLraProof.h.

References d_op, d_r, and LFSCLraAxiom().

int LFSCLraAxiom::checkOp ( )

inlinevirtual

Reimplemented from LFSCProof.

Definition at line 53 of file LFSCLraProof.h.

References d_op.

Member Data Documentation

RefPtr< LFSCProof > LFSCLraAxiom::eq

staticprivate

Definition at line 37 of file LFSCLraProof.h.

Referenced by MakeEq().

int LFSCLraAxiom::d_op

private

Definition at line 38 of file LFSCLraProof.h.

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

Rational LFSCLraAxiom::d_r

private

Definition at line 39 of file LFSCLraProof.h.

Referenced by clone(), and print_pf().

---

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

• LFSCLraProof.h
• LFSCLraProof.cpp