LFSCLraAxiom Class Reference

#include <LFSCLraProof.h>

Inheritance 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 More...
void	Ref ()
	reference More...
void	Unref ()
	unreference More...

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 ()
Protected Member Functions inherited from Obj
void	indent (std::ostream &s, int ind=0)
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
Protected Attributes inherited from Obj
ostringstream	oignore
int	refCount
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
Static Protected Attributes inherited from LFSCObj
static LFSCPrinter *	printer
static int	formula_i = 1
static int	trusted_i = 1
static int	term_i = 1
static int	tnorm_i = 1
static int	lfsc_mode
static bool	debug_conv
static bool	debug_var
static bool	cvc3_mimic
static bool	cvc3_mimic_input
static Rational	nullRat
static ExprMap< int >	nnode_map
static ExprMap< Expr >	cas_map
static ExprMap< Expr >	skolem_vars
static ExprMap< bool >	temp_visited
static ExprMap< int >	d_formulas
static ExprMap< int >	d_trusted
static ExprMap< int >	d_pn
static ExprMap< int >	d_pn_form
static ExprMap< int >	d_terms
static ExprMap< bool >	input_vars
static ExprMap< bool >	input_preds
static std::map< int, bool >	pntNeeded
static ExprMap< bool >	d_formulas_printed
static Expr	d_pf_expr
static ExprMap< bool >	d_assump_map
static ExprMap< bool >	d_rules
static Expr	d_bool_res_str
static Expr	d_assump_str
static Expr	d_iff_mp_str
static Expr	d_impl_mp_str
static Expr	d_iff_trans_str
static Expr	d_real_shadow_str
static Expr	d_cycle_conflict_str
static Expr	d_real_shadow_eq_str
static Expr	d_basic_subst_op_str
static Expr	d_mult_ineqn_str
static Expr	d_right_minus_left_str
static Expr	d_eq_trans_str
static Expr	d_eq_symm_str
static Expr	d_canon_plus_str
static Expr	d_refl_str
static Expr	d_cnf_convert_str
static Expr	d_learned_clause_str
static Expr	d_minus_to_plus_str
static Expr	d_plus_predicate_str
static Expr	d_negated_inequality_str
static Expr	d_flip_inequality_str
static Expr	d_optimized_subst_op_str
static Expr	d_iff_true_elim_str
static Expr	d_basic_subst_op1_str
static Expr	d_basic_subst_op0_str
static Expr	d_canon_mult_str
static Expr	d_canon_invert_divide_str
static Expr	d_iff_true_str
static Expr	d_mult_eqn_str
static Expr	d_rewrite_eq_symm_str
static Expr	d_implyWeakerInequality_str
static Expr	d_implyWeakerInequalityDiffLogic_str
static Expr	d_imp_mp_str
static Expr	d_rewrite_implies_str
static Expr	d_rewrite_or_str
static Expr	d_rewrite_and_str
static Expr	d_rewrite_iff_symm_str
static Expr	d_iff_not_false_str
static Expr	d_iff_false_str
static Expr	d_iff_false_elim_str
static Expr	d_not_to_iff_str
static Expr	d_not_not_elim_str
static Expr	d_const_predicate_str
static Expr	d_rewrite_not_not_str
static Expr	d_rewrite_not_true_str
static Expr	d_rewrite_not_false_str
static Expr	d_if_lift_rule_str
static Expr	d_CNFITE_str
static Expr	d_var_intro_str
static Expr	d_int_const_eq_str
static Expr	d_rewrite_eq_refl_str
static Expr	d_iff_symm_str
static Expr	d_rewrite_iff_str
static Expr	d_implyNegatedInequality_str
static Expr	d_uminus_to_mult_str
static Expr	d_lessThan_To_LE_rhs_rwr_str
static Expr	d_rewrite_ite_same_str
static Expr	d_andE_str
static Expr	d_implyEqualities_str
static Expr	d_addInequalities_str
static Expr	d_CNF_str
static Expr	d_cnf_add_unit_str
static Expr	d_minisat_proof_str
static Expr	d_or_final_s
static Expr	d_and_final_s
static Expr	d_ite_s
static Expr	d_iff_s
static Expr	d_imp_s
static Expr	d_or_mid_s
static Expr	d_and_mid_s
Static Protected Attributes inherited from Obj
static bool	errsInit = false
static ofstream	errs
static bool	indentFlag = false

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