haskell - 将 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