content: -----------------------------------------------------------------------------
  -- |
  -- Module    : TestSuite.Basics.Quantifiers
  -- Copyright : (c) Levent Erkok
  -- License   : BSD3
  -- Maintainer: erkokl@gmail.com
  -- Stability : experimental
  --
  -- Various combinations of quantifiers
  -----------------------------------------------------------------------------
  
  {-# LANGUAGE CPP                 #-}
  {-# LANGUAGE DataKinds           #-}
  {-# LANGUAGE FlexibleContexts    #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications    #-}
  
  #if MIN_VERSION_base(4,19,0)
  {-# LANGUAGE TypeAbstractions    #-}
  #endif
  
  {-# OPTIONS_GHC -Wall -Werror #-}
  
  module TestSuite.Basics.Quantifiers(tests) where
  
  import Control.Monad (void)
  
  import Utils.SBVTestFramework
  
  data Q = E  -- exists
         | A  -- all
  
  instance Show Q where
     show E = "exists"
     show A = "forall"
  
  tests :: TestTree
  tests = testGroup "Basics.Quantifiers" $ concatMap mkGoal goals ++ concatMap mkPred preds ++ others
     where mkGoal (g, nm) = [ goldenCapturedIO ("quantified_sat"   ++ "_" ++ nm) $ \rf -> void $ satWith   z3{verbose=True, redirectVerbose=Just rf} g
                            ]
           mkPred (p, nm) = [ goldenCapturedIO ("quantified_sat"   ++ "_" ++ nm) $ \rf -> void $ satWith   z3{verbose=True, redirectVerbose=Just rf} p
                            , goldenCapturedIO ("quantified_prove" ++ "_" ++ nm) $ \rf -> void $ proveWith z3{verbose=True, redirectVerbose=Just rf} p
                            ]
  
           others = [ goldenCapturedIO "quantifiedB_0" $ check $ \(ExistsN @4 xs)   -> sAll (.< (20 :: SWord8)) xs .&& sum (1 : xs) .== (0::SWord8)
                    , goldenCapturedIO "quantifiedB_1" $ check $ \(ExistsN @4 xs)   -> sum xs .== (0::SWord8)
                    , goldenCapturedIO "quantifiedB_2" $ check $ \k (ForallN @4 xs) -> sum xs .== (k::SWord8)
                    , goldenCapturedIO "quantifiedB_3" $ check $ \k (ExistsN @4 xs) -> sum xs .== (k::SWord8)
                    , goldenCapturedIO "quantifiedB_4" $ check $ \(ExistsN @4 xs) (Exists k) -> sum xs .== (k::SWord8)
                    , goldenCapturedIO "quantifiedB_5" $ check $ \(ExistsN @4 xs) (Forall k) -> sum xs .== (k::SWord8)
                    , goldenCapturedIO "quantifiedB_6" $ check $ quantifiedBool (quantifiedBool (\(Exists (x::SBool)) -> x) )
                    , goldenCapturedIO "quantifiedB_7" $ check $ \(Exists (x :: SBool)) -> quantifiedBool (quantifiedBool (\(Exists (y::SBool)) -> x .|| y) )
                    , goldenCapturedIO "quantifiedB_8" $ check $ \(Exists (x :: SBool)) -> quantifiedBool (\(Exists (y::SBool)) -> x .|| y)
                    , goldenCapturedIO "quantifiedB_9" $ check $ quantifiedBool $ \(Exists (x :: SBool)) -> quantifiedBool (\(Exists (y::SBool)) -> x .|| y)
                    , goldenCapturedIO "quantifiedB_A" $ check $ \(Exists a) (Forall b) (Exists c) (Forall d) ->  a + b + c + d .== (0::SInteger)
                    , goldenCapturedIO "quantifiedB_B" $ check $ \(Forall a) (Exists b) (Forall c) (Exists d) ->  a + b + c + d .== (0::SInteger)
                    ]
             where check p rf = do res <- satWith z3{verbose=True, redirectVerbose=Just rf} p
                                   appendFile rf $ "\nRESULT: "  ++ show res ++ "\n"
  
           qs   = [E, A]
  
           acts = [ (\x y -> x + (y - x) .== y  , "thm")
                  , (\x y -> x .== y .&& x ./= y, "contradiction")
                  , (\x y -> x .== y + 1        , "satisfiable")
                  ]
  
           goals = [(t1 q1 q2 a, show q1 ++ show q2 ++ "_" ++ an ++ "_c") | q1      <- qs
                                                                          , q2      <- qs
                                                                          , (a, an) <- acts
                                                                          ]
  
           preds = [(t2 q1 q2 a, show q1 ++ show q2 ++ "_" ++ an ++ "_p") | q1       <- qs
                                                                          , q2       <- qs
                                                                          , (a, an)  <- acts
                                                                          ]
  
           t1 :: Q -> Q -> (SWord8 -> SWord8 -> SBool) -> ConstraintSet
           t1 E E act = constrain $ \(Exists x) (Exists y) -> act x y
           t1 E A act = constrain $ \(Exists x) (Forall y) -> act x y
           t1 A E act = constrain $ \(Forall x) (Exists y) -> act x y
           t1 A A act = constrain $ \(Forall x) (Forall y) -> act x y
  
           t2 :: Q -> Q -> (SWord8 -> SWord8 -> SBool) -> Predicate
           t2 E E act = pure $ quantifiedBool $ \(Exists x) (Exists y) -> act x y
           t2 E A act = pure $ quantifiedBool $ \(Exists x) (Forall y) -> act x y
           t2 A E act = pure $ quantifiedBool $ \(Forall x) (Exists y) -> act x y
           t2 A A act = pure $ quantifiedBool $ \(Forall x) (Forall y) -> act x y
  
  {- HLint ignore module "Reduce duplication"     -}
  {- HLint ignore module "Unused LANGUAGE pragma" -}
  