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

use super::*;

#[test]
fn primal_graph_simplicial() {
    // Triangle: vars 0,1,2 all co-occur in one clause
    let f = make_formula(3, vec![vec![1, 2, 3]]);
    let g = PrimalGraph::new(3, &f.clauses);
    assert!(g.is_simplicial(0));
    assert!(g.is_simplicial(1));
    assert!(g.is_simplicial(2));
}

#[test]
fn primal_graph_not_simplicial() {
    // Path: 0-1, 1-2 but not 0-2
    let f = make_formula(3, vec![vec![1, 2], vec![2, 3]]);
    let g = PrimalGraph::new(3, &f.clauses);
    assert!(!g.is_simplicial(1));
    assert!(g.is_simplicial(0));
    assert!(g.is_simplicial(2));
}