-----------------------------------------------------------------------------
-- |
-- Module    : TestSuite.Queries.DSat
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Testing dsat value extraction
-----------------------------------------------------------------------------

{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module TestSuite.Queries.DSat (tests)  where

import Data.SBV.Control

import Utils.SBVTestFramework

-- Test suite
tests :: TestTree
tests =
  testGroup "Basics.Query.DSat"
    [ goldenCapturedIO "dsat01" testQuery
    ]

testQuery :: FilePath -> IO ()
testQuery rf = do r <- runSMTWith dReal{verbose=True, redirectVerbose=Just rf} fv
                  appendFile rf ("\n FINAL:" ++ show r ++ "\nDONE!\n")

fv :: Symbolic (Maybe String, [AlgReal], [RationalCV], [Integer], [Bool])
fv = do a0 <- sReal    "a0"
        i0 <- sInteger "i0"
        b0 <- sBool    "b0"

        constrain $ a0 .> 2
        constrain $ a0 .<= 5

        query $ do a1 :: SReal    <- freshVar "a1"
                   i1 :: SInteger <- freshVar "i1"
                   b1 :: SBool    <- freshVar "b1"

                   constrain $ a1 .> 3
                   constrain $ a1 .<= 12

                   cs <- checkSat

                   case cs of
                     DSat p -> do va0 <- getValue a0
                                  va1 <- getValue a1
                                  vi0 <- getValue i0
                                  vi1 <- getValue i1
                                  vb0 <- getValue b0
                                  vb1 <- getValue b1

                                  let rva0 = algRealToRational va0
                                      rva1 = algRealToRational va1

                                      check r = case r of
                                                  RatInterval lo hi -> if realPoint lo <= realPoint hi
                                                                       then r
                                                                       else error $ "Bounds violated for: " ++ show r
                                                  _                 -> r

                                  pure (p, [va0, va1], map check [rva0, rva1], [vi0, vi1], [vb0, vb1])

                     _   -> error "didn't expect non-DSat here!"