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
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 equivalentSMaybe Integer
. That should be a very direct correspondence. Here's an example use: