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