Ouro.hs

import Data.SBV

leftAppend :: SInteger -> SInteger -> SInteger
leftAppend k n = ite (n .< 10       ) (n + k *10)
               $ ite (n .< 100      ) (n + k *100)
               $ ite (n .< 1000     ) (n + k * 1000)
               $ ite (n .< 10000    ) (n + k * 10000)
               $ ite (n .< 100000   ) (n + k * 100000)
               $ ite (n .< 1000000  ) (n + k * 1000000)
               $ ite (n .< 10000000 ) (n + k * 10000000)
               $ ite (n .< 100000000) (n + k * 100000000)
                                      (n + k * 1000000000)

isOuroboros :: SInteger -> SInteger -> SBool
isOuroboros k n = k * n .== rotated
  where (rest, tens) = n `sQuotRem` 10
        rotated      = leftAppend tens rest

firstOuroboros :: SInteger -> SInteger -> SInteger -> IO OptimizeResult
firstOuroboros k start end = optimizeWith z3{isNonModelVar = (== "min_o")} Lexicographic $ do
                o <- sInteger "o"
                constrain $ o .>= start
                constrain $ o .<= end
                minimize "min_o" o
                return $ isOuroboros k o

-- $ time ./ouro
-- Optimal model:
--   o = 102564 :: Integer
-- Optimal model:
--   o = 142857 :: Integer
-- Unsatisfiable.
-- ./ouro  0.12s user 0.01s system 63% cpu 0.209 total
main :: IO ()
main = do print =<< firstOuroboros 4 1 100000000
          print =<< firstOuroboros 5 1 100000000
          print =<< firstOuroboros 6 1 1000000000