25 lines
No EOL
901 B
Text
25 lines
No EOL
901 B
Text
// Where's Waldo is a puzzle where the goal is to find Waldo in the picture of a crowd
|
|
// In this example, the crowd is a series of numbers, ideally* all prime but one, and Waldo is a non-prime number
|
|
// * we don't enforce only one number being non-prime, so there could be multiple Waldos
|
|
|
|
def isWaldo(a):
|
|
// make sure that p and q are both non zero
|
|
// we can't check inequalities, so let's create binary
|
|
// variables
|
|
p1 = if p == 1 then 0 else 1 fi // "p != 1"
|
|
q1 = if q == 1 then 0 else 1 fi // "q != 1"
|
|
q1 * p1 == 1 // "p1 and q1"
|
|
|
|
// we know how to factor a
|
|
a == p * q
|
|
|
|
return 1
|
|
|
|
// define all
|
|
def main(a0, a1, a2, a3):
|
|
// prover provides the index of Waldo
|
|
waldo = if index == 0 then a0 else 0 fi
|
|
waldo = waldo + if index == 1 then a1 else 0 fi
|
|
waldo = waldo + if index == 2 then a2 else 0 fi
|
|
waldo = waldo + if index == 3 then a3 else 0 fi
|
|
return isWaldo(waldo) |