cfallin / boolean_expression Goto Github PK

Looks like commit 0105215 introduced a general from implementation that overlaps with any T that implements certain traits. This will break code that tries to provide its own implementation of From<T> (example attached).

https://github.com/cucapra/futil/blob/80aed57976ddac86a99c54dc546d42be16f073cc/calyx/src/passes/simplify_guards.rs#L10-L20

AFAIK, rust's trait system doesn't allow for multiple conflicting implementations so the upstream crate has to hide the implementation/not provide it.

On a side note, thanks for implementing this crate and open sourcing it!

Hi!

Love the library. I am currently mapping my Expr<T> into Expr<bool> and would like to avoid providing a hashmap with true in it. Would it be an idea for something along the lines of the snippet below (naming tbd) to directly return a boolean?

impl Expr<bool> {
  pub fn evaluate_bool(self) -> bool {
    ...
  }
}

This would be cleaner (and maybe slightly faster) than

expr.map(|f| f.do_stuff()).evaluate(&[(true, true)].iter().cloned().collect())
// vs
expr.map(|f| f.do_stuff()).evaluate_bool()

Here's my example program:

use boolean_expression::{BDD, Expr};

fn main() {
    let node = |name: &str| Expr::Terminal(name.to_string());

    let a_select = (node("as0") & node("ai0")) | (node("as1") & node("ai1")) | (node("as2") & node("ai2")) | (node("as3") & node("ai3")) | (node("as4") & node("ai4")) | (node("as5") & node("ai5")) | (node("as6") & node("ai6"));
    let b_select = (node("bs0") & node("bi0")) | (node("bs1") & node("bi1")) | (node("bs2") & node("bi2")) | (node("bs3") & node("bi3")) | (node("bs4") & node("bi4")) | (node("bs5") & node("bi5")) | (node("bs6") & node("bi6"));

    let a_inverted = a_select ^ node("ainv");
    let b_inverted = b_select ^ node("binv");

    let andxor = (!node("andxor") & a_inverted.clone() & b_inverted.clone()) | (node("andxor") & (a_inverted.clone() ^ b_inverted.clone()));
    let muxout = (!node("muxsel") & a_inverted) | (node("muxsel") & b_inverted);

    let output = (!node("usemux") & andxor) | (node("usemux") & muxout);

    let mut bdd = BDD::new();
    let top = bdd.from_expr(&output);

    println!("{}", bdd.to_dot(top));
}

If you look at the output dot, there's a lot of duplication of things like the a_select and b_select muxes, much of which I would argue is unnecessary.

From this snippet of the output, it seems to me that all the "b_inv is true" nodes can be merged and all the "b_inv is false" nodes can be merged. If you then recursively follow this upwards, this would remove a lot of redundancy.

I happened to be looking at my dependencies and noticed that this crate is bringing in a bunch of dependencies that are only used while testing. They can be made dev-dependencies in order to not be runtime dependencies.

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?

So, while experimenting with boolean_expression, I found that calling PersistedBDD::persist() on an empty BDD panics.

thread 'main' panicked at 'index out of bounds: the len is 0 but the index is 0', /home/lofty/.cargo/registry/src/github.com-1ecc6299db9ec823/boolean_expression-0.4.3/src/bdd.rs:629:25

Should the <= in

        while self.next_output_func <= f {

be < instead?