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

//! The in-process Arjun binding, over the budget policy and the shim
//! `arjun_lib` keeps to itself.

use crate::cnf::Clause;
use crate::cnf::CnfFormula;
use crate::cnf::Literal;
use crate::cnf::VarId;
use crate::error::VitriError;
use crate::preprocess::arjun::ArjunOptions;
use crate::preprocess::arjun_lib::budget_class::*;
use crate::preprocess::arjun_lib::shim::*;
use crate::preprocess::arjun_lib::*;
use num_rational::BigRational;
use std::time::Duration;
use std::time::Instant;

mod anytime;
mod count_preserve;
mod knobs;
mod learnt_clauses;