#include <LFSCLraProof.h>
Static Public Member Functions |
static LFSCProof * | MakeEq () |
static LFSCProof * | Make (Rational r, int op) |
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 () |
Additional Inherited Members |
| LFSCProof () |
virtual long int | get_length () |
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 |
Detailed Description
Definition at line 35 of file LFSCLraProof.h.
Constructor & Destructor Documentation
LFSCLraAxiom::LFSCLraAxiom |
( |
int |
op | ) |
|
|
inlineprivate |
LFSCLraAxiom::LFSCLraAxiom |
( |
int |
op, |
|
|
Rational |
r |
|
) |
| |
|
inlineprivate |
virtual LFSCLraAxiom::~LFSCLraAxiom |
( |
| ) |
|
|
inlineprivatevirtual |
Member Function Documentation
long int LFSCLraAxiom::get_length |
( |
| ) |
|
|
inlineprivate |
void LFSCLraAxiom::print_pf |
( |
std::ostream & |
s, |
|
|
int |
ind = 0 |
|
) |
| |
|
virtual |
bool LFSCLraAxiom::isTrivial |
( |
| ) |
|
|
inlinevirtual |
int LFSCLraAxiom::checkOp |
( |
| ) |
|
|
inlinevirtual |
Member Data Documentation
The documentation for this class was generated from the following files: