问DPLL算法回溯树的c++文件和方法是什么？
EN

Stack Overflow用户

提问于 2016-08-04 01:52:42

回答 1查看 100关注 0票数 2

我正在尝试查找Z3的c++文件，如果在当前分支上找不到解决方案，算法将在该文件中进行回溯。我已经检查了所有的文件，并在python文件上尝试了调试模式，但到目前为止还没有成功。我只想向该方法添加一条print语句，这样我就可以知道它何时返回到前一个节点并尝试新的路径。

谢谢!

dpll

回答 1

Stack Overflow用户

发布于 2016-08-04 02:08:45

这取决于Z3使用哪个解算器来解决您的问题。它通常在源/smt中使用smt_context.cpp。可以在context::pop_scope方法中跟踪相关的回跳。还有其他的求解器:src/sat_solver用于位向量和布尔问题。它有一个类似的pop方法。最后，nlsat用于实数上的非线性多项式运算。

票数 1

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/38750546

复制

相似问题

问DPLL算法回溯树的c++文件和方法是什么？
EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问DPLL算法回溯树的c++文件和方法是什么？EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问DPLL算法回溯树的c++文件和方法是什么？
EN