{-# LANGUAGE NoImplicitPrelude #-}

-- | This will not succeed when 'smtFloatMode' is 'FloatUninterpreted', as Clang
-- will turn @input /= 30.0@ below into a more complicated expression that also
-- checks if @30.0@ is NaN or not. This is logically equivalent to the original
-- specification, but an SMT solver cannot conclude this when all of the
-- floating-point operations involved are treated as uninterpreted functions.
--
-- To make this work, we set 'smtFloatMode' to 'FloatIEEE' instead. This works
-- because all of the floating-point operations in the specification below are
-- native to SMT-LIB.
module Copilot.Verifier.Examples.ShouldPass.FPNegation where

import Copilot.Compile.C99 (mkDefaultCSettings)
import Copilot.Verifier ( Verbosity, VerifierOptions(..)
                        , defaultVerifierOptions, verifyWithOptions )
import Copilot.Verifier.FloatMode (FloatMode(..))
import qualified Copilot.Library.PTLTL as PTLTL
import Language.Copilot

input :: Stream Float
input :: Stream Float
input = String -> Maybe [Float] -> Stream Float
forall a. Typed a => String -> Maybe [a] -> Stream a
extern String
"input" Maybe [Float]
forall a. Maybe a
Nothing

-- | MyProperty
--   @
--   Input is never 30.0
--   @
propMyProperty :: Stream Bool
propMyProperty :: Stream Bool
propMyProperty = Stream Bool -> Stream Bool
PTLTL.alwaysBeen (Stream Float
input Stream Float -> Stream Float -> Stream Bool
forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
/= Stream Float
30.0)

-- | Clock that increases in one-unit steps.
clock :: Stream Int64
clock :: Stream Int64
clock = [Int64
0] [Int64] -> Stream Int64 -> Stream Int64
forall a. Typed a => [a] -> Stream a -> Stream a
++ (Stream Int64
clock Stream Int64 -> Stream Int64 -> Stream Int64
forall a. Num a => a -> a -> a
+ Stream Int64
1)

-- | First Time Point
ftp :: Stream Bool
ftp :: Stream Bool
ftp = [Bool
True] [Bool] -> Stream Bool -> Stream Bool
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Bool
false

pre :: Stream Bool -> Stream Bool
pre :: Stream Bool -> Stream Bool
pre = ([Bool
False] [Bool] -> Stream Bool -> Stream Bool
forall a. Typed a => [a] -> Stream a -> Stream a
++)

tpre :: Stream Bool -> Stream Bool
tpre :: Stream Bool -> Stream Bool
tpre = ([Bool
True] [Bool] -> Stream Bool -> Stream Bool
forall a. Typed a => [a] -> Stream a -> Stream a
++)

notPreviousNot :: Stream Bool -> Stream Bool
notPreviousNot :: Stream Bool -> Stream Bool
notPreviousNot = Stream Bool -> Stream Bool
not (Stream Bool -> Stream Bool)
-> (Stream Bool -> Stream Bool) -> Stream Bool -> Stream Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stream Bool -> Stream Bool
PTLTL.previous (Stream Bool -> Stream Bool)
-> (Stream Bool -> Stream Bool) -> Stream Bool -> Stream Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stream Bool -> Stream Bool
not

-- | Complete specification. Calls C handler functions when properties are
-- violated.
spec :: Spec
spec :: Spec
spec = do
  String -> Stream Bool -> [Arg] -> Spec
trigger String
"handlerMyProperty" (Stream Bool -> Stream Bool
not Stream Bool
propMyProperty) []

verifySpec :: Verbosity -> IO ()
verifySpec :: Verbosity -> IO ()
verifySpec Verbosity
verb = do
  Spec
spec' <- Spec -> IO Spec
forall a. Spec' a -> IO Spec
reify Spec
spec
  VerifierOptions -> CSettings -> [String] -> String -> Spec -> IO ()
verifyWithOptions
    (VerifierOptions
defaultVerifierOptions
      { verbosity = verb
      , smtFloatMode = FloatIEEE
      })
    CSettings
mkDefaultCSettings [] String
"fpNegation" Spec
spec'