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

//! Vtree specification strings: what they parse to, and what they build.
//!
//! Shared by the parsing topics: [`parse_ok`], which parses a spec and fails
//! the case rather than the assertion if it does not parse at all.

use crate::cnf::CnfFormula;
use crate::cnf::{Clause, Literal};
use crate::decompose::Binarization;
use crate::decompose::BuildLimits;
use crate::decompose::Place;
use crate::decompose::Reading;
use crate::decompose::Root;
use crate::decompose::SelectionCtx;
use crate::spec::*;
use crate::vtree::VarId;

mod build;
mod conversion;
mod params;
mod vocabulary;

fn parse_ok(spec: &str) -> ParsedSpec<'_> {
    parse_vtree_spec(spec).unwrap_or_else(|e| panic!("{spec} must parse: {e}"))
}