我正在將 SQL 謂詞翻譯成 Z3 語言。SQL 謂詞運算式非常接近 Z3 中的運算式：
where x y > 0
====
(declare-const x Int)
(declare-const y Int)
(assert (> ( x y) 0)))
但我不知道如何表示 Null 值。在裸 Z3 中，我可以定義資料型別：
(declare-datatype
NullableInt
(
(justInt (theInt Int))
(nullInt)
)
)
# where x is null or x > 10
(declare-const x NullableInt)
(assert (ite (= x nullInt) true (> (justInt x) 10)))
SBV 沒有宣告資料型別。
我想到的第一個選項是將所有x參考替換為x 1thenx = 0可以被視為null
uj5u.com熱心網友回復：
SBV 完全支持可選值，對Maybe資料型別進行建模：
https://hackage.haskell.org/package/sbv-8.16/docs/Data-SBV-Maybe.html
所以，我會像在常規 Haskell 中那樣對其進行建模，即通過Maybe Integer; 或者用 SBV 的說法，它的符號等價物SMaybe Integer。那應該是非常直接的通信。這是一個使用示例：
ghci> import Data.SBV
ghci> import qualified Data.SBV.Maybe as SM
ghci> sat $ \mi -> SM.maybe sTrue (.>= 10) mi
Satisfiable. Model:
s0 = Nothing :: Maybe Integer
ghci> sat $ \mi -> SM.maybe sFalse (.>= 10) mi
Satisfiable. Model:
s0 = Just 10 :: Maybe Integer
轉載請註明出處，本文鏈接：https://www.uj5u.com/gongcheng/316868.html
下一篇：為什么這個定點計算不停止？