-----------------------------------------------------------------------------
-- |
-- Module    : TestSuite.Basics.ModelValidate
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Few validate tests
-----------------------------------------------------------------------------

{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module TestSuite.Basics.ModelValidate (testsABC, tests)  where

import qualified Control.Exception as C
import Data.List (isPrefixOf)

import Utils.SBVTestFramework

-- Test suite, this needs ABC
testsABC :: TestTree
testsABC = testGroup "Basics.ModelValidate.ABC" [
             goldenCapturedIO "validate_0" testABC
           ]
    where testABC goldFile = do r <- satWith abc{verbose=True, redirectVerbose = Just goldFile, validateModel = True} (free "x" >>= \x -> pure $ x .< (10::SWord8))
                                appendFile goldFile ("\nFINAL OUTPUT:\n" ++ show r ++ "\n")

tests :: TestTree
tests = testGroup "Basics.ModelValidate" [
             goldenCapturedIO "validate_1" $ t  satWith    t1
           , goldenCapturedIO "validate_2" $ t  satWith    t2
           , goldenCapturedIO "validate_3" $ t  satWith    t3
           , goldenCapturedIO "validate_4" $ t  proveWith  t3
           , goldenCapturedIO "validate_5" $ t  satWith    t4
           , goldenCapturedIO "validate_6" $ t  proveWith  t4
           , goldenCapturedIO "validate_7" $ tE satWith    t5
           ]
    where t f test goldFile = do r <- f defaultSMTCfg{verbose=True, redirectVerbose = Just goldFile, validateModel = True} test
                                 appendFile goldFile ("\nFINAL OUTPUT:\n" ++ show r ++ "\n")

          tE f test goldFile = do r <- f defaultSMTCfg{verbose=True, redirectVerbose = Just goldFile, validateModel = True} test
                                  appendFile goldFile ("\nFINAL OUTPUT:\n" ++ show r ++ "\n")
                               `C.catch` (\(e::C.SomeException) -> appendFile goldFile ("\nEXCEPTION RAISED:\n" ++ pick (show e) ++ "\n"))
              where pick s = unlines [l | l <- lines s, "***" `isPrefixOf` l]

          t1, t2 :: Predicate
          t1 = free "x" >>= \x -> pure $ fpAdd sRTZ x x   .== (x::SFloat)
          t2 = free "x" >>= \x -> pure $ fpFMA sRNE x x x .== (x::SFloat)

          t3 :: Predicate
          t3 = do x <- sInteger "x"
                  constrain $ x .> x   -- Constraining with False! i.e., any theorem will follow, and will be trivially unsat
                  pure sFalse

          t4 :: Predicate
          t4 = do x <- sInteger "x"
                  y <- sInteger "y"
                  constrain $ x .> y
                  constrain $ x .> 12
                  return $ x .== y+3

          t5 :: Predicate
          t5 = do x <- free "x"
                  pure $ quantifiedBool $ \(Forall y) -> fpIsPoint y .=> x .<= (y::SFloat)