Z3在C++中最大化

在Z3中，通过模型x = true和y = true，可以清楚地评估以下最大值为2。Z3在C++中最大化

(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”。

附录：鉴于最近的一些答案和讨论，似乎很清楚，我所要求的并不是正常的功能。因此，我改变了这个问题，要求提供一个方法的具体细节，以便目前的工作成为现实。

来源

2014-07-04 d' alar' cop

替代方法：MS是否提供Z3的源代码？如果是这样，你可以调试正确解析和评估的第一种方法。 – Samuel

我不确定他们这么做。不过，我知道我的例子在他们的网站上运行。 –

http://z3.codeplex.com/SourceControl/latest#README – Samuel

感谢您指出这个问题。优化功能不是SMT-LIB2的一部分。他们是自定义扩展。此外，解析SMT-LIB2基准的函数没有任何方法可以反映优化编译指示。 API解析器无法识别这些扩展的原因是，优化功能未在该解析器中注册（它们使用命令行解析器注册）。当然，它们未在“unstable”分支中注册为解析器，并且它们也未在包含优化扩展的“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扩展的简短教程。

来源

2014-07-06 15:26:42

Z3中的优化特性在`opt'分支中处于沉重构造之下，并未与不稳定或主分支集成在一起。很有可能并非所有功能都已添加到API中。又见尼古拉的这些问题的答案：

Encoding “at-most-k/at-least-k booleans are true” constraints in Z3

Simplex in z3 via for-all

来源

2014-07-04 10:36:49

谢谢。几个问题。 1）你说“这很可能......”有什么方法可以让我们更确定这一点吗？ 2）我们可以在家里建立和使用这个'opt'分支吗（顺便说一下，最近的提交并不是最近的那些）？ 3）那么有什么方法可以使用任何语言或任何平台（Windows/Linux）使问题中显示的Z3输入在使用网站之外运行？ Millionen Dank –

嗨，我刚刚下载并尝试'opti'分支。命令行Z3仍然没有选择“最大化”条件。在代码里面，我看到一些看起来很神秘的函数，名字如“z3_check_opti”。我认为这些都与这个问题有关，但我真的不太清楚如何利用这个问题。你有什么想法？ –

1）是的。 2）是的。 3）是，但不方便。有些事情需要超过一周才能实施。 –

Z3在C++中最大化

回答

相关问题