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

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

------------------------------------------------------------------------------------------
-- 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

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

{-# 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

; Automatically generated by SBV. Do not edit.
(set-option :produce-models true)
; Has unbounded values (Int/Real) or uninterpreted sorts; no logic specified.
; --- uninterpreted sorts ---
(declare-sort A 0)  ; N.B. Uninterpreted: A.A: not a nullary constructor
; --- literal constants ---
(define-fun s_2 () Bool false)
(define-fun s_1 () Bool true)
; --- skolem constants ---
(declare-fun s0 () Int) ; tracks user variable "x1"

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

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

{------------------------------------------------
A Haskell solution to: http://www.coinheist.com/rubik/a_regular_crossword/grid.pdf
using the Z3 SMT solver.

Z3 finds the following solution in about 7 mins
on my Mac Core-i5, and another 7 mins to prove
it's unique.

   NHPEHAS
   DIOMOMTH