Quantified.hs

-----------------------------------------------------------------------------
-- |
-- Module    : TestSuite.Optimization.Quantified
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Test suite for optimization with quantifiers
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE ScopedTypeVariables #-}

module TestSuite.Optimization.Quantified(tests) where

import Data.List (isPrefixOf)

import Utils.SBVTestFramework
import qualified Control.Exception as C

-- Test suite
tests :: TestTree
tests =
  testGroup "Optimization.Reals"
    [ goldenVsStringShow "optQuant1" $ opt  q1
    , goldenVsStringShow "optQuant2" $ opt  q2
    , goldenVsStringShow "optQuant3" $ opt  q3
    , goldenVsStringShow "optQuant4" $ opt  q4
    , goldenString       "optQuant5" $ optE q5
    ]
    where opt    = optimize Lexicographic
          optE q = (show <$> optimize Lexicographic q) `C.catch` (\(e::C.SomeException) -> return (pick (show e)))
          pick s = unlines [l | l <- lines s, "***" `isPrefixOf` l]

q1 :: ConstraintSet
q1 = do a <- sInteger "a"
        [b1, b2] <- sIntegers ["b1", "b2"]
        constrain $ \(Forall x) ->     2 * (a * x + b1) .== 2
                                   .&& 4 * (a * x + b2) .== 4
        constrain $ a .>= 0
        minimize "goal" $ 2*a

q2 :: ConstraintSet
q2 = do a <- sInteger "a"
        [b1, b2] <- sIntegers ["b1", "b2"]
        constrain $ \(Forall x) ->     2 * (a * x + b1) .== 2
                                   .&& 4 * (a * x + b2) .== 4
                                   .&& a .>= 0
        minimize "goal" a

q3 :: ConstraintSet
q3 = do a <- sInteger "a"
        [b1, b2] <- sIntegers ["b1", "b2"]
        minimize "goal" a
        constrain $ \(Forall x) ->     2 * (a * x + b1) .== 2
                                   .&& 4 * (a * x + b2) .== 4
        constrain $ a .>= 0

q4 :: ConstraintSet
q4 = do a <- sInteger "a"
        [b1, b2] <- sIntegers ["b1", "b2"]
        minimize "goal" $ 2*a
        constrain $ \(Forall x) ->     2 * (a * x + b1) .== 2
                                   .&& 4 * (a * x + b2) .== 4
        constrain $ a .>= 0

q5 :: ConstraintSet
q5 = do a <- sInteger "a"
        constrain $ \(Exists y) -> a .>= (y :: SInteger)
        constrain $ a .>= 0
        b <- sInteger "b"
        constrain $ b .>= 0
        minimize "goal" $ a+b

{- HLint ignore module "Reduce duplication" -}