CVC3
2.4.1
|
#include <LFSCBoolProof.h>
LFSCAssume::LFSCAssume | ( | int | v, |
LFSCProof * | pf, | ||
bool | assm, | ||
int | type | ||
) | [inline, private] |
Definition at line 96 of file LFSCBoolProof.h.
virtual LFSCAssume::~LFSCAssume | ( | ) | [inline, private, virtual] |
Definition at line 97 of file LFSCBoolProof.h.
long int LFSCAssume::get_length | ( | ) | [inline, private, virtual] |
virtual LFSCAssume* LFSCAssume::AsLFSCAssume | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 100 of file LFSCBoolProof.h.
void LFSCAssume::print_pf | ( | std::ostream & | s, |
int | ind = 0 |
||
) | [virtual] |
Implements LFSCProof.
Definition at line 161 of file LFSCBoolProof.cpp.
References d_assm, d_var, d_type, CVC3::abs(), and d_pf.
void LFSCAssume::print_struct | ( | std::ostream & | s, |
int | ind = 0 |
||
) | [virtual] |
static LFSCProof* LFSCAssume::Make | ( | int | v, |
LFSCProof * | pf, | ||
bool | assm = true , |
||
int | type = 3 |
||
) | [inline, static] |
Definition at line 103 of file LFSCBoolProof.h.
References LFSCAssume().
Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCProof::Make_CNF(), TReturn::normalize_tr(), and TReturn::normalize_to_tf().
LFSCProof* LFSCAssume::clone | ( | ) | [inline, virtual] |
Implements LFSCProof.
Definition at line 106 of file LFSCBoolProof.h.
References LFSCAssume(), d_var, d_pf, RefPtr::get(), d_assm, and d_type.
int LFSCAssume::getNumChildren | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 107 of file LFSCBoolProof.h.
LFSCProof* LFSCAssume::getChild | ( | int | n | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 108 of file LFSCBoolProof.h.
References d_pf, and RefPtr::get().
int LFSCAssume::checkBoolRes | ( | std::vector< int > & | clause | ) | [inline, virtual] |
int LFSCAssume::d_var [private] |
Definition at line 92 of file LFSCBoolProof.h.
Referenced by print_pf(), print_struct(), clone(), and checkBoolRes().
RefPtr< LFSCProof > LFSCAssume::d_pf [private] |
Definition at line 93 of file LFSCBoolProof.h.
Referenced by print_pf(), print_struct(), get_length(), clone(), getChild(), and checkBoolRes().
bool LFSCAssume::d_assm [private] |
Definition at line 94 of file LFSCBoolProof.h.
Referenced by print_pf(), print_struct(), and clone().
int LFSCAssume::d_type [private] |
Definition at line 95 of file LFSCBoolProof.h.
Referenced by print_pf(), clone(), and checkBoolRes().