CVC3
2.4.1
|
#include <LFSCBoolProof.h>
Public Member Functions | |
virtual LFSCClausify * | AsLFSCClausify () |
void | print_pf (std::ostream &s, int ind=0) |
void | print_struct (std::ostream &s, int ind=0) |
LFSCProof * | clone () |
int | getNumChildren () |
LFSCProof * | getChild (int n) |
int | checkBoolRes (std::vector< int > &clause) |
![]() | |
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 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 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 | checkOp () |
int | getChOp () |
void | setChOp (int c) |
![]() | |
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 (int v, LFSCProof *pf) |
static LFSCProof * | Make (const Expr &e, LFSCProof *p, bool cascadeOr=false) |
![]() | |
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 | |
LFSCClausify (int v, LFSCProof *pf) | |
virtual | ~LFSCClausify () |
long int | get_length () |
Static Private Member Functions | |
static LFSCProof * | Make_i (const Expr &e, LFSCProof *p, std::vector< Expr > &exprs, const Expr &end) |
Private Attributes | |
int | d_var |
RefPtr< LFSCProof > | d_pf |
Friends | |
class | LFSCPrinter |
Additional Inherited Members | |
![]() | |
LFSCProof () | |
virtual | ~LFSCProof () |
![]() | |
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) |
![]() | |
int | printCounter |
LFSCProof * | rplProof |
long int | strLen |
int | chOp |
int | assumeVar |
int | assumeVarUsed |
std::vector< int > | br |
bool | brComputed |
![]() | |
static int | pf_counter = 0 |
static std::map< LFSCProof *, int > | lambdaMap |
static std::map< LFSCProof *, LFSCProof * > | lambdaPrintMap |
static int | lambdaCounter = 1 |
Definition at line 60 of file LFSCBoolProof.h.
|
inlineprivate |
Definition at line 66 of file LFSCBoolProof.h.
|
inlineprivatevirtual |
Definition at line 67 of file LFSCBoolProof.h.
|
inlineprivatevirtual |
Reimplemented from LFSCProof.
Definition at line 68 of file LFSCBoolProof.h.
References d_pf, and LFSCProof::get_string_length().
|
staticprivate |
Definition at line 134 of file LFSCBoolProof.cpp.
References CVC3::abs(), CVC3::Expr::getKind(), Make(), LFSCProofGeneric::Make(), LFSCAssume::Make(), OR, and LFSCObj::queryM().
Referenced by Make().
|
inlinevirtual |
Reimplemented from LFSCProof.
Definition at line 72 of file LFSCBoolProof.h.
|
virtual |
Implements LFSCProof.
Definition at line 114 of file LFSCBoolProof.cpp.
References CVC3::abs(), d_pf, d_var, and LFSCProof::print().
|
inlinevirtual |
Definition at line 76 of file LFSCBoolProof.h.
References LFSCClausify().
Referenced by LFSCConvert::cvc3_to_lfsc(), Make(), LFSCProof::Make_CNF(), Make_i(), and TReturn::normalize_tr().
Definition at line 121 of file LFSCBoolProof.cpp.
References CVC3::Expr::arity(), LFSCObj::cascade_expr(), Make(), Make_i(), and LFSCObj::queryM().
|
inlinevirtual |
Implements LFSCProof.
Definition at line 80 of file LFSCBoolProof.h.
References d_pf, d_var, RefPtr< T >::get(), and LFSCClausify().
|
inlinevirtual |
Reimplemented from LFSCProof.
Definition at line 81 of file LFSCBoolProof.h.
|
inlinevirtual |
Reimplemented from LFSCProof.
Definition at line 82 of file LFSCBoolProof.h.
References d_pf, and RefPtr< T >::get().
|
inlinevirtual |
Reimplemented from LFSCProof.
Definition at line 83 of file LFSCBoolProof.h.
References LFSCProof::checkBoolRes(), d_pf, and d_var.
|
friend |
Definition at line 63 of file LFSCBoolProof.h.
|
private |
Definition at line 64 of file LFSCBoolProof.h.
Referenced by checkBoolRes(), clone(), print_pf(), and print_struct().
Definition at line 65 of file LFSCBoolProof.h.
Referenced by checkBoolRes(), clone(), get_length(), getChild(), and print_pf().