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
-
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