Struct term_rewriting::Rule

pub struct Rule {
    pub lhs: Term,
    pub rhs: Vec<Term>,
}

A rewrite rule equating a left-hand-side Term with one or more right-hand-side Terms.

Fields

lhs: Term

rhs: Vec<Term>

Methods

impl Rule

pub fn display(&self, sig: &Signature) -> String

A serialized representation of the Rule.

pub fn pretty(&self, sig: &Signature) -> String

A human-readable serialization of the Rule.

pub fn size(&self) -> usize

Return the total number of subterms across all terms in the rule.

pub fn len(&self) -> usize

Return the number of RHSs in the rule

pub fn is_empty(&self) -> bool

Is the rule empty?

pub fn rhs(&self) -> Option<Term>

Give the lone RHS, if it exists

pub fn clauses(&self) -> Vec<Rule>

Return a list of the clauses in the Rule.

pub fn new(lhs: Term, rhs: Vec<Term>) -> Option<Rule>

Construct a rewrite rule from a left-hand-side (LHS) Term with one or more right-hand-side (RHS) Terms. Returns None if the rule is not valid.

Valid rules meet two conditions:

1. lhs is an Application. This prevents a single rule from matching all possible terms
2. A Term in rhs can only use a Variable if it appears in lhs. This prevents rewrites from inventing arbitrary terms.

pub fn add(&mut self, t: Term)

Add a clause to the rule from a term.

pub fn merge(&mut self, r: &Rule)

Add clauses to the rule from another rule.

pub fn discard(&mut self, r: &Rule) -> Option<Rule>

Discard clauses from the rule.

pub fn contains(&self, r: &Rule) -> Option<HashMap<Variable, Term>>

Check whether the rule contains certain clauses.

pub fn variables(&self) -> Vec<Variable>

Get all the Variables in the Rule.

pub fn operators(&self) -> Vec<Operator>

Get all the Operators in the Rule.

pub fn subterms(&self) -> Vec<(usize, &Term, Place)>

Get all the subterms and places in a Rule.

pub fn at(&self, p: &[usize]) -> Option<&Term>

Get a specific subterm in a Rule

pub fn replace(&self, place: &[usize], subterm: Term) -> Option<Rule>

Replace one subterm with another in a Rule

pub fn pmatch(r1: Rule, r2: Rule) -> Option<HashMap<Variable, Term>>

Match one rule against another.

pub fn unify(r1: Rule, r2: Rule) -> Option<HashMap<Variable, Term>>

Unify two rules.

pub fn alpha(r1: &Rule, r2: &Rule) -> Option<HashMap<Variable, Term>>

Compute the alpha equivalence between two rules.

pub fn substitute(&self, sub: &HashMap<Variable, Term>) -> Rule

Substitute through a rule

Trait Implementations

impl Debug for Rule

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

Formats the value using the given formatter.

impl Clone for Rule

fn clone(&self) -> Rule

Returns a copy of the value.

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

Performs copy-assignment from source.

impl PartialEq for Rule

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

This method tests for self and other values to be equal, and is used by ==.

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

This method tests for !=.

impl Eq for Rule

impl Hash for Rule

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given [Hasher].

fn hash_slice<H>(data: &[Self], state: &mut H) where     H: Hasher,

Feeds a slice of this type into the given [Hasher].