binary-decision-diagram - 通过CUDD计算图像后获取BDD的所有变量（C接口）

Question

我卡在CUDD（C接口）的BDD上的操作上，我不知道我们在计算图像时是否可以删除一些变量（从BDD的一个状态到另一个状态）以及如何传递结果BDD（最终BDD ) 要获取所有变量，有人可以告诉我我们是否可以通过 CUDD 做到这一点吗？干杯

Answer 1

我从未使用过 CUDD，但 BDD 中使用的变量列表通常称为它的support。从 BDD 中删除变量通常是通过存在量化来完成的。

Grepping源代码，我发现

/**Function********************************************************************

  Synopsis    [Finds the variables on which a DD depends.]

  Description [Finds the variables on which a DD depends.
  Returns a BDD consisting of the product of the variables if
  successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_VectorSupport Cudd_ClassifySupport]

  ******************************************************************************/
DdNode *
Cudd_Support(
  DdManager * dd /* manager */,
  DdNode * f /* DD whose support is sought */)

和

/**Function********************************************************************

  Synopsis [Existentially abstracts all the variables in cube from f.]

  Description [Existentially abstracts all the variables in cube from f.
  Returns the abstracted BDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddUnivAbstract Cudd_addExistAbstract]

******************************************************************************/
DdNode *
Cudd_bddExistAbstract(
  DdManager * manager,
  DdNode * f,
  DdNode * cube)