Getting all outcomes of a Trace

[zbjornson]

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!

[joshrule]

Hmmm... In the TRS above, the rule for Not operates over the constant q rather than the variable q_. My guess is that you want the rule Not to be Not(Not(q_)) = q_;, right?

[zbjornson]

Gah, you're right, thanks. That solves the term that was not commented-out (Not(Not(a))). I'm still not getting simplifications of the other terms that are commented out though. And(a Or(a b)) with any of the three strategies has no outcomes. A single rewrite() with Strategy::All produces And(Or(a, b), a) and And(a, Or(b, a)) instead of a, for example. See something else I'm missing?

[joshrule]

I don't see anything obvious. 0.7.0 is fairly old code - I've pushed the library much further and fixed many bugs on the develop branch. You might swap to using that and then see if it fixes the issue.

[zbjornson]

Hrm, still no luck. With develop:

extern crate term_rewriting;
use term_rewriting::{Signature, Strategy, NumberRepresentation, trace::*, parse_trs, parse_term};

fn main() {
    let mut sig = Signature::default();
    let t = parse_trs(&mut sig,
        "And(a_ Or(a_ b_)) = a_;").unwrap();
    let patterns = t.patterns(&sig);

    let term = parse_term(&mut sig, "And(a Or(a b))").unwrap();

    let trace = Trace::new(&t, &sig, &term, 0.5, 10, None, &patterns, Strategy::All, NumberRepresentation::default());
    for idx in trace.iter() {
        println!("{}", trace[idx].term().pretty(&sig));
    }
}

And(a, Or(a, b))

Since that term is a perfect match for the rule, I'm guessing I don't have the rule specified properly.

[joshrule]

Ack - sorry to be slow here. I don't have the ability to easily test this on my work machine, but I will try to take a closer look this weekend.

[zbjornson]

No problem and no rush, really appreciate your help if/when you get to it.

[joshrule]

Aha - there was a bug in term unification. I just pushed some changes to develop that should resolve this issue. Check out 34e011d.