如何检查symTake的UnionM类型结果是否等于具体列表？

我想检查symTake返回的UnionM [SymInteger]类型的result是否能等于[1, 2]。我可以直接检查普通符号整数列表和[1,2]的相等性，比如：

x :: SymInteger
x = "x"

y :: SymInteger
y = "y"

main :: IO ()
main = do
    print $ [x, y] .== [1, 2]

但不知道怎么对UnionM里的列表做同样的操作，而且文档说明不能直接拆箱UnionM中的内容。我的目标代码如下：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}

import Grisette

x :: SymInteger
x = "x"

y :: SymInteger
y = "y"

numbers :: [SymInteger]
numbers = [x, y]

n :: SymInteger
n = "n"

result :: UnionM [SymInteger]
result = symTake n numbers

main :: IO ()
main = do
    print $ result .== [1, 2] -- 此处会因类型不匹配报错

解决方案 #

要检查UnionM包裹的列表是否能等于目标列表，核心思路是遍历UnionM的所有分支，分别判断每个分支的列表与目标列表的相等性，再合并这些条件并检查是否存在可满足的情况。

可以通过以下两种方式实现：

方法1：使用fmap + merge + isSatisfiable

main :: IO ()
main = do
  -- 给UnionM的每个分支列表做相等性判断，得到UnionM SymBool
  let branchConds = fmap (.== [1, 2]) result
  -- 合并所有分支的条件，得到表示"是否存在分支满足相等"的SymBool
  let overallCond = merge branchConds
  -- 检查该条件是否可满足
  print $ isSatisfiable overallCond

方法2：使用unionWith简化代码

unionWith可以直接将UnionM a转换为UnionM b，这里用它直接生成每个分支的相等条件，再合并检查：

main :: IO ()
main = do
  let overallCond = unionWith (\lst -> lst .== [1, 2]) result
  print $ isSatisfiable $ merge overallCond

原理说明 #

• symTake返回的UnionM [SymInteger]是符号执行中的分支集合，每个分支对应n取不同值时的take结果（比如n≤0时取空列表，n=1时取[x]，n≥2时取[x,y]）。
• 不能直接用.==比较UnionM [SymInteger]和[SymInteger]，因为类型不匹配。必须先对每个分支单独做相等判断，再通过merge将分支条件合并为一个全局的符号布尔值，最后用isSatisfiable验证是否存在变量取值让条件成立。

内容的提问来源于stack exchange，提问作者Stefanos Baziotis