| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Documentation.SBV.Examples.Puzzles.SquareBirthday
Description
As of January 2026, to access the careers link at http://math.inc, you need to solve the following puzzle:
Suppose that today is June 1, 2025. We call a date "square" if all of its components (day, month, and year) are perfect squares. I was born in the last millennium, and my next birthday (relative to that date) will be the last square date in my life. If you sum the square roots of the components of that upcoming square birthday (day, month, year), you obtain my age on June 1, 2025. My mother would have been born on a square date if the month were a square number; in reality it is not a square date, but both the month and day are perfect cubes. When was I born, and when was my mother born?
So, let's solve it using SBV.
Synopsis
- data Month
- data Date = MkDate {}
- cv2Month :: String -> [CV] -> Month
- _undefiner_Month :: a
- cv2Date :: String -> [CV] -> Date
- _undefiner_Date :: a
- type SDate = SBV Date
- type SMonth = SBV Month
- sJan :: SBV Month
- sFeb :: SBV Month
- sMar :: SBV Month
- sApr :: SBV Month
- sMay :: SBV Month
- sJun :: SBV Month
- sJul :: SBV Month
- sAug :: SBV Month
- sSep :: SBV Month
- sOct :: SBV Month
- sNov :: SBV Month
- sDec :: SBV Month
- isJan :: SBV Month -> SBool
- isFeb :: SBV Month -> SBool
- isMar :: SBV Month -> SBool
- isApr :: SBV Month -> SBool
- isMay :: SBV Month -> SBool
- isJun :: SBV Month -> SBool
- isJul :: SBV Month -> SBool
- isAug :: SBV Month -> SBool
- isSep :: SBV Month -> SBool
- isOct :: SBV Month -> SBool
- isNov :: SBV Month -> SBool
- isDec :: SBV Month -> SBool
- sCaseMonth :: Mergeable result => SBV Month -> result -> result -> result -> result -> result -> result -> result -> result -> result -> result -> result -> result -> result
- sMkDate :: SBV Integer -> SBV Month -> SBV Integer -> SBV Date
- isMkDate :: SBV Date -> SBool
- getMkDate_1 :: SBV Date -> SBV Integer
- sday :: SBV Date -> SBV Integer
- getMkDate_2 :: SBV Date -> SBV Month
- smonth :: SBV Date -> SBV Month
- getMkDate_3 :: SBV Date -> SBV Integer
- syear :: SBV Date -> SBV Integer
- sCaseDate :: Mergeable result => SBV Date -> (SBV Integer -> SBV Month -> SBV Integer -> result) -> result
- symDate :: String -> Symbolic SDate
- today :: SDate
- onOrAfter :: SDate -> SDate -> SBool
- after :: SDate -> SDate -> SBool
- age :: SDate -> SInteger
- squareYears :: [(Integer, Integer)]
- squareDate :: SDate -> SBool
- sqrSum :: SDate -> SInteger
- puzzle :: IO ()
Documentation
Months in a year.
Instances
A date. We use unbounded integers for day and year, which simplifies coding, though one can also enumerate the possible values from the problem itself.
Instances
_undefiner_Month :: a Source #
Autogenerated definition to avoid unused-variable warnings from GHC.
_undefiner_Date :: a Source #
Autogenerated definition to avoid unused-variable warnings from GHC.
sCaseMonth :: Mergeable result => SBV Month -> result -> result -> result -> result -> result -> result -> result -> result -> result -> result -> result -> result -> result Source #
Case analyzer for the type Month.
sMkDate :: SBV Integer -> SBV Month -> SBV Integer -> SBV Date Source #
Symbolic version of the constructor MkDate.
sCaseDate :: Mergeable result => SBV Date -> (SBV Integer -> SBV Month -> SBV Integer -> result) -> result Source #
Case analyzer for the type Date.
symDate :: String -> Symbolic SDate Source #
Get a symbolic date with the given name. Since we used integers for the day and year fields, we constrain them appropriately. Note that one can further constrain days based on the year and month; but that level detail isn't necessary for the current problem.
onOrAfter :: SDate -> SDate -> SBool Source #
A date is on or after another, if the month-day combo is lexicographically later. Note that we ignore the year for this comparison, as we're interested if the anniversary of a date is after or not.
age :: SDate -> SInteger Source #
The age based on a given date is the difference between years less than one. We have to adjust by 1 if today happens to be after the given date.
squareYears :: [(Integer, Integer)] Source #
We can let years to range over arbitrary integers. But that complicates the job of the solver. So, based on what we know from the problem, we restrict our attention to years betweek 1900 and 2100. Note that there are only two years that satisfy this in that range: 1936 and 2025. (Any other square year makes no sense for the setting of the problem.) To simplify the square-root computation, we also store the square root in this list as the second component:
>>>squareYears[(1936,44),(2025,45)]
squareDate :: SDate -> SBool Source #
A date is square if all its components are.
Formalizing the puzzle. We literally write down the description in SBV notation. As with any formalization, this step is subjective; there could be many different ways to express the same problem. The description below is quite faithful to the problem description given. We have:
>>>puzzleMe : Sep 25, 1971 Mom: Aug 1, 1936