support if_then_else op about biodivine-lib-bdd

[daemontus]

Right now, this functionality can be implemented using the "ternary apply" operator:

#[test]
fn test_if_then_else() {
    let set = BddVariableSet::new_anonymous(3);
    let vars = set.variables();
    let v1 = set.mk_literal(vars[0], true);
    let v2 = set.mk_literal(vars[1], true);
    let v3 = set.mk_literal(vars[2], true);
    // ITE(v1, v2, v3) = (v1 & v2) | (!v1 & v3)
    let if_then_else = bdd![(v1 & v2) | ((!v1) & v3)];

    fn ite_function(a: Option<bool>, b: Option<bool>, c: Option<bool>) -> Option<bool> {
        match (a, b, c) {
            // If "a" is known, we can just "implement" ITE and return "b"/"c".
            (Some(true), _, _) => b,
            (Some(false), _, _) => c,
            // The next two cases are not strictly necessary, but
            // can cause the operation to finish sooner if the result
            // is already determined, even when "a" is still unknown.
            (None, Some(false), Some(false)) => Some(false),
            (None, Some(true), Some(true)) => Some(true),
            // Otherwise, we return None until "a" becomes known.
            (None, _, _) => None,
        }
    }
    let ternary = Bdd::ternary_op(&v1, &v2, &v3, ite_function);

    assert_eq!(ternary, if_then_else);
}

For now, you can use the code above as a workaround. This is still a single BDD operation, so it should be comparable in overhead to other "native" ITE implementations. However, I fully agree that this should be part of the library directly. I'll make sure to add it to the next release :)

[gipsyh]

thanks！

[daemontus]

This is now supported in 0.5.0.