c++ - C++ 中的 Z3 最大化

Question

在 Z3 中，以下显然被评估为最大值 2，模型 x=true 且 y=true。

(declare-const x Bool)
(declare-const y Bool)
(declare-const z Bool)
(assert(= z false))
(maximize(
  +  
    (ite (= x true) 1 0) 
    (ite (= y true) 1 0) 
    (ite (= z true) 1 0)
  )
)
(check-sat)
(get-model)

我如何使用 C/C++ API 实现它？我试过使用这个简单地解析:

Z3_ast parsed = Z3_parse_smtlib2_string(c,<The above Z3>,0,0,0,0,0,0);
z3::expr simpleExample(c, parsed);
s.add(simpleExample);

但它打印“unsupported\n ;maximize”。

我不介意手动构建表达式——而不是使用构建的文件。我根本不知道要为“maximize”使用哪些 expr 函数或运算符。

附录:根据最近的一些回答和讨论，很明显我目前要求的不是正常功能。因此，我改变了问题，以询问使这项工作按目前情况进行的方法的具体细节。

Answer 1

感谢您指出这个问题。优化功能不是 SMT-LIB2 的一部分。它们是自定义扩展。此外，解析 SMT-LIB2 基准的函数没有任何方法反射(reflect)优化编译指示。 API解析器无法识别的原因这些扩展是优化功能未在该解析器中注册(它们在命令行解析器中注册)。当然他们没有注册“不稳定”分支中的解析器，它们也没有在解析器中注册在包含优化扩展的“opt”分支中。根据你的帖子，我几乎想“修复”这个问题，但我现在不确定为什么它会有用，因为该解析器无法使用这些扩展。Z3 有其他扩展也没有为 SMT-LIB2 解析器公开。所以现在，我倾向于让 API 公开的解析器只接受正确的 SMT-LIB2。

请注意，Christoph 指出优化功能只是“opt”分支的一部分。欢迎您尝试一下，但它仍然有很多问题。 API就我而言有关“功能完整”(回答(1))。您可以在 Python、Java 和 .NET 中使用它。 OCaml 集成正在等待对 OCaml API 的其他更改。我没有机会为 API 提供任何详尽的文档，但在 http://rise4fun.com/Z3/tutorial/optimization 上有一个关于 SMT-LIB 扩展的简短教程。 .