vj_sim/constraints/

bdd.rs

//! Bit-blasting of the constraint IR into reduced ordered BDDs (plan C3).
//!
//! Every [`Expr`] node becomes a vector of BDDs, one per result bit, least
//! significant first; the whole constraint set becomes one BDD over the
//! random variables' bits whose models are exactly the legal assignments.
//! The gadgets (ripple-carry adder, comparator chain, barrel shifter,
//! shift-add multiplier, restoring divider, ...) live in [`super::blast`],
//! generic over the gate type so the SAT fallback ([`super::sat`]) shares
//! them; this module is the BDD instance of them plus the variable layout.
//! The unit tests check every gadget against the IR's own direct evaluator
//! ([`super::ir::eval`]) on exhaustive or dense assignment sets.
//!
//! # Variable order
//!
//! BDD variable order is *interleaved by bit position* (bit 0 of every random
//! variable, then bit 1, ...). Adders and comparators over two or more
//! variables are linear in that order and exponential in the
//! "all of x, then all of y" order. This order is internal and unrelated to
//! the LRM solve order, which the sampler (`solve`) applies independently
//! by choosing variables in any order it likes.
//!
//! # Definedness (division by zero)
//!
//! [`ir::eval`](super::ir::eval) reports `x / 0` and `x % 0` as an error, and
//! `&&`, `||`, `->` and `?:` only evaluate the operand they need. The blaster
//! mirrors that with a *definedness* BDD carried beside every value: `/` and
//! `%` contribute "divisor is non-zero", short-circuit operators gate the
//! right operand's definedness by the left operand's value, and the final
//! conjunct is `value & defined`. So an assignment on which `eval` would
//! return `DivideByZero` is not a model; it is "not legal", the same way the
//! LRM treats a constraint expression it cannot evaluate as unsatisfied.
//!
//! # Node budget
//!
//! Some functions have no small BDD in any variable order; the multiplier
//! is the canonical one (Bryant 1991). Every apply is run with a node limit
//! ([`NODE_BUDGET`], or the one passed to [`compile`]); exceeding it is the
//! typed [`BddBuildError::TooLarge`], never a hang or an out-of-memory. That
//! error is the trigger of the SAT fallback ([`super::sat`]), which
//! [`super::solve::Engine`] switches to.

use super::blast::{Blaster, Gates};
use super::ir::{ConstraintEvalError, Expr, IrError, StateId, Ty, VarId};
use biodivine_lib_bdd::{Bdd, BddValuation, BddVariable, BddVariableSet, op_function};
use core::fmt;
use num_bigint::BigUint;
use num_traits::Zero;

/// The default per-BDD node limit.
///
/// Calibrated by `tests/constraint_bdd.rs::calibrate_node_budget` (an
/// `#[ignore]`d benchmark: `cargo test -p vj-sim --release --test
/// constraint_bdd -- --ignored --nocapture`). Measured results, `--release`,
/// the final BDD size of the whole formula and the time to build or to give
/// up (the formula is `x * y == z` over three `w`-bit variables unless
/// noted):
///
/// | formula              | outcome at 200k budget | final nodes | seconds |
/// |----------------------|------------------------|-------------|---------|
/// | `x + y == z`, 64-bit | builds                 | 572         | 0.00    |
/// | `x < y`, 64-bit      | builds                 | 193         | 0.00    |
/// | `x / y == z`, 10-bit | builds                 | 8,160       | 0.11    |
/// | multiplier, w = 8    | builds                 | 2,692       | 0.00    |
/// | multiplier, w = 10   | builds                 | 14,456      | 0.01    |
/// | multiplier, w = 12   | builds                 | 77,179      | 0.06    |
/// | multiplier, w = 13   | builds                 | 181,226     | 0.17    |
/// | multiplier, w = 14   | `TooLarge` (fits 500k) | 412,469 at 500k | 0.45 |
/// | multiplier, w = 16   | `TooLarge`             | -           | 0.45    |
/// | multiplier, w = 32   | `TooLarge`             | -           | 0.88    |
/// | multiplier, w = 64   | `TooLarge`             | -           | 2.05    |
///
/// The multiplier's BDD grows by about 2.3x per extra bit of width, so the
/// knee is sharp: 200,000 keeps every adder, comparator, shifter and
/// divider up to the 64-bit machine widths (all under 10,000 nodes in the
/// runs above) plus a multiplier up to 13 bits on the exact path, and any
/// formula that is hopeless for BDDs gives up in about a second. Raising it to
/// 2,000,000 still cannot build a 16-bit multiplier (it fails after 4.9 s)
/// while a failing 32-bit one then takes 28 s and a 64-bit one 47 s to be
/// reported; lowering it to 100,000 loses the 13-bit multiplier for only a
/// 2x saving on the failure path. Each node is 16 bytes, so one BDD is
/// bounded to about 3 MiB.
pub const NODE_BUDGET: usize = 200_000;

/// The largest number of BDD variables (the library's own cap).
pub const MAX_BDD_VARS: usize = u16::MAX as usize - 2;

