1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
|
-----------------------------------------------------------------------------
-- |
-- 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" -}
|
