LFSCProof Class Reference

#include <LFSCProof.h>

Inherits LFSCObj.

Inherited by LFSCAssume, LFSCBoolRes, LFSCClausify, LFSCLem, LFSCLraAdd, LFSCLraAxiom, LFSCLraContra, LFSCLraMulC, LFSCLraPoly, LFSCLraSub, LFSCPfLambda, LFSCPfLet, LFSCPfVar, LFSCProofExpr, and LFSCProofGeneric.

Collaboration diagram for LFSCProof:

Public Member Functions
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 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 void	print_pf (std::ostream &s, int ind=0)=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 ()
virtual LFSCProof *	clone ()=0
virtual int	getNumChildren ()
virtual LFSCProof *	getChild (int n)
virtual int	checkOp ()
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 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 ()

Protected Member Functions
	LFSCProof ()
virtual long int	get_length ()
virtual	~LFSCProof ()

Protected Attributes
int	printCounter
LFSCProof *	rplProof
long int	strLen
int	chOp
int	assumeVar
int	assumeVarUsed
std::vector< int >	br
bool	brComputed

Static Protected Attributes
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

Friends
class	LFSCPrinter

Additional Inherited Members
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)

Detailed Description

Definition at line 26 of file LFSCProof.h.

Constructor & Destructor Documentation

LFSCProof::LFSCProof ( )

protected

Definition at line 11 of file LFSCProof.cpp.

References assumeVar, assumeVarUsed, brComputed, chOp, pf_counter, printCounter, rplProof, and strLen.

virtual LFSCProof::~LFSCProof ( )

inlineprotectedvirtual

Definition at line 44 of file LFSCProof.h.

Member Function Documentation

virtual long int LFSCProof::get_length ( )

inlineprotectedvirtual

Reimplemented in LFSCLraContra, LFSCLraPoly, LFSCPfLet, LFSCAssume, LFSCLraSub, LFSCProofGeneric, LFSCLraMulC, LFSCClausify, LFSCPfLambda, LFSCLem, LFSCLraAxiom, LFSCPfVar, LFSCLraAdd, LFSCBoolRes, and LFSCProofExpr.

Definition at line 43 of file LFSCProof.h.

Referenced by get_string_length().

virtual LFSCProofExpr* LFSCProof::AsLFSCProofExpr ( )

inlinevirtual

Reimplemented in LFSCProofExpr.

Definition at line 46 of file LFSCProof.h.

virtual LFSCLraAdd* LFSCProof::AsLFSCLraAdd ( )

inlinevirtual

Reimplemented in LFSCLraAdd.

Definition at line 47 of file LFSCProof.h.

virtual LFSCLraSub* LFSCProof::AsLFSCLraSub ( )

inlinevirtual

Reimplemented in LFSCLraSub.

Definition at line 48 of file LFSCProof.h.

virtual LFSCLraMulC* LFSCProof::AsLFSCLraMulC ( )

inlinevirtual

Reimplemented in LFSCLraMulC.

Definition at line 49 of file LFSCProof.h.

Referenced by LFSCLraMulC::Make().

virtual LFSCLraAxiom* LFSCProof::AsLFSCLraAxiom ( )

inlinevirtual

Reimplemented in LFSCLraAxiom.

Definition at line 50 of file LFSCProof.h.

virtual LFSCLraContra* LFSCProof::AsLFSCLraContra ( )

inlinevirtual

Reimplemented in LFSCLraContra.

Definition at line 51 of file LFSCProof.h.

virtual LFSCLraPoly* LFSCProof::AsLFSCLraPoly ( )

inlinevirtual

Reimplemented in LFSCLraPoly.

Definition at line 52 of file LFSCProof.h.

Referenced by TReturn::normalize_to_tf().

virtual LFSCBoolRes* LFSCProof::AsLFSCBoolRes ( )

inlinevirtual

Reimplemented in LFSCBoolRes.

Definition at line 53 of file LFSCProof.h.