/// Why a constraint set could not be turned into a BDD.
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum BddBuildError {
    /// A BDD operation would exceed the node budget; the engine falls back
    /// to SAT.
    TooLarge {
        /// The budget that was exceeded.
        budget: usize,
        /// The IR operation being blasted when it was exceeded.
        during: &'static str,
    },
    /// The CNF the SAT fallback would build exceeds its clause limit.
    CnfTooLarge {
        /// The clause limit that was exceeded.
        limit: usize,
        /// The IR operation being blasted when it was exceeded.
        during: &'static str,
    },
    /// More random-variable bits than the BDD library has variables.
    TooManyBits {
        /// Total bits requested.
        bits: usize,
    },
    /// The IR is ill-typed (a builder bug).
    Ir(IrError),
    /// A state variable read has an X/Z bit (LRM 18.3, decision E9).
    StateUnknown(StateId),
    /// The IR names a state variable the caller did not supply.
    UnboundState(StateId),
    /// The IR names a random variable the caller did not declare.
    UnboundVar(VarId),
    /// The IR still holds an array-level node (a run-time expansion bug).
    Unexpanded,
    /// The IR uses a random variable at a width other than its declaration.
    VarWidthMismatch {
        /// The variable.
        var: VarId,
        /// Its declared width.
        declared: u32,
        /// The width the expression reads it at.
        used: u32,
    },
}

impl fmt::Display for BddBuildError {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            BddBuildError::TooLarge { budget, during } => write!(
                f,
                "constraint BDD exceeded the {budget}-node budget while building `{during}`"
            ),
            BddBuildError::CnfTooLarge { limit, during } => write!(
                f,
                "constraint CNF exceeded the {limit}-clause limit while building `{during}`"
            ),
            BddBuildError::TooManyBits { bits } => write!(
                f,
                "{bits} random-variable bits exceed the BDD backend's {MAX_BDD_VARS}-variable limit"
            ),
            BddBuildError::Ir(e) => fmt::Display::fmt(e, f),
            BddBuildError::StateUnknown(s) => {
                fmt::Display::fmt(&ConstraintEvalError::StateUnknown(*s), f)
            }
            BddBuildError::UnboundState(s) => {
                fmt::Display::fmt(&ConstraintEvalError::UnboundState(*s), f)
            }
            BddBuildError::UnboundVar(v) => {
                fmt::Display::fmt(&ConstraintEvalError::UnboundVar(*v), f)
            }
            BddBuildError::Unexpanded => fmt::Display::fmt(&ConstraintEvalError::Unexpanded, f),
            BddBuildError::VarWidthMismatch {
                var,
                declared,
                used,
            } => write!(
                f,
                "random variable #{var} is declared {declared} bits wide but read as {used}"
            ),
        }
    }
}

impl std::error::Error for BddBuildError {}

impl From<IrError> for BddBuildError {
    fn from(e: IrError) -> Self {
        BddBuildError::Ir(e)
    }
}

/// Where each random variable's bits live in the BDD.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Layout {
    /// Declared type of each variable, indexed by [`VarId`].
    pub tys: Vec<Ty>,
    /// `bits[v][i]` is the BDD variable for bit `i` (LSB = 0) of variable `v`.
    pub bits: Vec<Vec<BddVariable>>,
}

impl Layout {
    /// Interleaved layout (module docs) for variables of the given types.
    pub fn interleaved(tys: &[Ty]) -> Result<Layout, BddBuildError> {
        let total: usize = tys.iter().map(|t| t.width as usize).sum();
        if total > MAX_BDD_VARS {
            return Err(BddBuildError::TooManyBits { bits: total });
        }
        let max_w = tys.iter().map(|t| t.width).max().unwrap_or(0);
        let mut bits: Vec<Vec<BddVariable>> = tys
            .iter()
            .map(|t| Vec::with_capacity(t.width as usize))
            .collect();
        let mut next = 0usize;
        for pos in 0..max_w {
            for (v, t) in tys.iter().enumerate() {
                if t.width > pos {
                    bits[v].push(BddVariable::from_index(next));
                    next += 1;
                }
            }
        }
        Ok(Layout {
            tys: tys.to_vec(),
            bits,
        })
    }

    /// Total number of BDD variables.
    pub fn num_bits(&self) -> usize {
        self.tys.iter().map(|t| t.width as usize).sum()
    }

    /// The BDD valuation that encodes `values` (one per variable).
    ///
    /// # Panics
    /// If `values` does not have one entry per declared variable.
    pub fn encode(&self, values: &[BigUint]) -> BddValuation {
        assert_eq!(values.len(), self.tys.len(), "one value per variable");
        let n = u16::try_from(self.num_bits()).expect("checked by interleaved()");
        let mut val = BddValuation::all_false(n);
        for (v, vars) in self.bits.iter().enumerate() {
            for (i, bv) in vars.iter().enumerate() {
                val.set_value(*bv, values[v].bit(i as u64));
            }
        }
        val
    }

