问题标签 [cudd]

假设DdManager有四个变量：x, y, x', y'并且我有一个由xand构建的 BDD y。现在我想更改x为x', y,y'即获得由x'and构建的相同 BDD y'。

我怎样才能使用 CUDD 包得到这个？当我想实现模型检查算法时遇到了这个问题。我想知道如何实现这个操作或者我是否误解了符号模型检查算法？非常感谢！

我正在尝试运行一个简单的程序来学习如何使用 CUDD 包版本 3.0.0。我下载了软件包并安装了它：（ 1- ./configure 2- make 3- make check）。

我创建了以下简单程序：

我想创建一个makefile来编译它，我该怎么做？此外，如果我想通过命令行编译它，我该如何链接它的库？

我知道 CUDD 支持 ADD（代数决策图），但我似乎无法弄清楚如何将 ADD 用于多个输出布尔函数。此类函数的 ADD 需要有多个叶子，每个叶子代表一个布尔输出向量（可能编码为整数）。例如，0101 为 5，1000 为 8 等等。有谁知道这样的 DD 是否可以在 CUDD 中构建？

我正在研究二元决策图的可变排序。到目前为止，我们已经使用了不可逆电路。但不是我们需要使用 Reversible Benchmarks 来实现一些方法。但是我没有任何方法可以使用 C 语言中的 CUDD 库来读取基准文件（例如 blif、kiss、slif 文件）。我已经在互联网上寻找可用资源。有人请帮我找出路。

我正在尝试将 CUDD 的变量排序启发式用于另一个程序。我创建了一个 BDD，尝试了一些变量排序以查看哪个最小化大小，现在我想提取变量排序。我怎样才能做到这一点？

根据这个答案，ddpython 包为您提供了一种检查每个变量级别的方法，但我在 C/C++ 接口中没有看到相应的函数。那个 python 绑定是如何把它拉下来的？它是否需要通过访问 CUDD 内部cuddInt.h？

我正在使用 CUDD C++ 接口。

我没有找到关于这个图书馆的太多信息。

如何获得 BDD 的两个孩子？

例如：

现在，有了 f，我想得到它的 then 孩子和 else 孩子。文档说 DdNode 有这个孩子，但我不知道如何访问它们。

谢谢你。

我目前正在使用 PyCUDD，它是 SWIG 为 C 包 CUDD 生成的 Python 包装器。我目前正在尝试让 CUDD 从 C 代码中打印一些调试信息，但是 C 代码中的任何 printfs 似乎都不会产生任何输出 - 将它们放在 .i 文件中以供 SWIG 产生输出，将它们放在在 C 代码中没有。我不确定这是 SWIG 的特定属性还是将 C 代码编译为共享对象库的属性。

（特别令人沮丧的是，我知道我曾经遇到过这个问题并且之前已经解决了这个问题，但我现在似乎找不到任何东西来搜索这个问题，而且我显然忘了在那件事上留下笔记。）

是否可以使用 CUDD 获得 (x0 ∧ x1 ) ∨ (x0 ∧!x1 ) ∨ (!x0 ∧ x1 ) ∨ (!x 0 ∧!x 1 ) 的 bdd，它仍然具有代表变量 x0 和 x1 的节点? 我知道上面的布尔公式简化为常数函数 1。但我仍然想要一个不简化公式但将其表示为对应于 x0 和 x1 的 BDD“包含”节点的 BDD。如果不在 CUDD 中，是否可以使用其他工具来执行此操作？

在我的 ADD 计算中，我经常在叶子中有重复的值。它们应该被自动压缩吗？

例如：

-0-0-- 191.452

-0-1-- 191.452

-1-0-- 191.452

-1-1-- 191.452

一种猜测是它们具有不同的尾数，未显示。但我也有更多尾数的值：

---0-0 8.14148

---0-1 9.65706

---1-0 8.14148

---1-1 9.65706

我只能假设隐藏的数字是不同的，所以它们出现在不同的叶子中......

它似乎只显示6位数字。我可以更改此设置吗？谁能证实我的怀疑？非常感谢。

我正在使用 Cudd_PrintInfo 来解决 CUDD 的性能问题。

打印出统计数据后，我发现点击率非常低。我尝试了有无垃圾收集，但它保持不变。此外，碰撞也很高。
我该如何解决这些问题？
（我真的应该把这两个问题分开吗……？）

使用垃圾收集：

没有垃圾收集：