```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 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 ``` ```------------------------------------------------------------------------------ --- Library for constraint programming with arithmetic constraints over reals. --- --- @author Michael Hanus --- @version December 2020 ------------------------------------------------------------------------------ module CLP.R(CFloat, minimumFor, minimize, maximumFor, maximize) where -- The operator declarations are similar to the standard arithmetic operators. infixl 7 *., /. infixl 6 +., -. infix 4 <., >., <=., >=. --- Abstract type to represent floats used in constraints. data CFloat = CF Float instance Eq CFloat where (CF f1) == (CF f2) = f1 == f2 instance Ord CFloat where compare (CF f1) (CF f2) = compare f1 f2 x < y = x <. y x > y = x >. y x <= y = x <=. y x >= y = x >=. y instance Show CFloat where show (CF f) = show f instance Num CFloat where x + y = x +. y x - y = x -. y x * y = x *. y negate (CF x) = CF (negate x) abs x | x >= 0 = x | otherwise = negate x signum x | x > 0 = 1 | x == 0 = 0 | otherwise = -1 fromInt x = i2f x instance Fractional CFloat where x / y = x /. y fromFloat x = CF x --- Addition on floats in arithmetic constraints. (+.) :: CFloat -> CFloat -> CFloat (CF x) +. (CF y) = CF ((prim_CLPR_plus \$! y) \$! x) prim_CLPR_plus :: Float -> Float -> Float prim_CLPR_plus external --- Subtraction on floats in arithmetic constraints. (-.) :: CFloat -> CFloat -> CFloat (CF x) -. (CF y) = CF ((prim_CLPR_minus \$! y) \$! x) prim_CLPR_minus :: Float -> Float -> Float prim_CLPR_minus external --- Multiplication on floats in arithmetic constraints. (*.) :: CFloat -> CFloat -> CFloat (CF x) *. (CF y) = CF ((prim_CLPR_times \$! y) \$! x) prim_CLPR_times :: Float -> Float -> Float prim_CLPR_times external --- Division on floats in arithmetic constraints. (/.) :: CFloat -> CFloat -> CFloat (CF x) /. (CF y) = CF ((prim_CLPR_div \$! y) \$! x) prim_CLPR_div :: Float -> Float -> Float prim_CLPR_div external --- "Less than" constraint on floats. (<.) :: CFloat -> CFloat -> Bool (CF x) <. (CF y) = (prim_CLPR_le \$! y) \$! x prim_CLPR_le :: Float -> Float -> Bool prim_CLPR_le external --- "Greater than" constraint on floats. (>.) :: CFloat -> CFloat -> Bool (CF x) >. (CF y) = (prim_CLPR_ge \$! y) \$! x prim_CLPR_ge :: Float -> Float -> Bool prim_CLPR_ge external --- "Less than or equal" constraint on floats. (<=.) :: CFloat -> CFloat -> Bool (CF x) <=. (CF y) = (prim_CLPR_leq \$! y) \$! x prim_CLPR_leq :: Float -> Float -> Bool prim_CLPR_leq external --- "Greater than or equal" constraint on floats. (>=.) :: CFloat -> CFloat -> Bool (CF x) >=. (CF y) = (prim_CLPR_geq \$! y) \$! x prim_CLPR_geq :: Float -> Float -> Bool prim_CLPR_geq external --- Conversion function from integers to floats. --- Rigid in the first argument, i.e., suspends until the first argument --- is ground. i2f :: Int -> CFloat i2f x = CF (prim_CLPR_i2f \$# x) prim_CLPR_i2f :: Int -> Float prim_CLPR_i2f external --- Computes the minimum with respect to a given constraint. --- (minimumFor g f) evaluates to x if (g x) is satisfied and --- (f x) is minimal. The evaluation fails if such a minimal value --- does not exist. The evaluation suspends if it contains --- unbound non-local variables. minimumFor :: (a -> Bool) -> (a -> Float) -> a minimumFor external --- Minimization constraint. --- (minimize g f x) is satisfied if (g x) is satisfied and --- (f x) is minimal. The evaluation suspends if it contains --- unbound non-local variables. minimize :: Data a => (a -> Bool) -> (a -> Float) -> a -> Bool minimize g f x = minimumFor g f =:= x --- Computes the maximum with respect to a given constraint. --- (maximumFor g f) evaluates to x if (g x) is satisfied and --- (f x) is maximal. The evaluation fails if such a maximal value --- does not exist. The evaluation suspends if it contains --- unbound non-local variables. maximumFor :: (a -> Bool) -> (a -> Float) -> a maximumFor external --- Maximization constraint. --- (maximize g f x) is satisfied if (g x) is satisfied and --- (f x) is maximal. The evaluation suspends if it contains --- unbound non-local variables. maximize :: Data a => (a -> Bool) -> (a -> Float) -> a -> Bool maximize g f x = maximumFor g f =:= x -- end of CLP.R ```