Function biodivine_lib_bdd::_impl_bdd::_impl_boolean_ops::apply_with_flip

fn apply_with_flip<T>(
    left: &Bdd, 
    right: &Bdd, 
    flip_left_if: Option<BddVariable>, 
    flip_right_if: Option<BddVariable>, 
    flip_out_if: Option<BddVariable>, 
    terminal_lookup: T
) -> Bdd where
    T: Fn(Option<bool>, Option<bool>) -> Option<bool>, 

(internal) Universal function to implement standard logical operators.

The terminal_lookup function takes the two currently considered terminal BDD nodes (none if the node is not terminal) and returns a boolean if these two nodes can be evaluated by the function being implemented. For example, if one of the nodes is false and we are implementing and, we can immediately evaluate to false.

Additionally, you can provide flip_left_if, flip_right_if and flip_out_if BddVariables which will, given the corresponding node has the given decision variable, flip the low/high link of the node. This is used to implement faster state-space generators for asynchronous systems.

The reason why we allow this behaviour in apply, is that flipping the pointers in a BDD is cheap, but breaks the DFS order, which may result in unexpected behaviour. Furthermore, since the function is generic, in most performance intensive paths, it should be optimized anyway.