LeventErkok

{-# OPTIONS_GHC -Wall            #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Data.SBV
import Control.Exception as E

-- Node indexes, support upto 2^16 entries (no of inputs + no of AND gates)
type Node = SWord16

-- Values that flow through the AND gates

LeventErkok

module LSB(main) where

import Data.Word
import Data.Array.Unboxed
import Data.Bits
import Data.SBV

-- Kmett's implementation of finding the least significant bit set in a 64 bit word
-- Adapted from the original implementation at:
--    http://github.com/ekmett/algebra/blob/master/Numeric/Coalgebra/Geometric.hs#L72

LeventErkok

(set-option :mbqi true)
(set-option :produce-models true)
; --- literal constants ---
(define-fun s_2 () (_ BitVec 1) #b0)
(define-fun s_1 () (_ BitVec 1) #b1)
(define-fun s68 () (_ BitVec 8) #x00)
(define-fun s83 () (_ BitVec 8) #x01)
(define-fun s89 () (_ BitVec 8) #x02)
(define-fun s95 () (_ BitVec 8) #x03)
(define-fun s101 () (_ BitVec 8) #x04)

LeventErkok

(set-option :mbqi true)
(set-option :produce-models true)
; --- literal constants ---
(define-fun s_2 () (_ BitVec 1) #b0)
(define-fun s_1 () (_ BitVec 1) #b1)
(define-fun s68 () (_ BitVec 8) #x00)
(define-fun s83 () (_ BitVec 8) #x01)
(define-fun s89 () (_ BitVec 8) #x02)
(define-fun s95 () (_ BitVec 8) #x03)
(define-fun s101 () (_ BitVec 8) #x04)

LeventErkok

{-
SBV can only generate straight-line code. While this usually leads to
faster and nicely optimizable code, it also inevitably can lead to code
explosion.. What we need is a way to control what parts of the code is
"inlined". The trick is to extract the "body" of the loop and uninterpret
it, and call it from the main program. Then, we use the library code
generation function to put the two together.

For instance, let's say we want to generate code for the following
Haskell function:

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

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

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)