-----------------------------------------------------------------------------
-- |
-- Module      :  Data.SBV.Plugin.Examples.Maximum
-- Copyright   :  (c) Levent Erkok
-- License     :  BSD3
-- Maintainer  :  erkokl@gmail.com
-- Stability   :  experimental
--
-- Shows that a naive definition of maximum doing bit-vector arithmetic
-- is incorrect.
-----------------------------------------------------------------------------

{-# LANGUAGE CPP #-}

#ifndef HADDOCK
{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}
#endif

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Plugin.Examples.Maximum where

import Data.SBV.Plugin

-- | Compute the maximum of three integers, which
-- is intuitively correct for unbounded values, but
-- not for bounded bit-vectors.
myMax :: Int -> Int -> Int -> Int
myMax :: Int -> Int -> Int -> Int
myMax Int
x Int
y Int
z | Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
y Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 = Int
x
            | Int
yInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& Int
yInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 = Int
y
            | Bool
otherwise            = Int
z

-- | Show that this function fails to compute maximum correctly.
-- We have:
--
-- @
-- [SBV] a.hs:11:1-7 Proving "correct", using Z3.
-- [Z3] Falsifiable. Counter-example:
--   x = -2816883406898309583 :: Int64
--   y = -2816883406898309583 :: Int64
--   z =  6694719001794338309 :: Int64
-- @
correct :: Proved (Int -> Int -> Int -> Bool)
correct :: Proved (Int -> Int -> Int -> Bool)
correct Int
x Int
y Int
z = Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
x Bool -> Bool -> Bool
&& Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
y Bool -> Bool -> Bool
&& Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
z
  where m :: Int
m = Int -> Int -> Int -> Int
myMax  Int
x Int
y Int
z