ResolutionProofDAG (JavaSMT Solver Library)

java.lang.Object
- org.sosy_lab.java_smt.basicimpl.AbstractProofDAG
- - org.sosy_lab.java_smt.ResolutionProofDAG

All Implemented Interfaces:

ProofDAG
```
public class ResolutionProofDAG
extends AbstractProofDAG
```
This class represents a resolution proof DAG. Its nodes might be of the type ResolutionProofDAG.AxiomProofNode or ResolutionProofDAG.ResolutionProofNode. It is used to represent proofs based on the RESOLUTE proof format from SMTInterpol.

See Also:

ResProofRule

- Nested Class Summary
  
  Nested Classes
  Modifier and Type Class Description
  
  static class ResolutionProofDAG.AxiomProofNode
  
  static class ResolutionProofDAG.ResolutionProofNode
  - Nested classes/interfaces inherited from class org.sosy_lab.java_smt.basicimpl.AbstractProofDAG
    AbstractProofDAG.AbstractProofNode
- Constructor Summary
  
  Constructors
  Constructor Description
  
  ResolutionProofDAG()
- Method Summary
  - Methods inherited from class org.sosy_lab.java_smt.basicimpl.AbstractProofDAG
    accept, addEdge, addNode, getNode, getNodes
  - Methods inherited from class java.lang.Object
    clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Constructor Detail
  - ResolutionProofDAG
```
public ResolutionProofDAG()
```