Module compile 

The compiler: a CNF formula and a vtree in, a Tree Decision Diagram out.

compile_cnf groups the clauses by their scope, the lowest vtree node whose subtree covers every variable of the clause, and works bottom-up: at each vtree node it conjoins the children’s diagrams, then the clauses scoped there, a batch at a time, minimizing as it goes. A formula whose clauses fall into independent components, groups that share no variable, is compiled one component at a time; ComponentPlan says whether the compiler finds them, takes them from the vtree construction, or compiles the formula whole. Output says what the compile produces: the Boolean diagram, or a counting diagram that marginalizes each level once its last clause is in, weighted or not, with variables forgotten for a projected count, or the Boolean diagram of such a projection.

A finished compile returns Compiled: the diagram, the largest size it reached, and how many projected variables it left free. It never returns a partial diagram: a compile that cannot finish says why with GiveUp.

The run count counts with this same compile, one component at a time where the formula splits, and retries a count that ran out of memory on smaller pieces of the formula.

Structs

CompileOptions

What a whole-formula compile is being asked for.

Compiled

What a finished compile returns.

Enums

ComponentPlan

Which independent components a compile splits the formula into.

GiveUp

Why a compile has no diagram to return.

Output

What a compile produces.

Functions

compile_cnf

Compile a CNF formula into a canonical TDD, guided by the vtree.