Z3最大化C ++ [英] Z3 Maximize in C++

问题描述

在Z3，下面是明确评估，以最多2，与模型X =真和y =真。

In Z3, the following is clearly evaluated to a maximum of 2, with the model x=true and 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？我已经使用这个简单的尝试解析：

How could I implement this using the C/C++ APIs? I've tried simply parsing using this:

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);

但它打印不受支持\\ N;最大限度地

我不介意手动构建前pression - 而不是使用一个构造的文件。我根本不知道要使用为其EXPR函数或运算符最大化

I wouldn't mind constructing the expression manually - rather than using a constructed file. I simply didn't know which expr functions or operators to use for "maximize".

附录：
在最近的一些解答和讨论来看，它似乎非常清楚，我请求是不是在目前正常功能。于是，我改变的问题，要求的一种方式，使这项工作的具体细节情况来看的时刻。

ADDENDUM: In light of some recent answers and discussions, it seems clear that what I am requesting is not normal functionality at the moment. So, I alter the question to ask for the specific details of a way to make this work as things stand at the moment.

推荐答案

感谢您指出了这个问题。优化功能不是SMT-LIB2的一部分。他们是自定义扩展。此外，该分析SMT-LIB2基准的功能没有任何办法
反射回来优化编译指示。为什么API解析器不承认的理由
这些扩展的是，优化功能不与解析器注册
（它们与命令行解析器注册）。当然，他们不会与注册
在不稳定分支解析器，并且它们也没有与分析器注册
在包含优化扩展的选择分支。
我几乎想修理这个，根据您的文章，但我现在不能确定
为什么自认为解析器没有使用这些扩展的方式，将是有益的。
Z3具有还没有暴露的SMT-LIB2解析器其他扩展。
所以现在，我倾向于保持在API暴露解析器只接受适当的SMT-LIB2。

Thanks for pointing out this issue. The optimization features are not part of SMT-LIB2. They are custom extensions. Also, the function that parses SMT-LIB2 benchmarks does not have any way to reflect back the optimization pragmas. The reason why the API parser does not recognize these extensions is that the optimization features are not registered with that parser (they are registered with the command-line parser). Of course they are not registered with the parser in the "unstable" branch, and they are also not registered with the parser in the "opt" branch that contains the optimization extensions. I was almost tempted to "fix" this, based on your post, but I am now not sure why it would be useful since that parser has no way of using those extensions. Z3 has other extensions that are also not exposed for the SMT-LIB2 parser. So for now, I am inclined to keep the parser exposed by the API to only accept proper SMT-LIB2.

需要注意的是克里斯托夫指出，优化功能只是一个选择分支的一部分。
欢迎您来尝试一下，但它仍然搅动了不少。该API是尽可能我
关注功能齐全（回答（1））。你可以在Python，Java和.NET使用它。 OCaml的整合正在等待其他变化OCaml中的API。我还没有机会以提供API的大量文件，但上的 http://rise4fun.com/Z3/tutorial/optimization 。

Note that Christoph points out that the optimization features are only part of an "opt" branch. You are welcome to try it out, but it is still churning quite a bit. The API is as far as I am concerned "feature complete" (to answer (1)). You can use it from Python, Java and .NET. The OCaml integration is pending other changes to OCaml APIs. I have not had an opportunity to provide any extensive documentation for the APIs, but there is a short tutorial for the SMT-LIB extensions on http://rise4fun.com/Z3/tutorial/optimization.

这篇关于Z3最大化C ++的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！