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

//! Which formula's variables a numbering is expressed over.
//!
//! Preprocessing renumbers, so the same `u32` names a different variable
//! depending on which file it came from. Every representation that crosses one
//! of those boundaries — the projection show set, the literal-weight table — is
//! keyed by one of the markers here, so a value expressed over one formula's
//! variables cannot be handed to a consumer expecting another's.

/// Implementation detail of [`Space`]: its supertrait, which only the three
/// markers below implement, so the set of variable spaces is closed.
pub(crate) mod sealed {
    /// Sealing supertrait — see [`super::Space`].
    pub trait Sealed {}
}

/// A variable space a numbering can be expressed in.
///
/// Sealed: the three markers below are all there are, and a fourth space would
/// be a fourth numbering for this crate to keep straight.
pub trait Space: sealed::Sealed + Copy + 'static {}

/// The input CNF's own variable ids, as the file numbers them.
#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Default)]
pub struct Original;

/// `reduced.cnf`'s variable ids — what preprocessing renumbered the survivors
/// into.
#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Default)]
pub struct Reduced;

/// One component's dense `0..num_vars` ids, the space `components/compNNN.cnf`
/// and its vtree are written in.
#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Default)]
pub struct Local;

impl sealed::Sealed for Original {}
impl Space for Original {}
impl sealed::Sealed for Reduced {}
impl Space for Reduced {}
impl sealed::Sealed for Local {}
impl Space for Local {}