Variable Substitution

[Hirtol]

Hi, I'm trying to implement a symbolic solver using oxidd, but this requires some variable substitution here and there. For example, if we have the following:

// Create two sets of `n_variables` (say 2)
let variables = manager
            .with_manager_exclusive(|man| (0..n_variables).flat_map(|x| BDDFunction::new_var(man)).collect_vec());
let variables_prime = manager
            .with_manager_exclusive(|man| (0..n_variables).flat_map(|x| BDDFunction::new_var(man)).collect_vec());

let bdd_expr = variables[0].and(&variables[1]);

// Ideal API, replace variables[0] with variables_prime[0], etc.
let substituted_expr = bdd_expr.substitute(&variables, &variables_prime);

Is there any way at the moment to replace the variable references from bdd_expr to variables_prime[0] and variables_prime[1] instead? In essence cloning the structure of the existing BDD nodes, but positioned on the 'lower' levels. An approximation seems to be possible by using Level::swap, but this swaps all nodes of that level, not just bdd_expr's nodes.

[nhusung]

Hi and thank you for the request. If I understand it correctly, the substitute method you desire corresponds to BuDDy’s bdd_veccompose() and CUDD’s Cudd_bddVectorCompose(). Such an operation is not implemented yet, but I’m willing to implement it (should not take long).

EDIT: In your concrete case, an operation like BuDDy’s bdd_replace() would probably suffice, right?

[Hirtol]

Thanks for the consideration! I was initially thinking of Cudd_bddSwapVariables() (or bdd_replace()), but a veccompose() equivalent seems like a better, and more general, fit.

[Hirtol]

Many thanks for implementing this, can confirm that it works well (and faster than the hack-job I did in the interim)!