问题标签 [cudd]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
binary-decision-diagram - 在 CUDD 中传递布尔表达式时出错(在 BuDDy 中工作)
我正在尝试使用 CUDD 查找 Shared-BDD 中的节点总数。 我已经使用 BuDDy-2.4 编写了 C 代码并且运行良好但是当我使用 CUDD 而不是 BuDDy 时,我的程序显示错误。
我的 BuDDY C 文件是:
我的 CUDD C 程序是:
但是这个 CUDD C 程序显示错误
cudd - BLIF 输入到图形输出(文本和图片)
我最近才开始使用 CUDD。
我有一个 BLIF 格式的电路,我想将它输入到 CUDD,我知道它会给我 BDD,我也想要 ZDD。
我已经阅读了自述文件,但是对于我的生活,我根本找不到如何使用它。
谁能告诉我如何详细输入 blif 到 CUDD?(什么命令以及在哪里编写命令)
对不起,如果这太基本了。
c - CUDD Binary Decision Trees. Linking to libcudd.a
Does anyone on this community have experience with compiling linking the CUDD package for manipulating BDDs? Seems like a great resource if I can only compile something simple... Getting a lot of following. I am a novice with C, mainly Py guy, so any help would be highly appreciated. (I've tried using tulip-dd in Py, but that is a limited experience). Thanks in advance.
cudd - CUDD BDD:构建一个布尔值作为连词的析取但得到运行时错误:分段错误
是否有使用 CUDD(不要与 CUDA 混淆)来操作 BDD 的经验的人知道为什么我可能不断收到可怕的“分段错误(转储核心)”。我怀疑这可能与引用取消引用有关,我承认我不完全理解。任何提示指针表示赞赏。我(评论了我一直在尝试的一些事情):
c++ - CUDD C++ 接口,用于将布尔值转换为 BDD 和生成的 minterms 集(到割集)
我正在与(https://github.com/ivmai/cudd)合作,目标是执行以下重复过程:
(1) 输入:(相干,非递减)布尔函数表达式 top = a_1 a_2 a_3...+ x_1 x_2 x_3... + z_1 z_2 z_3...)。我正在使用的布尔值有数千个变量(ai...zj)和数百个术语。
(2) 处理:将布尔值转换为 BDD 以简化最小项或互斥割集(我们在可靠性世界中称之为)的计算。
(3) 输出:取一组我的最小割集(minterms)。通过将 (2) 中找到的所有小项相加来计算顶部事件概率。
我找到了一种使用劳动密集型手动 C 接口来构建布尔值的方法。我还发现了如何使用出色的 tulip-dd Py 界面来实现它,但无法像 cudd 那样进行扩展。
现在我希望通过 cudd 的 C++ 接口,我可以两全其美(我要求太多了吗?)也就是说,tulip-dd 的便利性和 cudd 的可扩展性。所以这里有一些示例代码。我失败的地方是第 3 步,打印出我以前可以在 C 中完成的最小术语。我如何使用 C++ 接口来完成它?!请参阅代码中的注释以了解我的具体想法和尝试。
谢谢,桂
c++ - 可爱的 C++ 接口。将字符串格式的布尔表达式读入 cudd 的建议?
我之前的帖子CUDD C++ Interface for convert Booleans to BDDs and result set of minterms (to cutsets)的后续文章。
在 Python 上运行的 tulip-dd BDD 库中,可以将布尔表达式定义和读取为字符串。这使得整个 I/O 过程非常方便。
现在,我们刚刚在上一篇文章中看到,使用 cudd C++ 接口,我们可以使用紧凑的数学符号方便地定义一个布尔表达式,例如x1*x2 + x3*x4
以及如何从该表达式产生最小项的总和。但是 cudd 是否也允许我们将字符串用于布尔表达式?我怀疑不是,如果不是,我将不得不找到一种方法将上面 sum 乘积的字符串等价转换为等价的 Boolean: "x1*x2+x3*x4"
to x1*x2+x3*x4
。
model-checking - CUDD:ZDD 的量化
我正在使用 CUDD ( https://github.com/ivmai/cudd ) 使用 bdd 和 zdd 功能进行模型检查,我想知道如何量化 zdds。
对于 bdd,有 bddExistAbstract 和 bddUnivAbstract 函数(参见http://web.mit.edu/sage/export/tmp/y/usr/share/doc/polybori/cudd/cuddAllDet.html#Cudd_bddUnivAbstract)。
该手册说,这些函数普遍地和存在地从 bdd 中抽象出给定的变量(以封面形式)。我不太清楚“抽象出来”是什么意思,因此我坚持弄清楚量化如何改变 zdds。
你们能帮忙吗?谢谢。
cudd - Cudd_PrintMinterm,访问产品总和中的各个最小项
这可能是本论坛常驻 CUDD/BDD 专家@DCTLib 的问题,但如果其他人有见解,当然欢迎!
考虑给定的最小项,例如: 0--0---0--0---0----11 1 。
我需要单独取每个 minterm 并用 P(x_i) 替换“1”(我正在处理变量的概率),用 1-P(x_i) 替换 0,用 1 替换“-”。然后我将其中的因素相乘一个最小项,P(x_i)...(1-P(x_j)) 并将它们加起来以获得顶部事件的概率。(对应于最小项的概率的和积)
我需要一一处理的原因是我正在处理会炸毁内存的大文件。一旦我超过 80-100 个变量,您就处于整个 minterm 文本文件转储大小的 TB OoM 中. 如果可能,我想获取每个 minterm,将其添加到运行总和中,并在添加后将其删除。
希望这很清楚,但如果不是,可能需要一些迭代。谢谢,
cudd - CUDD 上的递归方法
这是@DCTLib 在下面的帖子中提出的建议的后续行动。
Cudd_PrintMinterm,访问产品总和中的各个最小术语
我一直在追求建议的 (b) 部分,并将在单独的帖子中分享一些伪代码。
同时,在他的 (b) 部分建议中,@DCTLib 发布了指向https://github.com/VerifiableRobotics/slugs/blob/master/src/BFAbstractionLibrary/BFCudd.cpp的链接。我一直在尝试阅读这个程序。Somenzi 的经典论文 Binary Decision Diagrams 中有一个递归函数,它描述了一种计算满足分配数量的算法(下图,图 7)。我一直在尝试比较两者,蛞蝓和图 7。但很难看到任何相似之处。但是C对我来说几乎是不可思议的。你知道蛞蝓 BFCudd 是否基于 Somenze 图 7,@DCTLib?
谢谢,桂
cudd - CUDD 上的多态 DD(Python 版本,tulip-DD)
对于那里的 CUDD 大师,我实际上使用的是 Python 等价物 tulip-dd: https ://github.com/tulip-control/dd 。
我正在尝试绘制由以下定义的 MDD 或多状态决策图:
我的问题之一是如何绘制 MDD。我试过了:
但是自动机没有这样的方法。