1 
use std::collections::HashSet;
2 

            

        

            

                3
            

            

                
            

            

                
use oxidd::BooleanFunction;

            

        

            

                4
            

            

                
            

            

                
use oxidd::Function;

            

        

            

                5
            

            

                
            

            

                
use oxidd::HasLevel;

            

        

            

                6
            

            

                
            

            

                
use oxidd::Manager;

            

        

            

                7
            

            

                
            

            

                
use oxidd::ManagerRef;

            

        

            

                8
            

            

                
            

            

                
use oxidd::VarNo;

            

        

            

                9
            

            

                
            

            

                
use oxidd::bdd::BDDFunction;

            

        

            

                10
            

            

                
            

            

                
use oxidd::bdd::BDDManagerRef;

            

        

            

                11
            

            

                
            

            

                
use oxidd::util::OutOfMemory;

            

        

            

                12
            

            

                
            

            

                

            

        

            

                13
            

            

                
            

            

                

            

        

            

                14
            

            

                
            

            

                
/// The BDD representing the support variables of a BDD function.

            

        

            

                15
            

            

                
            

            

                
pub type BDDSupport = BDDFunction;

            

        

            

                16
            

            

                
            

            

                

            

        

            

                17
            

            

                
            

            

                
/// Computes the support (set of variables) of the given BDD function.

            

        

            

                18
            

            

                
            

            

                
/// 

            

        

            

                19
            

            

                
            

            

                
/// # Details

            

        

            

                20
            

            

                
            

            

                
/// 

            

        

            

                21
            

            

                
            

            

                
/// The `support` is the variables on which the `BDD` is defined, and other

            

        

            

                22
            

            

                
            

            

                
/// variables are irrelevant or don't care, formally:

            

        

            

                23
            

            

                
            

            

                
///

            

        

            

                24
            

            

                
            

            

                
/// > support(f) = { x_i | exists x_0, ..., x_{i-1}, x_{i+1}, ..., x_n : f(x_0, ..., x_{i-1}, true, x_{i+1}, ..., x_n) != f(x_0, ..., x_{i-1}, false, x_{i+1}, ..., x_n) }

            

        

            

                25
            

            

                
            

            

                
pub fn support(manager_ref: &BDDManagerRef, function: &BDDFunction) -> Result<Vec<VarNo>, OutOfMemory> {

            

        

            

                26
            

            

                
            

            

                
    let mut result = HashSet::new();

            

        

            

                27
            

            

                
            

            

                
    support_rec(manager_ref, function, &mut result);

            

        

            

                28
            

            

                
            

            

                
    Ok(result.into_iter().collect())

            

        

            

                29
            

            

                
            

            

                
}

            

        

            

                30
            

            

                
            

            

                

            

        

            

                31
            

            

                
            

            

                
/// Recursive implementation of [support].

            

        

            

                32
            

            

                
            

            

                
fn support_rec(manager_ref: &BDDManagerRef, function: &BDDFunction, result: &mut HashSet<VarNo>) {

            

        

            

                33
            

            

                
            

            

                
    manager_ref.with_manager_shared(|manager| {

            

        

            

                34
            

            

                
            

            

                
        let node = manager.get_node(function.as_edge(manager)).unwrap_inner();

            

        

            

                35
            

            

                
            

            

                
        result.insert(node.level());

            

        

            

                36
            

            

                
            

            

                

            

        

            

                37
            

            

                
            

            

                
        // Recurse into cofactors

            

        

            

                38
            

            

                
            

            

                
        if let Some((low, high)) = function.cofactors() {

            

        

            

                39
            

            

                
            

            

                
            support_rec(manager_ref, &low, result);

            

        

            

                40
            

            

                
            

            

                
            support_rec(manager_ref, &high, result);

            

        

            

                41
            

            

                
            

            

                
        }

            

        

            

                42
            

            

                
            

            

                
    })

            

        

            

                43
            

            

                
            

            

                
}