This was such a pleasure to read! Thank you for sharing!
My understanding is that solvers are like regexes. They can easily get out of hand in runtime complexity. At least this is what I have experienced from iOS's AutoLayout solver
My understanding is that solvers are like regexes. They can easily get out of hand in runtime complexity. At least this is what I have experienced from iOS's AutoLayout solver
from z3 import \*
a, b, c = Ints('a b c')
x, y = Ints('x y')
s = Solver()
s.add(a > 5)
s.add(a % 2 == 0)
theorem = Exists([b, c],
And(
a == b + c,
And(
Not(Exists([x, y], And(x > 1, y > 1, x \* y == b))),
Not(Exists([x, y], And(x > 1, y > 1, x \* y == c))),
)
)
)
if s.check(Not(theorem)) == sat:
print(f"Counterexample: {s.model()}")
else:
print("Theorem true")For the iOS AutoLayout, what kind of issues have you seen, and how complex were the problems?