-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Misc.Definitions
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Demonstrates how we can add actual SMT-definitions for functions
-- that cannot otherwise be defined in SBV. Typically, these are used
-- for recursive definitions.
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Misc.Definitions where

import Data.SBV

-- | Sum of numbers from 0 to the given number.
-- Note that this cannot be defined as a regular Haskell function, as
-- it wouldn't terminate as it recurses on a symbolic argument.
sumToN :: SInteger -> SInteger
sumToN :: SInteger -> SInteger
sumToN = String -> SInteger -> SInteger
forall a. Uninterpreted a => String -> a
uninterpret String
"sumToN"

-- | Add the definition of sum to the SMT solver. Note that SBV
-- performs no checks on your definition, neither that it is
-- well formed, or even has the correct type!
defineSum :: Symbolic ()
defineSum :: Symbolic ()
defineSum = String -> [String] -> Symbolic ()
forall (m :: * -> *). SolverContext m => String -> [String] -> m ()
addSMTDefinition String
"sumToN"
                [ String
"(define-fun-rec sumToN ((x Int)) Int"
                , String
"                (ite (<= x 0)"
                , String
"                     0"
                , String
"                     (+ x (sumToN (- x 1)))))"
                ]

-- | A simple proof using 'sumToN'. We get a failure, because we haven't
-- given the solver the definition, and thus it goes completely uninterpreted.
--
-- We have:
--
-- >>> badExample
-- Falsifiable. Counter-example:
--   sumToN :: Integer -> Integer
--   sumToN _ = 0
--
-- Since 'sumToN' remains uninterpreted, the solver gave us a model that obviously
-- fails the property.
badExample :: IO ThmResult
badExample :: IO ThmResult
badExample = Predicate -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (Predicate -> IO ThmResult) -> Predicate -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ do
        let check :: SBool
check = SInteger -> SInteger
sumToN SInteger
5 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
15  -- Should fail, even though 5*6/2 = 15
        SBool -> Predicate
forall (f :: * -> *) a. Applicative f => a -> f a
pure SBool
check :: Predicate

-- | Same example, except this time we give the solver the definition of the function,
-- and thus the proof goes through.
--
-- We have:
--
-- >>> goodExample
-- Q.E.D.
--
-- In this case, the solver has the definition, and proves the predicate as expected.
goodExample :: IO ThmResult
goodExample :: IO ThmResult
goodExample = Predicate -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (Predicate -> IO ThmResult) -> Predicate -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ do
        Symbolic ()
defineSum
        let check :: SBool
check = SInteger -> SInteger
sumToN SInteger
5 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
15  -- Should fail, even though 5*6/2 = 15
        SBool -> Predicate
forall (f :: * -> *) a. Applicative f => a -> f a
pure SBool
check :: Predicate