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!
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