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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86

use crate::cnf::Clause;
use crate::cnf::CnfFormula;
use crate::cnf::Literal;
use crate::decompose::hybrid::*;
use crate::decompose::{ConversionRequest, Reading};
use crate::tests::td_fixture::make_test_td;
use crate::vtree::VarId;
use crate::vtree::VtreeIdx;

fn make_test_formula() -> CnfFormula {
    let clauses = vec![
        Clause::new(vec![
            Literal {
                var: VarId(0),
                positive: true,
            },
            Literal {
                var: VarId(1),
                positive: false,
            },
        ]),
        Clause::new(vec![
            Literal {
                var: VarId(1),
                positive: true,
            },
            Literal {
                var: VarId(2),
                positive: true,
            },
        ]),
        Clause::new(vec![
            Literal {
                var: VarId(2),
                positive: false,
            },
            Literal {
                var: VarId(3),
                positive: true,
            },
        ]),
        Clause::new(vec![
            Literal {
                var: VarId(3),
                positive: false,
            },
            Literal {
                var: VarId(4),
                positive: true,
            },
        ]),
        Clause::new(vec![
            Literal {
                var: VarId(4),
                positive: false,
            },
            Literal {
                var: VarId(5),
                positive: true,
            },
        ]),
    ];
    CnfFormula {
        num_vars: 6,
        clauses,
    }
}

#[test]
fn guided_bisect_with_precomputed_td() {
    let formula = make_test_formula();
    let td = make_test_td();
    let dials = crate::decompose::BisectDials {
        imbalance: 0.30,
        base_seed: 0,
        effort_scale: 1.0,
    };
    let conversion = ConversionRequest::open(Reading::default(), None);
    let result = vtree_from_guided_bisect(&formula, &td, dials, conversion);
    assert!(result.is_ok());
    let vtree = result.unwrap();
    let leaf_count = (0..vtree.num_nodes())
        .filter(|&i| vtree.node(VtreeIdx(i as u32)).is_leaf())
        .count();
    assert_eq!(leaf_count, 6);
}