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

//! Preprocessing passes tested through items their own modules keep to
//! themselves. A pass with its own directory carries its tests there instead;
//! what reaches only the crate root is tested from `src/tests/preprocess/`.

mod bve_project;
mod cadical;
mod cadical_ffi;
mod count_preserve;
mod equivalence;
mod fork_budget;
mod gates;
mod pipelines;
mod probe_engine;
mod projected;
mod renumber;
mod simplify;
mod tarjan;
mod unit_propagation;
mod weighted_lift;