将 Haskell Int 值转换为 SBV 约束的常量

Question

我看到很多使用 SBV 库的示例，如下所示：

f :: IO SatResult
f = sat $ do
      x <- sInteger "x"
      constraint $ x .< 200

对于接受 Haskell Int 的函数，我想在通过 Data.SBV 库传递给 Z3 的约束公式中使用该 Int：

f :: Int -> IO SatResult
f i = sat $ do
          x <- sInteger "x"
          constraint $ x .< (g i)
        where
          g = ???

如何从 Haskell Int 转换为 SInteger 或 OrdSymbolic 和 EqSymbolic 的一些适当实例以与 (.<) 和 (.==) 一起使用？

谢谢！

Answer 1

函数文字应该这样做。你可能有要的类型，虽然更加清晰，如Integer，Int8，Int16等等，而不是只Int。

你也可以只做fromIntegral，因为数字符号类型是Num类的实例：

Prelude Data.SBV> (fromIntegral (2::Int)) :: SInteger
2 :: SInteger