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

use crate::cnf::Clause;
use crate::cnf::CnfFormula;
use crate::preprocess::cadical::*;
use crate::preprocess::cadical_ffi::Terminator;
use crate::tests::common::lit;
use std::time::Duration;

#[test]
fn wall_clock_terminator_fires_after_deadline() {
    let mut t = WallClockTerminator::new(Duration::from_millis(5));
    std::thread::sleep(Duration::from_millis(20));
    assert!(t.terminated());
}

#[test]
fn wall_clock_terminator_not_yet_fired() {
    let mut t = WallClockTerminator::new(Duration::from_secs(60));
    assert!(!t.terminated());
}

#[test]
fn preprocess_cadical_budgeted_with_huge_budget_matches_default() {
    let f = CnfFormula {
        num_vars: 2,
        clauses: vec![
            Clause::new(vec![lit(0, true)]),
            Clause::new(vec![lit(0, false), lit(1, true)]),
        ],
    };
    let (a, fa) = preprocess_cadical_budgeted(&f, 3, Some(Duration::from_secs(60)));
    let (b, fb) = preprocess_cadical_budgeted(&f, 3, None);
    assert_eq!(fa, fb);
    assert_eq!(a.num_vars, b.num_vars);
    assert_eq!(a.clauses.len(), b.clauses.len());
}