content: {-# LANGUAGE CPP #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeOperators #-}
  
  module Grisette.SymPrim.QuantifierTests (quantifierTests) where
  
  import Grisette
    ( AsKey (AsKey),
      Function ((#)),
      GenSymSimple (simpleFresh),
      LogicalOp (symImplies),
      ModelOps (isEmptyModel),
      SimpleListSpec (SimpleListSpec),
      SymEq ((.==)),
      SymOrd ((.>)),
      runFresh,
      solve,
      z3,
    )
  import Grisette.Internal.SymPrim.Quantifier (existsFresh, existsSym, forallFresh, forallSym)
  import Grisette.Internal.SymPrim.SymInteger (SymInteger)
  import Grisette.SymPrim (type (=~>))
  import Test.Framework (Test, testGroup)
  import Test.Framework.Providers.HUnit (testCase)
  import Test.HUnit (assertBool, (@?=))
  
  #if MIN_VERSION_sbv(10,1,0)
  sbvVersionCheck :: Test -> Test
  sbvVersionCheck = id
  #else
  sbvVersionCheck :: Test -> Test
  sbvVersionCheck _ = testGroup "Quantifier" []
  #endif
  
  quantifierTests :: Test
  quantifierTests =
    sbvVersionCheck $
      testGroup
        "Quantifier"
        [ testCase "Basic" $ do
            let l@[x, y] = ["x", "y"] :: [SymInteger]
            r <- solve z3 $ forallSym l $ (x .== y) `symImplies` (x + 1 .== y + 1)
            case r of
              Left err -> error $ show err
              Right mo ->
                assertBool "no elements should be in the model" $ isEmptyModel mo,
          testCase "Basic2" $ do
            let [x, y] = ["x", "y"] :: [SymInteger]
            r <- solve z3 $ forallSym x $ existsSym y $ x .> y
            case r of
              Left err -> error $ show err
              Right mo ->
                assertBool "no elements should be in the model" $ isEmptyModel mo,
          testCase "With ufunc" $ do
            -- https://github.com/LeventErkok/sbv/issues/711
            let f = "f" :: SymInteger =~> SymInteger
            let x = "x" :: SymInteger
            let y = "y" :: SymInteger
            r <-
              solve z3 $
                forallSym x $
                  forallSym y $
                    (x .== y) `symImplies` ((f # x) .== (f # y))
            case r of
              Left err -> error $ show err
              Right _ -> return (),
          testCase "fresh" $ do
            let x = flip runFresh "x" $
                  forallFresh (SimpleListSpec 2 ()) $ \(l :: [SymInteger]) ->
                    existsFresh (SimpleListSpec 2 ()) $ \(r :: [SymInteger]) ->
                      return $ l .== r
            let r = flip runFresh "x" $ do
                  l :: [SymInteger] <- simpleFresh (SimpleListSpec 2 ())
                  r <- simpleFresh (SimpleListSpec 2 ())
                  return $ forallSym l $ existsSym r $ l .== r
            AsKey x @?= AsKey r
        ]
  