    /// The variable values a BDD valuation encodes.
    pub fn decode(&self, val: &BddValuation) -> Vec<BigUint> {
        self.bits
            .iter()
            .map(|vars| {
                let mut x = BigUint::zero();
                for (i, bv) in vars.iter().enumerate() {
                    if val.value(*bv) {
                        x.set_bit(i as u64, true);
                    }
                }
                x
            })
            .collect()
    }
}

/// The result of [`compile`]: one BDD whose models are the legal assignments.
#[derive(Clone, Debug)]
pub struct Compiled {
    /// The conjunction of every constraint (and definedness side condition).
    pub bdd: Bdd,
    /// Variable-to-BDD-variable mapping.
    pub layout: Layout,
}

impl Compiled {
    /// Whether the assignment `values` is a model.
    pub fn accepts(&self, values: &[BigUint]) -> bool {
        self.bdd.eval_in(&self.layout.encode(values))
    }
}

/// Bit-blasts the conjunction of `conjuncts` over variables of types
/// `var_tys` (indexed by [`VarId`]) with state variables fixed to `states`
/// (a `None` entry is an X/Z-holding state and fails if read). Every BDD
/// operation is limited to `budget` nodes.
pub fn compile(
    var_tys: &[Ty],
    states: &[Option<BigUint>],
    conjuncts: &[Expr],
    budget: usize,
) -> Result<Compiled, BddBuildError> {
    let layout = Layout::interleaved(var_tys)?;
    let n = u16::try_from(layout.num_bits()).expect("checked by interleaved()");
    let gates = BddGates {
        set: BddVariableSet::new_anonymous(n),
        layout: &layout,
        budget,
    };
    let mut acc = gates.set.mk_true();
    {
        let widths: Vec<usize> = layout.bits.iter().map(Vec::len).collect();
        let b = Blaster {
            g: &gates,
            widths: &widths,
            states,
        };
        for c in conjuncts {
            c.validate()?;
            let t = b.conjunct(c)?;
            acc = gates.and("constraint conjunction", &acc, &t)?;
        }
    }
    Ok(Compiled { bdd: acc, layout })
}

type OpFn = fn(Option<bool>, Option<bool>) -> Option<bool>;

/// The BDD back end of the shared bit-blaster ([`super::blast`]): a bit is a
/// [`Bdd`], and every binary operation is limited to `budget` nodes.
struct BddGates<'a> {
    set: BddVariableSet,
    layout: &'a Layout,
    budget: usize,
}

impl BddGates<'_> {
    fn lim(&self, during: &'static str, f: OpFn, a: &Bdd, b: &Bdd) -> Result<Bdd, BddBuildError> {
        Bdd::binary_op_with_limit(self.budget, a, b, f).ok_or(BddBuildError::TooLarge {
            budget: self.budget,
            during,
        })
    }
}

impl Gates for BddGates<'_> {
    type Bit = Bdd;

    fn constant(&self, v: bool) -> Bdd {
        if v {
            self.set.mk_true()
        } else {
            self.set.mk_false()
        }
    }

    fn as_const(&self, a: &Bdd) -> Option<bool> {
        if a.is_true() {
            Some(true)
        } else if a.is_false() {
            Some(false)
        } else {
            None
        }
    }

    fn input(&self, var: VarId, i: usize) -> Bdd {
        self.set.mk_var(self.layout.bits[var as usize][i])
    }

    fn not(&self, a: &Bdd) -> Bdd {
        a.not()
    }

    fn and(&self, d: &'static str, a: &Bdd, b: &Bdd) -> Result<Bdd, BddBuildError> {
        if a.is_false() || b.is_false() {
            return Ok(self.set.mk_false());
        }
        if a.is_true() {
            return Ok(b.clone());
        }
        if b.is_true() || a == b {
            return Ok(a.clone());
        }
        self.lim(d, op_function::and, a, b)
    }

    fn or(&self, d: &'static str, a: &Bdd, b: &Bdd) -> Result<Bdd, BddBuildError> {
        if a.is_true() || b.is_true() {
            return Ok(self.set.mk_true());
        }
        if a.is_false() {
            return Ok(b.clone());
        }
        if b.is_false() || a == b {
            return Ok(a.clone());
        }
        self.lim(d, op_function::or, a, b)
    }

    fn xor(&self, d: &'static str, a: &Bdd, b: &Bdd) -> Result<Bdd, BddBuildError> {
        if a.is_false() {
            return Ok(b.clone());
        }
        if b.is_false() {
            return Ok(a.clone());
        }
        if a.is_true() {
            return Ok(b.not());
        }
        if b.is_true() {
            return Ok(a.not());
        }
        if a == b {
            return Ok(self.set.mk_false());
        }
        self.lim(d, op_function::xor, a, b)
    }

    fn mux(&self, d: &'static str, s: &Bdd, a: &Bdd, b: &Bdd) -> Result<Bdd, BddBuildError> {
        if s.is_true() {
            return Ok(a.clone());
        }
        if s.is_false() {
            return Ok(b.clone());
        }
        if a == b {
            return Ok(a.clone());
        }
        let t = self.and(d, s, a)?;
        let e = self.and(d, &s.not(), b)?;
        self.or(d, &t, &e)
    }
}