CVC3
2.4.1
|
#include <sat_proof.h>
Public Member Functions | |
SatProofNode (CVC3::Theorem theorem) | |
SatProofNode (SatProofNode *left, SatProofNode *right, SAT::Lit lit) | |
bool | isLeaf () |
CVC3::Theorem | getLeaf () |
SatProofNode * | getLeftParent () |
SatProofNode * | getRightParent () |
SAT::Lit | getLit () |
bool | hasNodeProof () |
CVC3::Proof | getNodeProof () |
void | setNodeProof (CVC3::Proof pf) |
Private Attributes | |
CVC3::Theorem | d_theorem |
SatProofNode * | d_left |
SatProofNode * | d_right |
SAT::Lit | d_lit |
CVC3::Proof | d_proof |
Definition at line 37 of file sat_proof.h.
|
inline |
Definition at line 45 of file sat_proof.h.
References DebugAssert, and CVC3::Theorem::isNull().
|
inline |
Definition at line 52 of file sat_proof.h.
References DebugAssert.
|
inline |
Definition at line 58 of file sat_proof.h.
References CVC3::Theorem::isNull().
Referenced by generateSatProof(), getLeaf(), getLeftParent(), getLit(), getRightParent(), and printSatProof().
|
inline |
Definition at line 59 of file sat_proof.h.
References d_theorem, DebugAssert, and isLeaf().
Referenced by generateSatProof(), and printSatProof().
|
inline |
Definition at line 60 of file sat_proof.h.
References d_left, DebugAssert, and isLeaf().
Referenced by generateSatProof(), and printSatProof().
|
inline |
Definition at line 61 of file sat_proof.h.
References d_right, DebugAssert, and isLeaf().
Referenced by generateSatProof(), and printSatProof().
|
inline |
Definition at line 62 of file sat_proof.h.
References d_lit, DebugAssert, and isLeaf().
Referenced by generateSatProof().
|
inline |
Definition at line 63 of file sat_proof.h.
References CVC3::Proof::isNull().
Referenced by generateSatProof().
|
inline |
Definition at line 64 of file sat_proof.h.
References d_proof, DebugAssert, and CVC3::Proof::isNull().
Referenced by generateSatProof().
|
inline |
Definition at line 65 of file sat_proof.h.
Referenced by generateSatProof().
|
private |
Definition at line 39 of file sat_proof.h.
Referenced by getLeaf().
|
private |
Definition at line 40 of file sat_proof.h.
Referenced by getLeftParent().
|
private |
Definition at line 41 of file sat_proof.h.
Referenced by getRightParent().
|
private |
Definition at line 42 of file sat_proof.h.
Referenced by getLit().
|
private |
Definition at line 43 of file sat_proof.h.
Referenced by getNodeProof().