[SOLVED] Combining Tuples in SBV?

Combining Tuples in SBV?

Basically I'm wondering, is there any way to write a function of the following type with the SBV library:

(SBV a, SBV b) -> SBV (a,b)

This seems like it should be possible: if we have two symbolic values, we can make a new symbolic value, as a concrete pair whose elements are either the symbolic or concrete values of the two inputs. But I can't find anything like this, and the SBV type does not have its constructors exposed.

Is this possible?

Solution

Sounds like you need the tuple function. Here's an example:

import Data.SBV
import Data.SBV.Tuple

tup :: (SymVal a, SymVal b) => (SBV a, SBV b) -> SBV (a, b)
tup = tuple

tst :: Predicate
tst = do x <- sInteger "x"
         y <- sInteger "y"
         z <- sTuple "xy"

         return $ tup (x, y) .== z

Of course, tuple itself can handle arity upto 8; the above is just one instantiation at the exact type you wanted. We have:

$ ghci a.hs
GHCi, version 8.6.4: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( a.hs, interpreted )
Ok, one module loaded.
*Main> sat tst
Satisfiable. Model:
  x  =     0 :: Integer
  y  =     1 :: Integer
  xy = (0,1) :: (Integer, Integer)

There's also the untuple function that goes in the other direction. They are both in the Data.SBV.Tuple module that you have to explicitly import. (You can also find lens-like accessors in the same module, which lets you write, ^._1, ^._2 etc. to extract fields of tuples; as in z^._2 for the above example.)