public class CTree
extends java.lang.Object
Modifier and Type | Method and Description |
---|---|
static java.util.Collection<CTree> |
buildFrom(Trace trace)
Builds the collection of C-trees described by the specified proof-search
trace.
|
int |
getId() |
_Prover |
getProver()
Returns the prover that generated the C-tree.
|
CTreeNode |
getRoot()
Returns the node at the root of the C-tree.
|
ProofSearchResult |
getStatus()
Returns the status of the C-tree.
|
static void |
toLatex(java.util.Collection<CTree> ctrees,
java.io.PrintStream out,
_LatexCTreeFormatter formatter)
TODO: move to CTreeLatexGenerator
Prints on the specified stream the LaTeX of the specified collection of
C-trees.
|
void |
toLatex(java.io.PrintStream out,
_LatexCTreeFormatter formatter)
TDOO: move to CTreeLatexGenerator
Prints on the specified stream the LaTeX of this C-tree.
|
public _Prover getProver()
public int getId()
public CTreeNode getRoot()
public ProofSearchResult getStatus()
public static java.util.Collection<CTree> buildFrom(Trace trace)
trace
- the trace of the proof-search.public static void toLatex(java.util.Collection<CTree> ctrees, java.io.PrintStream out, _LatexCTreeFormatter formatter)
ctrees
- the C-trees to represent.out
- the stream.formatter
- the formatter used to generate the latex of the C-trees.public void toLatex(java.io.PrintStream out, _LatexCTreeFormatter formatter)
out
- the stream.formatter
- the formatter used to generate the latex of this C-tree.