CVC3  2.4.1
Public Member Functions | Static Public Member Functions | Private Member Functions | Private Attributes | List of all members
LFSCProofGeneric Class Reference

#include <LFSCUtilProof.h>

Inheritance diagram for LFSCProofGeneric:
LFSCProof LFSCObj Obj

Public Member Functions

virtual LFSCProofGenericAsLFSCProofGeneric ()
void print_pf (std::ostream &s, int ind=0)
LFSCProofclone ()
int getNumChildren ()
LFSCProofgetChild (int n)
- Public Member Functions inherited from LFSCProof
virtual LFSCProofExprAsLFSCProofExpr ()
virtual LFSCLraAddAsLFSCLraAdd ()
virtual LFSCLraSubAsLFSCLraSub ()
virtual LFSCLraMulCAsLFSCLraMulC ()
virtual LFSCLraAxiomAsLFSCLraAxiom ()
virtual LFSCLraContraAsLFSCLraContra ()
virtual LFSCLraPolyAsLFSCLraPoly ()
virtual LFSCBoolResAsLFSCBoolRes ()
virtual LFSCLemAsLFSCLem ()
virtual LFSCClausifyAsLFSCClausify ()
virtual LFSCAssumeAsLFSCAssume ()
virtual LFSCPfVarAsLFSCPfVar ()
virtual LFSCPfLambdaAsLFSCPfLambda ()
virtual LFSCPfLetAsLFSCPfLet ()
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)
virtual void print_struct (std::ostream &s, int ind=0)
void setRplProof (LFSCProof *p)
virtual void fillHoles ()
virtual int checkOp ()
int getChOp ()
void setChOp (int c)
virtual int checkBoolRes (std::vector< int > &clause)
- Public Member Functions inherited from LFSCObj
 LFSCObj ()
- Public Member Functions inherited from Obj
 Obj ()
virtual ~Obj ()
int GetRefCount ()
 get ref count
void Ref ()
 reference
void Unref ()
 unreference

Static Public Member Functions

static LFSCProofMake (vector< RefPtr< LFSCProof > > &d_pfs, std::vector< string > &d_strs, bool db_str=false)
static LFSCProofMake (string str_pre, LFSCProof *sub_pf, string str_post, bool db_str=false)
static LFSCProofMake (string str_pre, LFSCProof *sub_pf1, LFSCProof *sub_pf2, string str_post, bool db_str=false)
static LFSCProofMakeStr (const char *c, bool db_str=false)
static LFSCProofMakeUnk ()
- Static Public Member Functions inherited from LFSCProof
static int make_lambda (LFSCProof *p)
static LFSCProofMake_CNF (const Expr &form, const Expr &reason, int pos)
static LFSCProofMake_not_not_elim (const Expr &pf, LFSCProof *p)
static LFSCProofMake_mimic (const Expr &pf, LFSCProof *p, int numHoles)
static LFSCProofMake_and_elim (const Expr &form, LFSCProof *p, int n, const Expr &expected)
static int get_proof_counter ()
- Static Public Member Functions inherited from LFSCObj
static void initialize (const Expr &pf_expr, int lfscm)
- Static Public Member Functions inherited from Obj
static void print_error (const char *c, std::ostream &s)
static void print_warning (const char *c)
static void initialize ()

Private Member Functions

 LFSCProofGeneric (vector< RefPtr< LFSCProof > > &d_pfs, vector< string > &d_strs, bool db_str=false)
virtual ~LFSCProofGeneric ()
long int get_length ()

Private Attributes

vector< RefPtr< LFSCProof > > d_pf
vector< string > d_str
bool debug_str

Additional Inherited Members

- Protected Member Functions inherited from LFSCProof
 LFSCProof ()
