Z3 API: 解析定点 SMTLib 字符串时崩溃

Question

我正在尝试使用 Z3 的 C/C++ API 来解析 SMTLib2 格式的定点约束（特别是 SeaHorn 生成的文件）。但是，我的应用程序在解析字符串时崩溃（我正在使用 Z3_fixedpoint_from_string 方法）。我使用的 Z3 版本是 4.5.1 64 位。

我尝试解析的 SMTLib 文件适用于我从源代码编译的 Z3 二进制文件，但在调用 Z3_fixedpoint_from_string 时遇到分段错误。我将问题缩小到我认为问题与向定点上下文添加关系有关的程度。下面是一个在我的机器上产生段错误的简单示例：

#include "z3.h"

int main()
{
    Z3_context c = Z3_mk_context(Z3_mk_config());
    Z3_fixedpoint f = Z3_mk_fixedpoint(c);

    Z3_fixedpoint_from_string (c, f, "(declare-rel R ())");

    Z3_del_context(c);
}

运行此代码与 valgrind 报告大量无效读写。所以，要么这不是 API 应该使用的方式，要么某处存在问题。不幸的是，我找不到任何关于如何以编程方式使用定点引擎的示例。但是，例如调用 Z3_fixedpoint_from_string (c, f, "(declare-var x Int)"); 就可以了。

顺便说一句，Z3_del_fixedpoint() 在哪里？

Answer 1

固定点对象 "f" 被引用计数。调用者负责在创建后立即获取引用计数。使用C++智能指针来控制它更容易，类似于我们为其他对象控制它的方式。 C++ API 没有定点对象的包装器，因此您必须按照其他包装器的样式创建自己的包装器。

而不是 del_fixedpoint 使用引用计数器。

class fixedpoint : public object {
     Z3_fixedpoint m_fp;
public:
    fixedpoint(context& c):object(c) { mfp = Z3_mk_fixedpoint(c); Z3_fixedpoint_inc_ref(c, m_fp); }
    ~fixedpoint() { Z3_fixedpoint_dec_ref(ctx(), m_fp); }
    operator Z3_fixedpoint() const { return m_fp; }

    void from_string(char const* s) {
         Z3_fixedpoint_from_string (ctx(), m_fp, s);
    }

};

int main()
{
   context c;
   fixedpoint f(c);
   f.from_string("....");       
}

Z3 API: 解析定点 SMTLib 字符串时崩溃

Z3 API: Crash when parsing fixed point SMTLib string

z3