通过 CUDD(C 接口)执行计算映像后获取 BDD 的所有变量

Question

我被困在 CUDD（C 接口）的 BDD 上的操作上，我不知道我们在执行计算映像时是否可以删除一些变量（从 BDD 的一种状态到另一种状态）以及如何传输结果 BDD（最终 BDD）以获取所有变量，任何人都可以告诉我我们是否可以通过 CUDD 做到这一点？干杯

Answer 1

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

清理源代码，我发现

/**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)