bitwright 0.11.0

Hash-consed fixed-width bit-vector expressions: exact evaluation, bit-level facts, and verified simplification.
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

//! The MBA service (feature `mba`): simplification of mixed Boolean-arithmetic expressions by a
//! pluggable solver, behind an evidence gate. See `docs/design.md` §9.
//!
//! The engine lowers a fragment of the arena (`+ − * neg & | ^ ~`, constant shifts, casts) into
//! an [`MbaExpr`] over its atoms, asks the configured [`MbaSolver`], and accepts an answer only
//! with exact evidence: the linear-MBA signature (complete for linear MBA), exhaustive
//! evaluation for small inputs, an [`EquivalenceProver`], or, if the configuration trusts them,
//! the backend's certificate or sampling. The lifted result must also agree with the original
//! expression at seeded points, and it replaces the node only when the DAG gets smaller.
//!
//! ```
//! use bitwright::engine::{Engine, Phase, Strategy};
//! use bitwright::mba::MbaConfig;
//! use bitwright::{Context, ParseOptions, Width};
//!
//! let engine = Engine::builder()
//!     .builtin()
//!     .strategy(Strategy::new("mba", vec![Phase::Mba(MbaConfig::default())]))
//!     .build()?;
//! let mut cx = Context::new();
//! let e = cx.parse("(x ^ y) + 2 * (x & y) + ((x | y) - (x & y) - (x ^ y))", &ParseOptions::width(Width::W64))?;
//! let out = engine.simplify(&mut cx, e)?;
//! let want = cx.parse("x + y", &ParseOptions::width(Width::W64))?;
//! assert_eq!(out.expr, want);
//! # Ok::<(), Box<dyn std::error::Error>>(())
//! ```

mod batch;
pub(crate) mod certify;
mod expr;
mod lower;
mod nf;
mod solve;
mod threaded;

pub use crate::engine::CertStats;
pub use certify::NativeProver;
pub use nf::{NfOptions, NfStats, NormalFormSolver};
pub use threaded::ThreadedSolver;

pub use expr::{MNode, MOp, MbaError, MbaExpr, Shape};
pub use lower::{Bindings, MbaLimits, Refusal, lift, lower};
pub(crate) use lower::{fits, lift_id, lower_id};
pub use solve::{
    CacheEntry, CacheKey, Claim, EquivalenceProver, MbaAnswer, MbaBudget, MbaCacheStore, MbaSolver,
    MemoryCache, NoCache, SignatureSolver, Verdict,
};

/// Which evidence beyond bitwright's own checks is accepted.
#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)]
#[non_exhaustive]
pub struct MbaTrust {
    /// Accept a solver's `Proved` or `Certified` claim.
    pub backend_certificates: bool,
    /// Accept agreement at sampled points (not a proof).
    pub sampled: bool,
}

setters!(MbaTrust {
    with_backend_certificates: backend_certificates: bool,
    with_sampled: sampled: bool,
});

impl Default for MbaTrust {
    /// Neither: answers are accepted on bitwright's own certificates, or on the proof of a
    /// configured [`EquivalenceProver`], only.
    fn default() -> Self {
        MbaTrust {
            backend_certificates: false,
            sampled: false,
        }
    }
}

/// The configuration of a `Phase::Mba`.
#[derive(Copy, Clone, Debug, Default, PartialEq, Eq, Hash)]
#[non_exhaustive]
pub struct MbaConfig {
    /// What is lowered and asked about.
    pub limits: MbaLimits,
    /// Which evidence is accepted.
    pub trust: MbaTrust,
    /// Passed to the solver.
    pub budget: MbaBudget,
}

setters!(MbaConfig {
    with_limits: limits: MbaLimits,
    with_trust: trust: MbaTrust,
    with_budget: budget: MbaBudget,
});

/// The version of the lowering (part of every cache key).
pub(crate) const LOWERING_VERSION: u64 = 1;

#[cfg(test)]
mod tests;