Struct BoolExpr 

pub struct BoolExpr { /* private fields */ }

A boolean expression for logic minimisation

BoolExpr provides a high-level interface for building and minimising Boolean functions. Expressions can be constructed programmatically, parsed from strings, or composed from existing expressions, then minimised using the Espresso algorithm.

Construction Methods

Three ways to build expressions:

1. expr! macro (recommended) - Clean syntax without explicit references
2. Method API - Explicit .and(), .or(), .not() calls
3. Operator overloading - Requires & references

Minimisation

Expressions support direct minimisation via:

• .minimize() - Fast heuristic algorithm (~99% optimal)
• .minimize_exact() - Slower but guaranteed minimal result

Implementation Details

Internal representation: Uses Binary Decision Diagrams (BDDs) for efficient operations and canonical form. This is an implementation detail that makes the high-level API practical for complex expressions.

Each BoolExpr contains:

• Node ID - Reference to BDD structure in global manager
• Manager Reference - Shared access to global singleton BDD manager
• DNF Cache - Lazily cached cubes for Espresso minimisation
• AST Cache - Lazily cached syntax tree for display

The BDD manager is a global singleton (protected by RwLock) shared by all expressions, providing structural sharing and canonical representation.

Cloning

Cloning is very cheap - copies Arc references and node ID. OnceLock::clone() copies the cached content (Arc pointers), so clones share the actual cached data. The BDD structure itself is shared via the global manager.

Thread Safety

Thread-safe via global BDD manager with RwLock protection. Multiple threads can safely create and manipulate expressions concurrently.

Examples

Method-based API

use espresso_logic::BoolExpr;

let a = BoolExpr::variable("a");
let b = BoolExpr::variable("b");
let expr = a.and(&b).or(&a.not().and(&b.not()));
println!("{}", expr);  // Uses factored display

Using expr! macro (recommended)

use espresso_logic::{BoolExpr, expr};

let a = BoolExpr::variable("a");
let b = BoolExpr::variable("b");
// No & references needed!
let expr = expr!(a * b + !a * !b);
println!("{}", expr);

BDD Operations

use espresso_logic::BoolExpr;

let expr = BoolExpr::parse("a * b + b * c").unwrap();

// Query BDD properties
println!("BDD nodes: {}", expr.node_count());
println!("Variables: {}", expr.var_count());

// All operations are efficient BDD operations
let vars = expr.collect_variables();
println!("Variables: {:?}", vars);

Implementations

impl BoolExpr

pub fn fold<T, F>(&self, f: F) -> T

