Исключение из Z3 работает пример минимизации для Data.SBV

Question

При запуске примера для функции оптимизации в библиотеке Data.SBV для Haskell:

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 в качестве решателя, и это версия 4.5.1, 64-разрядная, работающая на MacOS.

призвание sat а также prove работать как положено. Есть идеи? Спасибо!

Answer 1

Скорее всего, вы используете старую версию Z3. Функции оптимизации в SBV опираются на некоторые, еще не официально выпущенные функции Z3. Вы можете скачать один из здесь:

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

и попробовать?

(Есть открытый билет для Z3, чтобы иметь новую версию именно для этой проблемы, но неясно, когда они обойдут ее: https://github.com/Z3Prover/z3/issues/1231)