#include <LFSCUtilProof.h>
Inherits LFSCProof.
Public Member Functions
- virtual LFSCProofExpr * AsLFSCProofExpr ()
- void print_pf (std::ostream &s, int ind)
- LFSCProof * clone ()
- void fillHoles ()
Static Public Member Functions
Private Member Functions
- LFSCProofExpr (const Expr &e, bool isH=false)
- void initialize ()
- virtual ~LFSCProofExpr ()
- long int get_length ()
Private Attributes
Detailed Description
Definition at line 6 of file LFSCUtilProof.h.
Constructor & Destructor Documentation
| LFSCProofExpr::LFSCProofExpr | ( | const Expr & | e, |
| bool | isH = false |
||
| ) | [private] |
Definition at line 23 of file LFSCUtilProof.cpp.
References LFSCObj::cascade_expr(), d_e, initialize(), and isHole.
| virtual LFSCProofExpr::~LFSCProofExpr | ( | ) | [inline, private, virtual] |
Definition at line 12 of file LFSCUtilProof.h.
Member Function Documentation
| void LFSCProofExpr::initialize | ( | ) | [private] |
Reimplemented from Obj.
Definition at line 7 of file LFSCUtilProof.cpp.
References d_e, LFSCObj::printer, and LFSCPrinter::set_print_expr().
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 d_e, isHole, LFSCPrinter::print_expr(), and LFSCObj::printer.
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 d_e, isHole, and LFSCProofExpr().
| void LFSCProofExpr::fillHoles | ( | ) | [inline, virtual] |
Member Data Documentation
bool LFSCProofExpr::isHole [private] |
Definition at line 8 of file LFSCUtilProof.h.
Referenced by clone(), fillHoles(), LFSCProofExpr(), and print_pf().
Expr LFSCProofExpr::d_e [private] |
Definition at line 9 of file LFSCUtilProof.h.
Referenced by clone(), initialize(), LFSCProofExpr(), and print_pf().
The documentation for this class was generated from the following files:
