never executed always true always false
1 {-
2 - Module : Conjure.Process.Boost
3 - Description : Strengthen a model using type- and domain-inference.
4 - Copyright : Billy Brown 2017
5 - License : BSD3
6
7 Processing step that attempts to strengthen an Essence model, using methods described in the "Reformulating Essence Specifications for Robustness" paper.
8 -}
9
10 {-# LANGUAGE QuasiQuotes #-}
11
12 module Conjure.Process.Boost ( boost ) where
13
14 import Data.List ( find, union )
15 import Data.Map.Strict ( Map )
16 import qualified Data.Map.Strict as M ( (!?), empty, union )
17
18 import Conjure.Prelude
19 import Conjure.Language
20 import Conjure.Language.Domain.AddAttributes
21 import Conjure.Language.NameResolution ( resolveNames )
22 -- These two are needed together
23 import Conjure.Language.Expression.DomainSizeOf ()
24 import Conjure.Language.DomainSizeOf ( domainSizeOf )
25 import Conjure.Compute.DomainOf ( domainOf )
26 import Conjure.UI.Model ( evaluateModel )
27 import Conjure.UI.VarSymBreaking ( outputVarSymBreaking )
28 import Conjure.Process.Enumerate ( EnumerateDomain )
29
30
31 -- aeson
32 import qualified Data.Aeson as JSON ( decodeStrict )
33 -- shelly
34 import Shelly ( run )
35 -- directory
36 import System.Directory ( removeFile )
37 -- text
38 import qualified Data.Text.Encoding as T ( encodeUtf8 )
39 -- uniplate zipper
40 import Data.Generics.Uniplate.Zipper ( Zipper, zipper, down, fromZipper, hole, replaceHole, right, up )
41
42
43 type ExpressionZ = Zipper Expression Expression
44 type FindVar = (Name, Domain () Expression)
45 type AttrPair = (AttrName, Maybe Expression)
46 type ToAddToRem = ([ExpressionZ], [ExpressionZ])
47
48 -- | Strengthen a model using type- and domain-inference.
49 boost ::
50 MonadFailDoc m =>
51 MonadIO m =>
52 MonadLog m =>
53 MonadUserError m =>
54 NameGen m =>
55 EnumerateDomain m =>
56 (?typeCheckerMode :: TypeCheckerMode) =>
57 LogLevel -> -- ^ Log level to use.
58 Bool -> -- ^ Generate logs for rule applications.
59 Model -> -- ^ Model to strengthen.
60 m Model -- ^ Strengthened model.
61 boost logLevel logRuleSuccesses = resolveNames >=> return . fixRelationProj >=> core
62 where
63 -- core :: ... => Model -> m Model
64 core model1 = do
65 -- Apply attribute rules to each decision (find) variable
66 (model2, toAddToRem) <- foldM (\modelAndToKeep findAndCstrs@((n, d), _) ->
67 foldM (\(m1, tatr1) (rule, name) -> do
68 (attrs, tatr2) <- nested rule m1 findAndCstrs
69 let m2 = foldr (uncurry3 addAttrsToModel) m1 attrs
70 when (((not (null attrs) && m1 /= m2) ||
71 (tatr2 /= mempty && toAddRem tatr2 tatr1 /= tatr1)) &&
72 logRuleSuccesses)
73 (log logLevel $ name <+> if null attrs
74 then vcat $ map (pretty . hole) (fst tatr2)
75 else pretty n <+> ":" <+> pretty d)
76 return (m2, toAddRem tatr2 tatr1))
77 modelAndToKeep [ (surjectiveIsTotalBijective, "function marked total and bijective")
78 , (totalInjectiveIsBijective, "function marked bijective")
79 , (definedForAllIsTotal, "function marked total")
80 , (diffArgResultIsInjective, "function marked injective")
81 , (varSize, "added or refined domain size attribute")
82 , (setSize, "added or refined set domain size attribute")
83 , (mSetSizeOccur, "added or refined multiset occurrence attribute")
84 , (mSetOccur, "added or refined multiset occurrence attribute")
85 , (partRegular, "marked partition regular")
86 , (numPartsToAttr, "added or refined partition domain numParts attribute")
87 , (partSizeToAttr, "added or refined partition domain partSize attribute")
88 , (funcRangeEqSet, "equated function range and set")
89 , (forAllIneqToIneqSum, "lifted arithmetic relation from two forAlls to a sum")
90 , (fasterIteration, "refined distinctness condition on forAll")
91 ])
92 (model1, ([], []))
93 (zip (collectFindVariables model1)
94 (repeat $ map zipper $ collectConstraints model1))
95
96 -- Apply constraint additions and removals
97 model3' <- resolveNames $
98 addConstraints (fst toAddToRem) $
99 remConstraints (snd toAddToRem) model2
100 model3 <- evaluateModel model3'
101
102 -- Apply type change rules to each decision (find) variable
103 (model4, toAddToRem') <- foldM (\modelAndToKeep findAndCstrs@((n, d), _) ->
104 foldM (\(m1, tatr1) (rule, name) -> do
105 (dom, tatr2) <- rule m1 findAndCstrs
106 when ((dom /= d || toAddRem tatr2 tatr1 /= tatr1) &&
107 logRuleSuccesses)
108 (log logLevel $ name <+> pretty n <+> ":" <+> pretty d)
109 return (updateDecl (n, dom) m1, toAddRem tatr2 tatr1))
110 modelAndToKeep [ (mSetToSet, "multiset changed to set")
111 -- , (relationToFunction, "relation to function")
112 ])
113 (model3, ([], []))
114 (zip (collectFindVariables model3)
115 (repeat $ map zipper $ collectConstraints model3))
116
117 -- Apply constraint additions and removals
118 model5' <- resolveNames $
119 addConstraints (fst toAddToRem') $
120 remConstraints (snd toAddToRem') model4
121 model5 <- evaluateModel model5'
122
123 -- Make another pass if the model was updated, but stop if it contains machine names
124 if model1 == model5 || any containsMachineName (collectConstraints model5)
125 then return model5
126 else core model5
127 -- Does an expression contain a reference with a machine name?
128 containsMachineName = any isMachineName . universe
129 isMachineName (Reference MachineName{} _) = True
130 isMachineName _ = False
131
132 -- | 'uncurry' for functions of three arguments and triples.
133 uncurry3 :: (a -> b -> c -> d) -> ((a, b, c) -> d)
134 uncurry3 f (x, y, z) = f x y z
135
136 -- | Collect decision (find) variables from a model, returning their name and domain.
137 collectFindVariables :: Model -> [FindVar]
138 collectFindVariables = mapMaybe collectFind . mStatements
139 where
140 collectFind (Declaration (FindOrGiven Find n d)) = Just (n, d)
141 collectFind _ = Nothing
142
143 -- | Collect the constraints in a model.
144 collectConstraints :: Model -> [Expression]
145 collectConstraints = concatMap getSuchThat . mStatements
146 where
147 getSuchThat (SuchThat cs) = cs
148 getSuchThat _ = []
149
150 -- | Add constraints to a model.
151 addConstraints :: [ExpressionZ] -> Model -> Model
152 addConstraints [] m = m
153 addConstraints cs m@Model { mStatements = stmts }
154 = m { mStatements = addConstraints' stmts }
155 where
156 addConstraints' (SuchThat cs':ss) = SuchThat (cs' `union` map fromZipper cs) : ss
157 addConstraints' (s:ss) = s : addConstraints' ss
158 addConstraints' [] = [SuchThat (map fromZipper cs)]
159
160 -- | Remove a list of constraints from a model.
161 remConstraints :: [ExpressionZ] -> Model -> Model
162 remConstraints cs m@Model { mStatements = stmts }
163 = m { mStatements = filter (not . emptySuchThat) $ map remConstraints' stmts }
164 where
165 remConstraints' (SuchThat cs') = SuchThat $ filter (`notElem` map fromZipper cs) cs'
166 remConstraints' s = s
167 emptySuchThat (SuchThat []) = True
168 emptySuchThat _ = False
169
170 -- | Update the domain of a declaration in a model.
171 updateDecl :: FindVar -> Model -> Model
172 updateDecl (n, d) m@Model { mStatements = stmts } = m { mStatements = map updateDecl' stmts }
173 where
174 updateDecl' (Declaration (FindOrGiven Find n' _))
175 | n == n' = Declaration (FindOrGiven Find n d)
176 updateDecl' decl = decl
177
178 -- | Try adding an attribute at a given depth of a variable's domain, in a model.
179 addAttrsToModel :: FindVar -> Int -> [AttrPair] -> Model -> Model
180 addAttrsToModel (n, _) depth attrs m
181 = let d = snd <$> find (\(n', _) -> n == n') (collectFindVariables m)
182 in case d >>= flip (addAttrsToDomain depth) attrs of
183 Just d' -> updateDecl (n, d') m
184 Nothing -> m
185 where
186 addAttrsToDomain :: (MonadFailDoc m) => Int -> Domain () Expression -> [AttrPair] -> m (Domain () Expression)
187 addAttrsToDomain 0 dom = addAttributesToDomain dom . map mkAttr
188 addAttrsToDomain level (DomainSet r as inner) = addAttrsToDomain (level - 1) inner >=> (pure . DomainSet r as)
189 addAttrsToDomain level (DomainMSet r as inner) = addAttrsToDomain (level - 1) inner >=> (pure . DomainMSet r as)
190 addAttrsToDomain level (DomainMatrix index inner) = addAttrsToDomain (level - 1) inner >=> (pure . DomainMatrix index)
191 addAttrsToDomain level (DomainFunction r as from inner) = addAttrsToDomain (level - 1) inner >=> (pure . DomainFunction r as from)
192 addAttrsToDomain level (DomainSequence r as inner) = addAttrsToDomain (level - 1) inner >=> (pure . DomainSequence r as)
193 addAttrsToDomain level (DomainPartition r as inner) = addAttrsToDomain (level - 1) inner >=> (pure . DomainPartition r as)
194 addAttrsToDomain _ _ = const (failDoc "[addAttrsToDomain] not a supported nested domain")
195 -- Special treatment for functions
196 mkAttr (attr, Just [essence| image(&f, &_) |]) = (attr, Just [essence| max(range(&f)) |])
197 mkAttr (attr, Just [essence| image(&f, &_) - 1 |]) = (attr, Just [essence| max(range(&f)) - 1 |])
198 mkAttr (attr, Just [essence| image(&f, &_) + 1 |]) = (attr, Just [essence| max(range(&f)) + 1 |])
199 mkAttr (attr, e') = (attr, e')
200
201 -- | Does an expression directly reference a given name variable?
202 nameExpEq :: Name -> Expression -> Bool
203 nameExpEq n (Reference n' _) = n == n'
204 nameExpEq n [essence| image(&f, &x) |] = nameExpEq n f || nameExpEq n x
205 nameExpEq n [essence| &f(&x) |] = nameExpEq n f || nameExpEq n x
206 nameExpEq n [essence| defined(&f) |] = nameExpEq n f
207 nameExpEq n [essence| range(&f) |] = nameExpEq n f
208 nameExpEq n [essence| |&x| |] = nameExpEq n x
209 nameExpEq _ _ = False
210
211 -- | Does a reference refer to an abstract pattern?
212 refersTo :: Expression -> AbstractPattern -> Bool
213 refersTo (Reference n _) a = n `elem` namesFromAbstractPattern a
214 refersTo _ _ = False
215
216 -- | Get a single name from an abstract pattern.
217 nameFromAbstractPattern :: (MonadFailDoc m) => AbstractPattern -> m Name
218 nameFromAbstractPattern a = case namesFromAbstractPattern a of
219 [n] -> pure n
220 [] -> failDoc "[nameFromAbstractPattern] no names in abstract pattern"
221 _ -> failDoc "[nameFromAbstractPattern] more than one name in abstract pattern"
222
223 -- | Get the list of names from an abstract pattern.
224 namesFromAbstractPattern :: AbstractPattern -> [Name]
225 namesFromAbstractPattern (Single n) = [n]
226 namesFromAbstractPattern (AbsPatTuple ns) = concatMap namesFromAbstractPattern ns
227 namesFromAbstractPattern (AbsPatMatrix ns) = concatMap namesFromAbstractPattern ns
228 namesFromAbstractPattern (AbsPatSet ns) = concatMap namesFromAbstractPattern ns
229 namesFromAbstractPattern _ = []
230
231 -- | Get the list of names from a generator.
232 namesFromGenerator :: Generator -> [Name]
233 namesFromGenerator (GenDomainNoRepr a _) = namesFromAbstractPattern a
234 namesFromGenerator (GenDomainHasRepr n _) = [n]
235 namesFromGenerator (GenInExpr a _) = namesFromAbstractPattern a
236
237 -- | Find an expression at any depth of unconditional forAll expressions.
238 findInUncondForAll :: (Expression -> Bool) -> [ExpressionZ] -> [Expression]
239 findInUncondForAll p = map hole . findInUncondForAllZ p
240
241 -- | Find an expression at any depth of unconditional forAll expressions,
242 -- returning a Zipper containing the expression's context.
243 findInUncondForAllZ :: (Expression -> Bool) -> [ExpressionZ] -> [ExpressionZ]
244 findInUncondForAllZ p = concatMap findInForAll
245 where
246 findInForAll z | p (hole z) = [z]
247 findInForAll z
248 = case hole z of
249 [essence| forAll &_ in defined(&_) . &_ |]
250 -> []
251 [essence| forAll &x, &y : &_, &x' != &y' . &_ |]
252 | x' `refersTo` x && y' `refersTo` y
253 -> maybe [] findInForAll (down z >>= down)
254 [essence| forAll &x, &y in &_, &x' != &y' . &_ |]
255 | x' `refersTo` x && y' `refersTo` y
256 -> maybe [] findInForAll (down z >>= down)
257 Op (MkOpAnd (OpAnd (Comprehension _ gorcs)))
258 | all (not . isCondition) gorcs
259 -> maybe [] findInForAll (down z >>= down)
260 [essence| &_ /\ &_ |]
261 -> maybe [] findInForAll (down z)
262 `union`
263 maybe [] findInForAll (right z >>= down)
264 -- Only accept OR cases if both sides contain a match
265 [essence| &_ \/ &_ |]
266 -> let leftResult = maybe [] findInForAll (down z)
267 rightResult = maybe [] findInForAll (right z >>= down)
268 in if not (null leftResult) && not (null rightResult)
269 then leftResult `union` rightResult
270 else []
271 _ -> []
272 isCondition Condition{} = True
273 isCondition _ = False
274
275 -- | Lens function over a binary expression.
276 type BinExprLens m = Proxy m -> (Expression -> Expression -> Expression,
277 Expression -> m (Expression, Expression))
278
279 -- | Get the lens for an expression and the values it matches.
280 matching :: Expression
281 -> [(BinExprLens Maybe, a)]
282 -> Maybe (a, (Expression, Expression))
283 matching e ops = case mapMaybe (\(f1, f2) -> (,) f2 <$> match f1 e) ops of
284 [x] -> pure x
285 _ -> failDoc $ "no matching operator for expression:" <+> pretty e
286
287 -- | (In)equality operator lens pairs.
288 ineqOps :: [(BinExprLens Maybe, BinExprLens Identity)]
289 ineqOps = [ (opEq, opEq)
290 , (opLt, opLt)
291 , (opLeq, opLeq)
292 , (opGt, opGt)
293 , (opGeq, opGeq)
294 ]
295
296 -- | Opposites of (in)equality operator lens pairs.
297 oppIneqOps :: [(BinExprLens Maybe, BinExprLens Identity)]
298 oppIneqOps = [ (opEq, opEq)
299 , (opLt, opGt)
300 , (opLeq, opGeq)
301 , (opGt, opLt)
302 , (opGeq, opLeq)
303 ]
304
305 -- | (In)equality operator to size attribute modifier pairs.
306 ineqSizeAttrs :: [(BinExprLens Maybe, (AttrName, Expression -> Maybe Expression))]
307 ineqSizeAttrs = [ (opEq, ("size", Just))
308 , (opLt, ("maxSize", Just . \x -> x - 1))
309 , (opLeq, ("maxSize", Just))
310 , (opGt, ("minSize", Just . (+ 1)))
311 , (opGeq, ("minSize", Just))
312 ]
313
314 -- | (In)equality operator to size attribute modifier pairs.
315 ineqOccurAttrs :: [(BinExprLens Maybe, [(AttrName, Expression -> Maybe Expression)])]
316 ineqOccurAttrs = [ (opEq, [ ("minOccur", Just), ("maxOccur", Just) ])
317 , (opLt, [ ("maxOccur", Just . \x -> x - 1) ])
318 , (opLeq, [ ("maxOccur", Just) ])
319 , (opGt, [ ("minOccur", Just . (+ 1)) ])
320 , (opGeq, [ ("minOccur", Just) ])
321 ]
322
323 -- | Unzip where the key is a 'Maybe' but the values should all be combined.
324 unzipMaybeK :: Monoid m => [(Maybe a, m)] -> ([a], m)
325 unzipMaybeK = foldr (\(mx, y) (xs, z) ->
326 case mx of
327 Just x -> (x:xs, y `mappend` z)
328 Nothing -> ( xs, y `mappend` z))
329 ([], mempty)
330
331 -- | Does an expression contain a find variable?
332 isFind :: Expression -> Bool
333 isFind (Reference _ (Just (DeclNoRepr Find _ _ _))) = True
334 isFind (Reference _ (Just (DeclHasRepr Find _ _))) = True
335 isFind Reference{} = False
336 isFind Constant{} = False
337 isFind [essence| &f(&_) |] = isFind f
338 isFind [essence| image(&f, &_) |] = isFind f
339 isFind e = any isFind $ children e
340
341 -- | Add expressions to the ToAdd list.
342 toAdd :: [ExpressionZ] -> ToAddToRem -> ToAddToRem
343 toAdd e = first (`union` e)
344
345 -- | Add expressions to the ToRemove list.
346 toRem :: [ExpressionZ] -> ToAddToRem -> ToAddToRem
347 toRem e = second (`union` e)
348
349 -- | Combine two 'ToAddToRem' values.
350 toAddRem :: ToAddToRem -> ToAddToRem -> ToAddToRem
351 toAddRem (ta, tr) = toAdd ta . toRem tr
352
353 -- | Apply a rule to arbitrary levels of nested domains.
354 nested :: (MonadFailDoc m, MonadLog m, NameGen m, ?typeCheckerMode :: TypeCheckerMode)
355 => (Model -> (FindVar, [ExpressionZ])
356 -> m ([AttrPair], ToAddToRem))
357 -> Model
358 -> (FindVar, [ExpressionZ])
359 -> m ([(FindVar, Int, [AttrPair])], ToAddToRem)
360 nested rule m fc@(fv, cs) = do
361 -- Apply the rule at the top level
362 (attrs, toAddToRem) <- rule m fc
363 -- Look deeper into the domain if possible, for forAll constraints involving it
364 nestedResults <- fmap mconcat $ forM cs $ \c ->
365 case hole c of
366 [essence| forAll &x in &gen . &_ |] | nameExpEq (fst fv) gen ->
367 -- Create the new decision variable at this level
368 case (,) <$> nameFromAbstractPattern x
369 <*> (domainOf gen >>= innerDomainOf) of
370 Left _ -> return mempty
371 Right fv' -> do
372 -- Apply the rule from here
373 out <- nested rule m (fv', mapMaybe (down >=> down) [c])
374 case out of
375 ([], _) -> return mempty
376 -- The rule was applied, so unwrap the variable and increase the depth
377 (vs, tatr') -> return ( [ (fv, d + 1, as) | (_, d, as) <- vs ]
378 , tatr')
379 _ -> return mempty
380 -- Do not add a modification if there are no attributes
381 let attrs' = if null attrs then [] else [(fv, 0, attrs)]
382 return $ mappend nestedResults (attrs', toAddToRem)
383
384 -- | If a function is surjective or bijective, and its domain and codomain
385 -- are of equal size, then it is total and bijective.
386 surjectiveIsTotalBijective :: (MonadFailDoc m, MonadLog m)
387 => Model
388 -> (FindVar, [ExpressionZ])
389 -> m ([AttrPair], ToAddToRem)
390 surjectiveIsTotalBijective _ ((_, dom), _)
391 = case dom of
392 DomainFunction _ (FunctionAttr _ p j) from to
393 | (p == PartialityAttr_Partial && j == JectivityAttr_Bijective) ||
394 j == JectivityAttr_Surjective -> do
395 (fromSize, toSize) <- functionDomainSizes from to
396 if fromSize == toSize
397 then return ([("total", Nothing), ("bijective", Nothing)], mempty)
398 else return mempty
399 DomainSequence _ (SequenceAttr (SizeAttr_Size s ) j) to
400 | j `elem` [JectivityAttr_Bijective, JectivityAttr_Surjective] -> do
401 toSize <- domainSizeOf to
402 if s == toSize
403 then return ([("bijective", Nothing)], mempty)
404 else return mempty
405 _ -> return mempty
406
407 -- | Calculate the sizes of the domain and codomain of a function.
408 functionDomainSizes :: (MonadFailDoc m)
409 => Domain () Expression -- ^ The function's domain.
410 -> Domain () Expression -- ^ The function's codomain.
411 -> m (Expression, Expression) -- ^ The sizes of the two.
412 functionDomainSizes from to = (,) <$> domainSizeOf from <*> domainSizeOf to
413
414 -- | If a function is total and injective, and its domain and codomain
415 -- are of equal size, then it is bijective.
416 totalInjectiveIsBijective :: (MonadFailDoc m, MonadLog m)
417 => Model
418 -> (FindVar, [ExpressionZ])
419 -> m ([AttrPair], ToAddToRem)
420 totalInjectiveIsBijective _ ((_, dom), _)
421 = case dom of
422 DomainFunction _ (FunctionAttr _ PartialityAttr_Total JectivityAttr_Injective) from to -> do
423 (fromSize, toSize) <- functionDomainSizes from to
424 if fromSize == toSize
425 then return ([("bijective", Nothing)], mempty)
426 else return mempty
427 _ -> return mempty
428
429 -- | If a function is defined for all values in its domain, then it is total.
430 definedForAllIsTotal :: (MonadFailDoc m, MonadLog m, ?typeCheckerMode :: TypeCheckerMode)
431 => Model
432 -> (FindVar, [ExpressionZ])
433 -> m ([AttrPair], ToAddToRem)
434 definedForAllIsTotal _ ((n, dom), cs)
435 -- Is the function called with parameters generated from its domain in an expression?
436 = let definedIn from e = any (funcCalledWithGenParams from) (children e)
437 in case dom of
438 DomainFunction _ (FunctionAttr _ PartialityAttr_Partial _) from _
439 | any (definedIn from) $ findInUncondForAll isOp cs
440 -> return ([("total", Nothing)], mempty)
441 _ -> return mempty
442 where
443 -- Look for operator expressions but leave comprehensions, ANDs and ORs up to findInUncondForAll
444 isOp (Op (MkOpAnd (OpAnd Comprehension{}))) = False
445 isOp [essence| &_ /\ &_ |] = False
446 isOp [essence| &_ \/ &_ |] = False
447 -- Disallow implications which may remove some cases
448 isOp [essence| &_ -> &_ |] = False
449 isOp Op{} = True
450 isOp _ = False
451 -- Determine whether a function is called with values generated from its domain
452 funcCalledWithGenParams d [essence| image(&f, ¶m) |]
453 = nameExpEq n f && case domainOf param of
454 Right d' -> d' == d
455 Left _ -> False
456 funcCalledWithGenParams _ _ = False
457
458 -- | If all distinct inputs to a function have distinct results, then it is injective.
459 -- It will also be total if there are no conditions other than the disequality between
460 -- the two inputs.
461 diffArgResultIsInjective :: (MonadFailDoc m, MonadLog m, ?typeCheckerMode :: TypeCheckerMode)
462 => Model
463 -> (FindVar, [ExpressionZ])
464 -> m ([AttrPair], ToAddToRem)
465 diffArgResultIsInjective _ ((n, DomainFunction _ (FunctionAttr _ _ ject) from _), cs)
466 | (ject == JectivityAttr_None || ject == JectivityAttr_Surjective) &&
467 not (null $ findInUncondForAll isDistinctDisequality cs)
468 -- It is known that no inputs are ignored
469 = return ([("injective", Nothing), ("total", Nothing)], mempty)
470 where
471 -- Match a very specific pattern, which will also add the total attribute
472 isDistinctDisequality [essence| &i != &j -> image(&f, &i') != image(&f', &j') |]
473 = f == f' && i == i' && j == j' &&
474 nameExpEq n f && -- the function is the one under consideration
475 domIsGen i && domIsGen j -- the values are generated from the function's domain
476 isDistinctDisequality _ = False
477 domIsGen x = case domainOf x of
478 Right dom -> dom == from
479 Left _ -> False
480 diffArgResultIsInjective _ _ = return mempty
481
482 -- | Set a size attribute on a variable.
483 varSize :: (MonadFailDoc m, MonadLog m)
484 => Model
485 -> (FindVar, [ExpressionZ])
486 -> m ([AttrPair], ToAddToRem)
487 varSize _ ((n, _), cs) = do
488 results <- forM cs $ \c ->
489 case matching (hole c) ineqSizeAttrs of
490 -- Do not allow find variables to be put in attributes
491 Just ((attr, f), (cardinalityOf -> Just x, e)) | nameExpEq n x && not (isFind e)
492 -> pure (Just (attr, f e), ([], [c]))
493 _ -> pure (Nothing, mempty)
494 return $ unzipMaybeK results
495
496
497 cardinalityOf :: Expression -> Maybe Expression
498 cardinalityOf [essence| |&x| |] = Just x
499 cardinalityOf [essence| sum([1 | &_ <- &x]) |] = Just x
500 cardinalityOf _ = Nothing
501
502
503 -- | Set the minimum size of a set based on it being a superset of another.
504 setSize :: (MonadFailDoc m, MonadLog m, NameGen m, ?typeCheckerMode :: TypeCheckerMode)
505 => Model
506 -> (FindVar, [ExpressionZ])
507 -> m ([AttrPair], ToAddToRem)
508 setSize _ ((n, DomainSet{}), cs)
509 = fmap mconcat $ forM (findInUncondForAllZ isSubSupSet cs) $ \c ->
510 case hole c of
511 -- subset(Eq)
512 [essence| &l subset &r |] | nameExpEq n r -> return (minSize l (+ 1), mempty)
513 [essence| &l subset &r |] | nameExpEq n l -> return (maxSize r (\x -> x - 1), mempty)
514 [essence| &l subsetEq &r |] | nameExpEq n r -> return (minSize l id, mempty)
515 [essence| &l subsetEq &r |] | nameExpEq n l -> return (maxSize r id, mempty)
516 -- supset(Eq)
517 [essence| &l supset &r |] | nameExpEq n l -> return (minSize r (+ 1), mempty)
518 [essence| &l supset &r |] | nameExpEq n r -> return (maxSize l (\x -> x - 1), mempty)
519 [essence| &l supsetEq &r |] | nameExpEq n l -> return (minSize r id, mempty)
520 [essence| &l supsetEq &r |] | nameExpEq n r -> return (maxSize l id, mempty)
521 _ -> return mempty
522 where
523 isSubSupSet [essence| &_ subset &_ |] = True
524 isSubSupSet [essence| &_ subsetEq &_ |] = True
525 isSubSupSet [essence| &_ supset &_ |] = True
526 isSubSupSet [essence| &_ supsetEq &_ |] = True
527 isSubSupSet _ = False
528 minSize [essence| defined(&g) |] f
529 = case domainOf g of
530 Right (DomainFunction _ (FunctionAttr _ PartialityAttr_Total _) from _) ->
531 case domainSizeOf from of
532 Just s -> [("minSize", Just (f s))]
533 Nothing -> mempty
534 _ -> mempty
535 minSize [essence| range(&g) |] f
536 = case domainOf g of
537 Right (DomainFunction _ (FunctionAttr _ PartialityAttr_Total j) from to)
538 | j == JectivityAttr_Bijective || j == JectivityAttr_Surjective ->
539 case domainSizeOf to of
540 Just s -> [("minSize", Just (f s))]
541 Nothing -> mempty
542 | j == JectivityAttr_Injective ->
543 case domainSizeOf from of
544 Just s -> [("minSize", Just (f s))]
545 Nothing -> mempty
546 | otherwise -> [("minSize", Just (f 1))]
547 _ -> mempty
548 minSize e f = case domainOf e of
549 Right (DomainSet _ (SetAttr (SizeAttr_Size mn)) _) ->
550 [("minSize", Just (f mn))]
551 Right (DomainSet _ (SetAttr (SizeAttr_MinSize mn)) _) ->
552 [("minSize", Just (f mn))]
553 Right (DomainSet _ (SetAttr (SizeAttr_MinMaxSize mn _)) _) ->
554 [("minSize", Just (f mn))]
555 _ -> mempty
556 -- TODO: extend for Matrix, MSet, Partition and Sequence
557 maxSize [essence| defined(&g) |] f
558 = case domainOf g >>= innerDomainOf of
559 Right (DomainTuple [d, _]) ->
560 case domainSizeOf d of
561 Just s -> [("maxSize", Just (f s))]
562 Nothing -> mempty
563 _ -> mempty
564 maxSize [essence| range(&g) |] f
565 = case domainOf g >>= innerDomainOf of
566 Right (DomainTuple [_, d]) ->
567 case domainSizeOf d of
568 Just s -> [("maxSize", Just (f s))]
569 Nothing -> mempty
570 _ -> mempty
571 maxSize e f = case domainOf e of
572 Right (DomainSet _ (SetAttr (SizeAttr_Size mx)) _) ->
573 [("maxSize", Just (f mx))]
574 Right (DomainSet _ (SetAttr (SizeAttr_MaxSize mx)) _) ->
575 [("maxSize", Just (f mx))]
576 Right (DomainSet _ (SetAttr (SizeAttr_MinMaxSize _ mx)) _) ->
577 [("maxSize", Just (f mx))]
578 Right d@(DomainSet _ (SetAttr SizeAttr_None) _) ->
579 case domainSizeOf d of
580 Just mx -> [("maxSize", Just (f mx))]
581 Nothing -> mempty
582 _ -> mempty
583 -- TODO: extend for Matrix, MSet, Partition and Sequence
584 setSize _ _ = return mempty
585
586 -- | The maxSize, and minOccur attributes of an mset affect its maxOccur and minSize attributes.
587 mSetSizeOccur :: (MonadFailDoc m, MonadLog m)
588 => Model
589 -> (FindVar, [ExpressionZ])
590 -> m ([AttrPair], ToAddToRem)
591 mSetSizeOccur _ ((_, d), _)
592 = case d of
593 -- Ordering is important here, as there is a rule that applies
594 -- to maxSize and minOccur, but none that applies to minSize
595 -- and maxOccur. size uses the maxSize rule, but can ignore a
596 -- minOccur because it cannot have its minSize changed.
597 -- size -> maxOccur
598 DomainMSet _ (MSetAttr (SizeAttr_Size mx) _) _
599 -> return ([("maxOccur", Just mx)], mempty)
600 -- minOccur -> minSize
601 DomainMSet _ (MSetAttr _ (OccurAttr_MinOccur mn)) _
602 -> return ([("minSize", Just mn)], mempty)
603 DomainMSet _ (MSetAttr _ (OccurAttr_MinMaxOccur mn _)) _
604 -> return ([("minSize", Just mn)], mempty)
605 -- maxSize -> maxOccur
606 DomainMSet _ (MSetAttr (SizeAttr_MaxSize mx) _) _
607 -> return ([("maxOccur", Just mx)], mempty)
608 DomainMSet _ (MSetAttr (SizeAttr_MinMaxSize _ mx) _) _
609 -> return ([("maxOccur", Just mx)], mempty)
610 _ -> return mempty
611
612 -- | Infer multiset occurrence attributes from constraints.
613 mSetOccur :: (MonadFailDoc m, MonadLog m)
614 => Model
615 -> (FindVar, [ExpressionZ])
616 -> m ([AttrPair], ToAddToRem)
617 mSetOccur _ ((n, DomainMSet _ _ d), cs)
618 = return $ mconcat $ flip mapMaybe (findInUncondForAllZ (not . null . isFreq) cs) $ \e ->
619 case isFreq (hole e) of
620 [] -> Nothing
621 -- Only remove constraints if they are all used up.
622 -- Because freq(a, b) = c adds two attributes, removing constraints
623 -- in an AND expression cannot work, in the case of freq(a, b) = c /\ e
624 -- because there are two attributes and two terms, but term e may not
625 -- be removed.
626 as -> let tattr = case hole e of
627 AbstractLiteral AbsLitMatrix{} -> mempty
628 _ -> ([], [e])
629 in Just (as, tattr)
630 where
631 isFreq :: Expression -> [AttrPair]
632 isFreq (AbstractLiteral (AbsLitMatrix _ es)) = concatMap isFreq es
633 isFreq e = case matching e oppIneqOps of
634 Just (_, ([essence| freq(&x, &v) |], e'))
635 | valid x v e' -> case matching e ineqOccurAttrs of
636 Just (as, _) -> map (second ($ e')) as
637 Nothing -> []
638 -- Flip the terms
639 Just (oper, (l, r@[essence| freq(&x, &v) |]))
640 | valid x v l -> isFreq $ make oper r l
641 _ -> []
642 -- Make sure that the expression's components are valid
643 valid :: Expression -> Expression -> Expression -> Bool
644 valid x v e = nameExpEq n x && isGen v && isConst e
645 -- Make sure that the value is generated from the mset's domain
646 isGen (Reference _ (Just (InComprehension (GenDomainNoRepr _ d')))) = d == d'
647 isGen (Reference _ (Just (DeclNoRepr Quantified _ d' _))) = d == d'
648 isGen (Reference _ (Just (InComprehension (GenInExpr _ e )))) = nameExpEq n e
649 isGen _ = False
650 -- Make sure that the mset is being equated to a constant
651 isConst (Reference _ (Just (DeclNoRepr Given _ _ _))) = True
652 isConst (Constant ConstantInt{}) = True
653 isConst _ = False
654 mSetOccur _ _ = return mempty
655
656 -- | Mark a partition regular if there is a constraint on its parts constraining them to be of equal size.
657 partRegular :: (MonadFailDoc m, MonadLog m, ?typeCheckerMode :: TypeCheckerMode)
658 => Model
659 -> (FindVar, [ExpressionZ])
660 -> m ([AttrPair], ToAddToRem)
661 partRegular _ ((_, DomainPartition{}), cs) = do
662 attrs <- forM cs $ \c ->
663 case hole c of
664 -- [essence| forAll &x in parts(&p) . forAll &y in parts(&p') . &xCard = &yCard |]
665 [essence| and([ &xCard = &yCard | &x <- parts(&p), &y <- parts(&p') ]) |]
666 | Just (Reference x' _) <- cardinalityOf xCard
667 , Just (Reference y' _) <- cardinalityOf yCard
668 , or [ and [x == Single x', y == Single y']
669 , and [x == Single y', y == Single x']
670 ]
671 , p == p'
672 -> pure (Just ("regular", Nothing), ([], [c]))
673 _ -> pure (Nothing, mempty)
674 return $ unzipMaybeK attrs
675 partRegular _ _ = return mempty
676
677
678 -- | Convert constraints acting on the number of parts in a partition to an attribute.
679 numPartsToAttr :: (MonadFailDoc m, MonadLog m)
680 => Model
681 -> (FindVar, [ExpressionZ])
682 -> m ([AttrPair], ToAddToRem)
683 numPartsToAttr _ ((n, DomainPartition{}), cs) = do
684 attrs <- forM cs $ \c ->
685 case matching (hole c) ineqSizeAttrs of
686 -- Do not allow find variables to be put in attributes
687 Just ((attr, f), ([essence| |parts(&x)| |], e)) | nameExpEq n x && not (isFind e)
688 -> pure (Just (changeAttr attr, f e), ([], [c]))
689 _ -> pure (Nothing, mempty)
690 return $ unzipMaybeK attrs
691 where
692 -- Change a size attribute name to a numParts attribute name
693 changeAttr "size" = "numParts"
694 changeAttr "minSize" = "minNumParts"
695 changeAttr "maxSize" = "maxNumParts"
696 changeAttr a = a
697 numPartsToAttr _ _ = return mempty
698
699 -- | Convert constraints acting on the sizes of parts in a partition to an attribute.
700 partSizeToAttr :: (MonadFailDoc m, MonadLog m)
701 => Model
702 -> (FindVar, [ExpressionZ])
703 -> m ([AttrPair], ToAddToRem)
704 partSizeToAttr _ ((n, DomainPartition{}), cs) = do
705 attrs <- forM cs $ \c ->
706 case hole c of
707 [essence| forAll &x in parts(&p) . &xCard = &e |]
708 | Just x' <- cardinalityOf xCard
709 , valid p x x' e
710 -> pure (Just ("partSize", Just e), ([], [c]))
711 [essence| forAll &x in parts(&p) . &xCard < &e |]
712 | Just x' <- cardinalityOf xCard
713 , valid p x x' e
714 -> pure (Just ("maxPartSize", Just (e - 1)), ([], [c]))
715 [essence| forAll &x in parts(&p) . &xCard <= &e |]
716 | Just x' <- cardinalityOf xCard
717 , valid p x x' e
718 -> pure (Just ("maxPartSize", Just e), ([], [c]))
719 [essence| forAll &x in parts(&p) . &xCard > &e |]
720 | Just x' <- cardinalityOf xCard
721 , valid p x x' e
722 -> pure (Just ("minPartSize", Just (e + 1)), ([], [c]))
723 [essence| forAll &x in parts(&p) . &xCard >= &e |]
724 | Just x' <- cardinalityOf xCard
725 , valid p x x' e
726 -> pure (Just ("minPartSize", Just e), ([], [c]))
727 _ -> pure (Nothing, mempty)
728 return $ unzipMaybeK attrs
729 where
730 -- Make sure that the expression's components are valid
731 valid :: Expression -> AbstractPattern -> Expression -> Expression -> Bool
732 valid p x v e = nameExpEq n p && v `refersTo` x && not (isFind e)
733 partSizeToAttr _ _ = return mempty
734
735 -- | Equate the range of a function to a set of the former is a subset of the latter
736 -- and all values in the set are results of the function.
737 funcRangeEqSet :: (MonadFailDoc m, MonadLog m)
738 => Model
739 -> (FindVar, [ExpressionZ])
740 -> m ([AttrPair], ToAddToRem)
741 funcRangeEqSet _ ((n, DomainSet{}), cs)
742 -- Get references to the set and the function whose range it is a superset of
743 = let funcSubsets = mapMaybe funcSubsetEqOf $
744 findInUncondForAllZ (isJust . funcSubsetEqOf . zipper) cs
745 -- Reduce the functions to those whose values are equated to the values in the set
746 fsToUse = flip filter funcSubsets $ \(_, f) ->
747 not $ null $ findInUncondForAll (funcValEqSetVal (hole f)) cs
748 -- Transform the functions into new constraints, preserving structure
749 csToAdd = flip mapMaybe fsToUse $ \(s, f) ->
750 let f' = hole f
751 in replaceHole [essence| range(&f') = &s |] <$>
752 (up f >>= up)
753 in return ([], (csToAdd, []))
754 where
755 -- Get the function whose range is a subsetEq of the set
756 funcSubsetEqOf z = case hole z of
757 [essence| range(&_) subsetEq &s |] | nameExpEq n s
758 -> (,) s <$> (down z >>= down)
759 [essence| &s supsetEq range(&_) |] | nameExpEq n s
760 -> (,) s <$> (down z >>= right >>= down)
761 _ -> Nothing
762 -- Are the values of the function equal to the values of the set?
763 funcValEqSetVal f [essence| forAll &x in &s . image(&f', &_) = &x' |]
764 = nameExpEq n s && f == f' && x' `refersTo` x
765 funcValEqSetVal f [essence| forAll &x in &s . &x' = image(&f', &_) |]
766 = nameExpEq n s && f == f' && x' `refersTo` x
767 funcValEqSetVal _ _ = False
768 funcRangeEqSet _ _ = return mempty
769
770
771 -- | An (in)equality in a forAll implies that the (in)equality also applies to
772 -- the sums of both terms.
773 forAllIneqToIneqSum :: (MonadFailDoc m, MonadLog m, NameGen m, ?typeCheckerMode :: TypeCheckerMode)
774 => Model
775 -> (FindVar, [ExpressionZ])
776 -> m ([AttrPair], ToAddToRem)
777 forAllIneqToIneqSum _ (_, cs) = do
778 let matches = mapMaybe matchParts $ findInUncondForAllZ (isJust . matchParts . zipper) cs
779 csToAdd <- mapMaybe mkConstraint <$> filterM partsAreNumeric matches
780 return ([], (csToAdd, []))
781 where
782 -- Match and extract the desired parts of the expression
783 matchParts :: ExpressionZ -> Maybe (Generator, Maybe ExpressionZ, Expression, Expression)
784 matchParts z = case hole z of
785 Op (MkOpAnd (OpAnd (Comprehension e [Generator g])))
786 -> matching e ineqOps >>=
787 uncurry (matchComponents g z) . snd
788 _ -> Nothing
789 -- Match the components of the expression of interest
790 matchComponents :: Generator -> ExpressionZ -> Expression -> Expression
791 -> Maybe (Generator, Maybe ExpressionZ, Expression, Expression)
792 matchComponents g z e1 e2
793 | refInExpr (namesFromGenerator g) e1 && refInExpr (namesFromGenerator g) e2
794 = Just (g, down z >>= down, e1, e2)
795 matchComponents _ _ _ _ = Nothing
796 -- Is a name referred to in an expression?
797 refInExpr names = any (\e -> any (`nameExpEq` e) names) . universe
798 -- Are the parts of the matched expression numeric?
799 partsAreNumeric (_, _, e1, e2) = (&&) <$> domainIsNumeric e1 <*> domainIsNumeric e2
800 domainIsNumeric e = case domainOf e of
801 Right DomainInt{} -> return True
802 Right (DomainAny _ (TypeInt _)) -> return True
803 _ -> return False
804 -- Replace the forAll with the (in)equality between sums
805 mkConstraint :: (Generator, Maybe ExpressionZ, Expression, Expression) -> Maybe ExpressionZ
806 mkConstraint (gen, Just z, _, _)
807 -- Use matching with ineqOps to get the operation that is used on the two expressions
808 = case matching (hole z) ineqOps of
809 Just (f, (e1, e2))
810 -> let mkSumOf = Op . MkOpSum . OpSum . flip Comprehension [Generator gen]
811 -- Two steps to get out of the forAll, and replace it with the constraint
812 in replaceHole (make f (mkSumOf e1) (mkSumOf e2)) <$> (up z >>= up)
813 _ -> Nothing
814 mkConstraint _ = Nothing
815
816 -- | Iterate slightly faster over a domain if generating two distinct variables.
817 fasterIteration :: (MonadFailDoc m, MonadFailDoc m,MonadIO m, MonadLog m, ?typeCheckerMode :: TypeCheckerMode)
818 => Model
819 -> (FindVar, [ExpressionZ])
820 -> m ([AttrPair], ToAddToRem)
821 fasterIteration m (_, cs) = do
822 let iters = findInUncondForAllZ (isJust . doubleDistinctIter . zipper) cs
823 fmap ((,) [] . mconcat) $ forM iters $ \z -> do
824 -- Find the equivalent variables
825 [equivs] <- sequence [ findEquivVars (hole z) ]
826 -- Only apply to equivalent variables and make the new constraint
827 case doubleDistinctIter z >>= onlyEquivalent equivs >>= changeIterator of
828 Nothing -> return mempty
829 -- Remove the old constraint
830 Just z' -> return ([z'], [z])
831 where
832 -- Match the elemenents of interest in the constraint
833 doubleDistinctIter z
834 = case hole z of
835 Op (MkOpAnd (OpAnd (Comprehension _ [ Generator (GenInExpr x v)
836 , Generator (GenInExpr y v')
837 , Condition [essence| &x' != &y' |]
838 ])))
839 | v == v' && x' `refersTo` x && y' `refersTo` y
840 -> Just ((x, x'), (y, y'), v, down z >>= down)
841 Op (MkOpAnd (OpAnd (Comprehension _ [ Generator (GenDomainNoRepr x d)
842 , Generator (GenDomainNoRepr y d')
843 , Condition [essence| &x' != &y' |]
844 ])))
845 | d == d' && x' `refersTo` x && y' `refersTo` y
846 -> Just ((x, x'), (y, y'), Domain d, down z >>= down)
847 _ -> Nothing
848 -- Find which variables are equivalent in an expression
849 findEquivVars :: (MonadIO m) => Expression -> m (Map Text Text)
850 findEquivVars e = case e of
851 [essence| forAll &_, &_ : &_, &_ . &e' |] -> liftIO $ findSyms e'
852 [essence| forAll &_, &_ in &_, &_ . &e' |] -> liftIO $ findSyms e'
853 _ -> return M.empty
854 -- Find the symmetries in an expression
855 findSyms :: Expression -> IO (Map Text Text)
856 findSyms e = do
857 let m' = addConstraints [zipper e] $ remConstraints cs m
858 let filename = ".tmp-variable-strengthening.json"
859 outputVarSymBreaking filename m'
860 symmetries <- ferret $ stringToText filename
861 removeFile filename
862 case (JSON.decodeStrict $ T.encodeUtf8 symmetries) :: Maybe [Map Text Text] of
863 Nothing -> return M.empty
864 Just ss -> return $ foldr M.union M.empty ss
865 -- Only perform the modification if the variables are equivalent in the expression
866 onlyEquivalent es v@((x, _), (y, _), _, _)
867 = case namesFromAbstractPattern x of
868 [Name nx] -> case namesFromAbstractPattern y of
869 [Name ny] -> case es M.!? nx of
870 Just ny' | ny == ny' -> Just v
871 _ -> Nothing
872 _ -> Nothing
873 _ -> Nothing
874 -- Change the iterator to use the new, faster notation
875 changeIterator ((x, x'), (y, y'), v, Just z)
876 = let e = hole z
877 in case v of
878 r@Reference{}
879 -> case domainOf r of
880 Left _ -> Nothing
881 Right DomainSet{}
882 -> replaceHole [essence| forAll {&x, &y} subsetEq &v . &e |] <$>
883 (up z >>= up)
884 Right _
885 -> replaceHole [essence| forAll &x, &y in &v, &y' > &x' . &e |] <$>
886 (up z >>= up)
887 Op MkOpDefined{}
888 -> replaceHole [essence| forAll &x, &y in &v, &y' > &x' . &e |] <$>
889 (up z >>= up)
890 Domain d
891 -> replaceHole [essence| forAll &x, &y : &d, &y' > &x' . &e |] <$>
892 (up z >>= up)
893 _ -> Nothing
894 changeIterator _ = Nothing
895
896 -- | Call ferret's symmetry detection on a JSON file
897 ferret :: Text -> IO Text
898 ferret path = sh (run "symmetry_detect" [ "--json", path ]) `catch`
899 (\(_ :: SomeException) -> return "{}")
900
901 -- | Change the type of a multiset with `maxOccur 1` to set.
902 mSetToSet :: (MonadFailDoc m, MonadLog m)
903 => Model
904 -> (FindVar, [ExpressionZ])
905 -> m (Domain () Expression, ToAddToRem)
906 mSetToSet _ ((n, DomainMSet r (MSetAttr sa oa) d), cs) | maxOccur1 oa = do
907 let dom' = DomainSet r (SetAttr sa) d
908 let torem = filter (any (nameExpEq n) . universe . hole) cs
909 let toadd = map (zipper . transform (\e -> if nameExpEq n e
910 then [essence| toMSet(&e) |]
911 else e)
912 . hole)
913 cs
914 return (dom', (toadd, torem))
915 where
916 maxOccur1 (OccurAttr_MaxOccur 1) = True
917 maxOccur1 (OccurAttr_MinMaxOccur _ 1) = True
918 maxOccur1 _ = False
919 mSetToSet _ ((_, dom), _) = return (dom, mempty)
920
921 -- relationToFunction ::
922 -- MonadFailDoc m =>
923 -- MonadLog m =>
924 -- Model ->
925 -- (FindVar, [ExpressionZ]) ->
926 -- m (Domain () Expression, ToAddToRem)
927 -- -- relationToFunction _ ((n, DomainRelation r (MSetAttr sa oa) d), cs) | maxOccur1 oa = do
928 -- -- let dom' = DomainSet r (SetAttr sa) d
929 -- -- let torem = filter (any (nameExpEq n) . universe . hole) cs
930 -- -- let toadd = map (zipper . transform (\e -> if nameExpEq n e
931 -- -- then [essence| toMSet(&e) |]
932 -- -- else e)
933 -- -- . hole)
934 -- -- cs
935 -- -- return (dom', (toadd, torem))
936 -- -- where
937 -- -- maxOccur1 (OccurAttr_MaxOccur 1) = True
938 -- -- maxOccur1 (OccurAttr_MinMaxOccur _ 1) = True
939 -- -- maxOccur1 _ = False
940 -- relationToFunction _ ((_, dom), _) = return (dom, mempty)