#include <LFSCBoolProof.h>
Inherits LFSCProof.
Public Member Functions
- virtual LFSCBoolRes * AsLFSCBoolRes ()
- 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 (LFSCProof *pf1, LFSCProof *pf2, int v, bool col)
- static LFSCProof * Make (LFSCProof *p1, LFSCProof *p2, const Expr &res, const Expr &pf, bool cascadeOr=false)
- static LFSCProof * MakeC (LFSCProof *p, const Expr &res)
Private Member Functions
- LFSCBoolRes (LFSCProof *pf1, LFSCProof *pf2, int v, bool col)
- virtual ~LFSCBoolRes ()
- long int get_length ()
Private Attributes
- RefPtr< LFSCProof > d_children [2]
- int d_var
- bool d_col
Detailed Description
Definition at line 6 of file LFSCBoolProof.h.
Constructor & Destructor Documentation
Definition at line 12 of file LFSCBoolProof.h.
References d_children.
| virtual LFSCBoolRes::~LFSCBoolRes | ( | ) | [inline, private, virtual] |
Definition at line 17 of file LFSCBoolProof.h.
Member Function Documentation
| long int LFSCBoolRes::get_length | ( | ) | [inline, private, virtual] |
| virtual LFSCBoolRes* LFSCBoolRes::AsLFSCBoolRes | ( | ) | [inline, virtual] |
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, and d_var.
| 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, and d_var.
Definition at line 32 of file LFSCBoolProof.cpp.
References LFSCProof::isTrivial(), and LFSCBoolRes().
Referenced by LFSCConvert::cvc3_to_lfsc(), Make(), and MakeC().
| LFSCProof * LFSCBoolRes::Make | ( | LFSCProof * | p1, |
| LFSCProof * | p2, | ||
| const Expr & | res, | ||
| const Expr & | pf, | ||
| bool | cascadeOr = false |
||
| ) | [static] |
Definition at line 66 of file LFSCBoolProof.cpp.
References LFSCObj::cascade_expr(), CVC3::Expr::getKind(), CVC3::Expr::isNot(), Make(), MakeC(), OR, Obj::print_error(), and LFSCObj::queryM().
Definition at line 93 of file LFSCBoolProof.cpp.
References CVC3::abs(), CVC3::Expr::isOr(), Make(), and LFSCObj::queryM().
Referenced by Make().
| LFSCProof* LFSCBoolRes::clone | ( | ) | [inline, virtual] |
Implements LFSCProof.
Definition at line 32 of file LFSCBoolProof.h.
References d_children, d_col, d_var, and LFSCBoolRes().
| int LFSCBoolRes::getNumChildren | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 33 of file LFSCBoolProof.h.
| LFSCProof* LFSCBoolRes::getChild | ( | int | n | ) | [inline, virtual] |
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 d_children, d_var, and Obj::print_error().
Member Data Documentation
RefPtr< LFSCProof > LFSCBoolRes::d_children[2] [private] |
Definition at line 9 of file LFSCBoolProof.h.
Referenced by checkBoolRes(), clone(), get_length(), getChild(), LFSCBoolRes(), print_pf(), and print_struct().
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:
