Struct Context 

pub struct Context { /* private fields */ }

A hash-consed expression arena.

A context owns every node it creates. Nodes are immutable and appended in creation order, and every child index is lower than its parent’s, so ascending index order is a topological order. Structurally equal expressions are the same node (“equal handle implies equal value”; the converse does not hold). Every node is in canonical form: constants are folded, commutative operands are ordered (constants last) independently of construction order, and a fixed set of O(1) identities and cast collapses is applied (see docs/design.md §4.3).

use bitwright::{Context, Width};
let mut cx = Context::new();
let x = cx.symbol("x", Width::W32)?;
let one = cx.one(Width::W32)?;
let a = cx.add(one, x)?;
let b = cx.add(x, one)?;
assert_eq!(a, b);
let z = cx.xor(a, b)?;
assert_eq!(cx.as_const(z)?.map(|v| v.is_zero()), Some(true));

Implementations

impl Context

pub fn ext(&mut self, op: ExtId, args: &[Expr]) -> Result<Vec<Expr>, Error>

Every output of the extension call op(args) (1 to 3 arguments), in order. Needs a context built with a registry holding op (with_registry); outputs of calls on constants are constants.

pub fn ext_output( &mut self, op: ExtId, k: usize, args: &[Expr], ) -> Result<Expr, Error>

Output k of the extension call op(args).

pub fn constant(&mut self, v: &BitVec) -> Result<Expr, Error>

A constant.

pub fn constant_u64(&mut self, width: Width, v: u64) -> Result<Expr, Error>

The constant v, which must fit in width bits.

pub fn constant_u128(&mut self, width: Width, v: u128) -> Result<Expr, Error>

The constant v, which must fit in width bits.

pub fn constant_i128(&mut self, width: Width, v: i128) -> Result<Expr, Error>

The constant v, which must be representable as a signed width-bit value.

pub fn zero(&mut self, width: Width) -> Result<Expr, Error>

Zero.

pub fn one(&mut self, width: Width) -> Result<Expr, Error>

One.

pub fn ones(&mut self, width: Width) -> Result<Expr, Error>

All ones.

pub fn bool(&mut self, b: bool) -> Result<Expr, Error>

A 1-bit constant.

pub fn un(&mut self, op: UnOp, a: Expr) -> Result<Expr, Error>

A unary operator.

pub fn bin(&mut self, op: BinOp, a: Expr, b: Expr) -> Result<Expr, Error>

A binary operator; the operands must have the same width.

pub fn cmp( &mut self, op: impl Into<CmpOpExt>, a: Expr, b: Expr, ) -> Result<Expr, Error>

A comparison (1-bit result); the operands must have the same width.

pub fn zext(&mut self, a: Expr, to: Width) -> Result<Expr, Error>

Zero extension to to (at least the operand’s width; equal width is the identity).

pub fn sext(&mut self, a: Expr, to: Width) -> Result<Expr, Error>

Sign extension to to (at least the operand’s width; equal width is the identity).

pub fn trunc(&mut self, a: Expr, to: Width) -> Result<Expr, Error>

The low to bits.

pub fn extract(&mut self, a: Expr, lo: u16, len: Width) -> Result<Expr, Error>

Bits [lo, lo + len).

pub fn concat(&mut self, hi: Expr, lo: Expr) -> Result<Expr, Error>

hi in the high bits, lo in the low bits.

pub fn select( &mut self, cond: Expr, then: Expr, els: Expr, ) -> Result<Expr, Error>

cond ? then : els; the condition must be 1 bit wide.

impl Context

pub fn not(&mut self, a: Expr) -> Result<Expr, Error>

Bitwise complement.

pub fn neg(&mut self, a: Expr) -> Result<Expr, Error>

Two’s-complement negation.

pub fn popcnt(&mut self, a: Expr) -> Result<Expr, Error>

Number of set bits.

pub fn clz(&mut self, a: Expr) -> Result<Expr, Error>

Leading zeros (clz(0) = W).

pub fn ctz(&mut self, a: Expr) -> Result<Expr, Error>

Trailing zeros (ctz(0) = W).

pub fn bswap(&mut self, a: Expr) -> Result<Expr, Error>

Byte reversal (W % 8 == 0).

pub fn bitrev(&mut self, a: Expr) -> Result<Expr, Error>

Bit reversal.

impl Context

