#include <LFSCUtilProof.h>
Inherits LFSCProof.
|
static LFSCProof * | Make (vector< RefPtr< LFSCProof > > &d_pfs, std::vector< string > &d_strs, bool db_str=false) |
|
static LFSCProof * | Make (string str_pre, LFSCProof *sub_pf, string str_post, bool db_str=false) |
|
static LFSCProof * | Make (string str_pre, LFSCProof *sub_pf1, LFSCProof *sub_pf2, string str_post, bool db_str=false) |
|
static LFSCProof * | MakeStr (const char *c, bool db_str=false) |
|
static LFSCProof * | MakeUnk () |
|
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 () |
|
|
| 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 61 of file LFSCUtilProof.h.
LFSCProofGeneric::LFSCProofGeneric |
( |
vector< RefPtr< LFSCProof > > & |
d_pfs, |
|
|
vector< string > & |
d_strs, |
|
|
bool |
db_str = false |
|
) |
| |
|
inlineprivate |
virtual LFSCProofGeneric::~LFSCProofGeneric |
( |
| ) |
|
|
inlineprivatevirtual |
long int LFSCProofGeneric::get_length |
( |
| ) |
|
|
privatevirtual |
void LFSCProofGeneric::print_pf |
( |
std::ostream & |
s, |
|
|
int |
ind = 0 |
|
) |
| |
|
virtual |
static LFSCProof* LFSCProofGeneric::Make |
( |
vector< RefPtr< LFSCProof > > & |
d_pfs, |
|
|
std::vector< string > & |
d_strs, |
|
|
bool |
db_str = false |
|
) |
| |
|
inlinestatic |
Definition at line 80 of file LFSCUtilProof.h.
References LFSCProofGeneric().
Referenced by LFSCConvert::convert(), LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), LFSCPfLet::LFSCPfLet(), LFSCProof::Make_and_elim(), LFSCProof::Make_CNF(), LFSCClausify::Make_i(), LFSCProof::Make_mimic(), LFSCProof::Make_not_not_elim(), LFSCBoolRes::MakeC(), and TReturn::normalize_tr().
LFSCProof * LFSCProofGeneric::Make |
( |
string |
str_pre, |
|
|
LFSCProof * |
sub_pf, |
|
|
string |
str_post, |
|
|
bool |
db_str = false |
|
) |
| |
|
static |
LFSCProof * LFSCProofGeneric::MakeStr |
( |
const char * |
c, |
|
|
bool |
db_str = false |
|
) |
| |
|
static |
static LFSCProof* LFSCProofGeneric::MakeUnk |
( |
| ) |
|
|
inlinestatic |
int LFSCProofGeneric::getNumChildren |
( |
| ) |
|
|
inlinevirtual |
LFSCProof* LFSCProofGeneric::getChild |
( |
int |
n | ) |
|
|
inlinevirtual |
vector< string > LFSCProofGeneric::d_str |
|
private |
bool LFSCProofGeneric::debug_str |
|
private |
The documentation for this class was generated from the following files: