CODEWITHSUNDEEP
z3z3py
Asaf Bialystok
Asaf Bialystok

Reputation: 126

z3py sometimes hangs on Solver.check() on formulas that it can solve

In my usecase I try to use the solver to solve multiple formulas one after the other. Sometimes, the solver hangs on a certain formula, but when I try to run it again on the very same formula it succeeds immediately. Below is a minimal example in which I run the solver on the same formula multiple times, and after a few attempts it hangs indefinitely.

from z3 import *

def test_solve():
    s, s1, s2 = Strings('s s1 s2')
    i, t = Ints('i t')
    sl = Solver()
    start = datetime.now()
    sl.add(Not(Implies(And(i < t,
                           Contains(s, s1),
                           Not(SuffixOf(s1, s)),
                           Or(0 < i, PrefixOf(s1, s))),
                       Or(PrefixOf(s2, s), PrefixOf(s1, s)))))
    print(f"{attempt}: {sl.check()}. Solved in {datetime.now() - start}")

for attempt in range(20):
    test_solve()

This is its output:

0: sat. Solved in 0:00:00.504905
1: sat. Solved in 0:00:01.313257
2: sat. Solved in 0:00:00.543546
3: sat. Solved in 0:00:00.137668
4: sat. Solved in 0:00:00.268307
5: sat. Solved in 0:00:00.189427

It hangs on the 6th attempt. Is this an expected behavior? Is there anything I can do to mitigate this?

Upvotes: 0

Views: 229

Answers (1)

alias
alias

Reputation: 30525

No, I'd say this is not expected. It is true that there are "random" seeds etc. that are in play which can affect performance in each run; but the differences you're seeing (and I can replicate) are way too much to chalk it up to random seeds. The string solver that you are using has its problems, and I think this'd be a good test-case to report to the developers so they can take a look and see if they can spot why there's so much discrepancy. Please file it at: https://github.com/Z3prover/z3/issues

Upvotes: 1

Related Questions