CVC3  2.4.1
Public Member Functions | Static Public Member Functions | Protected Member Functions | Protected Attributes | Static Protected Attributes | Friends | List of all members
LFSCProof Class Referenceabstract

#include <LFSCProof.h>

Inheritance diagram for LFSCProof:
LFSCObj Obj LFSCAssume LFSCBoolRes LFSCClausify LFSCLem LFSCLraAdd LFSCLraAxiom LFSCLraContra LFSCLraMulC LFSCLraPoly LFSCLraSub LFSCPfLambda LFSCPfLet LFSCPfVar LFSCProofExpr LFSCProofGeneric

Public Member Functions

virtual LFSCProofExprAsLFSCProofExpr ()
 
virtual LFSCLraAddAsLFSCLraAdd ()
 
virtual LFSCLraSubAsLFSCLraSub ()
 
virtual LFSCLraMulCAsLFSCLraMulC ()
 
virtual LFSCLraAxiomAsLFSCLraAxiom ()
 
virtual LFSCLraContraAsLFSCLraContra ()
 
virtual LFSCLraPolyAsLFSCLraPoly ()
 
virtual LFSCBoolResAsLFSCBoolRes ()
 
virtual LFSCLemAsLFSCLem ()
 
virtual LFSCClausifyAsLFSCClausify ()
 
virtual LFSCAssumeAsLFSCAssume ()
 
virtual LFSCProofGenericAsLFSCProofGeneric ()
 
virtual LFSCPfVarAsLFSCPfVar ()
 
virtual LFSCPfLambdaAsLFSCPfLambda ()
 
virtual LFSCPfLetAsLFSCPfLet ()
 
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 LFSCProofclone ()=0
 
virtual int getNumChildren ()
 
virtual LFSCProofgetChild (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 More...
 
void Ref ()
 reference More...
 
void Unref ()
 unreference More...
 

Static Public Member Functions

static int make_lambda (LFSCProof *p)
 
static LFSCProofMake_CNF (const Expr &form, const Expr &reason, int pos)
 
static LFSCProofMake_not_not_elim (const Expr &pf, LFSCProof *p)
 
static LFSCProofMake_mimic (const Expr &pf, LFSCProof *p, int numHoles)
 
static LFSCProofMake_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
 
LFSCProofrplProof
 
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 LFSCPrinterprinter
 
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< Exprcas_map
 
static ExprMap< Exprskolem_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
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 
)
virtual void LFSCProof::print_pf ( std::ostream &  s,
int  ind = 0 
)
pure virtual
virtual bool LFSCProof::isTrivial ( )
inlinevirtual
long int LFSCProof::get_string_length ( )
inline
void LFSCProof::print_structure ( std::ostream &  s,
int  ind = 0 
)
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
virtual int LFSCProof::getNumChildren ( )
inlinevirtual
virtual LFSCProof* LFSCProof::getChild ( int  n)
inlinevirtual
int LFSCProof::checkOp ( )
virtual
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
virtual int LFSCProof::checkBoolRes ( std::vector< int > &  clause)
inlinevirtual
LFSCProof * LFSCProof::Make_CNF ( const Expr form,
const Expr reason,
int  pos 
)
static
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
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
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: