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("....");       
}