Expand description
Vtree construction for the compiler, and the descriptors of a formula’s independent components.
A vtree is a binary tree whose leaves are the formula’s variables. The
diagram the compiler builds follows its shape, so the vtree decides how
large the diagram grows. vitri builds every one, from a spec in its
vtree grammar,
the one the binary’s --vtree takes; "portfolio", the default, builds a
catalog of candidates and keeps the best-scoring one.
build_vtree builds one tree for the whole formula, and
build_vtree_with_components one per independent component as well when
the spec reads the formula’s structure; VtreeOptions are the options of
one request. A component is a group of clauses that shares no variable with
the rest: Component names its clauses and variables, and
ComponentVtree pairs it with the tree built for it.
Every construction asks vitri, and what it asks is decided here: the
selection context a request carries, the request itself and the conversion
of the trees that come back. The run’s frontends (crate::frontend), which
have vitri build a vtree beside its preprocessing, use the same selection
context and conversion.
Structs§
- Component
- An independent component of a formula: its clauses, and the formula variables it renumbers.
- Component
Vtree - A component and the vtree built for it, whose leaves are the component’s local variables.
- Vtree
Build - What a build returns: the vtree over every variable of the formula, and the component trees when the build split the formula.
- Vtree
Options - The options of one vtree request.
Functions§
- build_
vtree - Build one vtree for the whole formula from a spec, such as
"portfolio". - build_
vtree_ with_ components - Build a vtree for a formula from a spec, and one per independent component when the spec reads the formula’s structure and the formula has two or more components.