SymVal instance for Data.Complex

[arrowd]

Hello. Is there any reason for not having an instance SymVal (Complex a) given some sane constaints on a?

[LeventErkok]

There's no reason why this cannot be done. You can do it in user-space as well, there's no need for supporting this directly in SBV.

I try to put things into SBV if there's a direct corresponding type in SMTLib so we can take advantage of the corresponding logic. Since there's no complex-number theory in SMTLib, there's no point to really support this at the library level. Users can implement this using regular Haskell programming. (I'd start with a simple tuple, or maybe a datatype, containing two symbolic fields, make it an instance of Num and go from there.)

Let me know if you try this and run into issues.

[arrowd]

Complex type is already defined in base, that's why I thought there might be sense to have an instance for it in SBV.

Ok then, I'll do it on my side.

[arrowd]

Sorry for bumping this, but I'm a bit obscured how to write this instance. Instances for Maybe a and (a, b) use internal stuff, which is accessible only within SBV itself.

Specifically, I'm speaking of toCV and mkCVTup used to implement literal.

[LeventErkok]

If what you want are symbolic tuples and symbolic Maybe, SBV already supports those out-of-the box:

STuple: https://hackage.haskell.org/package/sbv-8.6/docs/Data-SBV-Tuple.html SMaybe: https://hackage.haskell.org/package/sbv-8.6/docs/Data-SBV-Maybe.html

Here's a simple tuple example: https://hackage.haskell.org/package/sbv-8.6/docs/src/Documentation.SBV.Examples.Misc.Tuple.html#example

You should be able to model your complex numbers directly on top of an STuple, by doing the proper Num class instantiations. Give that a try and let me know how it goes!

[arrowd]

So, you propose not using Data.Complex at all and use (a, a) instead?

[LeventErkok]

You can really do this in many different ways. I took a look at Data.Complex and looks like they are using RealFloat instances. That would pose some difficulties since RealFloat is a class with many methods that wouldn't make sense for a symbolic value. (Like exponent etc.) But you can use it and ignore the methods that you can't implement and substitute symbolic versions with slightly different names when you can.

But I'd much rather go with a simpler implementation, adding facilities as you need. Something like:

{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE ScopedTypeVariables  #-}

import Data.SBV
import Data.SBV.Control

data Complex a = a :+ a deriving Show
infix 6 :+

type SComplex a = Complex (SBV a)

instance Num a => Num (Complex a) where
    (x :+ y) + (x' :+ y') = (x+x')      :+ (y+y')
    (x :+ y) - (x' :+ y') = (x-x')      :+ (y-y')
    (x :+ y) * (x' :+ y') = (x*x'-y*y') :+ (x*y'+y*x')
    negate (x:+y)         = negate x :+ negate y
    abs _                 = error "SComplex.abs: TODO"
    signum _              = error "SComplex.signum: TODO"
    fromInteger n         = fromInteger n :+ 0

instance EqSymbolic (SComplex a) where
   a :+ b .== c :+ d = a .== c .&& b .== d

sComplex :: SymVal a => String -> Symbolic (SComplex a)
sComplex nm = do r <- free $ "nm" ++ "_real"
                 i <- free $ "nm" ++ "_imag"
                 pure $ r :+ i

getComplex :: SMTValue a => SComplex a -> Query (Complex a)
getComplex (r :+ i) = do rp <- getValue r
                         ip <- getValue i
                         pure $ rp :+ ip

test :: IO ()
test = runSMT $ do x :: SComplex Int32 <- sComplex "x"
                   y :: SComplex Int32 <- sComplex "y"

                   constrain $ x + 2 * y .== 2 * x + y + 3

                   query $ do cs <- checkSat
                              case cs of
                                Sat -> do xv <- getComplex x
                                          yv <- getComplex y
                                          io $ print xv
                                          io $ print yv
                                _  -> error $ "Solver said: " ++ show cs

When I run this, I get:

*Main> test
0 :+ 0
3 :+ 0

which isn't particularly exciting but should get you started.

You can then add OrdSymbolic instance, etc., as you need more and more features. Note that I also left abs/signum methods unimplemented, because they aren't easy to do in a symbolic context (you'd need access to square roots.) All of that can be done with some caveats, but of course it's best to implement as much as you actually need and take it from there.

Hope this gets you started. Let me know if you run into other issues.

[arrowd]

Right, I got fixed on SymVal instance for some reason, while to use .== you don't really need it. Thanks for sample code.