TransitiveClosure + Quantifiers extremely slow

Z3Prover / z3

The Z3 Theorem Prover

Other

10.13k stars 1.46k forks source link

TransitiveClosure + Quantifiers extremely slow #7167

Open tzlils opened 5 months ago

tzlils commented 5 months ago

from z3 import *

Bool = BoolSort()
S = FiniteDomainSort("S", 2)
R = Function("R", S, S, Bool)
TC_R = TransitiveClosure(R)
x,y = Consts("x y", S)
s = Solver()
s.add(ForAll([x, y], TC_R(x, y)))
print(s.check())
m = s.model()
print(m[R])

takes an unreasonable amount of time (i did not run it to completion) using (z3 4.13.0)

atlasyonatan commented 3 months ago

Any updates on this?