Open
Description
Hey,
I think I'm missing something basic here. I'm trying to get the fully simplified form of a term:
extern crate term_rewriting;
use term_rewriting::{Signature, Strategy, trace::*, parse_trs, parse_term};
fn main() {
let mut sig = Signature::default();
let t = parse_trs(&mut sig,
"Or(q_ q_) = q_;
And(q_ q_) = q_;
Or(a_ b_) = Or(b_ a_);
And(a_ b_) = And(b_ a_);
And(a_ Or(b_ c_)) = Or(And(a_ b_) And(a_ c_));
Or(a_ And(b_ c_)) = And(Or(a_ b_) Or(a_ c_));
Or(a_ 1) = 1;
And(a_ 0) = 0;
And(a_ Or(a_ b_)) = a_;
Or(a_ And(a_ b_)) = a_;
And(a_ 1) = a_;
Or(a_ 0) = a_;
Not(Not(q)) = q;
Or(a_ Not(a_)) = 1;
And(a_ Not(a_)) = 0;
Not(Or(a_ b_)) = And(Not(a_) Not(b_));
Not(And(a_ b_)) = Or(Not(a_) Not(b_));").unwrap();
// let term = parse_term(&mut sig, "Or(And(a b c) And(a b d))").unwrap();
// let term = parse_term(&mut sig, "And(a Or(a b))").unwrap();
let term = parse_term(&mut sig, "Not(Not(a))").unwrap();
let mut trace = Trace::new(&t, &term, 0.5, 1.0, None, Strategy::Normal);
let outcomes = trace.outcomes(50);
for oc in outcomes {
println!("{}", oc.term().pretty());
// expectation is that I'd pick the outcome with the fewest operators here...
}
}
This prints a single outcome: Not(Not(a))
. If I just call rewrite()
once, I get a
as expected, but that strategy doesn't work for terms that need more than one rewriting step. Could you help me figure out what I'm doing wrong here please?
Thanks!
Metadata
Metadata
Assignees
Labels
No labels