search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
239 stars 33 forks source link

Tables/arrays in lambdas #675

Closed LeventErkok closed 9 months ago

LeventErkok commented 9 months ago

Some examples that are problematic, though we do need some level of support for arrays in lambdas. (See Documentation.SBV.Examples.Misc.LambdaArray for the use case we need to support.)

Given:

foo :: SInteger -> SWord32
foo = smtFunction "foo" (\x -> select [1,2,3] 0 x)

Try:

satWith z3{verbose=True} $ \x -> foo x .== 2

Also:

sbv2smt (smtFunction "foo" (\x -> x + readArray (writeArray (lambdaAsArray (\q -> q::SInteger)) 1 2) 1))

and

sbv2smt (smtFunction "foo" (\(x :: SArray Integer Integer) -> readArray (writeArray x 1 2) 1))

and

putStrLn =<< sbv2smt (smtFunction "foo" (\x -> select [1] (0 :: SInteger) (x::SInteger)))