packages feed

sbv-7.0: SBVTestSuite/TestSuite/Optimization/Basics.hs

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

module TestSuite.Optimization.Basics(tests) where

import Utils.SBVTestFramework

-- Test suite
tests :: TestTree
tests =
  testGroup "Optimization.Basics"
    [ goldenVsStringShow "optBasics1" (optimize Lexicographic optBasics1)
    , goldenVsStringShow "optBasics2" (optimize Lexicographic optBasics2)
    ]

optBasics1 :: Goal
optBasics1 = do x <- sInteger "x"
                y <- sInteger "y"

                constrain $ x .< 2
                constrain $ y - x .< 1

                maximize "x_plus_y" $ x+y

optBasics2 :: Goal
optBasics2 = do x <- sInteger "x"
                y <- sInteger "y"

                constrain $ x .< 4
                constrain $ y - x .< 1
                constrain $ y .> 1

                minimize "x_plus_y" $ x+y