CVC3
2.4.1
|
#include <proof.h>
CVC3::Proof::Proof | ( | const Expr & | e | ) | [inline] |
CVC3::Proof::Proof | ( | const Proof & | p | ) | [inline] |
CVC3::Proof::Proof | ( | ) | [inline] |
Expr CVC3::Proof::getExpr | ( | ) | const [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().
bool CVC3::Proof::isNull | ( | ) | const [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().
std::string CVC3::Proof::toString | ( | ) | const [inline] |
std::ostream& operator<< | ( | std::ostream & | os, |
const Proof & | pf | ||
) | [friend] |
Expr CVC3::Proof::d_proof [private] |