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
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144

use super::*;

/// Apply a rotation two ways — pointer-only + `fixup_topo_after_rotate`
/// vs pointer-only + full `rebuild_topo` — and check that both produce
/// vtrees satisfying the topo invariants. The two `topo` arrays may
/// differ (fixup doesn't promise strict postorder), but each must be a
/// valid bottom-up order satisfying the root-last property.
fn check_fixup_equivalence_left(mut vtree: Vtree, v: VtreeIdx) {
    let mut via_rebuild = vtree.clone();
    let info_a = rotate_left_pointers(&mut vtree, v).expect("applicable");
    vtree.fixup_topo_after_rotate(&info_a, RotationKind::Left);
    assert_invariants(&vtree);

    let info_b = rotate_left_pointers(&mut via_rebuild, v).expect("applicable");
    via_rebuild.rebuild_topo();
    assert_invariants(&via_rebuild);
    assert_eq!(info_a.v_idx, info_b.v_idx);
    assert_eq!(info_a.w_idx, info_b.w_idx);
}

fn check_fixup_equivalence_right(mut vtree: Vtree, v: VtreeIdx) {
    let mut via_rebuild = vtree.clone();
    let info_a = rotate_right_pointers(&mut vtree, v).expect("applicable");
    vtree.fixup_topo_after_rotate(&info_a, RotationKind::Right);
    assert_invariants(&vtree);

    let info_b = rotate_right_pointers(&mut via_rebuild, v).expect("applicable");
    via_rebuild.rebuild_topo();
    assert_invariants(&via_rebuild);
    assert_eq!(info_a.v_idx, info_b.v_idx);
    assert_eq!(info_a.w_idx, info_b.w_idx);
}

#[test]
fn fixup_equivalence_left_at_root() {
    check_fixup_equivalence_left(Vtree::linear(5), Vtree::linear(5).root);
}

#[test]
fn fixup_equivalence_right_at_root_balanced() {
    // balanced(4) is the case the early-exit cannot use (right rotation
    // pre-fixup has C after w in topo) — exercises the slice-rotate path.
    check_fixup_equivalence_right(Vtree::balanced(4), Vtree::balanced(4).root);
}

#[test]
fn fixup_equivalence_right_at_root_balanced_8() {
    check_fixup_equivalence_right(Vtree::balanced(8), Vtree::balanced(8).root);
}

#[test]
fn fixup_equivalence_at_internal_non_root() {
    let vtree = Vtree::balanced(8);
    let target = (0..vtree.num_nodes() as u32)
        .map(VtreeIdx)
        .find(|&t| {
            if let VtreeNode::Internal {
                left,
                right,
                parent,
            } = *vtree.node(t)
            {
                parent.is_some() && !vtree.node(left).is_leaf() && !vtree.node(right).is_leaf()
            } else {
                false
            }
        })
        .expect("balanced(8) has at least one such node");
    check_fixup_equivalence_left(vtree.clone(), target);
    check_fixup_equivalence_right(vtree, target);
}

/// Round-trip: a sequence of rotations followed by their inverses (via
/// `unrotate_*`) restores the structure bit-for-bit and produces a
/// vtree that still satisfies the topo invariants at every step.
#[test]
fn fixup_round_trip_random_sequence() {
    let mut vtree = Vtree::balanced(8);
    let original = vtree.clone();
    let mut history: Vec<(RotationInfo, RotKindLocal)> = Vec::new();

    // Deterministic pseudo-random walk: try a left rotation at every
    // internal node bottom-up, then a right rotation, recording each
    // applicable success.
    let internal: Vec<VtreeIdx> = vtree
        .bottomup_topo()
        .iter()
        .copied()
        .filter(|&t| !vtree.node(t).is_leaf())
        .collect();
    for &t in &internal {
        if let Some(info) = rotate_left(&mut vtree, t) {
            assert_invariants(&vtree);
            history.push((info, RotKindLocal::Left));
        }
        if let Some(info) = rotate_right(&mut vtree, t) {
            assert_invariants(&vtree);
            history.push((info, RotKindLocal::Right));
        }
    }
    while let Some((info, kind)) = history.pop() {
        match kind {
            RotKindLocal::Left => unrotate_left(&mut vtree, &info),
            RotKindLocal::Right => unrotate_right(&mut vtree, &info),
        }
        assert_invariants(&vtree);
    }
    assert_equal(&vtree, &original);
}

/// Edge case: rotation where the misplaced subtree's root is a leaf.
/// This is the smallest possible misplaced subtree. The slice has at
/// most two elements and `rotate_left(1)` is a single swap.
#[test]
fn fixup_handles_single_node_misplaced_subtree() {
    let mut vtree = Vtree::linear(4);
    let root = vtree.root;
    let info = rotate_left(&mut vtree, root).expect("applicable");
    assert_invariants(&vtree);
    unrotate_left(&mut vtree, &info);
    assert_invariants(&vtree);
}

/// Edge case: two consecutive rotations at the same node.
#[test]
fn fixup_handles_consecutive_rotations_at_same_node() {
    let mut vtree = Vtree::balanced(8);
    let root = vtree.root;
    let _ = rotate_left(&mut vtree, root).expect("applicable");
    assert_invariants(&vtree);
    // After a left rotation at root, the new root's right child is what
    // was C (an internal subtree in balanced(8)) — try a left rotation
    // again. Applicability depends on whether new C's right subtree is
    // internal; if not, this is a no-op None.
    let _ = rotate_left(&mut vtree, root);
    assert_invariants(&vtree);
}

// Mirrors the crate-private `RotKind` — tests can't reference it directly.
#[derive(Copy, Clone, Debug)]
enum RotKindLocal {
    Left,
    Right,
}