LeventErkok

import Data.SBV

shiftLeft :: SWord32 -> SWord32 -> SWord32
shiftLeft = cgUninterpret "SBV_SHIFTLEFT" cCode hCode
  where cCode = ["#define SBV_SHIFTLEFT(x, y) ((x) << (y))"]
        hCode x y = select [x * literal (bit b) | b <- [0.. bitSize x - 1]] (literal 0) y

tstShiftLeft ::  SWord32 -> SWord32 -> SWord32 -> SWord32
tstShiftLeft x y z = x `shiftLeft` z + y `shiftLeft` z

LeventErkok

{-# LANGUAGE ScopedTypeVariables #-}

import Data.SBV

-- you can have arbitrary number of constrain/pConstrain's.. Of course, if they
-- are *hard to satisfy*, then generating tests can take a loong time. The algorithm
-- simply makes up random cases and runs the code to see if constraints are satisfied;
-- if not it tries again. So, with hard constraints, this process can take long. In
-- particular, consider "constrain false", :-)
code = do t <- free_

LeventErkok

import Data.SBV
import Data.List (partition)

sumSplit :: [Integer] -> IO (Maybe (Integer, [Integer], [Integer]))
sumSplit xs = do r <- satWith z3 $ do zs <- mkFreeVars (length xs)
                                      let sums sofar []            = sofar
                                          sums (i,o) ((f, v):rest) = sums (ite f (i+v, o) (i, o+v)) rest
                                          (f, s) = sums (0, 0) $ zip zs (map literal xs)
                                      return $ f .== s
                 case getModel r of

LeventErkok

function! OpenHaskellFile()
  let f = tr(matchstr(getline(line('.')), '\(import\s*qualified\|import\)\s*\zs[A-Za-z0-9.]\+'), ".", "/") . ".hs"
  if f == ".hs"
     echohl ErrorMsg
     echo "Not on a valid import line!"
     echohl NONE
     return
  endif
  if filereadable(f)
     if (&modified)

LeventErkok

import Data.SBV

-- symbolically compute the minumum element in a list
-- if the list is empty, 0 is returned.
sminimum xs = foldr (\a b -> ite (a .<= b) a b) 0 xs

-- prove some basic facts:
prop1 = prove $ \a b c -> sminimum [a, b, c] .<= (a :: SInteger)
prop2 = prove $ \a b c -> sminimum [a, b, c] .<= (b :: SInteger)
prop3 = prove $ \a b c -> sminimum [a, b, c] .<= (c :: SInteger)

LeventErkok

import Data.SBV

linDioph :: [Integer] -> Integer -> IO [[Integer]]
linDioph cs c = extractModels `fmap` lde (map literal cs) (literal c)
  where n = length cs
        as `less` bs = bAnd (zipWith (.<=) as bs) &&& bOr (zipWith (.<) as bs)
        lde xs x = allSat $ do
                let ok vs = bAny (.> 0) vs &&& bAll (.>= 0) vs &&& sum (zipWith (*) xs vs) .== x
                es <- mkExistVars n
                as <- mkForallVars n

LeventErkok

import Data.SBV

-- generate a model of 9 sInt8's that are always increasing and positive
-- I just named a0 below explicitly, but of course you can name any of
-- the parameters you want.
--
-- also see the functions: free/exists/forall/sBool/sBools/sInt8/sInt8s etc;
-- there's a pair (singular and plural) provided for each basic type SBV
-- supports.
tst = sat $ do as@(a0 : _) <- mapM free ['a' : show i | i <- [0..8]]

LeventErkok

import Data.SBV

-- An attempt to prove that the derivative of x^2 is 2x, using the
-- epsilon-delta definition of limit (http://en.wikipedia.org/wiki/(%CE%B5,_%CE%B4)-definition_of_limit)
-- inspired by: http://stackoverflow.com/questions/16367703/using-z3py-online-to-prove-that-the-derivative-of-x2-is-2x
-- That is, we try to prove:
--   forall x. forall epsilon>0. exists delta>0. forall d.
--        (0 < abs d < delta ==> abs (((x+d)^2 - x^2) / d - 2x) < epsilon)
-- Alas, z3 returns unknown; which is not very surprising due to the need for quantifiers.
dx2 :: IO ThmResult

LeventErkok

{-# LANGUAGE ScopedTypeVariables #-}

module Main (main) where

import qualified Data.SBV           as S
import qualified Data.SBV.Dynamic   as S hiding (satWith)
import qualified Data.SBV.Internals as S

import Data.List  (sort, nub)
import Data.Maybe (fromMaybe)

LeventErkok

module Main(main) where

import Data.Maybe (fromJust)
import Data.List (nub)

import Text.Parsec
import Text.Parsec.Language
import qualified Text.Parsec.Token as P

-- For the SMT solver interface