Struct term_rewriting::TRS

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

A first-order term rewriting system.

Examples

let mut sig = Signature::default();

// Constructing a TRS manually
let r0 = parse_rule(&mut sig, "A(x_) = A(B)").expect("parse of A(x_) = A(B)");
let r1 = parse_rule(&mut sig, "B = C | D").expect("parse of B = C | D");
let r2 = parse_rule(&mut sig, "E(F) = G").expect("parse of E(F) = G");

let t = TRS::new(vec![r0, r1, r2]);

// Constructing a TRS using the parser
let t = parse_trs(&mut sig, "A(x_) = A(B);\nB = C | D;\nE(F) = G;")
    .expect("parse of A(x_) = A(B); B = C | D; E(F) = G;");

// For better readability of the TRS
let t = parse_trs(&mut sig,
"A(x_) = A(B);
B = C | D;
E(F) = G;").expect("parse of A(x_) = A(B); B = C | D; E(F) = G;");

Fields

rules: Vec<Rule>

Methods

impl TRS

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

Constructs a Term Rewriting System from a list of Rules.

Examples

let mut sig = Signature::default();

let r0 = parse_rule(&mut sig, "A = B").expect("parse of A = B");
let r1 = parse_rule(&mut sig, "C(x_) = x_").expect("parse of C(x_) = x_");
let r2 = parse_rule(&mut sig, "D(y_) = D(E)").expect("parse of D(y_) = D(E)");
let new_trs = TRS::new(vec![r0, r1, r2]);

assert_eq!(new_trs.display(),
"A = B;
C(x_) = x_;
D(y_) = D(E);"
);

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

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

Return true if the TRS was changed, otherwise false.

Examples

let mut sig = Signature::default();

let mut t = parse_trs(&mut sig,
"A = B | C;
D = E;").expect("parse of A = B | C; D = E");
let mut r = rand::thread_rng();

let str_before = t.display();

assert!(t.make_deterministic(& mut r));

assert_ne!(t.display(), str_before);

let str_before = t.display();
let r = parse_rule(&mut sig, "C = B | D").expect("parse of C = B | D");

if t.insert_idx(1, r.clone()).is_err() {
    assert!(true);
}

assert_eq!(str_before, t.display());

assert!((t.display() ==
"A = B;
D = E;") ||
    (t.display() ==
"A = C;
D = E;"));

pub fn make_nondeterministic(&mut self) -> bool

Remove any [determinism] restriction the TRS might be under.

Return true if the TRS was changed, otherwise false.

See [determinism] for more information.

Examples

let mut sig = Signature::default();

let mut t = parse_trs(&mut sig,
"A = B | C;
D = E;").expect("parse of A = B | C; D = E");
let mut r = rand::thread_rng();

t.make_deterministic(& mut r);

let str_before = t.display();
let r = parse_rule(&mut sig, "C = B | D").expect("parse of C = B | D");
assert!(t.insert_idx(1, r.clone()).is_err());
assert_eq!(str_before, t.display());

assert!(t.make_nondeterministic());

t.insert_idx(1, r).expect("inserting C = B | D");

assert!((t.display() ==
"A = B;
C = B | D;
D = E;") ||
    (t.display() ==
"A = C;
C = B | D;
D = E;"));

pub fn is_deterministic(&self) -> bool

Report whether the TRS is currently deterministic.

See Deterministic System for more information.

Examples

let mut sig = Signature::default();

let mut t = parse_trs(&mut sig,
"A = B | C;
D = E;").expect("parse of A = B | C; D = E");
let mut r = rand::thread_rng();

assert!(!t.is_deterministic());

t.make_deterministic(& mut r);

assert!(t.is_deterministic());

pub fn len(&self) -> usize

The number of Rules in the TRS.

Examples

let mut sig = Signature::default();

let t = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;").expect("parse of A = B; C = D | E; F(x_) = G;");

assert_eq!(t.len(), 3);

pub fn is_empty(&self) -> bool

Are there any Rules in the TRS?

Examples

let mut sig = Signature::default();

let t = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;").expect("parse of A = B; C = D | E; F(x_) = G;");

assert!(!t.is_empty());

let t = parse_trs(&mut sig, "").expect("parse of blank string");

assert!(t.is_empty());

pub fn size(&self) -> usize

Return the number of total number of subterms across all Rules in the TRS.

See Term for more information.

Examples

let mut sig = Signature::default();

let t = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;").expect("parse of A = B; C = D | E; F(x_) = G;");

assert_eq!(t.size(), 8);

pub fn display(&self) -> String

Serialize a TRS.

Examples

let mut sig = Signature::default();

let t = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;").expect("parse of A = B; C = D | E; F(x_) = G;");

assert_eq!(t.display(),
"A = B;
C = D | E;
F(x_) = G;");

let trs = parse_trs(&mut sig,
"A(x_ y_ z_) = A(x_ DECC(DECC(DIGIT(1) 0) 5) SUCC(SUCC(ZERO)));
CONS(B CONS(C CONS(D NIL))) = CONS(C CONS(D NIL));
B C D E = B C | D E;")
    .expect("parse of A(x_ y_ z_) = A(x_ DECC(DECC(DIGIT(1) 0) 5) SUCC(SUCC(ZERO)));
    CONS(B CONS(C CONS(D NIL))) = CONS(C CONS(D NIL));
    B C D E = B C | D E;");

assert_eq!(trs.display(),
"A(x_ y_ z_) = A(x_ DECC(DECC(DIGIT(1) 0) 5) SUCC(SUCC(ZERO)));
CONS(B CONS(C CONS(D NIL))) = CONS(C CONS(D NIL));
.(.(.(B C) D) E) = .(B C) | .(D E);");

pub fn pretty(&self) -> String

A human-readable serialization of the TRS.

Examples

let mut sig = Signature::default();

let trs = parse_trs(&mut sig,
"A(x_ y_ z_) = A(x_ DECC(DECC(DIGIT(1) 0) 5) SUCC(SUCC(ZERO)));
CONS(B CONS(C CONS(D NIL))) = CONS(C CONS(D NIL));
B C D E = B C | D E;")
    .expect("parse of A(x_ y_ z_) = A(x_ DECC(DECC(DIGIT(1) 0) 5) SUCC(SUCC(ZERO)));
    CONS(B CONS(C CONS(D NIL))) = CONS(C CONS(D NIL));
    B C D E = B C | D E;");

assert_eq!(trs.pretty(),
"A(x_, y_, z_) = A(x_, 105, 2);
[B, C, D] = [C, D];
B C D E = B C | D E;");

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

All the clauses in the TRS.

Examples

let mut sig = Signature::default();

let t = parse_trs(&mut sig,
"A = B;
C = D | E;
F = G;").expect("parse of A = B; C = D | E; F = G;");

let r0 = parse_rule(&mut sig, "A = B").expect("parse of A = B");
let r1 = parse_rule(&mut sig, "C = D").expect("parse of C = D");
let r2 = parse_rule(&mut sig, "C = E").expect("parse of C = E");
let r3 = parse_rule(&mut sig, "F = G").expect("parse of F = G");

assert_eq!(t.clauses(), vec![r0, r1, r2, r3]);

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

All the Operators in the TRS.

Examples

let mut sig = Signature::default();

let t = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;").expect("parse of A = B; C = D | E; F(x_) = G;");

let ops: Vec<String> = t.operators().iter().map(|o| o.display()).collect();

assert_eq!(ops, vec!["A", "B", "C", "D", "E", "F", "G"]);

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

Do two TRSs unify?

Examples

let mut sig = Signature::default();

let t0 = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;").expect("parse of A = B; C = D | E; F(x_) = G;");

let t1 = parse_trs(&mut sig,
"A = B;
C = D | E;
F(H) = G;").expect("parse of A = B; C = D | E; F(H) = G;");

assert!(TRS::unifies(t0.clone(), t1));

let t2 = parse_trs(&mut sig,
"B = A;
C = D | E;
F(y_) = G;").expect("parse of A = B; C = D | E; F(y_) = G;");

assert!(!TRS::unifies(t0, t2));

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

Does one TRS [match] another?

See [match] for more information.

Examples

let mut sig = Signature::default();

let t0 = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;").expect("parse of A = B; C = D | E; F(x_) = G;");

let t1 = parse_trs(&mut sig,
"A = B;
C = D | E;
F(H) = G;").expect("parse of A = B; C = D | E; F(H) = G;");

assert!(TRS::pmatches(t0.clone(), t1));

let t2 = parse_trs(&mut sig,
"B = A;
C = D | E;
F(y_) = G;").expect("parse of A = B; C = D | E; F(y_) = G;");

assert!(!TRS::pmatches(t0.clone(), t2));

let t3 = parse_trs(&mut sig,
"A = B | C;
C = D | E;
F(x_) = G;").expect("parse of A = B | C; C = D | E; F(x_) = G");

assert!(TRS::pmatches(t0.clone(), t3));

let t4 = parse_trs(&mut sig,
"A = B;
C = D;
D = E;").expect("parse of A = B; C = D; D = E;");

assert!(!TRS::pmatches(t0, t4));

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

Are two TRSs Alpha Equivalent?

Examples

let mut sig = Signature::default();

let t0 = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;").expect("parse of A = B; C = D | E; F(x_) = G;");

let t1 = parse_trs(&mut sig,
"A = B;
C = D | E;
F(H) = G;").expect("parse of A = B; C = D | E; F(H) = G;");

assert!(!TRS::alphas(&t0, &t1));

let t2 = parse_trs(&mut sig,
"A = B;
C = D | E;
F(y_) = G;").expect("parse of A = B; C = D | E; F(y_) = G;");

assert!(TRS::alphas(&t0, &t2));

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

Perform a single rewrite step.

Examples

let mut sig = Signature::default();

let t = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;").expect("parse of A = B; C = D | E; F(x_) = G;");

let term = parse_term(&mut sig, "J(F(C) K(C A))").expect("parse of J(F(C) K(C A))");

let rewritten_terms = &t.rewrite(&term, Strategy::Normal).unwrap();
assert_eq!(rewritten_terms.len(), 1);
assert_eq!(rewritten_terms[0].display(), "J(G K(C A))");

let rewritten_terms = &t.rewrite(&term, Strategy::Eager).unwrap();
assert_eq!(rewritten_terms.len(), 2);
assert_eq!(rewritten_terms[0].display(), "J(F(D) K(C A))");
assert_eq!(rewritten_terms[1].display(), "J(F(E) K(C A))");

let rewritten_terms = &t.rewrite(&term, Strategy::All).unwrap();
assert_eq!(rewritten_terms.len(), 6);
assert_eq!(rewritten_terms[0].display(), "J(G K(C A))");
assert_eq!(rewritten_terms[1].display(), "J(F(D) K(C A))");
assert_eq!(rewritten_terms[2].display(), "J(F(E) K(C A))");
assert_eq!(rewritten_terms[3].display(), "J(F(C) K(D A))");
assert_eq!(rewritten_terms[4].display(), "J(F(C) K(E A))");
assert_eq!(rewritten_terms[5].display(), "J(F(C) K(C B))");

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

Examples

let mut sig = Signature::default();

let t = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;").expect("parse of A = B; C = D | E; F(x_) = G;");

let a = parse_term(&mut sig, "A").expect("parse of A");

assert_eq!(t.get(&a).unwrap().1.display(), "A = B");

let c = parse_term(&mut sig, "C").expect("parse of C");

assert_eq!(t.get(&c).unwrap().1.display(), "C = D | E");

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

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

Examples

let mut sig = Signature::default();

let t = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;").expect("parse of A = B; C = D | E; F(x_) = G;");

assert_eq!(t.get_idx(0).unwrap().display(), "A = B");

assert_eq!(t.get_idx(1).unwrap().display(), "C = D | E");

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

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

Examples

let mut sig = Signature::default();

let t = parse_trs(&mut sig,
"A(a_ b_) = B(b_ b_);
D(c_ e_) = D(E F);").expect("parse of A(a_ b_) = B(b_ b_); D(c_ e_) = D(E F);");

let r = parse_rule(&mut sig, "A(x_ y_) = B(y_ y_)").expect("parse of A(x_ y_) = B(y_ y_)");

assert_eq!(t.get_clause(&r).unwrap().1.display(), "A(a_ b_) = B(b_ b_)");

let r = parse_rule(&mut sig, "D(w_ q_) = D(E F)").expect("parse of D(w_ q_) = D(E F)");

assert_eq!(t.get_clause(&r).unwrap().1.display(), "D(c_ e_) = D(E F)");

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.

Examples

let mut sig = Signature::default();

let mut t = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;").expect("parse of A = B; C = D | E; F(x_) = G;");

let a = parse_term(&mut sig, "A").expect("parse of A");
let c = parse_term(&mut sig, "C").expect("parse of C");

assert_eq!(t.remove(&a).expect("removing A = B").display(), "A = B");

assert_eq!(t.remove(&c).expect("removing C = D").display(), "C = D | E");

assert_eq!(t.display(), "F(x_) = G;");

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.

Examples

let mut sig = Signature::default();

let mut t = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;").expect("parse of A = B; C = D | E; F(x_) = G;");

assert_eq!(t.remove_idx(0).expect("removing A = B").display(), "A = B");

assert_eq!(t.remove_idx(0).expect("removing C = D").display(), "C = D | E");

assert_eq!(t.display(), "F(x_) = G;");

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.

Examples

let mut sig = Signature::default();

let mut t = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;").expect("parse of A = B; C = D | E; F(x_) = G;");

let r = parse_rule(&mut sig, "C = D").expect("parse of C = D");

assert_eq!(t.remove_clauses(&r).expect("removing C = D").display(), "C = D");

assert_eq!(t.display(),
"A = B;
C = E;
F(x_) = G;");

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.

Examples

let mut sig = Signature::default();

let mut t = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;").expect("parse of A = B; C = D | E; F(x_) = G;");

let r = parse_rule(&mut sig, "D = G").expect("parse of D = G");

t.insert(1, r).expect("inserting D = G at index 1");

assert_eq!(t.display(),
"A = B;
D = G;
C = D | E;
F(x_) = G;");

let r = parse_rule(&mut sig, "D = A").expect("parse of D = A");

t.insert(0, r).expect("inserting D = A with D = G");

assert_eq!(t.display(),
"A = B;
D = G | A;
C = D | E;
F(x_) = G;");

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.

Examples

let mut sig = Signature::default();

let mut t = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;").expect("parse of A = B; C = D | E; F(x_) = G;");

let r = parse_rule(&mut sig, "D = G").expect("parse of D = G");

t.insert_idx(1, r).expect("inserting D = G at index 1");

assert_eq!(t.display(),
"A = B;
D = G;
C = D | E;
F(x_) = G;");

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

Inserts a series of Rules into the TRS at the index provided if possible.

Examples

let mut sig = Signature::default();

let mut t = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = H;").expect("parse of A = B; C = D | E; F(x_) = H;");

let r0 = parse_rule(&mut sig, "G(y_) = y_").expect("parse of G(y_) = y_");
let r1 = parse_rule(&mut sig, "B = C").expect("parse of B = C");
let r2 = parse_rule(&mut sig, "E = F | B").expect("parse of E = F | B");

t.inserts_idx(2, vec![r0, r1, r2]).expect("inserting 3 rules at index 2");

assert_eq!(t.display(),
"A = B;
C = D | E;
G(y_) = y_;
B = C;
E = F | B;
F(x_) = H;");

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

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

Examples

let mut sig = Signature::default();

let mut t = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;").expect("parse of A = B; C = D | E; F(x_) = G;");

let r = parse_rule(&mut sig, "A = H").expect("parse of A = H");

let t = t.insert_clauses(&r).expect("inserting A = H with A = B");

assert_eq!(t.display(),
"A = B | H;
C = D | E;
F(x_) = G;");

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.

Examples

let mut sig = Signature::default();

let mut t = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;").expect("parse of A = B; C = D | E; F(x_) = G;");

let r = parse_rule(&mut sig, "G(y_) = y_").expect("parse of G(y_) = y_");

t.push(r).expect("inserting G(y_) = y_ at index 0");

assert_eq!(t.display(),
"G(y_) = y_;
A = B;
C = D | E;
F(x_) = G;");

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

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

Examples

let mut sig = Signature::default();

let mut t = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = H;").expect("parse of A = B; C = D | E; F(x_) = H;");

let r0 = parse_rule(&mut sig, "G(y_) = y_").expect("parse of G(y_) = y_");
let r1 = parse_rule(&mut sig, "B = C").expect("parse of B = C");
let r2 = parse_rule(&mut sig, "E = F | B").expect("parse of E = F | B");

t.pushes(vec![r0, r1, r2]).expect("inserting 3 rules at index 0");

assert_eq!(t.display(),
"G(y_) = y_;
B = C;
E = F | B;
A = B;
C = D | E;
F(x_) = H;");

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

Move a Rule from index i to j if possible.

Examples

let mut sig = Signature::default();

let mut t = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;
H = I;").expect("parse of A = B; C = D | E; F(x_) = G; H = I;");

t.move_rule(0, 2).expect("moving rule from index 0 to index 2");

assert_eq!(t.display(),
"C = D | E;
F(x_) = G;
A = B;
H = I;");

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.

Examples

let mut sig = Signature::default();

let mut t = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;").expect("parse of A = B; C = D | E; F(x_) = G;");

let r = parse_rule(&mut sig, "C = D").expect("parse of C = D");
let r_new = parse_rule(&mut sig, "C = A").expect("parse of C = A");

t.replace(0, &r, r_new).expect("replaceing C = D with C = A");

assert_eq!(t.display(),
"A = B;
C = E | A;
F(x_) = G;");

Trait Implementations

impl PartialEq<TRS> 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 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 Eq for TRS

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