bitwright 0.14.0

//! SMT-LIB 2.6 (QF_BV, and QF_BVFP for floating point) export and import (feature `smtlib`).
//!
//! bitwright's semantics are SMT-LIB's (total division, shifts past the width), so every
//! expression has an exact QF_BV counterpart: operators map directly, and the ones QF_BV lacks
//! (population count, leading and trailing zeros, byte swap, bit reverse, `pdep`, `pext`, the high
//! half of a product, rotations by a symbolic count) are expanded. Floating-point operations use
//! the FloatingPoint theory, a result's bits declared and pinned by one assertion (SMT-LIB has
//! no standard `fp.to_ieee_bv`), and what SMT-LIB leaves open written out as bitwright defines
//! it (the canonical NaN, `−0 < +0` in `min`/`max`, saturating conversions to integers). Any
//! SMT-LIB 2.6 solver can then evaluate an expression, check an equivalence, or prove a rule at
//! any widths ([`rule_obligation`]). [`import`] reads a QF_BV subset back, and QF_BVFP terms
//! over floats.
//!
//! ```
//! use bitwright::{Context, ParseOptions, Width};
//! let mut cx = Context::new();
//! let e = cx.parse("udiv(x, y) + (x << 3)", &ParseOptions::width(Width::W8))?;
//! let smt = bitwright::smtlib::export(&mut cx, &[e])?;
//! assert!(smt.contains("(declare-const |x| (_ BitVec 8))"));
//! assert!(smt.contains("bvudiv"));
//! assert!(smt.contains("(define-fun root0 () (_ BitVec 8)"));
//!
//! // And back, into another context. (Operators SMT-LIB lacks come back expanded.)
//! let mut other = Context::new();
//! let script = bitwright::smtlib::import(&mut other, &smt)?;
//! let back = script.definition("root0").unwrap();
//! assert_eq!(other.display(back).to_string(), cx.display(e).to_string());
//! # Ok::<(), bitwright::Error>(())
//! ```

mod export;
mod fp;
mod import;
mod obligation;
#[cfg(test)]
mod tests;

pub use import::{Import, import};
pub use obligation::rule_obligation;

use crate::error::Error;
use crate::expr::{Context, Expr};
use crate::facts::{Assumptions, Reliance};

/// The expressions as SMT-LIB 2.6: a `declare-const` per symbol, a `define-fun` per node
/// (operands first, so sharing is kept; the names `n…` are internal), and `define-fun rootK` for
/// the `K`-th root. Symbols keep their names where SMT-LIB can spell them (see [`import`] for
/// integer and fresh keys); others are named `sym!id`.
pub fn export(cx: &mut Context, roots: &[Expr]) -> Result<String, Error> {
    export::emit(cx, roots)
}

/// A complete script asking whether `a` and `b` can differ: `unsat` from a solver proves them
/// equal at their width; with `sat`, the model is a counterexample, unless the expressions
/// contain extension operations exported as uninterpreted functions (then the script says
/// `QF_UFBV`, and a model may rest on values the real operation never takes).
pub fn equivalence_query(cx: &mut Context, a: Expr, b: Expr) -> Result<String, Error> {
    if cx.width(a)? != cx.width(b)? {
        return Err(Error::Unsupported("different widths".into()));
    }
    let body = export::emit(cx, &[a, b])?;
    let mut s = logic(&body);
    s.push_str(&body);
    s.push_str("(assert (not (= root0 root1)))\n(check-sat)\n");
    Ok(s)
}

/// [`equivalence_query`] where the constraints of `assumptions` in `relied` hold: each is
/// asserted, so `unsat` proves `a` and `b` equal wherever they hold. Pass the
/// [`relies_on`](crate::engine::RootOutcome::relies_on) of a rewrite to check it independently
/// under exactly what it relied on.
pub fn equivalence_query_under(
    cx: &mut Context,
    a: Expr,
    b: Expr,
    assumptions: &Assumptions,
    relied: Reliance,
) -> Result<String, Error> {
    if cx.width(a)? != cx.width(b)? {
        return Err(Error::Unsupported("different widths".into()));
    }
    let mut roots = vec![a, b];
    for (id, e, f) in assumptions.constraints() {
        if relied.may_use(id) {
            let value = cx.id(e)?;
            let predicate = crate::facts::facts_predicate(cx, value, f)?;
            roots.push(cx.handle(predicate));
        }
    }
    let body = export::emit(cx, &roots)?;
    let mut s = logic(&body);
    s.push_str(&body);
    for k in 2..roots.len() {
        s.push_str(&format!("(assert (= root{k} #b1))\n"));
    }
    s.push_str("(assert (not (= root0 root1)))\n(check-sat)\n");
    Ok(s)
}

/// The `set-logic` line for a script: `QF_BV`, or `QF_UFBV` when extension operations without an
/// SMT-LIB definition were declared as uninterpreted functions. (Then `unsat` still proves
/// equality, but `sat` may be an artefact of the uninterpreted function, not a counterexample.)
fn logic(body: &str) -> String {
    let uf = body.contains("(declare-fun ");
    let fp = body.contains("(_ to_fp ");
    String::from(match (uf, fp) {
        (false, false) => "(set-logic QF_BV)\n",
        (true, false) => "(set-logic QF_UFBV)\n",
        (false, true) => "(set-logic QF_BVFP)\n",
        (true, true) => "(set-logic ALL)\n",
    })
}