CVC3
2.4.1
|
#include <LFSCUtilProof.h>
Public Member Functions | |
virtual LFSCPfLet * | AsLFSCPfLet () |
void | print_pf (std::ostream &s, int ind=0) |
void | print_struct (std::ostream &s, int ind=0) |
LFSCProof * | clone () |
![]() | |
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 bool | isLraMulC () |
void | print (std::ostream &s, int ind=0) |
virtual bool | isTrivial () |
long int | get_string_length () |
void | print_structure (std::ostream &s, int ind=0) |
void | setRplProof (LFSCProof *p) |
virtual void | fillHoles () |
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 LFSCProof * | Make (LFSCProof *letPf, LFSCPfVar *pv, LFSCProof *body, bool isTh, std::vector< int > &fv) |
![]() | |
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 () |
Private Member Functions | |
LFSCPfLet (LFSCProof *letPf, LFSCPfVar *pv, LFSCProof *body, bool isTh, LFSCProof *letPfRpl, LFSCProof *pvRpl) | |
LFSCPfLet (LFSCProof *letPf, LFSCPfVar *pv, LFSCProof *body, bool isTh, std::vector< int > &fv) | |
virtual | ~LFSCPfLet () |
long int | get_length () |
Private Attributes | |
RefPtr< LFSCProof > | d_letPf |
RefPtr< LFSCPfVar > | d_pv |
RefPtr< LFSCProof > | d_body |
RefPtr< LFSCProof > | d_letPfRpl |
RefPtr< LFSCProof > | d_pvRpl |
bool | d_isTh |
Definition at line 95 of file LFSCUtilProof.h.
|
inlineprivate |
Definition at line 105 of file LFSCUtilProof.h.
|
private |
Definition at line 124 of file LFSCUtilProof.cpp.
References CVC3::abs(), d_letPfRpl, d_pvRpl, RefPtr< T >::get(), LFSCPfVar::Make(), LFSCPfLambda::Make(), LFSCProofGeneric::Make(), and LFSCPfVar::MakeV().
|
inlineprivatevirtual |
Definition at line 110 of file LFSCUtilProof.h.
|
inlineprivatevirtual |
Reimplemented from LFSCProof.
Definition at line 111 of file LFSCUtilProof.h.
References d_body, d_letPf, d_pv, and LFSCProof::get_string_length().
|
inlinevirtual |
Reimplemented from LFSCProof.
Definition at line 115 of file LFSCUtilProof.h.
|
virtual |
Implements LFSCProof.
Definition at line 153 of file LFSCUtilProof.cpp.
References d_body, d_isTh, d_letPf, d_letPfRpl, d_pv, d_pvRpl, std::endl(), LFSCProof::fillHoles(), RefPtr< T >::get(), LFSCProof::lambdaPrintMap, and LFSCProof::print().
|
virtual |
Reimplemented from LFSCProof.
Definition at line 169 of file LFSCUtilProof.cpp.
References d_body, d_letPf, d_pv, RefPtr< T >::get(), LFSCProof::lambdaPrintMap, and LFSCProof::print_structure().
|
inlinestatic |
Definition at line 118 of file LFSCUtilProof.h.
References LFSCPfLet().
Referenced by LFSCConvert::make_let_proof().
|
inlinevirtual |
Implements LFSCProof.
Definition at line 122 of file LFSCUtilProof.h.
References d_body, d_isTh, d_letPf, d_letPfRpl, d_pv, d_pvRpl, RefPtr< T >::get(), and LFSCPfLet().
Definition at line 97 of file LFSCUtilProof.h.
Referenced by clone(), get_length(), print_pf(), and print_struct().
Definition at line 98 of file LFSCUtilProof.h.
Referenced by clone(), get_length(), print_pf(), and print_struct().
Definition at line 99 of file LFSCUtilProof.h.
Referenced by clone(), get_length(), print_pf(), and print_struct().
Definition at line 101 of file LFSCUtilProof.h.
Referenced by clone(), LFSCPfLet(), and print_pf().
Definition at line 103 of file LFSCUtilProof.h.
Referenced by clone(), LFSCPfLet(), and print_pf().
|
private |
Definition at line 104 of file LFSCUtilProof.h.
Referenced by clone(), and print_pf().