z3 中的常量 – C++ 中的分段错误 api

Question

z3 的以下 c++ api 代码导致分段错误：11 （z3 版本 4.4.0 运行 Mac OS 10.10.2）

#include "../z3/include/z3++.h"

int main() {
  z3::context c;

  z3::sort A = z3::sort(c);
  z3::expr x = c.constant("x", A);
}

我是不是做错了什么？

Answer 1

表达式 z3::sort(c) 将 A 初始化为与上下文相关联的排序对象，但不是实际（较低级别）的排序对象。（另请参阅 C++ example 以了解如何构造常用的排序。）

我相信目前没有方便的 C++ 风格的方法来构造未解释的排序。为此，我们需要使用 C-API 函数 Z3_mk_uninterpreted_sort（然后可以使用 z3::sort(c, ...) 包装）

constants in z3 – segmentation fault in c++ api