Ускорете 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`

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