haskell - 什么模式适合在 SBV 公式中表示 Null 值

Question

我正在将 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

Answer 1

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