Struct Subst

pub struct Subst(/* private fields */);

A substitution.

Implementations

impl Subst

pub fn new() -> Subst

Creates a new, empty substitution.

pub fn apply_to_term<'a>(&'a self, term: &'a Term) -> Arc<Term>

Applies a substitution to a term.

pub fn apply_to_lit(&self, lit: &Lit) -> Lit

Applies a substitution to a lit.

pub fn get(&self, k: usize) -> Option<&Arc<Term>>

Gets the replacement for the given variable index, if any.

pub fn merge(&self, other: Subst) -> Subst

Merges with another substitution. The substitution on the left should be the “older” one.

pub fn push(&mut self, k: usize, v: Arc<Term>)

Adds a binding to the substitution.

Trait Implementations

impl Clone for Subst

fn clone(&self) -> Subst

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Subst

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

Formats the value using the given formatter.

impl Default for Subst

fn default() -> Subst

Returns the “default value” for a type.