CVC3
2.4.1
|
#include <LFSCLraProof.h>
LFSCLraPoly::LFSCLraPoly | ( | LFSCProof * | pf, |
int | var, | ||
int | op | ||
) | [inline, private] |
Definition at line 116 of file LFSCLraProof.h.
References d_op, and LFSCProof::checkOp().
virtual LFSCLraPoly::~LFSCLraPoly | ( | ) | [inline, private, virtual] |
Definition at line 122 of file LFSCLraProof.h.
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 d_var, kind_to_str(), get_normalized(), d_op, get_not(), CVC3::abs(), and d_pf.
Definition at line 127 of file LFSCLraProof.h.
References LFSCLraPoly().
Referenced by LFSCConvert::cvc3_to_lfsc(), Make(), TReturn::normalize_tr(), and TReturn::normalize_to_tf().
Definition at line 117 of file LFSCLraProof.cpp.
References LFSCObj::queryAtomic(), is_eq_kind(), CVC3::Expr::getKind(), LFSCObj::queryM(), is_opposite(), CVC3::MINUS, LFSCObj::queryMt(), LFSCObj::d_pn_form, Make(), LFSCProof::setChOp(), get_normalized(), CVC3::Expr::isNot(), std::endl(), and Obj::print_error().
LFSCProof* LFSCLraPoly::clone | ( | ) | [inline, virtual] |
Implements LFSCProof.
Definition at line 131 of file LFSCLraProof.h.
References LFSCLraPoly(), d_pf, RefPtr::get(), d_var, and d_op.
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::get().
int LFSCLraPoly::checkOp | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 134 of file LFSCLraProof.h.
References get_normalized(), d_op, and d_var.
RefPtr< LFSCProof > LFSCLraPoly::d_pf [private] |
Definition at line 113 of file LFSCLraProof.h.
Referenced by print_pf(), get_length(), clone(), and getChild().
int LFSCLraPoly::d_var [private] |
Definition at line 114 of file LFSCLraProof.h.
Referenced by print_pf(), clone(), and checkOp().
int LFSCLraPoly::d_op [private] |
Definition at line 115 of file LFSCLraProof.h.
Referenced by print_pf(), LFSCLraPoly(), clone(), and checkOp().