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