什么模式适合在 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 + 1 然后 x = 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

什么模式适合在 SBV 公式中表达 Null 值

What pattern is suitable for expressing Null value in a SBV formula

haskell

sbv