Z3 Maximize in C++

Z3 Maximize in C++

本文关键字：C++ in Maximize Z3      更新时间：2023-10-16

在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 "

我不介意手工构造表达式——而不是使用构造好的文件。我只是不知道用哪个expr函数或运算符来表示"maximize"。

附录:根据最近的一些回答和讨论，很明显，我所要求的目前不是正常的功能。所以，我改变了这个问题，询问具体的细节，以实现目前的情况。

感谢您指出这个问题。优化特性不是SMT-LIB2的一部分。它们是自定义扩展。此外，解析SMT-LIB2基准测试的函数没有任何方法以反映优化pragmas。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扩展的简短教程。

Z3中的优化特性在' opt'分支中进行了大量构建，并没有与不稳定分支或主分支集成。很有可能还没有将所有的功能添加到API中。参见Nikolaj对这些问题的回答:

在Z3中编码"最多k/至少k个布尔值为真"约束

相关文章：