将SQL谓词转换为Z3时SBV公式表示Null值的适用模式是什么？

你最初想到的用特殊值标记Null的方案存在值域冲突问题：如果业务逻辑中x本身就可以等于你预留的Null标记值（比如你用的0），会出现语义错误。SBV生态中最通用、无冲突的可空值表示模式如下：

方案：值+布尔标记成对声明 #

对每个可空字段，同时声明两个变量：

• 一个和字段类型一致的值变量，存储非Null状态下的实际值
• 一个布尔类型的标记变量，标记当前字段是否为Null

示例1：实现 where x is null or x > 10 逻辑 #

对应的SBV（Haskell接口）代码如下：

-- 声明可空字段x的两个关联变量
x_val <- sInt32 "x_val"
x_null <- sBool "x_null"

-- 对应SQL谓词的断言
constraint = x_null .|| (x_val .> 10)
constrain constraint

示例2：实现 where x + y > 0 逻辑（x、y均为可空Int） #

SQL中任意操作数为Null时，运算结果为UNKNOWN，WHERE子句中UNKNOWN等同于不满足条件，对应实现：

x_val <- sInt32 "x_val"
x_null <- sBool "x_null"
y_val <- sInt32 "y_val"
y_null <- sBool "y_null"

constraint = sNot x_null .&& sNot y_null .&& (x_val + y_val .> 0)
constrain constraint

方案优势 #

1. 完全不压缩原始类型的值域，不会出现业务值和Null标记冲突的问题
2. 天然对齐SQL的三值逻辑判断规则，所有Null相关的语义都可以通过布尔标记直接实现
3. 支持任意可空类型（Int、字符串、浮点数等），不需要针对不同类型调整标记值

内容的提问来源于stack exchange，提问作者Daniil Iaitskov