Skip to content

Instantly share code, notes, and snippets.

@LeventErkok
Created November 23, 2018 15:56
Show Gist options
  • Save LeventErkok/facfd067b813028390c89803b3a0e887 to your computer and use it in GitHub Desktop.
Save LeventErkok/facfd067b813028390c89803b3a0e887 to your computer and use it in GitHub Desktop.
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment