例外Data.SBV

Question

ための例を最小：

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 

Iが得る次のエラー：

*** 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コンビネータでも発生します。

スタックバージョン1.5とSBVバージョン7.3のGHCバージョン8.0.2を使用しています 私はソルバーとしてZ3を使用していますが、これはMacOS上で動作するバージョン4.5.1の64ビットです。

satとproveを期待通りに呼び出す。何か案は？ありがとう！

Answer 1

ほとんどの場合、古いバージョンのZ3を使用しています。 SBVの最適化機能は、まだ公式にリリースされていないZ3の機能に依存しています。

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

をし、それを試してみる：あなたはここからダウンロードできますか？

（そこまさにこの問題のために新しいリリースを持っているZ3のためのオープンチケットだが、彼らはそれを周りに買ってあげるとき、それは明らかではない。https://github.com/Z3Prover/z3/issues/1231）