z3 - 跟踪 z3 内存泄漏

标签 z3

我们遇到了一些与内存泄漏相关的问题。我们正在使用具有引用计数垃圾收集的上下文。以下是对情况的简短描述:

通过在最新的 unstable 上使用 ScalaZ3,我们创建了大量的重新计数上下文(400-500),我们在这些上下文中使用了很少的求解器(<5),检查了几个公式,然后删除了所有内容。我们尝试在删除上下文本身之前删除所有内容。我们看到内存占用量不断增加(高达几 Gb),即使我们一次只使用 5 或 6 个新鲜的小上下文。

1) 当上下文被删除时,Z3 会释放上下文中所有对象的内存吗? (即使是 refcount > 0 的那些)如果不是,原因可能是我们忘记删除引用几个对象。

2) 您是否有任何工具/提示可以帮助我们追踪内存中剩余的内容。也许在 open_log 生成的文件之上?或者在 gcc 下重放日志时要看哪里?

谢谢!

最佳答案

1) Z3 会在删除上下文时释放部分内存,但我们不保证在引用计数器未正确使用时会删除所有内存。

2) 我通常使用 Valgrind 来跟踪内存泄漏。我认为这太棒了。我们可以在文件z3.log中创建执行日志,然后执行

       valgrind z3 z3.log

顺便说一句,在 Debug模式下编译也可能有帮助。在 Debug模式下,Z3 还会报告删除上下文时仍然存在的 AST 列表。

关于z3 - 跟踪 z3 内存泄漏,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/17235412/

相关文章:

斯卡拉^Z3 : Delete previous assertion

python - 在 Z3 中,有没有办法生成未定义数量的假设来检查?

c++ - C++ API 缺少修改方法

python - 如何区分 bool 和 z3 表达式?

c++ - 在 C++ 中使用 Z3 API 的段错误

floating-point - 如何在 SMT-LIB 标准中表示浮点常量(如 1e307)?

java - 为什么从 z3 java API 获取查询结果比直接从 z3 获取查询结果慢?

java - Z3:检查模型是否唯一

python - (Z3Py) 函数声明有任何限制吗?

java - Z3 Java API 文档