CVC3
2.4.1
|
#include <LFSCProof.h>
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) |
![]() | |
LFSCObj () | |
![]() | |
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 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 void | initialize (const Expr &pf_expr, int lfscm) |
![]() | |
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 () |
![]() | |
void | indent (std::ostream &s, int ind=0) |
Protected Attributes | |
int | printCounter |
LFSCProof * | rplProof |
long int | strLen |
int | chOp |
int | assumeVar |
int | assumeVarUsed |
std::vector< int > | br |
bool | brComputed |
![]() | |
ostringstream | oignore |
int | refCount |
Friends | |
class | LFSCPrinter |
Additional Inherited Members | |
![]() | |
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) |
Definition at line 26 of file LFSCProof.h.
|
protected |
Definition at line 11 of file LFSCProof.cpp.
References assumeVar, assumeVarUsed, brComputed, chOp, pf_counter, printCounter, rplProof, and strLen.
|
inlineprotectedvirtual |
Definition at line 44 of file LFSCProof.h.
|
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().
|
inlinevirtual |
Reimplemented in LFSCProofExpr.
Definition at line 46 of file LFSCProof.h.
|
inlinevirtual |
Reimplemented in LFSCLraAdd.
Definition at line 47 of file LFSCProof.h.
|
inlinevirtual |
Reimplemented in LFSCLraSub.
Definition at line 48 of file LFSCProof.h.
|
inlinevirtual |
Reimplemented in LFSCLraMulC.
Definition at line 49 of file LFSCProof.h.
Referenced by LFSCLraMulC::Make().
|
inlinevirtual |
Reimplemented in LFSCLraAxiom.
Definition at line 50 of file LFSCProof.h.
|
inlinevirtual |
Reimplemented in LFSCLraContra.
Definition at line 51 of file LFSCProof.h.
|
inlinevirtual |
Reimplemented in LFSCLraPoly.
Definition at line 52 of file LFSCProof.h.
Referenced by TReturn::normalize_to_tf().
|
inlinevirtual |
Reimplemented in LFSCBoolRes.
Definition at line 53 of file LFSCProof.h.
|
inlinevirtual |
Reimplemented in LFSCLem.
Definition at line 54 of file LFSCProof.h.
|
inlinevirtual |
Reimplemented in LFSCClausify.
Definition at line 55 of file LFSCProof.h.
|
inlinevirtual |
Reimplemented in LFSCAssume.
Definition at line 56 of file LFSCProof.h.
|
inlinevirtual |
Reimplemented in LFSCProofGeneric.
Definition at line 57 of file LFSCProof.h.
|
inlinevirtual |
Reimplemented in LFSCPfVar.
Definition at line 58 of file LFSCProof.h.
|
inlinevirtual |
Reimplemented in LFSCPfLambda.
Definition at line 59 of file LFSCProof.h.
|
inlinevirtual |
Reimplemented in LFSCPfLet.
Definition at line 60 of file LFSCProof.h.
|
inlinevirtual |
Reimplemented in LFSCLraMulC.
Definition at line 62 of file LFSCProof.h.
|
inlinestatic |
Definition at line 63 of file LFSCProof.h.
References lambdaCounter.
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().
|
pure virtual |
Implemented in LFSCLraContra, LFSCLraPoly, LFSCPfLet, LFSCLraSub, LFSCAssume, LFSCProofGeneric, LFSCLraMulC, LFSCClausify, LFSCPfLambda, LFSCLem, LFSCLraAxiom, LFSCPfVar, LFSCLraAdd, LFSCBoolRes, and LFSCProofExpr.
Referenced by print().
|
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().
|
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().
|
inlinevirtual |
Reimplemented in LFSCPfLet, LFSCAssume, LFSCClausify, LFSCLem, LFSCPfVar, and LFSCBoolRes.
Definition at line 86 of file LFSCProof.h.
Referenced by print_structure().
|
inline |
Definition at line 91 of file LFSCProof.h.
|
virtual |
Reimplemented in LFSCProofExpr.
Definition at line 61 of file LFSCProof.cpp.
References fillHoles(), getChild(), and getNumChildren().
Referenced by fillHoles(), and LFSCPfLet::print_pf().
|
pure virtual |
Implemented in LFSCLraContra, LFSCLraPoly, LFSCPfLet, LFSCAssume, LFSCLraSub, LFSCProofGeneric, LFSCClausify, LFSCLraMulC, LFSCPfLambda, LFSCLem, LFSCLraAxiom, LFSCPfVar, LFSCBoolRes, LFSCLraAdd, and LFSCProofExpr.
|
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().
|
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().
|
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().
|
inline |
Definition at line 103 of file LFSCProof.h.
References chOp.
Referenced by TReturn::normalize_to_tf(), and TReturn::normalize_tr().
|
inline |
Definition at line 104 of file LFSCProof.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCLraPoly::Make(), TReturn::normalize_to_tf(), and TReturn::normalize_tr().
|
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().
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().
Definition at line 372 of file LFSCProof.cpp.
References CVC3::Expr::isNot(), and LFSCProofGeneric::Make().
Referenced by LFSCConvert::cvc3_to_lfsc().
Definition at line 384 of file LFSCProof.cpp.
References LFSCProofGeneric::Make().
Referenced by LFSCConvert::cvc3_to_lfsc().
|
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().
|
inlinestatic |
Definition at line 114 of file LFSCProof.h.
References pf_counter.
|
friend |
Definition at line 97 of file LFSCProof.h.
|
staticprotected |
Definition at line 28 of file LFSCProof.h.
Referenced by get_proof_counter(), and LFSCProof().
|
staticprotected |
Definition at line 29 of file LFSCProof.h.
Referenced by print(), and print_structure().
Definition at line 30 of file LFSCProof.h.
Referenced by print(), LFSCPfLambda::print_pf(), LFSCPfLet::print_pf(), LFSCPfLet::print_struct(), and print_structure().
|
protected |
Definition at line 31 of file LFSCProof.h.
Referenced by LFSCProof(), print(), and print_structure().
|
protected |
Definition at line 32 of file LFSCProof.h.
Referenced by LFSCProof(), print(), and print_structure().
|
staticprotected |
Definition at line 33 of file LFSCProof.h.
Referenced by make_lambda().
|
protected |
Definition at line 34 of file LFSCProof.h.
Referenced by get_string_length(), and LFSCProof().
|
protected |
Definition at line 35 of file LFSCProof.h.
Referenced by checkOp(), getChOp(), and LFSCProof().
|
protected |
Definition at line 36 of file LFSCProof.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), and LFSCProof().
|
protected |
Definition at line 37 of file LFSCProof.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), and LFSCProof().
|
protected |
Definition at line 39 of file LFSCProof.h.
|
protected |
Definition at line 40 of file LFSCProof.h.
Referenced by LFSCProof().