virtual LFSCLem* LFSCProof::AsLFSCLem ( )

inlinevirtual

Reimplemented in LFSCLem.

Definition at line 54 of file LFSCProof.h.

virtual LFSCClausify* LFSCProof::AsLFSCClausify ( )

inlinevirtual

Reimplemented in LFSCClausify.

Definition at line 55 of file LFSCProof.h.

virtual LFSCAssume* LFSCProof::AsLFSCAssume ( )

inlinevirtual

Reimplemented in LFSCAssume.

Definition at line 56 of file LFSCProof.h.

virtual LFSCProofGeneric* LFSCProof::AsLFSCProofGeneric ( )

inlinevirtual

Reimplemented in LFSCProofGeneric.

Definition at line 57 of file LFSCProof.h.

virtual LFSCPfVar* LFSCProof::AsLFSCPfVar ( )

inlinevirtual

Reimplemented in LFSCPfVar.

Definition at line 58 of file LFSCProof.h.

virtual LFSCPfLambda* LFSCProof::AsLFSCPfLambda ( )

inlinevirtual

Reimplemented in LFSCPfLambda.

Definition at line 59 of file LFSCProof.h.

virtual LFSCPfLet* LFSCProof::AsLFSCPfLet ( )

inlinevirtual

Reimplemented in LFSCPfLet.

Definition at line 60 of file LFSCProof.h.

virtual bool LFSCProof::isLraMulC ( )

inlinevirtual

Reimplemented in LFSCLraMulC.

Definition at line 62 of file LFSCProof.h.

static int LFSCProof::make_lambda ( LFSCProof *  p )

inlinestatic

Definition at line 63 of file LFSCProof.h.

References lambdaCounter, and lambdaMap.

Referenced by LFSCConvert::make_let_proof().

void LFSCProof::print	(	std::ostream &	s,
		int	ind = 0
	)

Definition at line 23 of file LFSCProof.cpp.

References Obj::indent(), lambdaMap, lambdaPrintMap, print(), print_pf(), Obj::print_warning(), printCounter, and rplProof.

Referenced by print(), LFSCPrinter::print_LFSC(), LFSCBoolRes::print_pf(), LFSCLraAdd::print_pf(), LFSCPfLambda::print_pf(), LFSCClausify::print_pf(), LFSCLraMulC::print_pf(), LFSCAssume::print_pf(), LFSCLraSub::print_pf(), LFSCPfLet::print_pf(), LFSCLraPoly::print_pf(), LFSCLraContra::print_pf(), and print_structure().

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

pure virtual

Implemented in LFSCLraContra, LFSCLraPoly, LFSCPfLet, LFSCLraSub, LFSCAssume, LFSCProofGeneric, LFSCLraMulC, LFSCClausify, LFSCPfLambda, LFSCLem, LFSCLraAxiom, LFSCPfVar, LFSCLraAdd, LFSCBoolRes, and LFSCProofExpr.

Referenced by print().

virtual bool LFSCProof::isTrivial ( )

inlinevirtual

Reimplemented in LFSCLraAxiom.

Definition at line 72 of file LFSCProof.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCLraAdd::Make(), LFSCBoolRes::Make(), LFSCLraMulC::Make(), and LFSCLraSub::Make().

long int LFSCProof::get_string_length ( )

inline

Definition at line 73 of file LFSCProof.h.

References get_length(), get_string_length(), getChild(), getNumChildren(), and strLen.

Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCBoolRes::get_length(), LFSCLraAdd::get_length(), LFSCPfLambda::get_length(), LFSCClausify::get_length(), LFSCLraMulC::get_length(), LFSCProofGeneric::get_length(), LFSCLraSub::get_length(), LFSCAssume::get_length(), LFSCPfLet::get_length(), LFSCLraPoly::get_length(), LFSCLraContra::get_length(), and get_string_length().

void LFSCProof::print_structure	(	std::ostream &	s,
		int	ind = 0
	)

Definition at line 43 of file LFSCProof.cpp.

References Obj::indent(), lambdaMap, lambdaPrintMap, print(), print_struct(), Obj::print_warning(), printCounter, and rplProof.

Referenced by LFSCPrinter::print_LFSC(), LFSCBoolRes::print_struct(), LFSCAssume::print_struct(), and LFSCPfLet::print_struct().

virtual void LFSCProof::print_struct ( std::ostream &  s, int  ind = 0  )

inlinevirtual

Reimplemented in LFSCPfLet, LFSCAssume, LFSCClausify, LFSCLem, LFSCPfVar, and LFSCBoolRes.

Definition at line 86 of file LFSCProof.h.

Referenced by print_structure().

void LFSCProof::setRplProof ( LFSCProof *  p )

inline

Definition at line 91 of file LFSCProof.h.

References rplProof.

void LFSCProof::fillHoles ( )

virtual

Reimplemented in LFSCProofExpr.

Definition at line 61 of file LFSCProof.cpp.

References fillHoles(), getChild(), and getNumChildren().

Referenced by fillHoles(), and LFSCPfLet::print_pf().

virtual LFSCProof* LFSCProof::clone ( )

pure virtual

Implemented in LFSCLraContra, LFSCLraPoly, LFSCPfLet, LFSCAssume, LFSCLraSub, LFSCProofGeneric, LFSCClausify, LFSCLraMulC, LFSCPfLambda, LFSCLem, LFSCLraAxiom, LFSCPfVar, LFSCBoolRes, LFSCLraAdd, and LFSCProofExpr.

virtual int LFSCProof::getNumChildren ( )

inlinevirtual

Reimplemented in LFSCLraContra, LFSCLraPoly, LFSCAssume, LFSCLraSub, LFSCProofGeneric, LFSCClausify, LFSCLraMulC, LFSCPfLambda, LFSCBoolRes, and LFSCLraAdd.

Definition at line 100 of file LFSCProof.h.

Referenced by checkOp(), fillHoles(), and get_string_length().

virtual LFSCProof* LFSCProof::getChild ( int  n )

inlinevirtual

Reimplemented in LFSCLraContra, LFSCLraPoly, LFSCAssume, LFSCLraSub, LFSCProofGeneric, LFSCClausify, LFSCLraMulC, LFSCPfLambda, LFSCBoolRes, and LFSCLraAdd.

Definition at line 101 of file LFSCProof.h.

Referenced by checkOp(), fillHoles(), get_string_length(), and TReturn::normalize_to_tf().

int LFSCProof::checkOp ( )

virtual

Reimplemented in LFSCLraContra, LFSCLraPoly, LFSCLraSub, LFSCLraMulC, LFSCLraAxiom, and LFSCLraAdd.

Definition at line 83 of file LFSCProof.cpp.

References checkOp(), chOp, getChild(), and getNumChildren().

Referenced by checkOp(), LFSCLraContra::LFSCLraContra(), LFSCLraMulC::LFSCLraMulC(), LFSCLraPoly::LFSCLraPoly(), LFSCLraSub::LFSCLraSub(), and LFSCLraAdd::Make().

int LFSCProof::getChOp ( )

inline

Definition at line 103 of file LFSCProof.h.

References chOp.

Referenced by TReturn::normalize_to_tf(), and TReturn::normalize_tr().

void LFSCProof::setChOp ( int  c )

inline

Definition at line 104 of file LFSCProof.h.

References chOp.

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

virtual int LFSCProof::checkBoolRes ( std::vector< int > &  clause )

inlinevirtual

Reimplemented in LFSCAssume, LFSCClausify, LFSCLem, and LFSCBoolRes.

Definition at line 105 of file LFSCProof.h.

Referenced by LFSCBoolRes::checkBoolRes(), LFSCClausify::checkBoolRes(), and LFSCAssume::checkBoolRes().

LFSCProof * LFSCProof::Make_CNF ( const Expr &  form, const Expr &  reason, int  pos  )

static

Definition at line 104 of file LFSCProof.cpp.

