Search code examples
haskelltypesz3sbv

Turning Haskell Int values into Constants for SBV constraints

I see lots of examples of the SBV library being used like so:

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

For a function that takes in a Haskell Int, I would like to use that Int in my constraint formulas being passed to Z3 via the Data.SBV library:

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

How can I convert from a Haskell Int to an SInteger or some appropriate instance of OrdSymbolic and EqSymbolic to be used with (.<) and (.==)?

Thanks!

Solution

  • The function literal should do it. You'll probably have to be more clear on the type though, such as Integer, Int8, Int16 etc. instead of just Int.

    You can also just do fromIntegral, since numeric symbolic types are instances of the Num class:

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