Partial evaluation assuming a complex expression is true

[farnoy]

Hi and thanks for this helpful library.

I figured out how to do partial evaluation by substituting Terminals, but I don't know how to simplify an expression assuming some other expression is true.

Assuming it's always in SOP form, I could compare recursively until I find my "assumption" and substitute it with a constant, but it would be so fragile that even a different order of either expression would fail to match.

Ideally, what I'd like to do:

let x = Expr::Terminal(0);
let y = Expr::Terminal(1);
let z = Expr::Terminal(2);

let expr = x.clone() & y.clone() & z.clone();
let assumption = x.clone() & y.clone();

assert_eq!(black_box(expr, assumption), z);

Is this possible, or would I need to reach for some kind of SMT solver to be able to express this?

[cfallin]

Hi @farnoy,

This is a really interesting question! I've thought about it for a bit and I can't come up with any simple and fully general solutions, but maybe there's a trick I'm not seeing right now.

For a case where the "assumptions" are a single boolean product (AND of terminals and not-terminals), I think this reduces to just partial evaluation with the given term values; e.g. in your example, we could do a recursive transform on expr where we replace Terminal(0) and Terminal(1) with constant true, and simplify (a AND true == a, for example).

But if we have an assumption that is for example x OR y, then we can't simply take expr with x := true, expr with y := true, and then OR them. In other words this isn't distributive...

I suppose one could maybe build a BDD that contains both expressions and then merge the node for assumption with true and propagate/re-canonicalize up the DAG. That seems like it might work in some cases, though it's not clear to me that there will always be a node in common in cases where one might expect to simplify.

I'll think more about this though!

[farnoy]

Thanks,

My usecase consists of doing analysis at compile time to do validation and generate optimized code. For now, I'm forced to do very basic analysis, like expressions simplifying to a const value. I'd love to be able to do more robust checks, but it'll work for now.

The code generation part is working out great though. I'm using the following to generate a Rust expression that evaluates the boolean function:

fn evaluate_to_tokens(e: Expr<String>) -> TokenStream {
    match e {
        Expr::Terminal(ref name) => {
            let ident = syn::parse_str::<Ident>(name).unwrap();
            quote!(#ident)
        }
        Expr::Const(bool) => quote!(#bool),
        Expr::Not(inner) => {
            let inner = evaluate_to_tokens(*inner);
            quote!(!#inner)
        }
        Expr::And(a, b) => {
            let a = evaluate_to_tokens(*a);
            let b = evaluate_to_tokens(*b);
            quote!((#a && #b))
        }
        Expr::Or(a, b) => {
            let a = evaluate_to_tokens(*a);
            let b = evaluate_to_tokens(*b);
            quote!((#a || #b))
        }
    }
}

Every Terminal is supposed to be a boolean variable with the same name.