virtual long int get_length ()
virtual ~LFSCProof ()
- Static Protected Member Functions inherited from LFSCObj
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)
- Protected Attributes inherited from LFSCProof
int printCounter
LFSCProofrplProof
long int strLen
int chOp
int assumeVar
int assumeVarUsed
std::vector< int > br
bool brComputed
- Static Protected Attributes inherited from LFSCProof
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 61 of file LFSCUtilProof.h.

Constructor & Destructor Documentation

LFSCProofGeneric::LFSCProofGeneric ( vector< RefPtr< LFSCProof > > &  d_pfs,
vector< string > &  d_strs,
bool  db_str = false 
)
inlineprivate

Definition at line 67 of file LFSCUtilProof.h.

References d_pf, d_str, and debug_str.

Referenced by clone(), Make(), and MakeStr().

virtual LFSCProofGeneric::~LFSCProofGeneric ( )
inlineprivatevirtual

Definition at line 74 of file LFSCUtilProof.h.

Member Function Documentation

long int LFSCProofGeneric::get_length ( )
private

Definition at line 70 of file LFSCUtilProof.cpp.

References d_pf, d_str, debug_str, and LFSCProof::get_string_length().

virtual LFSCProofGeneric* LFSCProofGeneric::AsLFSCProofGeneric ( )
inlinevirtual

Reimplemented from LFSCProof.

Definition at line 77 of file LFSCUtilProof.h.

void LFSCProofGeneric::print_pf ( std::ostream &  s,
int  ind = 0 
)
virtual

Implements LFSCProof.

Definition at line 81 of file LFSCUtilProof.cpp.

References d_pf, and d_str.

static LFSCProof* LFSCProofGeneric::Make ( vector< RefPtr< LFSCProof > > &  d_pfs,
std::vector< string > &  d_strs,
bool  db_str = false 
)
inlinestatic
LFSCProof * LFSCProofGeneric::Make ( string  str_pre,
LFSCProof sub_pf,
string  str_post,
bool  db_str = false 
)
static

Definition at line 90 of file LFSCUtilProof.cpp.

References LFSCProofGeneric().

LFSCProof * LFSCProofGeneric::Make ( string  str_pre,
LFSCProof sub_pf1,
LFSCProof sub_pf2,
string  str_post,
bool  db_str = false 
)
static

Definition at line 100 of file LFSCUtilProof.cpp.

References LFSCProofGeneric().

LFSCProof * LFSCProofGeneric::MakeStr ( const char *  c,
bool  db_str = false 
)
static
static LFSCProof* LFSCProofGeneric::MakeUnk ( )
inlinestatic

Definition at line 88 of file LFSCUtilProof.h.

References MakeStr().

Referenced by LFSCConvert::cvc3_to_lfsc().

LFSCProof* LFSCProofGeneric::clone ( )
inlinevirtual

Implements LFSCProof.

Definition at line 89 of file LFSCUtilProof.h.

References d_pf, d_str, debug_str, and LFSCProofGeneric().

int LFSCProofGeneric::getNumChildren ( )
inlinevirtual

Reimplemented from LFSCProof.

Definition at line 90 of file LFSCUtilProof.h.

References d_pf.

LFSCProof* LFSCProofGeneric::getChild ( int  n)
inlinevirtual

Reimplemented from LFSCProof.

Definition at line 91 of file LFSCUtilProof.h.

References d_pf.

Member Data Documentation

vector< RefPtr< LFSCProof > > LFSCProofGeneric::d_pf
private

Definition at line 63 of file LFSCUtilProof.h.

Referenced by clone(), get_length(), getChild(), getNumChildren(), LFSCProofGeneric(), and print_pf().

vector< string > LFSCProofGeneric::d_str
private

Definition at line 64 of file LFSCUtilProof.h.

Referenced by clone(), get_length(), LFSCProofGeneric(), and print_pf().

bool LFSCProofGeneric::debug_str
private

Definition at line 65 of file LFSCUtilProof.h.

Referenced by clone(), get_length(), and LFSCProofGeneric().


The documentation for this class was generated from the following files: