LeventErkok

{-# LANGUAGE DeriveDataTypeable   #-}

import Data.SBV
import Data.Generics

-- boilerplate to get A to be an SMT-Lib uninterpreted sort
data A = A () deriving (Eq, Ord, Data, Typeable, Read, Show)
instance SymWord A
instance HasKind A
type SA = SBV A

LeventErkok

sat
(model
  ;; universe for A:
  ;;   A!val!1 A!val!0
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun A!val!1 () A)
  (declare-fun A!val!0 () A)
  ;; cardinality constraint:
  (forall ((x A)) (or (= x A!val!1) (= x A!val!0)))

LeventErkok

------------------------------------------------------------------------------------------
-- A formalization of the Cheryl's birtday problem; using Haskell/SBV
--
-- See: http://www.nytimes.com/2015/04/15/science/a-math-problem-from-singapore-goes-viral-when-is-cheryls-birthday.html
--
-- By Levent Erkok, This file is in the public domain. Use it as you wish!
--
-- NB. Thanks to Amit Goel for suggesting the formalization strategy used in here.
------------------------------------------------------------------------------------------

LeventErkok

import Data.SBV

choice = allSat $ do
             [a, b, c, d, e, f] <- sBools ["a", "b", "c", "d", "e", "f"]
             solve [ a .== bAnd [b, c, d, e]                             -- a. All of the below
                   , b .== bAnd (map bnot [c, d, e])                     -- b. None of the below
                   , c .== bAnd [a, b]                                   -- c. All of the above
                   , d .== ((1::SInteger) .== sum (map oneIf [a, b, c])) -- d. One of the above
                   , e .== bAnd (map bnot [a, b, c, d])                  -- e. None of the above
                   , f .== bAnd (map bnot [a, b, c, d, e])               -- f. None of the above

LeventErkok

module SendMoreMoney where

import Data.SBV

-- |
-- >>> sendMoreMoney
-- Solution #1:
--   s = 9 :: Integer
--   e = 5 :: Integer
--   n = 6 :: Integer

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: