vitri 0.2.0

CNF preprocessing and vtree construction (variable trees) for circuit compilation and model counting: preprocesses a DIMACS CNF, records the arithmetic to lift a model count back to the original, and builds a good vtree for it — for any d-DNNF/SDD/TDD compiler, or any model counter that takes a vtree.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

//! The vtree type: its shapes, its file format, and one construction on it.

use crate::vtree::*;

mod equality;
mod file_format;
mod lca;
mod reverse_rightmost_path;
mod rotation_shape;
mod structure;

/// The variables on the leaves under `node`, left to right. A rotation
/// re-brackets a decomposition without disturbing that order, and sorting the
/// same list gives the variable SET a node stands for — what the node IS,
/// independent of the id the tree happened to number it with.
fn leaves_under(vtree: &Vtree, node: VtreeIdx) -> Vec<u32> {
    let mut out = Vec::new();
    let mut stack = vec![node];
    while let Some(cur) = stack.pop() {
        match vtree.node(cur) {
            VtreeNode::Leaf { var, .. } => out.push(var.0),
            VtreeNode::Internal { left, right, .. } => {
                stack.push(*right);
                stack.push(*left);
            }
        }
    }
    out
}