CVC3
2.4.1
|
#include <LFSCBoolProof.h>
LFSCClausify::LFSCClausify | ( | int | v, |
LFSCProof * | pf | ||
) | [inline, private] |
Definition at line 66 of file LFSCBoolProof.h.
virtual LFSCClausify::~LFSCClausify | ( | ) | [inline, private, virtual] |
Definition at line 67 of file LFSCBoolProof.h.
long int LFSCClausify::get_length | ( | ) | [inline, private, virtual] |
LFSCProof * LFSCClausify::Make_i | ( | const Expr & | e, |
LFSCProof * | p, | ||
std::vector< Expr > & | exprs, | ||
const Expr & | end | ||
) | [static, private] |
Definition at line 134 of file LFSCBoolProof.cpp.
References CVC3::Expr::getKind(), OR, Make(), LFSCObj::queryM(), and CVC3::abs().
Referenced by Make().
virtual LFSCClausify* LFSCClausify::AsLFSCClausify | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 72 of file LFSCBoolProof.h.
void LFSCClausify::print_pf | ( | std::ostream & | s, |
int | ind = 0 |
||
) | [virtual] |
Implements LFSCProof.
Definition at line 114 of file LFSCBoolProof.cpp.
References d_var, CVC3::abs(), and d_pf.
void LFSCClausify::print_struct | ( | std::ostream & | s, |
int | ind = 0 |
||
) | [inline, virtual] |
Definition at line 76 of file LFSCBoolProof.h.
References LFSCClausify().
Referenced by Make(), Make_i(), LFSCConvert::cvc3_to_lfsc(), LFSCProof::Make_CNF(), and TReturn::normalize_tr().
Definition at line 121 of file LFSCBoolProof.cpp.
References CVC3::Expr::arity(), LFSCObj::cascade_expr(), Make_i(), Make(), and LFSCObj::queryM().
LFSCProof* LFSCClausify::clone | ( | ) | [inline, virtual] |
Implements LFSCProof.
Definition at line 80 of file LFSCBoolProof.h.
References LFSCClausify(), d_var, d_pf, and RefPtr::get().
int LFSCClausify::getNumChildren | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 81 of file LFSCBoolProof.h.
LFSCProof* LFSCClausify::getChild | ( | int | n | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 82 of file LFSCBoolProof.h.
References d_pf, and RefPtr::get().
int LFSCClausify::checkBoolRes | ( | std::vector< int > & | clause | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 83 of file LFSCBoolProof.h.
friend class LFSCPrinter [friend] |
Reimplemented from LFSCProof.
Definition at line 63 of file LFSCBoolProof.h.
int LFSCClausify::d_var [private] |
Definition at line 64 of file LFSCBoolProof.h.
Referenced by print_pf(), print_struct(), clone(), and checkBoolRes().
RefPtr< LFSCProof > LFSCClausify::d_pf [private] |
Definition at line 65 of file LFSCBoolProof.h.
Referenced by print_pf(), get_length(), clone(), getChild(), and checkBoolRes().