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

#include <LFSCBoolProof.h>

Inheritance diagram for LFSCBoolRes:
LFSCProof LFSCObj Obj

Public Member Functions

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

Static Public Member Functions

static LFSCProofMake (LFSCProof *pf1, LFSCProof *pf2, int v, bool col)
 
static LFSCProofMake (LFSCProof *p1, LFSCProof *p2, const Expr &res, const Expr &pf, bool cascadeOr=false)
 
static LFSCProofMakeC (LFSCProof *p, const Expr &res)
 
- 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

 LFSCBoolRes (LFSCProof *pf1, LFSCProof *pf2, int v, bool col)
 
virtual ~LFSCBoolRes ()
 
long int get_length ()
 

Private Attributes

RefPtr< LFSCProofd_children [2]
 
int d_var
 
bool d_col
 

Additional Inherited Members

- Protected Member Functions inherited from LFSCProof
 LFSCProof ()
 
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 6 of file LFSCBoolProof.h.

Constructor & Destructor Documentation

LFSCBoolRes::LFSCBoolRes ( LFSCProof pf1,
LFSCProof pf2,
int  v,
bool  col 
)
inlineprivate

Definition at line 12 of file LFSCBoolProof.h.

References d_children.

Referenced by clone(), and Make().

virtual LFSCBoolRes::~LFSCBoolRes ( )
inlineprivatevirtual

Definition at line 17 of file LFSCBoolProof.h.

Member Function Documentation

long int LFSCBoolRes::get_length ( )
inlineprivatevirtual

Reimplemented from LFSCProof.

Definition at line 18 of file LFSCBoolProof.h.

References d_children, and LFSCProof::get_string_length().

virtual LFSCBoolRes* LFSCBoolRes::AsLFSCBoolRes ( )
inlinevirtual

Reimplemented from LFSCProof.

Definition at line 22 of file LFSCBoolProof.h.

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

Implements LFSCProof.

Definition at line 7 of file LFSCBoolProof.cpp.

References CVC3::abs(), d_children, d_col, d_var, and LFSCProof::print().

void LFSCBoolRes::print_struct ( std::ostream &  s,
int  ind = 0 
)
virtual

Reimplemented from LFSCProof.

Definition at line 24 of file LFSCBoolProof.cpp.

References d_children, d_var, and LFSCProof::print_structure().

LFSCProof * LFSCBoolRes::Make ( LFSCProof pf1,
LFSCProof pf2,
int  v,
bool  col 
)
static

Definition at line 32 of file LFSCBoolProof.cpp.

References LFSCProof::isTrivial(), and LFSCBoolRes().

Referenced by LFSCConvert::cvc3_to_lfsc(), and Make().

LFSCProof * LFSCBoolRes::Make ( LFSCProof p1,
LFSCProof p2,
const Expr res,
const Expr pf,
bool  cascadeOr = false 
)
static
LFSCProof * LFSCBoolRes::MakeC ( LFSCProof p,
const Expr res 
)
static

Definition at line 93 of file LFSCBoolProof.cpp.

References CVC3::abs(), CVC3::Expr::isOr(), LFSCProofGeneric::Make(), and LFSCObj::queryM().

Referenced by Make().

LFSCProof* LFSCBoolRes::clone ( )
inlinevirtual

Implements LFSCProof.

Definition at line 32 of file LFSCBoolProof.h.

References d_children, d_col, d_var, and LFSCBoolRes().

int LFSCBoolRes::getNumChildren ( )
inlinevirtual

Reimplemented from LFSCProof.

Definition at line 33 of file LFSCBoolProof.h.

LFSCProof* LFSCBoolRes::getChild ( int  n)
inlinevirtual

Reimplemented from LFSCProof.

Definition at line 34 of file LFSCBoolProof.h.

References d_children, and RefPtr< T >::get().

int LFSCBoolRes::checkBoolRes ( std::vector< int > &  clause)
virtual

Reimplemented from LFSCProof.

Definition at line 41 of file LFSCBoolProof.cpp.

References LFSCProof::checkBoolRes(), d_children, d_var, and Obj::print_error().

Member Data Documentation

RefPtr< LFSCProof > LFSCBoolRes::d_children[2]
private
int LFSCBoolRes::d_var
private

Definition at line 10 of file LFSCBoolProof.h.

Referenced by checkBoolRes(), clone(), print_pf(), and print_struct().

bool LFSCBoolRes::d_col
private

Definition at line 11 of file LFSCBoolProof.h.

Referenced by clone(), and print_pf().


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