LeventErkok

import Data.SBV
import Data.SBV.Dynamic
import Data.SBV.Control
import Data.SBV.Internals

import Control.Monad.Reader (ask)

reachableCond :: SVal -> Symbolic SVal
reachableCond cond = do
  st <- ask

LeventErkok

{-# LANGUAGE OverloadedLists #-}

import Data.SBV
import Data.SBV.List ((.++), (.:))
import qualified Data.SBV.List as L

import Data.Typeable

lcase :: (Typeable a, SymWord a, Mergeable b) => SList a -> b -> (SBV a -> SList a -> b) -> b
lcase s e c = ite (L.null s) e (c (L.head s) (L.tail s))

LeventErkok

import Data.SBV

leftAppend :: SInteger -> SInteger -> SInteger
leftAppend k n = ite (n .< 10       ) (n + k *10)
               $ ite (n .< 100      ) (n + k *100)
               $ ite (n .< 1000     ) (n + k * 1000)
               $ ite (n .< 10000    ) (n + k * 10000)
               $ ite (n .< 100000   ) (n + k * 100000)
               $ ite (n .< 1000000  ) (n + k * 1000000)
               $ ite (n .< 10000000 ) (n + k * 10000000)

LeventErkok

import Control.Monad.Trans  (liftIO)
import Control.Monad.Reader (ask)

import Data.SBV.Dynamic

--------------------------------------------------------------------------------
-- I should really export the following four definitions from SBV.Dynamic
mkWordN :: Int -> String -> Symbolic SVal
mkWordN w nm = ask >>= liftIO . svMkSymVar Nothing (KBounded False w) (Just nm)

LeventErkok

import Data.SBV

hamiltonian :: Int -> [(Integer, Integer)] -> IO (Maybe [Integer])
hamiltonian n edges = extractModel `fmap` satWith z3 hcycle
  where isEdge p = bAny (.== p) [(literal x, literal y) | (x, y) <- edges]
        validNodes xs = allDifferent xs &&& bAll (\x -> x .>= 0 &&& x .< fromIntegral n) xs
        validEdges xs = bAll isEdge $ zip xs (tail xs ++ [head xs])
        hcycle = do order <- mkFreeVars n
                    return $ validNodes order &&& validEdges order

LeventErkok

import Data.SBV
import Data.List (zip4)

import qualified Data.Map as M

data MyTestData = TD0 Bool
                | TD1 Integer
                | TD2 Word32
                deriving Show

LeventErkok

import Data.SBV

p :: Goal
p = do a  <- sInteger "a"
       b  <- sInteger "b"
       ab <- sInteger "ab"

       constrain $ a*a - b*b .== 21
       constrain $ a*a + b*b .== 29

LeventErkok

import Data.SBV

p :: Bool -> Predicate
p bug = do
    a <- sInteger "a"
    b <- sInteger "b"

    -- We'll do our proof with a two-level case split. First on 'a', then on 'b'
    -- The conditions are rather arbitrary for illustrative examples here. But they
    -- are arbitrary SBool's, so you can code anything you want.

LeventErkok

stgEqType: unequal                                                                                                                                                  
  ((State                                                                                                                                                           
    -> Exp -> State# RealWorld -> (# State# RealWorld, State #)) :: *)                                                                                              
  ~R#                                                                                                                                                               
  ((State -> Exp -> IO State) :: *)                                                                                                                                 
  (() :: *) ~# (() :: *)                                                                                                                                            
ghc: panic! (the 'impossible' happ

LeventErkok

{-# LANGUAGE DeriveAnyClass     #-}
{-# LANGUAGE DeriveDataTypeable #-}

module Check where

import Data.SBV
import Data.Generics

-- One of three states we can be in
data State  = S0 | S1 | S2 deriving (Eq, Ord, Show, Read, Data, SymWord, HasKind)