CVC3
|
#include <proof.h>
Public Member Functions | |
Proof (const Expr &e) | |
Proof (const Proof &p) | |
Proof () | |
Expr | getExpr () const |
bool | isNull () const |
std::string | toString () const |
Private Attributes | |
Expr | d_proof |
Friends | |
std::ostream & | operator<< (std::ostream &os, const Proof &pf) |
|
inline |
Definition at line 46 of file proof.h.
References d_proof.
Referenced by CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::TheoremProducer::newPf(), CVC3::operator<<(), CVC3::operator==(), and CVC3::SearchEngineTheoremProducer::satProof().
|
inline |
Definition at line 47 of file proof.h.
References d_proof, and CVC3::Expr::isNull().
Referenced by CVC3::VCCmd::evaluateCommand(), SAT::SatProofNode::getNodeProof(), SAT::SatProofNode::hasNodeProof(), and CVC3::Theorem::Theorem().
|
friend |
|
private |