Время ожидания решателя в цикле с использованием z3 Python API

Согласно более раннему предложению, я пытаюсь установить раннее время ожидания для решателя при использовании z3Py.

Опять же, без всех подробностей, это то, что я пытаюсь:

for bits in range(A, B, incrmt)
    s = Solver();
    s.set("timeout", 30) #30, 3000, 30000, 60000 no change
    s.add(some constraints)
    if(s.check() == sat):
        print "Sat, %d," %(bits)
    else:
        print "Sat Unknown, %d," %(bits)
        break
    sys.stdout.flush()

По сути, тайм-аут никогда не происходит (даже со смехотворно малым временем в мс).

Источник

1 ответ

Решение

Вы используете Z3 на Linux или FreeBSD? На этих платформах была ошибка, связанная с таймерами. Я исправил проблему, но она пока не является частью официального релиза. Смотрите следующий пост для более подробной информации.

Источник
Другие вопросы по тегам