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

use crate::cnf::{Clause, CnfFormula, Literal, VarId, propagate_units};

fn formula(num_vars: u32, clauses: &[&[i32]]) -> CnfFormula {
    CnfFormula {
        num_vars,
        clauses: clauses
            .iter()
            .map(|clause| Clause::new(clause.iter().copied().map(Literal::from).collect()))
            .collect(),
    }
}

#[test]
fn propagation_returns_every_derived_assignment_and_the_residual() {
    let input = formula(3, &[&[1], &[-1, 2], &[1, 3]]);
    let propagated = propagate_units(&input);

    assert_eq!(
        propagated.forced,
        vec![Literal::pos(VarId(0)), Literal::pos(VarId(1))]
    );
    assert!(propagated.residual.clauses.is_empty());
    assert_eq!(propagated.residual.num_vars, input.num_vars);
}

#[test]
fn propagation_reports_a_contradiction_as_one_empty_clause() {
    let input = formula(1, &[&[1], &[-1]]);
    let propagated = propagate_units(&input);

    assert_eq!(propagated.residual.clauses.len(), 1);
    assert!(propagated.residual.clauses[0].is_empty());
}

#[test]
fn a_preexisting_empty_clause_is_immediately_canonicalized() {
    let input = formula(2, &[&[], &[1, 2]]);
    let propagated = propagate_units(&input);

    assert_eq!(propagated.residual.clauses, vec![Clause::new(vec![])]);
    assert!(propagated.forced.is_empty());
}