问题标签 [sbv]

我正在尝试用SBV解决算术问题。

例如

虽然我可以做有用的事情，但我更容易使用纯值（SatResult 或 Bool）而不是 IO monad。

根据文档

鉴于我使用的函数类型，我理解为什么我总是使用 IO monad。

但是查看函数的通用版本，例如 sFloats。

根据函数的类型，我可以使用与 IO 不同的 monad。这给了我希望，我们将获得一个更有用的 monad，例如 Identity monad。

不幸的是，查看示例总是可以解决 IO monad 中的问题，所以我找不到任何适合我的示例。此外，我没有太多使用 monad 的经验。

最后我的问题是：

在用 SBV 解决此类问题时，有什么方法可以避免 IO monad？

提前致谢

我正在将 SQL 谓词翻译成 Z3 语言。SQL 谓词表达式与 Z3 中的表达式非常接近：

但我看不到如何表示 Null 值。在裸 Z3 中，我可以定义数据类型：

SBV 没有声明数据类型。

我想到的第一个选择是将所有x引用替换为x + 1thenx = 0可以被视为null