References CVC3::abs(), AND, CVC3::Expr::arity(), LFSCObj::cascade_expr(), LFSCObj::d_and_final_s, LFSCObj::d_and_mid_s, LFSCObj::d_iff_s, LFSCObj::d_imp_s, LFSCObj::d_ite_s, LFSCObj::d_or_final_s, LFSCObj::d_or_mid_s, std::endl(), RefPtr< T >::get(), CVC3::Expr::getKind(), LFSCPfVar::Make(), LFSCClausify::Make(), LFSCProofGeneric::Make(), LFSCAssume::Make(), Make_and_elim(), LFSCProofGeneric::MakeStr(), NOT, Obj::print_error(), and LFSCObj::queryM().

Referenced by LFSCConvert::cvc3_to_lfsc().

LFSCProof * LFSCProof::Make_not_not_elim ( const Expr &  pf, LFSCProof *  p  )

static

Definition at line 372 of file LFSCProof.cpp.

References CVC3::Expr::isNot(), and LFSCProofGeneric::Make().

Referenced by LFSCConvert::cvc3_to_lfsc().

LFSCProof * LFSCProof::Make_mimic ( const Expr &  pf, LFSCProof *  p, int  numHoles  )

static

Definition at line 384 of file LFSCProof.cpp.

References LFSCProofGeneric::Make().

Referenced by LFSCConvert::cvc3_to_lfsc().

LFSCProof * LFSCProof::Make_and_elim ( const Expr &  form, LFSCProof *  p, int  n, const Expr &  expected  )

static

Definition at line 397 of file LFSCProof.cpp.

References CVC3::Expr::arity(), LFSCObj::cascade_expr(), LFSCProofGeneric::Make(), and Obj::print_error().

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

static int LFSCProof::get_proof_counter ( )

inlinestatic

Definition at line 114 of file LFSCProof.h.

References pf_counter.

Friends And Related Function Documentation

friend class LFSCPrinter

friend

Definition at line 97 of file LFSCProof.h.

Member Data Documentation

int LFSCProof::pf_counter = 0

staticprotected

Definition at line 28 of file LFSCProof.h.

Referenced by get_proof_counter(), and LFSCProof().

std::map< LFSCProof *, int > LFSCProof::lambdaMap

staticprotected

Definition at line 29 of file LFSCProof.h.

Referenced by make_lambda(), print(), and print_structure().

std::map< LFSCProof *, LFSCProof * > LFSCProof::lambdaPrintMap

staticprotected

Definition at line 30 of file LFSCProof.h.

Referenced by print(), LFSCPfLambda::print_pf(), LFSCPfLet::print_pf(), LFSCPfLet::print_struct(), and print_structure().

int LFSCProof::printCounter

protected

Definition at line 31 of file LFSCProof.h.

Referenced by LFSCProof(), print(), and print_structure().

LFSCProof* LFSCProof::rplProof

protected

Definition at line 32 of file LFSCProof.h.

Referenced by LFSCProof(), print(), print_structure(), and setRplProof().

int LFSCProof::lambdaCounter = 1

staticprotected

Definition at line 33 of file LFSCProof.h.

Referenced by make_lambda().

long int LFSCProof::strLen

protected

Definition at line 34 of file LFSCProof.h.

Referenced by get_string_length(), and LFSCProof().

int LFSCProof::chOp

protected

Definition at line 35 of file LFSCProof.h.

Referenced by checkOp(), getChOp(), LFSCProof(), and setChOp().

int LFSCProof::assumeVar

protected

Definition at line 36 of file LFSCProof.h.

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

int LFSCProof::assumeVarUsed

protected

Definition at line 37 of file LFSCProof.h.

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

std::vector< int > LFSCProof::br

protected

Definition at line 39 of file LFSCProof.h.

bool LFSCProof::brComputed

protected

Definition at line 40 of file LFSCProof.h.

Referenced by LFSCProof().

---

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

• LFSCProof.h
• LFSCProof.cpp