Skip to content

Commit

Permalink
constrained-generators: Fix test failure with narrowing
Browse files Browse the repository at this point in the history
  • Loading branch information
MaximilianAlgehed committed Nov 18, 2024
1 parent 6337f6f commit 03c1bdf
Show file tree
Hide file tree
Showing 2 changed files with 31 additions and 15 deletions.
33 changes: 18 additions & 15 deletions libs/constrained-generators/src/Constrained/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -3209,7 +3209,7 @@ narrowByFuelAndSize ::
(Specification fn a, Specification fn a) ->
(Specification fn a, Specification fn a)
narrowByFuelAndSize fuel size specs =
loop (1000 :: Int) (narrowFoldSpecs specs)
loop (100 :: Int) (onlyOnceTransformations $ narrowFoldSpecs specs)
where
loop 0 specs =
error $
Expand All @@ -3225,6 +3225,13 @@ narrowByFuelAndSize fuel size specs =
Nothing -> specs
Just specs' -> loop (n - 1) (narrowFoldSpecs specs')

-- Transformations only applied once. It's annoying to check if you're
-- going to change the spec with these so easier to just make sure you only apply
-- these once
onlyOnceTransformations (elemS, foldS)
| fuel == 1 = (elemS <> foldS, foldS)
| otherwise = (elemS, foldS)

canReach _ 0 s = s == 0
canReach e fuel s
-- You can reach it in one step
Expand All @@ -3246,9 +3253,11 @@ narrowByFuelAndSize fuel size specs =
where
d = a `div` b

go (elemS, foldS)
go (simplifySpec -> elemS, simplifySpec -> foldS)
-- There is nothing we can do
| fuel == 0 = Nothing
| ErrorSpec {} <- elemS = Nothing
| ErrorSpec {} <- foldS = Nothing
-- Give up as early as possible
| Just 0 <- knownUpperBound elemS
, Just 0 <- knownLowerBound elemS
Expand Down Expand Up @@ -3285,31 +3294,25 @@ narrowByFuelAndSize fuel size specs =
, Just s <- knownUpperBound foldS
, s < 0
, let c = divCeil (safeNegate s) fuel
, negate c < e =
, negate c < e
, maybe True (c <) (knownUpperBound elemS) =
Just (elemS <> leqSpec @fn c, foldS)
-- It's time to stop generating negative numbers
| Just s <- knownLowerBound foldS
, s > 0
, Just e <- knownUpperBound elemS
, e > 0
, not $ canReach e (fuel `div` 2) s
, not $ canReach e (fuel `div` 2 + 1) s
, maybe True (<= 0) (knownLowerBound elemS) =
Just (elemS <> gtSpec @fn 0, foldS)
-- It's time to stop generating positive numbers
| Just s <- knownUpperBound foldS
, s < 0
, Just e <- knownLowerBound elemS
, e < 0
, not $ canReach (safeNegate e) (fuel `div` 2) (safeNegate s)
, maybe True (<= 0) (knownLowerBound elemS) =
Just (elemS <> gtSpec @fn 0, foldS)
-- We HAVE to set the lower bound to the lower
-- bound on the sum
| Just s <- knownLowerBound foldS
, fuel == 1
, s `conformsToSpec` elemS
, maybe True (< s) (knownLowerBound elemS) =
Just (elemS <> geqSpec @fn s, foldS)
, not $ canReach (safeNegate e) (fuel `div` 2 + 1) (safeNegate s)
, maybe True (0 <=) (knownUpperBound elemS) =
Just (elemS <> ltSpec @fn 0, foldS)
-- There is nothing we need to do
| otherwise = Nothing

Expand All @@ -3329,7 +3332,7 @@ narrowFoldSpecs ::
narrowFoldSpecs specs = maybe specs narrowFoldSpecs (go specs)
where
-- Note: make sure there is some progress when returning Just or this will loop forever
go (elemS, foldS) = case (elemS, foldS) of
go (simplifySpec -> elemS, simplifySpec -> foldS) = case (elemS, foldS) of
-- Empty foldSpec
(_, ErrorSpec {}) -> Nothing
_ | isEmptyNumSpec foldS -> Just (elemS, ErrorSpec (NE.fromList ["Empty foldSpec:", show foldS]))
Expand Down
13 changes: 13 additions & 0 deletions libs/constrained-generators/test/Constrained/Test.hs
Original file line number Diff line number Diff line change
Expand Up @@ -182,6 +182,7 @@ tests nightly =
prop "[(Set Int, Set Bool)]" $ prop_gen_sound @BaseFn @[(Set Int, Set Bool)]
prop "Set (Set Bool)" $ prop_gen_sound @BaseFn @(Set (Set Bool))
negativeTests
prop "prop_noNarrowLoop" $ withMaxSuccess 1000 prop_noNarrowLoop

negativeTests :: Spec
negativeTests =
Expand Down Expand Up @@ -369,3 +370,15 @@ hasSizeSet = hasSize (rangeSize 1 3)

hasSizeMap :: Specification BaseFn (Map Int Int)
hasSizeMap = hasSize (rangeSize 1 3)

------------------------------------------------------------------------
-- Tests for narrowing
------------------------------------------------------------------------

prop_noNarrowLoop :: Int -> Int -> Specification BaseFn Int -> Specification BaseFn Int -> Property
prop_noNarrowLoop f s eSpec fSpec =
-- Make sure the fuel is non-negative
f >= 0 ==>
discardAfter 100_000 $
narrowByFuelAndSize f s (eSpec, fSpec) `seq`
property True

0 comments on commit 03c1bdf

Please sign in to comment.