where F: Fn(ExprNode<'_, T>) -> T + Copy,

Fold the expression tree depth-first from leaves to root

This method traverses the expression tree recursively, calling the provided function f on each node. The function receives an ExprNode containing the node type and accumulated results from child nodes.

This is useful for implementing custom expression transformations and analyses without needing access to private expression internals.

Examples

Count the number of operations in an expression:

use espresso_logic::{BoolExpr, ExprNode};

let a = BoolExpr::variable("a");
let b = BoolExpr::variable("b");
let expr = a.and(&b);

let op_count = expr.fold(|node| match node {
    ExprNode::Variable(_) | ExprNode::Constant(_) => 0,
    ExprNode::And(l, r) | ExprNode::Or(l, r) => l + r + 1,
    ExprNode::Not(inner) => inner + 1,
});

assert_eq!(op_count, 1); // Just AND

pub fn fold_with_context<C, T, F>(&self, context: C, f: F) -> T

where C: Copy, F: Fn(ExprNode<'_, ()>, C, &dyn Fn(C) -> T, &dyn Fn(C) -> T) -> T + Copy,

Fold with context parameter passed top-down through the tree

Unlike fold, which passes results bottom-up from children to parents, this method passes a context parameter top-down from parents to children. The function f receives the current node type, context from parent, and closures to recursively process children with modified context.

This is useful for operations like applying De Morgan’s laws where negations need to be pushed down through the tree.

Examples

Count depth with context tracking current level:

use espresso_logic::{BoolExpr, ExprNode};

let a = BoolExpr::variable("a");
let b = BoolExpr::variable("b");
let expr = a.and(&b).not();

// Count depth with context tracking current level
let max_depth = expr.fold_with_context(0, |node, depth, recurse_left, recurse_right| {
    match node {
        ExprNode::Variable(_) | ExprNode::Constant(_) => depth,
        ExprNode::Not(_) => recurse_left(depth + 1),
        ExprNode::And(_, _) | ExprNode::Or(_, _) => {
            let left_depth = recurse_left(depth + 1);
            let right_depth = recurse_right(depth + 1);
            left_depth.max(right_depth)
        }
    }
});

Apply De Morgan’s laws to push negations down:

use espresso_logic::{BoolExpr, ExprNode};
use std::collections::BTreeMap;
use std::sync::Arc;

fn to_dnf_naive(expr: &BoolExpr) -> Vec<BTreeMap<Arc<str>, bool>> {
    expr.fold_with_context(false, |node, negate, recurse_left, recurse_right| {
        match node {
            ExprNode::Variable(name) => {
                let mut cube = BTreeMap::new();
                cube.insert(Arc::from(name), !negate);
                vec![cube]
            }
            ExprNode::Not(()) => recurse_left(!negate), // Flip negation
            ExprNode::And((), ()) if negate => {
                // De Morgan: ~(A * B) = ~A + ~B
                let mut result = recurse_left(true);
                result.extend(recurse_right(true));
                result
            }
            ExprNode::Or((), ()) if negate => {
                // De Morgan: ~(A + B) = ~A * ~B (cross product)
                vec![] // Simplified for example
            }
            _ => vec![] // Other cases omitted
        }
    })
}

impl BoolExpr

pub fn collect_variables(&self) -> BTreeSet<Arc<str>>

Collect all variables used in this expression in alphabetical order

Returns a BTreeSet which maintains variables in sorted order. This ordering is used when converting to covers for minimisation.

pub fn to_cubes(&self) -> Vec<BTreeMap<Arc<str>, bool>>

Extract cubes (product terms) from the BDD using cached DNF

Returns a vector of cubes, where each cube is a map from variable name to its literal value (true for positive literal, false for negative literal).

Each cube represents one path from the root to the TRUE terminal.

This method uses the DNF cache to avoid expensive BDD traversal.

pub fn is_terminal(&self) -> bool

Check if this expression is a terminal (constant)

pub fn is_true(&self) -> bool

Check if this expression represents TRUE

pub fn is_false(&self) -> bool

Check if this expression represents FALSE

pub fn node_count(&self) -> usize

Get the number of nodes in this BDD representation

pub fn var_count(&self) -> usize

Get the variable count (number of distinct variables)

impl BoolExpr

pub fn equivalent_to(&self, other: &BoolExpr) -> bool

Check if two boolean expressions are logically equivalent

Note (v3.1.1+): All BoolExpr instances are BDDs internally (unified architecture).

Uses a two-phase BDD-based approach:

1. Fast BDD equality check - Compare the internal BDD representations directly. BDDs use canonical representation, so equal BDDs guarantee equivalence. Very fast (O(e) where e is expression size).
2. Exact minimisation fallback - If BDD representations differ, uses exact Espresso minimisation to guarantee equality. This handles cases where equivalent functions present different BDDs (not supposed to happen, but better safe than sorry). Even exact minimisation is typically much faster than exhaustive O(2^n) evaluation.

Performance

• BDD match: O(1) constant-time check when BDD representations are identical
• BDD mismatch: Espresso exact minimisation (typically still faster than O(2^n))

The BDD check is attempted first. If BDDs differ, Espresso exact minimisation is used to guarantee equality in cases where equivalent functions present different BDDs.

BDD-Only Checking

If you’re content with BDD-only equality checking (without the Espresso fallback), you can use the == operator instead, which performs a constant-time O(1) comparison of BDD representations:

use espresso_logic::BoolExpr;

let a = BoolExpr::variable("a");
let b = BoolExpr::variable("b");
let expr1 = a.and(&b);
let expr2 = a.and(&b);

// Constant-time BDD comparison (O(1))
assert!(expr1 == expr2);

Performance Comparison to v3.0

Version 3.1.1+ uses unified BDD architecture (all expressions are BDDs from construction):

• BDD comparison: O(1) constant-time check (BoolExpr is already a BDD)
• Minimisation fallback: Espresso heuristic (exact mode, typically efficient)
• Old approach (v3.0): O(2^n) exhaustive truth table evaluation (exponential)

This makes equivalency checking dramatically faster for expressions with many variables:

• 10 variables: 1,024× faster
• 20 variables: 1,048,576× faster
• 30 variables: Previously impossible, now feasible

Examples

use espresso_logic::BoolExpr;

let a = BoolExpr::variable("a");
let b = BoolExpr::variable("b");

// Different structures, same logic
let expr1 = a.and(&b);
let expr2 = b.and(&a); // Commutative

assert!(expr1.equivalent_to(&expr2));

pub fn evaluate(&self, assignment: &HashMap<Arc<str>, bool>) -> bool

Evaluate the expression with a given variable assignment

Traverses the BDD following the variable assignments until reaching a terminal node. Returns the boolean value of the terminal node.

Examples

use espresso_logic::BoolExpr;
use std::collections::HashMap;
use std::sync::Arc;

let a = BoolExpr::variable("a");
let b = BoolExpr::variable("b");
let expr = a.and(&b);

let mut assignment = HashMap::new();
assignment.insert(Arc::from("a"), true);
assignment.insert(Arc::from("b"), true);

assert_eq!(expr.evaluate(&assignment), true);

assignment.insert(Arc::from("b"), false);
assert_eq!(expr.evaluate(&assignment), false);

impl BoolExpr

pub fn and(&self, other: &BoolExpr) -> BoolExpr

Logical AND: create a new expression that is the conjunction of this and another

Computes the conjunction using the BDD ITE operation: and(f, g) = ite(f, g, false)

pub fn or(&self, other: &BoolExpr) -> BoolExpr

Logical OR: create a new expression that is the disjunction of this and another

Computes the disjunction using the BDD ITE operation: or(f, g) = ite(f, true, g)

pub fn not(&self) -> BoolExpr

Logical NOT: create a new expression that is the negation of this one

Computes the negation using the BDD ITE operation: not(f) = ite(f, false, true)

impl BoolExpr

pub fn parse(input: &str) -> Result<Self, ParseBoolExprError>

Parse a boolean expression from a string

Supports standard boolean operators:

• + or | for OR
• * or & for AND
• ~ or ! for NOT
• Parentheses for grouping
• Constants: 0, 1, true, false

impl BoolExpr

pub fn variable(name: &str) -> Self

Create a variable expression with the given name

pub fn constant(value: bool) -> Self

Create a constant expression (true or false)

pub fn to_bdd(&self) -> Self

👎Deprecated since 3.1.1: BoolExpr is now a BDD internally. Use clone() instead.

Convert this boolean expression to a Binary Decision Diagram

Deprecated: BoolExpr is now implemented as a BDD internally. This method simply clones the expression and exists for backwards compatibility.

Examples

use espresso_logic::BoolExpr;

let a = BoolExpr::variable("a");
let b = BoolExpr::variable("b");
let expr = a.and(&b);

let bdd = expr.to_bdd();  // Just returns a clone

pub fn from_expr(expr: &BoolExpr) -> Self

👎Deprecated since 3.1.1: BoolExpr and Bdd are now the same type. Use clone() instead.

Create a BoolExpr from a BDD (actually the same type)

Deprecated: BoolExpr and Bdd are now the same type. This method simply clones the expression and exists for backwards compatibility.

pub fn to_expr(&self) -> Self

👎Deprecated since 3.1.1: BoolExpr and Bdd are now the same type. Use clone() instead.

Convert this BDD to a BoolExpr (actually the same type)

Deprecated: BoolExpr and Bdd are now the same type. This method simply clones the expression and exists for backwards compatibility.

Trait Implementations

impl Add for &BoolExpr

Logical OR operator for references: &a + &b

Implements the + operator for boolean expressions using references. This is the most efficient form as it avoids unnecessary cloning.

Examples

use espresso_logic::BoolExpr;

let a = BoolExpr::variable("a");
let b = BoolExpr::variable("b");
let result = &a + &b;  // Equivalent to a.or(&b)

type Output = BoolExpr

The resulting type after applying the + operator.

fn add(self, rhs: &BoolExpr) -> BoolExpr

Performs the + operation.

impl Add for BoolExpr

Logical OR operator: a + b (delegates to reference version)

Implements the + operator for owned boolean expressions. Note: Using references (&a + &b) is preferred for efficiency.

Examples

use espresso_logic::BoolExpr;

let a = BoolExpr::variable("a");
let b = BoolExpr::variable("b");
// Both work, but references are preferred
let result1 = a.clone() + b.clone();
let result2 = &a + &b;

type Output = BoolExpr

The resulting type after applying the + operator.

fn add(self, rhs: BoolExpr) -> BoolExpr

Performs the + operation.

impl Clone for BoolExpr

fn clone(&self) -> BoolExpr

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for BoolExpr

Debug formatting for boolean expressions

Formats expressions with minimal parentheses based on operator precedence. Uses standard boolean algebra notation: * for AND, + for OR, ~ for NOT.

Examples

use espresso_logic::BoolExpr;

let a = BoolExpr::variable("a");
let b = BoolExpr::variable("b");
let c = BoolExpr::variable("c");
let expr = a.and(&b).or(&c);

println!("{:?}", expr);  // Outputs: a * b + c (no unnecessary parentheses)

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

Formats the value using the given formatter.

impl Display for BoolExpr

Display formatting for boolean expressions

Delegates to the Debug implementation. Use {} or {:?} interchangeably.

Examples

use espresso_logic::BoolExpr;

let a = BoolExpr::variable("a");
let b = BoolExpr::variable("b");
let expr = a.and(&b);

println!("{}", expr);  // Same as println!("{:?}", expr)

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

Formats the value using the given formatter.

impl From<&BoolExpr> for Cover

Convert a &BoolExpr into a Cover with a single output named “out”

This conversion extracts the cubes from the internal BDD representation without requiring ownership of the expression.

Examples

use espresso_logic::{BoolExpr, Cover};

let a = BoolExpr::variable("a");
// Note: BoolExpr uses BDD internally (v3.1.1+)

let cover = Cover::from(&a);
assert_eq!(cover.num_outputs(), 1);

fn from(expr: &BoolExpr) -> Self

Converts to this type from the input type.

impl From<&BoolExpr> for Dnf

Convert &BoolExpr to DNF

Note (v3.1.1+): BoolExpr IS a BDD internally. This extracts DNF from the internal BDD representation. Uses caching to avoid expensive BDD traversal.

fn from(expr: &BoolExpr) -> Self

Converts to this type from the input type.

impl From<BoolExpr> for Cover

Convert a BoolExpr into a Cover with a single output named “out”

This conversion uses the BDD representation for efficient DNF extraction.

Examples

use espresso_logic::{BoolExpr, Cover};

let a = BoolExpr::variable("a");
let b = BoolExpr::variable("b");
let expr = a.and(&b);

let cover: Cover = expr.into();
assert_eq!(cover.num_outputs(), 1);

fn from(expr: BoolExpr) -> Self

Converts to this type from the input type.

impl From<BoolExpr> for Dnf

Convert BoolExpr to DNF

Note (v3.1.1+): BoolExpr IS a BDD internally. This extracts DNF from the internal BDD representation, ensuring canonical form and automatic optimisations. Uses caching to avoid expensive BDD traversal.

fn from(expr: BoolExpr) -> Self

Converts to this type from the input type.

impl From<Dnf> for BoolExpr

Convert DNF to BoolExpr

Note (v3.1.1+): Creates a new BoolExpr with BDD as internal representation. Reconstructs a boolean expression in DNF form (OR of AND terms), which is then converted to BDD representation internally.

Examples

use espresso_logic::{BoolExpr, Dnf};

let a = BoolExpr::variable("a");
let b = BoolExpr::variable("b");
let expr = a.and(&b);

let dnf = Dnf::from(&expr);
let expr2 = BoolExpr::from(dnf);

assert!(expr.equivalent_to(&expr2));

fn from(dnf: Dnf) -> Self

Converts to this type from the input type.

impl Mul for &BoolExpr

Logical AND operator for references: &a * &b

Implements the * operator for boolean expressions using references. This is the most efficient form as it avoids unnecessary cloning.

Examples

use espresso_logic::BoolExpr;

let a = BoolExpr::variable("a");
let b = BoolExpr::variable("b");
let result = &a * &b;  // Equivalent to a.and(&b)

type Output = BoolExpr

The resulting type after applying the * operator.

fn mul(self, rhs: &BoolExpr) -> BoolExpr

Performs the * operation.

impl Mul for BoolExpr

Logical AND operator: a * b (delegates to reference version)

Implements the * operator for owned boolean expressions. Note: Using references (&a * &b) is preferred for efficiency.

Examples

use espresso_logic::BoolExpr;

let a = BoolExpr::variable("a");
let b = BoolExpr::variable("b");
// Both work, but references are preferred
let result1 = a.clone() * b.clone();
let result2 = &a * &b;

type Output = BoolExpr

The resulting type after applying the * operator.

fn mul(self, rhs: BoolExpr) -> BoolExpr

Performs the * operation.

impl Not for &BoolExpr

Logical NOT operator for references: !&a

Implements the ! operator for boolean expressions using references. This is the most efficient form as it avoids unnecessary cloning.

Examples

use espresso_logic::BoolExpr;

let a = BoolExpr::variable("a");
let result = !&a;  // Equivalent to a.not()

type Output = BoolExpr

The resulting type after applying the ! operator.

fn not(self) -> BoolExpr

Performs the unary ! operation.

impl Not for BoolExpr

Logical NOT operator: !a (delegates to reference version)

Implements the ! operator for owned boolean expressions. Note: Using references (!&a) is preferred for efficiency when the original expression is still needed.

Examples

use espresso_logic::BoolExpr;

let a = BoolExpr::variable("a");
// Both work, but references are preferred if you need 'a' later
let result1 = !a.clone();
let result2 = !&a;

type Output = BoolExpr

The resulting type after applying the ! operator.

fn not(self) -> BoolExpr

Performs the unary ! operation.

impl PartialEq for BoolExpr

PartialEq implementation that compares BDDs for canonical equality

Since BDDs are canonical, two BoolExprs are equal if and only if they represent the same logical function.

fn eq(&self, other: &Self) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for BoolExpr