-----------------------------------------------------------------------------
-- |
-- Module    : TestSuite.Queries.Interpolants
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Testing a few interpolant computations.
--
-----------------------------------------------------------------------------

{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module TestSuite.Queries.Interpolants (tests)  where

import Data.SBV.Control

import Utils.SBVTestFramework

-- Test suite
tests :: TestTree
tests =
  testGroup "Basics.QueryInterpolants"
    [ goldenCapturedIO "query_Interpolant1" $ testQuery mathSAT q1
    , goldenCapturedIO "query_Interpolant2" $ testQuery mathSAT q2
    , goldenCapturedIO "query_Interpolant3" $ testQuery z3      q3
    , goldenCapturedIO "query_Interpolant4" $ testQuery z3      q4
    ]

testQuery :: Show a => SMTConfig -> Symbolic a -> FilePath -> IO ()
testQuery s t rf = do r <- runSMTWith s{verbose=True, redirectVerbose=Just rf} t
                      appendFile rf ("\nFINAL OUTPUT:\n" ++ show r ++ "\n")

iConstraint :: String -> SBool -> Symbolic ()
iConstraint g = constrainWithAttribute [(":interpolation-group", g)]

q1 :: Symbolic String
q1 = do a <- sInteger "a"
        b <- sInteger "b"
        c <- sInteger "c"
        d <- sInteger "d"

        setOption $ ProduceInterpolants True

        iConstraint "c1" $ a .== b .&& a .== c
        iConstraint "c2" $ b .== d .&& sNot (c .== d)

        query $ do _ <- checkSat
                   getInterpolantMathSAT ["c1"]

q2 :: Symbolic String
q2 = do a <- sInteger "a"
        b <- sInteger "b"
        c <- sInteger "c"
        d <- sInteger "d"

        let f, g :: SInteger -> SInteger
            f = uninterpret "f"
            g = uninterpret "g"

        setOption $ ProduceInterpolants True

        iConstraint "c1" $ f a .== c .&& f b .== d
        iConstraint "c2" $   a .== b .&& g c ./= g d

        query $ do _ <- checkSat
                   getInterpolantMathSAT ["c1"]


q3 :: Symbolic String
q3 = do a <- sInteger "a"
        b <- sInteger "b"
        c <- sInteger "c"
        d <- sInteger "d"

        query $ getInterpolantZ3 [ a .== b .&& a .== c
                                 , b .== d .&& sNot (c .== d)
                                 ]

q4 :: Symbolic String
q4 = do a <- sInteger "a"
        b <- sInteger "b"
        c <- sInteger "c"
        d <- sInteger "d"

        let f, g :: SInteger -> SInteger
            f = uninterpret "f"
            g = uninterpret "g"

        query $ getInterpolantZ3 [ f a .== c .&& f b .== d
                                 ,   a .== b .&& g c ./= g d
                                 ]

{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}