Ускорьте z3-solver с правильной тактикой

Я создаю около 20 тысяч ограничений, и на моем компьютере их решение занимает около 3 минут. У меня разные ограничения, и ниже я привожу примеры и объясняю их. Я загрузил утверждения на http://filebin.ca/vKcV1gvuGG3.

Я заинтересован в решении более крупных систем ограничений, поэтому я хотел бы ускорить процесс. Я хотел бы спросить, есть ли у вас предложения, как их решить быстрее, например. используя соответствующую тактику. Из учебника по стратегиям я знаю тактику, но, похоже, я не получаю положительной разницы, применяя тактику ...

li - это метки дерева. Первый тип накладывает ограничения на значения меток. Значения меток обычно находятся в диапазоне от 10 до 20 различных значений.

Or(l6 == 11, Or(l6 == 0, l6 == 1, l6 == 2, l6 == 3, l6 == 4,
      l6 == 5, l6 == 6, l6 == 7, l6 == 8, l6 == 9, l6 == 10))

Второй тип связывает разные ярлыки друг с другом.

Implies(l12 == 0, Or(l10 == 2, l10 == 5, l10 == 7, l10 == 8, l10 == 10,
           False, False))

Третий тип определяет и связывает функции f: Int --> Int (или f: BitVector --> BitVector, с потерей полноты), где bound_{s, v} - это просто имя функции, а n - идентификатор узла. Цель состоит в том, чтобы найти удовлетворительное назначение для функций bound.

Implies(And(bound_s_v (18) >= 0, l18 == 0),
        And(bound_s_v (19) >= 0,
            bound_s_v (19) >=
            bound_s_v (18),
            bound_s_v (26) >= 0,
            bound_s_v (26) >=
            bound_s_v (18)))

Последний тип определяет, требуется ли граница (>= 0) или нет (== -1,)

Or(bound_s'_v'(0) >= 0, bound_s'_v'(0) == -1)

Также существует требование, чтобы для некоторого начального состояния требовалась граница:

`bound_s0_v0(0) >= 0`

Описание exutable файла: В первых 2-3 строках скрипт запускает решатель, импортирует z3, а в последней строке вызывает print s.check()