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

//! Tree-decomposition fixtures shared by vitri's construction tests.

use crate::decompose::TreeDecomposition;
use crate::tests::common::make_td;

/// A three-bag path decomposition of six variables, sharing two variables
/// across the first join and one across the second.
pub(crate) fn make_test_td() -> TreeDecomposition {
    make_td(
        vec![vec![0, 1, 2], vec![1, 2, 3], vec![3, 4, 5]],
        vec![(0, 1), (1, 2)],
        6,
    )
}