Struct Bindings 

pub struct Bindings { /* private fields */ }

Variable bindings during proof

This type manages variable-to-value mappings during backward chaining, with support for merging, conflict detection, and binding propagation.

Implementations

impl Bindings

pub fn new() -> Self

Create a new empty bindings set

pub fn bind(&mut self, var_name: String, value: Value) -> Result<()>

Bind a variable to a value

If the variable is already bound, this checks that the new value matches the existing binding. Returns an error if there’s a conflict.

Example

let mut bindings = Bindings::new();
bindings.bind("X".to_string(), Value::Number(42.0))?;

// This will succeed (same value)
bindings.bind("X".to_string(), Value::Number(42.0))?;

// This will fail (different value)
bindings.bind("X".to_string(), Value::Number(100.0))?; // Error!

pub fn get(&self, var_name: &str) -> Option<&Value>

Get binding for a variable

pub fn is_bound(&self, var_name: &str) -> bool

Check if variable is bound

pub fn merge(&mut self, other: &Bindings) -> Result<()>

Merge bindings from another set

This attempts to merge all bindings from other into this set. If any conflicts are detected, returns an error and leaves this set unchanged.

pub fn as_map(&self) -> &HashMap<String, Value>

Get all bindings as a map

pub fn len(&self) -> usize

Get number of bindings

pub fn is_empty(&self) -> bool

Check if bindings is empty

pub fn clear(&mut self)

Clear all bindings

pub fn from_map(map: HashMap<String, Value>) -> Self

Create bindings from a HashMap

pub fn into_map(self) -> HashMap<String, Value>

Convert bindings to HashMap (for backward compatibility)

pub fn to_map(&self) -> HashMap<String, Value>

Get bindings as HashMap clone

Trait Implementations

impl Clone for Bindings

fn clone(&self) -> Bindings

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Bindings

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

Formats the value using the given formatter.

impl Default for Bindings

fn default() -> Self

Returns the “default value” for a type.