Skip to content

Getting all outcomes of a Trace #46

Open
@zbjornson

Description

@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!

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions