1-----------------------------------------------------------------------------
2-- |
3-- Module    : TestSuite.Optimization.Floats
4-- Copyright : (c) Levent Erkok
5-- License   : BSD3
6-- Maintainer: erkokl@gmail.com
7-- Stability : experimental
8--
9-- Test suite for optimization routines, floats
10-----------------------------------------------------------------------------
11
12{-# OPTIONS_GHC -Wall -Werror #-}
13
14module TestSuite.Optimization.Floats (tests) where
15
16import Control.Monad (when)
17
18import Utils.SBVTestFramework
19
20-- Test suite
21tests :: TestTree
22tests =
23  testGroup "Optimization.Floats"
24    [ goldenVsStringShow "optFloat1a" $ optimizeWith z3{crackNum=True} Lexicographic (floatMinMax  (minimize "min-x") True)
25    , goldenVsStringShow "optFloat1b" $ optimizeWith z3{crackNum=True} Lexicographic (floatMinMax  (minimize "min-x") False)
26    , goldenVsStringShow "optFloat1c" $ optimizeWith z3{crackNum=True} Lexicographic (floatMinMax  (maximize "max-x") True)
27    , goldenVsStringShow "optFloat1d" $ optimizeWith z3{crackNum=True} Lexicographic (floatMinMax  (maximize "max-y") False)
28    , goldenVsStringShow "optFloat2a" $ optimizeWith z3{crackNum=True} Lexicographic (doubleMinMax (minimize "min-x") True)
29    , goldenVsStringShow "optFloat2b" $ optimizeWith z3{crackNum=True} Lexicographic (doubleMinMax (minimize "min-x") False)
30    , goldenVsStringShow "optFloat2c" $ optimizeWith z3{crackNum=True} Lexicographic (doubleMinMax (maximize "max-x") True)
31    , goldenVsStringShow "optFloat2d" $ optimizeWith z3{crackNum=True} Lexicographic (doubleMinMax (maximize "max-y") False)
32    , goldenVsStringShow "optFloat3"  $ optimizeWith z3{crackNum=True} Lexicographic q
33    , goldenVsStringShow "optFloat4"  $ optimizeWith z3{crackNum=True} Lexicographic r
34    ]
35
36floatMinMax :: (SFloat -> Symbolic ()) -> Bool -> Goal
37floatMinMax opt reqPoint = do x <- sFloat "x"
38
39                              when reqPoint $ constrain $ fpIsPoint x
40
41                              opt x
42
43doubleMinMax :: (SDouble -> Symbolic ()) -> Bool -> Goal
44doubleMinMax opt reqPoint = do x <- sDouble "x"
45
46                               when reqPoint $ constrain $ fpIsPoint x
47
48                               opt x
49
50q :: Goal
51q = do x <- sFloat "x"
52       y <- sFloat "y"
53
54       constrain $ fpIsPoint x
55       constrain $ fpIsPoint y
56       constrain $ x .== y
57       constrain $ x .> 0
58       constrain $ fpIsPoint $ x+y
59
60       maximize "metric-max-x+y" $ observe "max-x+y" (x+y)
61
62r :: Goal
63r = do x <- sFloat "x"
64       y <- sFloat "y"
65
66       constrain $ fpIsPoint x
67       constrain $ fpIsPoint y
68       constrain $ x .== y
69       constrain $ x .> 0
70       constrain $ fpIsPoint $ x+y
71
72       minimize "metric-min-x+y" $ observe "min-x+y" (x+y)
73
74{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}
75