sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Joel Burget Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Documentation.SBV.Examples.Misc.Tuple

Description

A basic tuple use case, also demonstrating regular expressions, strings, etc. This is a basic template for getting SBV to produce valid data for applications that require inputs that satisfy arbitrary criteria.

Synopsis

- type Dict a b = SBV [(a, b)]
- example :: IO [(String, Integer)]

# Documentation

type Dict a b = SBV [(a, b)] Source #

A dictionary is a list of lookup values. Note that we store the type `[(a, b)]` as a symbolic value here, mixing sequences and tuples.

example :: IO [(String, Integer)] Source #

Create a dictionary of length 5, such that each element has an string key and each value is the length of the key. We impose a few more constraints to make the output interesting. For instance, you might get:

     ghci> example
     [("nt_",3),("dHAk",4),("kzkk0",5),("mZxs9s",6),("c32'dPM",7)]

Depending on your version of z3, a different answer might be provided. Here, we check that it satisfies our length conditions:

    >>> import Data.List (genericLength)
    >>> example >>= \ex -> return (length ex == 5 && all (\(l, i) -> genericLength l == i) ex)
    True