Z3 运行的异常 Data.SBV 的最小化示例答案

【问题标题】：Exception from Z3 running minimize example for Data.SBVZ3 运行的异常 Data.SBV 的最小化示例
【发布时间】：2017-09-20 03:30:44
【问题描述】：

在为 Haskell 运行 example for the optimize function in the Data.SBV library 时：

problem :: Goal
problem = optimize Lexicographic $  do [x1, x2] <- mapM sReal ["x1", "x2"]

         constrain $ x1 + x2 .<= 10
         constrain $ x1 - x2 .>= 3
         constrain $ 5*x1 + 4*x2 .<= 35
         constrain $ x1 .>= 0
         constrain $ x2 .>= 0

         maximize "goal" $ 5 * x1 + 6 * x2
main = optimize Lexicographic problem

我收到以下错误：

*** Exception: 
*** Data.SBV: Unexpected response from the solver.
***    Context : set-option
***    Sent    : (set-option :pp.decimal false)
***    Expected: success
***    Received: unsupported
***              success

CallStack (from HasCallStack):
  error, called at ./Data/SBV/Control/Utils.hs:590:9 in sbv-7.3-35rX062AGHeFmuyHxSBaTE:Data.SBV.Control.Utils

类似下面的代码：

test = optimize Lexicographic $ do
                  x <- sInteger "x"
                  y <- sInteger "y"
                  maximize "goal" $ x + 2 * y

产生错误：

*** Exception: 
*** Data.SBV: Unexpected response from the solver.
***    Context : getModel
***    Sent    : (get-value (s0))
***    Expected: a value binding for kind: SInteger
***    Received: unsupported
***              ((s0 0))

CallStack (from HasCallStack):
  error, called at ./Data/SBV/Control/Utils.hs:590:9 in sbv-7.3-35rX062AGHeFmuyHxSBaTE:Data.SBV.Control.Utils

minimize 组合子作为最后一个表达式也会发生此错误。

我正在使用 GHC 版本 8.0.2 和堆栈版本 1.5 和 SBV 版本 7.3 我使用 Z3 作为求解器，它是在 MacOS 上运行的 4.5.1 64 位版本。

调用sat 和prove 可以正常工作。有任何想法吗？谢谢！

【问题讨论】：

标签： haskell z3 sbv

【解决方案1】：

您很可能使用的是旧版本的 Z3。 SBV 中的优化功能依赖于 Z3 的一些尚未正式发布的功能。你能从这里下载一个吗：

https://github.com/Z3Prover/bin/tree/master/nightly

试试看？

（对于 Z3 有一个开放的票证可以针对这个问题发布一个新版本，但不清楚他们什么时候会解决这个问题：https://github.com/Z3Prover/z3/issues/1231）

【讨论】：

谢谢，我试试看！