#include <LFSCLraProof.h>
Inherits LFSCProof.
Public Member Functions
- virtual LFSCLraPoly * AsLFSCLraPoly ()
- void print_pf (std::ostream &s, int ind=0)
- LFSCProof * clone ()
- int getNumChildren ()
- LFSCProof * getChild (int n)
- int checkOp ()
Static Public Member Functions
- static LFSCProof * Make (LFSCProof *pf, int var, int op)
- static LFSCProof * Make (const Expr &e, LFSCProof *p)
Private Member Functions
- LFSCLraPoly (LFSCProof *pf, int var, int op)
- virtual ~LFSCLraPoly ()
- long int get_length ()
Private Attributes
Detailed Description
Definition at line 110 of file LFSCLraProof.h.
Constructor & Destructor Documentation
| LFSCLraPoly::LFSCLraPoly | ( | LFSCProof * | pf, |
| int | var, | ||
| int | op | ||
| ) | [inline, private] |
Definition at line 116 of file LFSCLraProof.h.
References LFSCProof::checkOp(), and d_op.
| virtual LFSCLraPoly::~LFSCLraPoly | ( | ) | [inline, private, virtual] |
Definition at line 122 of file LFSCLraProof.h.
Member Function Documentation
| long int LFSCLraPoly::get_length | ( | ) | [inline, private, virtual] |
| virtual LFSCLraPoly* LFSCLraPoly::AsLFSCLraPoly | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 125 of file LFSCLraProof.h.
| void LFSCLraPoly::print_pf | ( | std::ostream & | s, |
| int | ind = 0 |
||
| ) | [virtual] |
Implements LFSCProof.
Definition at line 101 of file LFSCLraProof.cpp.
References CVC3::abs(), d_op, d_pf, d_var, get_normalized(), get_not(), and kind_to_str().
Definition at line 127 of file LFSCLraProof.h.
References LFSCLraPoly().
Referenced by LFSCConvert::cvc3_to_lfsc(), Make(), TReturn::normalize_to_tf(), and TReturn::normalize_tr().
Definition at line 117 of file LFSCLraProof.cpp.
References LFSCObj::d_pn_form, std::endl(), get_normalized(), CVC3::Expr::getKind(), is_eq_kind(), is_opposite(), CVC3::Expr::isNot(), Make(), CVC3::MINUS, Obj::print_error(), LFSCObj::queryAtomic(), LFSCObj::queryM(), LFSCObj::queryMt(), and LFSCProof::setChOp().
| LFSCProof* LFSCLraPoly::clone | ( | ) | [inline, virtual] |
Implements LFSCProof.
Definition at line 131 of file LFSCLraProof.h.
References d_op, d_pf, d_var, RefPtr< T >::get(), and LFSCLraPoly().
| int LFSCLraPoly::getNumChildren | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 132 of file LFSCLraProof.h.
| LFSCProof* LFSCLraPoly::getChild | ( | int | n | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 133 of file LFSCLraProof.h.
References d_pf, and RefPtr< T >::get().
| int LFSCLraPoly::checkOp | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 134 of file LFSCLraProof.h.
References d_op, d_var, and get_normalized().
Member Data Documentation
RefPtr< LFSCProof > LFSCLraPoly::d_pf [private] |
Definition at line 113 of file LFSCLraProof.h.
Referenced by clone(), get_length(), getChild(), and print_pf().
int LFSCLraPoly::d_var [private] |
Definition at line 114 of file LFSCLraProof.h.
Referenced by checkOp(), clone(), and print_pf().
int LFSCLraPoly::d_op [private] |
Definition at line 115 of file LFSCLraProof.h.
Referenced by checkOp(), clone(), LFSCLraPoly(), and print_pf().
The documentation for this class was generated from the following files:
