Struct Substitution 

pub struct Substitution { /* private fields */ }

A substitution maps variables to terms.

A substitution θ = {x₁/t₁, x₂/t₂, …} represents the simultaneous replacement of each variable xᵢ with term tᵢ.

Implementations

impl Substitution

pub fn empty() -> Self

Create an empty substitution (identity).

pub fn singleton(var: String, term: Term) -> Self

Create a substitution with a single binding.

pub fn from_map(bindings: HashMap<String, Term>) -> Self

Create a substitution from a map of bindings.

pub fn is_empty(&self) -> bool

Check if this is the empty substitution.

pub fn len(&self) -> usize

Get the number of bindings.

pub fn get(&self, var: &str) -> Option<&Term>

Get the binding for a variable, if it exists.

pub fn bind(&mut self, var: String, term: Term)

Add a binding to the substitution.

pub fn apply(&self, term: &Term) -> Term

Apply this substitution to a term.

This recursively replaces all occurrences of bound variables with their substituted values.

pub fn compose(&self, other: &Substitution) -> Substitution

Compose two substitutions: (σ ∘ θ)(x) = σ(θ(x))

The composition applies θ first, then σ.

pub fn domain(&self) -> Vec<String>

Get all bound variables.

pub fn range(&self) -> Vec<Term>

Get all terms that variables are bound to.

pub fn extend(&mut self, var: String, term: Term) -> Result<(), IrError>

Extend this substitution with a new binding.

Returns an error if the binding conflicts with existing bindings.

pub fn try_extend(&mut self, other: &Substitution) -> Result<(), IrError>

Try to extend this substitution with all bindings from another substitution.

This is used for subsumption checking where we need to merge substitutions. Returns an error if any binding conflicts with existing bindings.

Trait Implementations

impl Clone for Substitution

fn clone(&self) -> Substitution

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Substitution

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

Formats the value using the given formatter.

impl Default for Substitution

fn default() -> Substitution

Returns the “default value” for a type.

impl<'de> Deserialize<'de> for Substitution

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for Substitution

fn eq(&self, other: &Substitution) -> 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 Serialize for Substitution

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for Substitution