问题标签 [cudd]

我希望从 CUDD 库的管理器中删除一个变量。这个问题是 8 年前在这个线程中提出的，没有令人满意的答案。现在有人知道吗？

@DCTLib，您还记得下面的讨论吗？你提出了一个递归方程，这是正确的方法。

Cudd_PrintMinterm，访问产品总和中的各个最小项

现在，我正在考虑多状态可靠性，我们可以不失败或失败到 n-1 个不同的状态，其中 n >= 2。Tulip-dd 实现 MDD，如下所述：

https://github.com/tulip-control/dd/blob/master/doc.md#multi-valued-decision-diagrams-mdd

https://github.com/tulip-control/dd/issues/71

https://github.com/tulip-control/dd/issues/66

在下图中的图中，我们定义了一个 MDD，声明如下：

aut.declare_variable(x=(0,3)) u = aut.add_expr('x=i')

多值变量 (MSV) x、x=0、x=1、x=2 或 x=3 的每个值/状态都会导致特定的 BDD，如下图所示，采用四态这里以变量 x 为例。表示法是状态 0 代表正常状态​​，x 可以失败到不同的状态 1、2 和 3。失败概率在下表中分配。在下面的 BDD 中，我们（以及 tulip）使用二进制编码，带有两个位 x_1 和 x_0 来表示 MSV 的每个状态/值。最低有效位 (LSB)，即 x_0，始终是祖先。下面的每个 BDD 图都是特定值或状态的表示。

为了量化特定状态的 BDD，即顶部节点，我们必须知道二进制变量 x_0 和 x_1 在 BDD 中采用不同分支（then or else）的概率。这些分支概率没有直接给出，需要根据BDD结构计算。

这里的关键是在计算父节点概率之前必须知道子节点概率和父节点的分支概率。在之前的 BDD 量化中，我们在计算节点 x_1 概率时，就知道了从节点 x_1 到叶子节点的分支概率。我们不需要知道节点 x_1 是如何连接到节点 x_0 的。现在，对于这个四态变量 x，我们需要知道节点 x_1 是如何连接到节点 x_0（代表最低有效位的二进制变量）来确定从节点 x_1 到叶节点的分支概率。问题是如何实现这一点？

我正在使用 CUDD C++ 接口。我发现关于 C++ 库的信息非常少，但对于 C 语言来说非常详尽和丰富。

我有几个问题：

1. 如何获取 BDD 节点的两个子节点？C++ 接口的 C 中 Cudd_T(node) 和 Cudd_E(node) 的对应物是什么？
2. C++ 接口中 Cudd_NodeReadIndex(node) 的对应物是什么？

提前谢谢！

我正在使用https://github.com/tulip-control/dd/blob/master/doc.md#multi-valued-decision-diagrams-mddIoannis Filippidis 设计的包用于多值决策图上的以下两个功能，top以及successors.

我需要帮助编写第三个函数，，level（概述如下）。对于每个节点，都有一个唯一级别，如图所示。

我查看了 CUDD 的在线文档（http://web.mit.edu/sage/export/tmp/y/usr/share/doc/polybori/cudd/cuddIntro.html），这是一个二进制决策图库（ BDD），但找不到关闭自动使用 BDD 补边的方法。在我看来它确实应该存在，你知道它是否存在吗？

我正在开发一个应用程序，它通过进入 fanin 锥体并使用 fanin 的 BDD 对象为设计对象创建 BDD 节点。

我的应用程序占用了太多内存并被杀死。我尝试获取堆栈跟踪，但我看到许多（至少 400 000 个）“ddSuppInteract”堆栈帧。ddSuppInteract 被调用的原因是什么？