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

Question

我看到许多使用SBV库的例子如下：

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

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

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

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

谢谢!

Answer 1

函数字面量应该这样做。但是，您可能需要更清楚地说明类型，例如Integer、Int8、Int16等，而不仅仅是Int。

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

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