c - Z3 C-API 无约束地获取 const 的值

Question

我在一个使用 Z3 的 C API 的项目中，我正在试验枚举排序以将常数限制为一组有限值。

现在的问题是，只要没有为它定义约束，我就不会得到这个常量的值。但是此时我已经需要一个返回值，我想知道如何实现这一点。

• 是否存在可以强制将值分配给常量的约束？

• 使用在线评估器，我可以通过执行以下操作强制 Z3 返回一个值:

  (echo "starting Z3...")
  (declare-datatypes () ((S A B C)))
  (declare-const a S)
  (check-sat)
  (get-value (a))
  

但是我似乎无法使用 C-API 来实现它。我已经尝试过以下方法:

• 将创建 const 的 ast 放入求解器并获取模型。这给了我一个非法参数错误。
• 在不设置任何断言的情况下尝试从求解器获取模型会给我一个无效的使用错误

还有什么想法吗？我想我只是错过了一些东西。

Answer 1

以下代码片段对我有用:

using namespace z3;
void main() {
  context ctx;
  func_decl_vector cs(ctx);
  func_decl_vector ts(ctx);
  char const* abc[3] = {"A","B","C"};
  sort s = ctx.enumeration_sort("S", 3, abc, cs, ts);
  expr a = ctx.constant("a", s);
  solver so(ctx);
  so.check();
  expr b = so.get_model().eval(a, true);
  std::cout << b << "\n";
}

请注意，我将值“true”传递给 eval 的第二个参数。即使没有值(value)，这也会让评估者“完成”模型在检查可满足性(没有任何断言的求解器状态)时为“a”创建。模型完成默认为“false”。