4

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!

Matt Ahrens
  • 129
  • 7

1 Answers1

5

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
alias
  • 28,120
  • 2
  • 23
  • 40
  • Really? It has the type `SymWord a => a -> SBV a`, and I don't see a `SymWord Integer` instance. – Cirdec Sep 20 '17 at 17:00
  • Nevermind, there must be. There's a [`SIntegral Integer`](https://hackage.haskell.org/package/sbv-7.3/docs/Data-SBV.html#t:SIntegral) instance. – Cirdec Sep 20 '17 at 17:03
  • @Cirdec is right. It's important to be clear about the precise type; You can use `IntN` or `WordN` for `N=8,16,32,64`, or just `Integer`; whichever fits your purpose. – alias Sep 20 '17 at 17:07