Skip to content

Instantly share code, notes, and snippets.

@dmwit

dmwit/83601.cry

Created May 4, 2019 17:27
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save dmwit/8422ef509996c4e27ce045a26ec7ce29 to your computer and use it in GitHub Desktop.
Save dmwit/8422ef509996c4e27ce045a26ec7ce29 to your computer and use it in GitHub Desktop.
Download ZIP
cryptol code to solve https://puzzling.stackexchange.com/q/83601/8871; use `cryptol 83601.cry -c ':sat isSolution'` to run it
Raw
83601.cry
isSolution w o n e = all isDigit [w,o,n,e] /\ no*won*won == wonewon /\ no != 0 where
no = fromDigits [o,n]
won = fromDigits [n,o,w]
wonewon = fromDigits [n,o,w,e,n,o,w] : [32]
isDigit x = 0 <= x /\ x <= 9
fromDigits digits = sum [digit * 10^^exp | digit <- digits | exp <- [0...]]
@dmwit
Copy link
Author

dmwit commented May 4, 2019

And here's the output:

% cryptol 83601.cry -c ':sat isSolution'
Loading module Cryptol
Loading module Main
isSolution 0x00000001 0x00000003 0x00000007 0x00000000 = True
(Total Elapsed Time: 0.294s, using Z3)

@appgurueu
Copy link

👍

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment