The runtime of z3 is too long #7543
Unanswered
frankeyjin
asked this question in
Q&A
Replies: 0 comments
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Uh oh!
There was an error while loading. Please reload this page.
-
The following code takes almost 10 seconds to run:
from z3 import *
solver = Solver()
a, b, c, d = Ints('a b c d')
solver.add(a == b + c)
solver.add(a * b * c == 90)
solver.add(a * b + c == d)
solver.add(a>=0,a<=99,b>=0,b<=99,c>=0,c<=99,d>=0,d<=99)
if solver.check() == sat:
model = solver.model()
print(model)
But if I remove this line:
solver.add(a>=0,a<=99,b>=0,b<=99,c>=0,c<=99,d>=0,d<=99)
The running time drops to under 1 second.
Why is the time difference so large? I don't understand the reason.
Beta Was this translation helpful? Give feedback.
All reactions