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

函数literal应该这样做。不过，您可能需要更清楚地了解类型，例如 Integer , Int8 , Int16等等，而不仅仅是 Int .

你也可以做 fromIntegral ，因为数字符号类型是 Num 的实例类(class):

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