Я использую z3py для решения набора уравнений. Как бы вычислить его время выполнения? Он имеет переменные битвеков, которые должны выполняться в наборе линейных уравнений. Документация и руководство не дают возможности рассчитать время выполнения.как вычислить время выполнения Z3 sat solver
Вы запрашиваете (худший вариант) временная сложность использованных решателей? Если это так, я не думаю, что вы сможете получить хороший ответ: это зависит от (комбинации) логики (ов), в которые падает ваша проблема, например. QF_BV или UFNIA, а затем в процедурах ((полу) решения), которые решатель реализует для этой (комбинации) логики (ов).
Посмотрите документы от авторов Z3 (https://github.com/Z3Prover/z3/wiki/Publications) - они могут предоставить некоторые детали.