#include <LFSCBoolProof.h>
Inherits LFSCProof.
Public Member Functions
- virtual LFSCClausify * AsLFSCClausify ()
- void print_pf (std::ostream &s, int ind=0)
- void print_struct (std::ostream &s, int ind=0)
- LFSCProof * clone ()
- int getNumChildren ()
- LFSCProof * getChild (int n)
- int checkBoolRes (std::vector< int > &clause)
Static Public Member Functions
- static LFSCProof * Make (int v, LFSCProof *pf)
- static LFSCProof * Make (const Expr &e, LFSCProof *p, bool cascadeOr=false)
Private Member Functions
- LFSCClausify (int v, LFSCProof *pf)
- virtual ~LFSCClausify ()
- long int get_length ()
Static Private Member Functions
- static LFSCProof * Make_i (const Expr &e, LFSCProof *p, std::vector< Expr > &exprs, const Expr &end)
Private Attributes
Friends
- class LFSCPrinter
Detailed Description
Definition at line 60 of file LFSCBoolProof.h.
Constructor & Destructor Documentation
| 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.
Member Function Documentation
| 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::abs(), CVC3::Expr::getKind(), Make(), OR, and LFSCObj::queryM().
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 CVC3::abs(), d_pf, and d_var.
| void LFSCClausify::print_struct | ( | std::ostream & | s, |
| int | ind = 0 |
||
| ) | [inline, virtual] |
Definition at line 76 of file LFSCBoolProof.h.
References LFSCClausify().
Referenced by LFSCConvert::cvc3_to_lfsc(), Make(), LFSCProof::Make_CNF(), Make_i(), and TReturn::normalize_tr().
Definition at line 121 of file LFSCBoolProof.cpp.
References CVC3::Expr::arity(), LFSCObj::cascade_expr(), Make(), Make_i(), and LFSCObj::queryM().
| LFSCProof* LFSCClausify::clone | ( | ) | [inline, virtual] |
Implements LFSCProof.
Definition at line 80 of file LFSCBoolProof.h.
References d_pf, d_var, RefPtr< T >::get(), and LFSCClausify().
| 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< T >::get().
| int LFSCClausify::checkBoolRes | ( | std::vector< int > & | clause | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 83 of file LFSCBoolProof.h.
Friends And Related Function Documentation
friend class LFSCPrinter [friend] |
Reimplemented from LFSCProof.
Definition at line 63 of file LFSCBoolProof.h.
Member Data Documentation
int LFSCClausify::d_var [private] |
Definition at line 64 of file LFSCBoolProof.h.
Referenced by checkBoolRes(), clone(), print_pf(), and print_struct().
RefPtr< LFSCProof > LFSCClausify::d_pf [private] |
Definition at line 65 of file LFSCBoolProof.h.
Referenced by checkBoolRes(), clone(), get_length(), getChild(), and print_pf().
The documentation for this class was generated from the following files:
