CVC3
2.4.1
|
#include <LFSCUtilProof.h>
LFSCProofExpr::LFSCProofExpr | ( | const Expr & | e, |
bool | isH = false |
||
) | [private] |
Definition at line 23 of file LFSCUtilProof.cpp.
References d_e, LFSCObj::cascade_expr(), initialize(), and isHole.
virtual LFSCProofExpr::~LFSCProofExpr | ( | ) | [inline, private, virtual] |
Definition at line 12 of file LFSCUtilProof.h.
void LFSCProofExpr::initialize | ( | ) | [private] |
Reimplemented from Obj.
Definition at line 7 of file LFSCUtilProof.cpp.
References LFSCObj::printer, LFSCPrinter::set_print_expr(), and d_e.
Referenced by LFSCProofExpr().
long int LFSCProofExpr::get_length | ( | ) | [inline, private, virtual] |
Reimplemented from LFSCProof.
Definition at line 13 of file LFSCUtilProof.h.
virtual LFSCProofExpr* LFSCProofExpr::AsLFSCProofExpr | ( | ) | [inline, virtual] |
Reimplemented from LFSCProof.
Definition at line 15 of file LFSCUtilProof.h.
void LFSCProofExpr::print_pf | ( | std::ostream & | s, |
int | ind | ||
) | [virtual] |
Implements LFSCProof.
Definition at line 11 of file LFSCUtilProof.cpp.
References isHole, LFSCObj::printer, LFSCPrinter::print_expr(), and d_e.
Definition at line 17 of file LFSCUtilProof.h.
References LFSCProofExpr().
Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), and TReturn::normalize_tr().
LFSCProof* LFSCProofExpr::clone | ( | ) | [inline, virtual] |
Implements LFSCProof.
Definition at line 18 of file LFSCUtilProof.h.
References LFSCProofExpr(), d_e, and isHole.
void LFSCProofExpr::fillHoles | ( | ) | [inline, virtual] |
bool LFSCProofExpr::isHole [private] |
Definition at line 8 of file LFSCUtilProof.h.
Referenced by print_pf(), LFSCProofExpr(), clone(), and fillHoles().
Expr LFSCProofExpr::d_e [private] |
Definition at line 9 of file LFSCUtilProof.h.
Referenced by initialize(), print_pf(), LFSCProofExpr(), and clone().