I am translating SQL predicate into Z3 language. SQL predicate expression is very close to expressions in Z3:
where x y > 0
====
(declare-const x Int)
(declare-const y Int)
(assert (> ( x y) 0)))
but I don't see how to represent Null values. In bare Z3 I can define datatype:
(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 doesn't have declare-datatype.
First option which comes to my head is to replace all x
references
with x 1
then x = 0
could be treated as null
CodePudding user response:
SBV has full support for optional values, modeling the Maybe
datatype:
https://hackage.haskell.org/package/sbv-8.16/docs/Data-SBV-Maybe.html
So, I'd go by modeling it as you would in regular Haskell, i.e., via a Maybe Integer
; or in SBV parlance, its symbolic equivalent SMaybe Integer
. That should be a very direct correspondence. Here's an example use:
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