IntX.hs

{-# LANGUAGE DeriveAnyClass  #-}
{-# LANGUAGE DeriveGeneric   #-}
{-# LANGUAGE NamedFieldPuns  #-}

import Data.SBV
import Data.SBV.Control
import GHC.Generics (Generic)

data SIntX = SIntX { isInf :: SBool
                   , xVal  :: SInteger
                   }
                   deriving (Generic, Mergeable)

instance Show SIntX where
  show (SIntX inf val) = case (unliteral inf, unliteral val) of
                           (Just True,  _)      -> "oo"
                           (Just False, Just n) -> show n
                           _                    -> "<symbolic>"

inf :: SIntX
inf = SIntX { isInf = true, xVal = 0 }

nat :: SInteger -> SIntX
nat v = SIntX { isInf = false, xVal = v }

liftU :: (SInteger -> SInteger) -> SIntX -> SIntX
liftU op a = ite (isInf a) inf (nat (op (xVal a)))

liftB :: (SInteger -> SInteger -> SInteger) -> SIntX -> SIntX -> SIntX
liftB op a b = ite (isInf a ||| isInf b) inf (nat (xVal a `op` xVal b))

instance Num SIntX where
  (+)         = liftB (+)
  (*)         = liftB (*)
  negate      = liftU negate
  abs         = liftU abs
  signum      = liftU signum
  fromInteger = nat . literal

instance EqSymbolic SIntX where
  a .== b = ite (isInf a &&& isInf b) true
          $ ite (isInf a ||| isInf b) false
          $ xVal a .== xVal b

freeSIntX :: String -> Symbolic SIntX
freeSIntX nm = do i <- sBool    $ nm ++ "_isInf"
                  v <- sInteger $ nm ++ "_xVal"
                  return $ SIntX { isInf = i, xVal = v }

ex1 :: IO SatResult
ex1 = sat $ do x <- freeSIntX "x"
               return $ x .== x+1

data IntX = IntX (Maybe Integer) deriving Show

queryX :: SIntX -> Query IntX
queryX (SIntX {isInf, xVal}) = do
          b <- getValue isInf
          v <- getValue xVal
          return $ IntX $ if b then Nothing
                               else Just v

ex2 :: IO ()
ex2 = runSMT $ do x <- freeSIntX "x"
                  constrain $ x .== x+1

                  query $ do cs <- checkSat
                             case cs of
                               Unk   -> error "Solver said Unknown!"
                               Unsat -> error "Solver said Unsatisfiable!"
                               Sat   -> do v <- queryX x
                                           io $ print v