用什么模式表示SBV公式中的零值？

Question

我正在将SQL谓词转换为Z3语言。SQL谓词表达式非常接近于Z3中的表达式：

where x + y > 0
====
(declare-const x Int)
(declare-const y Int)
(assert (> (+ x y) 0)))

但我看不出如何表示空值。在裸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