[−][src]Struct term_rewriting::TRS
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
[src]
pub fn new(rules: Vec<Rule>) -> TRS
[src]
Constructs a Term Rewriting System
from a list of Rule
s.
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
[src]
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
[src]
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
[src]
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
[src]
The number of Rule
s 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
[src]
Are there any Rule
s 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
[src]
Return the number of total number of subterms across all Rule
s 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
[src]
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
[src]
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>
[src]
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>
[src]
All the Operator
s 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
[src]
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
[src]
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
[src]
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>>
[src]
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)>
[src]
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>
[src]
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)>
[src]
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>
[src]
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>
[src]
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>
[src]
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>
[src]
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>
[src]
&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>
[src]
&mut self,
idx: usize,
rules: Vec<Rule>
) -> Result<&mut TRS, TRSError>
Inserts a series of Rule
s 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>
[src]
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>
[src]
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>
[src]
Inserts a series of Rule
s 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>
[src]
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>
[src]
&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
[src]
impl Clone for TRS
[src]
fn clone(&self) -> TRS
[src]
fn clone_from(&mut self, source: &Self)
1.0.0[src]
Performs copy-assignment from source
. Read more
impl Eq for TRS
[src]
impl Debug for TRS
[src]
impl Hash for TRS
[src]
Auto Trait Implementations
Blanket Implementations
impl<T> From<T> for T
[src]
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
fn to_owned(&self) -> T
[src]
fn clone_into(&self, target: &mut T)
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,