pub fn add(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Addition.

pub fn sub(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Subtraction.

pub fn mul(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Multiplication.

pub fn umulhi(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

High half of the unsigned double-width product.

pub fn smulhi(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

High half of the signed double-width product.

pub fn udiv(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Unsigned division (udiv(x, 0) = ones).

pub fn urem(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Unsigned remainder (urem(x, 0) = x).

pub fn sdiv(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Signed division (bvsdiv).

pub fn srem(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Signed remainder (bvsrem).

pub fn and(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Bitwise and.

pub fn or(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Bitwise or.

pub fn xor(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Bitwise exclusive or.

pub fn shl(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Left shift (a count >= W gives 0).

pub fn lshr(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Logical right shift (a count >= W gives 0).

pub fn ashr(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Arithmetic right shift (a count >= W gives the sign fill).

pub fn rotl(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Rotate left by count mod W.

pub fn rotr(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Rotate right by count mod W.

pub fn pdep(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Parallel bit deposit.

pub fn pext(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Parallel bit extract.

impl Context

pub fn eq(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

a == b.

pub fn ne(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

a != b.

pub fn ult(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Unsigned a < b.

pub fn ule(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Unsigned a <= b.

pub fn ugt(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Unsigned a > b.

pub fn uge(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Unsigned a >= b.

pub fn slt(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Signed a < b.

pub fn sle(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Signed a <= b.

pub fn sgt(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Signed a > b.

pub fn sge(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Signed a >= b.

impl Context

Derived constructors: they build existing node kinds.

pub fn umin(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Unsigned minimum.

pub fn umax(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Unsigned maximum.

pub fn smin(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Signed minimum.

pub fn smax(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Signed maximum.

pub fn andn(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

a & ~b.

pub fn orn(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

a | ~b.

pub fn xnor(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

~(a ^ b).

pub fn bit(&mut self, a: Expr, i: u16) -> Result<Expr, Error>

Bit i as a 1-bit value.

pub fn abs(&mut self, a: Expr) -> Result<Expr, Error>

Absolute value (abs(smin) = smin).

pub fn add_carry(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

The carry out of a + b (1 bit).

pub fn sub_borrow(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

The borrow out of a - b (1 bit).

pub fn sadd_overflow(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Signed overflow of a + b (1 bit).

pub fn ssub_overflow(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

Signed overflow of a - b (1 bit).

pub fn add_sat_u(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

a + b clamped to the unsigned range: all ones when the sum carries out.

pub fn sub_sat_u(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

a - b clamped to the unsigned range: 0 when b exceeds a.

pub fn add_sat_s(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

a + b clamped to the signed range: the signed minimum or maximum on overflow.

pub fn sub_sat_s(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

a - b clamped to the signed range: the signed minimum or maximum on overflow.

pub fn mul_wide_u(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

The full 2W-bit unsigned product (2W <= 512).

pub fn mul_wide_s(&mut self, a: Expr, b: Expr) -> Result<Expr, Error>

The full 2W-bit signed product (2W <= 512).

impl Context

pub fn eval( &mut self, roots: &[Expr], env: &(impl Env + ?Sized), ) -> Result<Vec<BitVec>, Error>

Evaluates roots under env. Iterative and memoized per call: a shared node is evaluated once.

pub fn substitute( &mut self, roots: &[Expr], map: &[(Expr, Expr)], ) -> Result<Vec<Expr>, Error>

Simultaneously replaces every occurrence of each from by its to in roots (replacements are not substituted again), rebuilding through the canonicalizing constructors. Each pair must have equal widths.

pub fn substitute_bounded( &mut self, roots: &[Expr], s: &mut Substitution, max_visits: u64, ) -> Result<Option<Vec<Expr>>, Error>

Applies the substitution s to roots, working on at most max_visits nodes not already in its memo. Ok(None) when that limit stops it first: the progress is kept in s, so a later call continues where this one stopped. The walk never descends below a replaced node or a node the memo already answers.

impl Context

pub fn new() -> Self

An empty context with the default configuration. Allocates nothing until the first node.

pub fn with_config(config: ContextConfig) -> Self

An empty context.

pub fn with_registry(config: ContextConfig, registry: Arc<Registry>) -> Self

An empty context that can build the extension operations of registry.

pub fn registry(&self) -> Option<&Registry>

The extension operations this context can build.

pub fn extend_registry(&mut self, registry: Arc<Registry>) -> Result<(), Error>

Replaces the registry by one that extends it: every operation of the current registry is at the same position in registry (same name, revision and traits), so every existing node keeps its meaning and canonical form. Otherwise an error, and nothing changes.

pub fn config(&self) -> &ContextConfig

The configuration.

pub fn set_max_nodes(&mut self, n: u32)

Changes the node limit (ContextConfig::max_nodes). Existing nodes stay; a limit below the current size only stops new nodes from being created (lookups of existing structure still succeed).

pub fn len(&self) -> usize

The number of nodes.

pub fn is_empty(&self) -> bool

Whether the context has no nodes.

pub fn clear(&mut self)

Removes every node and symbol, keeping allocations. Handles created before the call become stale and are rejected with Error::StaleExpr.

pub fn counters(&self) -> ArenaCounters

Node creation counters.

pub fn mark(&self) -> Mark

The current position of the caller-growth counter.

pub fn caller_growth_since(&self, mark: Mark) -> u64

New nodes created by the caller since mark (all of them, if the mark is from another context or from before a clear()). Nodes created by the library itself are not counted.

pub fn width(&self, e: Expr) -> Result<Width, Error>

The width of an expression.

pub fn view(&self, e: Expr) -> Result<View, Error>

A read-only view of an expression’s top node.

pub fn children( &self, e: Expr, ) -> Result<impl Iterator<Item = Expr> + '_, Error>

The expression’s direct operands, in order.

pub fn as_const(&self, e: Expr) -> Result<Option<BitVec>, Error>

The value, if the expression is a constant node.

pub fn is_leaf(&self, e: Expr) -> Result<bool, Error>

Whether the expression is a constant or a symbol.

pub fn height(&self, e: Expr) -> Result<u32, Error>

Structural depth (leaves are 0), saturating at u32::MAX. O(1).

pub fn tree_size(&self, e: Expr) -> Result<u32, Error>

The size of the expression unfolded as a tree, saturating at u32::MAX. O(1).

pub fn symbol( &mut self, key: impl Into<SymbolKey>, width: Width, ) -> Result<Expr, Error>

The symbol for key, created at width width on first use. A key has exactly one width per context.

pub fn fresh_symbol(&mut self, width: Width) -> Result<Expr, Error>

A new symbol with a key that is not yet used in this context.

pub fn find_symbol(&self, key: &SymbolKey) -> Option<Expr>

The symbol for key, if it exists. Never creates.

pub fn symbol_id(&self, e: Expr) -> Result<Option<SymbolId>, Error>

The symbol id, if the expression is a symbol node.

pub fn symbol_key(&self, id: SymbolId) -> Option<&SymbolKey>

A symbol’s key.

pub fn symbol_width(&self, id: SymbolId) -> Option<Width>

A symbol’s width.

pub fn symbol_count(&self) -> usize

The number of symbols.

pub fn post_order(&mut self, roots: &[Expr]) -> Result<Vec<Expr>, Error>

Every node reachable from roots, each once, children before parents. Iterative.

pub fn symbols_in(&mut self, roots: &[Expr]) -> Result<Vec<SymbolId>, Error>

The symbols reachable from roots, sorted by key.

pub fn dag_size(&mut self, roots: &[Expr], cap: u32) -> Result<Bounded, Error>

The number of distinct nodes reachable from roots, walking at most cap + 1 nodes. Exact single-root results are cached.

impl Context

pub fn facts(&mut self, e: Expr) -> Result<Facts, Error>

Facts about e. If the per-query work cap (ContextConfig::fact_work) is reached, the answer is Facts::top (sound, just imprecise); see Context::try_facts.

pub fn try_facts(&mut self, e: Expr) -> Result<Option<Facts>, Error>

Facts about e, or None if the per-query work cap was reached first. Progress is kept: repeating the call for the same expression continues where it stopped.

pub fn exact(&mut self, e: Expr) -> Result<Option<BitVec>, Error>

The value of e if its facts pin exactly one.

pub fn enumerate_values( &mut self, e: Expr, limit: u32, ) -> Result<Option<Vec<BitVec>>, Error>

The values e’s facts allow, if there are at most limit of them (and at most 2^20 candidates to examine). Every value e can take is included; some included values may be impossible, since facts over-approximate.

pub fn facts_with( &mut self, e: Expr, assumptions: &Assumptions, ) -> Result<Option<Facts>, Error>

Facts about e under assumptions, or None if the assumptions are infeasible for the part of the expression that e depends on. Never pollutes the base cache.

pub fn facts_under( &mut self, e: Expr, assumptions: &Assumptions, ) -> Result<Option<(Facts, Reliance)>, Error>

Facts about e under assumptions, with the constraints they rely on; None if the assumptions are infeasible. Never pollutes the base cache.

pub fn prove(&mut self, q: Query<'_>) -> Result<Truth, Error>

Answers a question from facts. Every True/False is proved; Unknown otherwise.

pub fn prove_with( &mut self, q: Query<'_>, assumptions: &Assumptions, ) -> Result<Truth, Error>

Answers a question from facts under assumptions. Infeasible assumptions prove anything: every well-formed question is answered True.

pub fn prove_under( &mut self, q: Query<'_>, assumptions: &Assumptions, ) -> Result<Proof, Error>

Context::prove_with, also reporting the constraints the answer relies on.

impl Context

pub fn parse(&mut self, src: &str, opts: &ParseOptions) -> Result<Expr, Error>

Parses an expression in the text syntax (see docs/design.md §7.1), creating symbols as needed, and builds it through the canonicalizing constructors.

use bitwright::{Context, ParseOptions, Width};
let mut cx = Context::new();
let e = cx.parse("(y | x) + (y & x)", &ParseOptions::width(Width::W64))?;
// Built canonically: operands of commutative operators in one order.
assert_eq!(cx.display(e).to_string(), "(x & y) + (x | y)");

impl Context

pub fn display(&self, e: Expr) -> Display<'_>

The expression in the text syntax, with the default PrintOptions.

pub fn display_with(&self, e: Expr, opts: PrintOptions) -> Display<'_>

The expression in the text syntax.

Trait Implementations

impl Debug for Context

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for Context

fn default() -> Self

Returns the “default value” for a type.