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

//! Soundness gate for the export bundle, in every mode.
//!
//! The counts on both sides come from the crate's own brute-force oracles
//! ([`crate::tests::pmc_oracle`]) — ground truth, not hand-written constants
//! — and the reduced side is counted over the file that was actually WRITTEN and
//! re-parsed, so the DIMACS writer, the `c t` / `c p show` / `c p weight`
//! carry-forward and the record all sit inside the assertion rather than beside
//! it.
//!
//! The hand-written cases below pin specific structures (backbone, equivalences,
//! free vars, definitions, UNSAT); [`property`] then sweeps randomized small
//! instances through every mode, which is what catches the composition bugs
//! a fixed corpus never reaches.

use super::common::{Scratch, parse, rat};
use crate::bundle::*;
use crate::cnf::CnfFormula;
use crate::cnf::CnfMeta;
use crate::cnf::Mode;
use crate::cnf::rational_string;
use crate::cnf::{Clause, Literal};
use crate::cnf::{DimacsHeader, write_dimacs};
use crate::cnf::{Original, Reduced, ShowSet, VarId, Weights};
use crate::config::RunConfig;
use crate::preprocess::OriginalTarget;
use crate::tests::pmc_oracle::{brute_force_mc, brute_force_pmc, brute_force_pwmc};
use num_bigint::BigUint;
use num_rational::BigRational;

mod arjun;
mod compile;
mod components;
mod harness;
mod mc;
mod mode_selection;
mod projected;
mod property;
mod report;
mod run;
mod stages;
mod weighted;
mod writer;

use harness::*;