Struct term_rewriting::TRS

pub struct TRS {
    pub rules: Vec<Rule>,
    // some fields omitted
}

A first-order term rewriting system.

Fields

rules: Vec<Rule>

Methods

impl TRS

pub fn new(rules: Vec<Rule>) -> TRS

Constructs a term rewriting system from a list of rules.

pub fn make_deterministic<R: Rng>(&mut self, rng: &mut R) -> bool

Make self deterministic and restrict it to be so until further notice.

Return true if self was changed, otherwise false.

pub fn make_nondeterministic(&mut self) -> bool

Remove any determinism restriction self might be under.

Return true if self was changed, otherwise false.

pub fn is_deterministic(&self) -> bool

Report whether self is currently deterministic.

pub fn len(&self) -> usize

The number of rules in the TRS.

pub fn is_empty(&self) -> bool

Are there any rules in the TRS?

pub fn size(&self) -> usize

Return the number of total number of subterms across all rules.

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

A serialized representation of the TRS.

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

A human-readable serialization of the TRS.

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

All the clauses in the TRS.

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

All the operators in the TRS

pub fn unifies(trs1: TRS, trs2: TRS) -> bool

Do two TRSs unify?

pub fn pmatches(trs1: TRS, trs2: TRS) -> bool

Does one TRS match another?

pub fn alphas(trs1: &TRS, trs2: &TRS) -> bool

Are two TRSs alpha equivalent?

pub fn rewrite(&self, term: &Term) -> Option<Vec<Term>>

Perform a single rewrite step using a normal-order (leftmost-outermost) rewrite strategy.

pub fn get(&self, lhs: &Term) -> Option<(usize, Rule)>

Query a TRS for a Rule based on its left-hand-side; return both the Rule and its index if possible

pub fn get_idx(&self, idx: usize) -> Option<Rule>

Query a TRS for a Rule based on its index; return the Rule if possible.

pub fn get_clause(&self, rule: &Rule) -> Option<(usize, Rule)>

Query a TRS for specific Rule clauses; return them if possible.

pub fn remove(&mut self, lhs: &Term) -> Result<Rule, TRSError>

Query a TRS for a Rule based on its left-hand-side; delete and return the Rule if it exists.

pub fn remove_idx(&mut self, idx: usize) -> Result<Rule, TRSError>

Query a TRS for a Rule based on its index; delete and return the Rule if it exists.

pub fn remove_clauses(&mut self, rule: &Rule) -> Result<Rule, TRSError>

Query a TRS for a Rule based on its left-hand-side; delete and return the Rule if it exists.

pub fn insert(&mut self, idx: usize, rule: Rule) -> Result<&mut TRS, TRSError>

Try to merge a Rule with an existing Rule or else insert it at index i in the TRS if possible.

pub fn insert_idx(     &mut self,     idx: usize,     rule: Rule ) -> Result<&mut TRS, TRSError>

Insert a Rule at index i in the TRS if possible.

pub fn insert_clauses(&mut self, rule: &Rule) -> Result<&mut TRS, TRSError>

Merge a Rule with an existing Rule in the TRS if possible.

pub fn push(&mut self, rule: Rule) -> Result<&mut TRS, TRSError>

Insert new Rule clauses if possible and move the entire Rule if necessary to be the first in the TRS.

pub fn pushes(&mut self, rules: Vec<Rule>) -> Result<&mut TRS, TRSError>

a series of Rules at the beginning of the TRS if possible.

pub fn move_rule(&mut self, i: usize, j: usize) -> Result<&mut TRS, TRSError>

Move a Rule from index i to j if possible.

pub fn replace(     &mut self,     idx: usize,     rule1: &Rule,     rule2: Rule ) -> Result<&mut TRS, TRSError>

Remove some Rule clauses while also inserting others if possible.

The index i is used only in the case that the new clauses cannot be added to an existing Rule.

Trait Implementations

impl Debug for TRS

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

Formats the value using the given formatter.

impl Hash for TRS

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].

impl Clone for TRS

fn clone(&self) -> TRS

Returns a copy of the value.

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

Performs copy-assignment from source.

impl PartialEq for TRS

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

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

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

This method tests for !=.

impl Eq for TRS