Function compile_cnf 

pub fn compile_cnf(
    eng: &Engine,
    formula: &CnfFormula,
    vtree: &Arc<Vtree>,
    opts: CompileOptions<'_>,
) -> Result<Compiled, GiveUp>

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

By default (ComponentPlan::Detect) a formula whose clauses fall into independent components, groups that share no variable, is compiled one component at a time, each on a balanced vtree of its own, and the components’ diagrams are grafted into one; a formula with one component is compiled on vtree. CompileOptions::plan can instead ask for the whole formula on vtree, or for the caller’s own component vtrees.

The result’s vtree, the one its diagram carries, is the vtree to build any further operand on: and and the other operations refuse operands on different vtrees. It is vtree itself only when the formula was compiled whole and no rotation fired. A split compile’s result is on a vtree grafted from the components’ vtrees, and a counting compile may rotate its vtree to bring marginal levels together, onto a copy; vtree itself is never changed.

An Err is a give-up, never a partial diagram, so any count taken from an Ok is exact. A caller that runs this under a deadline it set — an attempt self-limiting at the wall, a reactive single shot with a fallback — treats GiveUp::Stopped as its own loss.

An empty clause makes the result the false diagram, on vtree.

Errors

• GiveUp::Stopped: CompileOptions::deadline passed.
• GiveUp::Refused: an apply was refused under the limits of the batch eng belongs to.
• GiveUp::OutOfMemory: an allocation was refused while reducing the finished diagram.
• GiveUp::Invalid: vtree, or a component’s vtree, does not place exactly its formula’s variables, or a ComponentPlan::Split does not partition the formula; a projected variable is outside the formula, or a literal weight is missing.