【发布时间】：2014-08-25 08:18:36
【问题描述】：
在 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 函数或运算符。
附录： 根据最近的一些答案和讨论，我现在要求的似乎不是正常的功能。所以，我改变了这个问题，询问目前情况的具体细节。
【问题讨论】：
-
替代方案：MS是否提供Z3的源代码？如果是这样，您可以调试正确解析和评估的第一种方法。
-
我不确定他们是否这样做。不过我确实知道我的示例适用于他们的网站。
-
我明白了，但我并没有真正理解你的意思。你到底在暗示什么？
-
抓住源头。构建、运行和调试您的代码。您可以在令牌解析器使用
maximize时进行调试，并检查它为什么会在 "unsupported ..." 上阻塞。您将看到失败的情况，您可能会获得一些见解。或者，您可以浏览源代码并检查maximize需要什么内部表示以及如何重新格式化您的代码。