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

//! The public simplify policy threaded into the one internal simplify path.

use super::super::plumbing::preprocess_config;
use crate::cnf::{Original, Weights};
use crate::config::{DvePolicy, RunConfig, SimplifyPolicy};
use crate::preprocess::simplify::{SimplifyPrefix, SimplifyPurpose};

fn no_weights() -> Weights<Original> {
    Weights::empty()
}

#[test]
fn custom_policy_reaches_the_count_simplify_config() {
    let config = RunConfig {
        simplify: SimplifyPolicy {
            backbone_budget_ms: Some(17),
            equivalence_budget_ms: None,
            detect_gates: false,
            dve: Some(DvePolicy {
                rounds: 4,
                budget_ms: 29,
            }),
        },
        ..RunConfig::default()
    };

    let internal = preprocess_config(&config, SimplifyPurpose::Count, &no_weights());
    assert_eq!(
        internal.prefix,
        SimplifyPrefix::Backbone {
            budget_ms: 17,
            equivalence_budget_ms: None,
        },
    );
    assert!(!internal.stages.gates);
    assert_eq!(
        internal.stages.dve.map(|dve| (dve.rounds, dve.budget_ms)),
        Some((4, 29)),
    );
}

#[test]
fn enabled_no_backbone_policy_resolves_to_eq_iter_with_the_count_tail() {
    let config = RunConfig {
        simplify: SimplifyPolicy {
            backbone_budget_ms: None,
            equivalence_budget_ms: None,
            detect_gates: true,
            dve: Some(DvePolicy {
                rounds: 4,
                budget_ms: 29,
            }),
        },
        ..RunConfig::default()
    };

    let internal = preprocess_config(&config, SimplifyPurpose::Count, &no_weights());
    assert_eq!(internal.prefix, SimplifyPrefix::EqIter);
    assert!(internal.stages.gates);
    assert_eq!(
        internal.stages.dve.map(|dve| (dve.rounds, dve.budget_ms)),
        Some((4, 29)),
    );
}

#[test]
fn the_stage_switch_explicitly_resolves_the_disabled_prefix() {
    let config = RunConfig {
        stages: crate::config::PreprocessStages {
            simplify: false,
            ..crate::config::PreprocessStages::default()
        },
        ..RunConfig::default()
    };

    let internal = preprocess_config(&config, SimplifyPurpose::Count, &no_weights());
    assert_eq!(internal.prefix, SimplifyPrefix::Disabled);
    assert_eq!(
        internal.stages,
        crate::preprocess::simplify::StageSet::none()
    );
}

#[test]
fn function_contract_caps_count_only_stages() {
    let config = RunConfig {
        simplify: SimplifyPolicy {
            detect_gates: true,
            dve: Some(DvePolicy {
                rounds: 4,
                budget_ms: 29,
            }),
            ..SimplifyPolicy::default()
        },
        ..RunConfig::default()
    };

    let internal = preprocess_config(&config, SimplifyPurpose::Function, &no_weights());
    assert!(!internal.stages.gates, "gate detection is count-only");
    assert!(internal.stages.dve.is_none(), "DVE is count-only");
}