z3: предложения Horn / фиксированные точки над индуктивными типами данных

Question

Я пытаюсь сделать утверждения об эквивалентности программ, используя фиксированные точки z3, и обнаружил, что любая рекурсия, даже тривиально разрешимая рекурсия, полностью подавляет z3. В этом руководстве по z3py в качестве примера использования фиксированных точек используется моделирование программ, при этом программы представлены рекурсивными типами данных. Я чувствую, что делаю что-то не так.

Вот простой пример:

from z3 import *

List = Datatype('List')
List.declare('nil')
List.declare('cons', ('car', List), ('cdr', List))
List = List.create()

nil = List.nil
cons = List.cons

a = Const('a', List)

RightLL = Function('RightLL', List, BoolSort())

fp = Fixedpoint()
fp.declare_var(a)
fp.register_relation(RightLL)

fp.fact(RightLL(nil))
fp.rule(RightLL(cons(nil, a)), RightLL(a))

BIG_ISH = cons(nil, cons(nil, cons(nil, cons(nil, cons(nil, cons(nil, cons(nil, cons(nil, cons(nil, cons(nil, nil))))))))))

fp.query(RightLL(BIG_ISH))

RightLL является унарным отношением для деревьев, продолжающихся только вправо. nil распространяется только вправо, и если вы это сделаете cons(nil, a) в списке aчто распространяется только вправо, оно продолжает расширяться вправо. Похоже, это должно быть тривиально.

Но на скромно глубоком дереве код вращается бесконечно. Вот статистика после перерыва на несколько минут:

(:SPACER-max-depth                     7
 :SPACER-max-query-lvl                 7
 :SPACER-num-active-lemmas             9
 :SPACER-num-ctp-blocked               11
 :SPACER-num-is_invariant              27
 :SPACER-num-lemmas                    21
 :SPACER-num-pobs                      6
 :SPACER-num-propagations              4
 :SPACER-num-queries                   18
 :added-eqs                            103061776
 :bool-inductive-gen                   15
 :bool-inductive-gen-failures          12
 :conflicts                            31312
 :datatype-accessor-ax                 10890974
 :datatype-constructor-ax              25388634
 :datatype-occurs-check                51492242
 :datatype-splits                      34477418
 :decisions                            38226758
 :del-clause                           656
 :final-checks                         23408
 :iuc_solver.num_proxies               63
 :max-memory                           55.70
 :memory                               55.33
 :minimized-lits                       3476
 :mk-bool-var                          52243150
 :mk-clause                            31440
 :num-allocs                           1205059883276.00
 :num-checks                           660
 :pool_solver.checks                   330
 :pool_solver.checks.sat               263
 :pool_solver.checks.undef             1
 :propagations                         36882678
 :restarts                             198
 :rlimit-count                         277012208
 :time.iuc_solver.get_iuc              0.00
 :time.iuc_solver.get_iuc.hyp_reduce2  0.00
 :time.pool_solver.proof               0.00
 :time.pool_solver.smt.total           197.77
 :time.pool_solver.smt.total.sat       193.37
 :time.pool_solver.smt.total.undef     4.22
 :time.spacer.init_rules               0.00
 :time.spacer.mbp                      0.00
 :time.spacer.solve                    197.88
 :time.spacer.solve.propagate          10.48
 :time.spacer.solve.reach              187.39
 :time.spacer.solve.reach.children     0.00
 :time.spacer.solve.reach.gen.bool_ind 168.29)

Честно говоря, я понятия не имею, что здесь может попробовать z3... Меньшие списки и списки, которые не соответствуют предикату (когда минус слева находится в верхней части дерева), заполняются быстро.

Я что делаю неправильно? Или z3 просто неспособен обрабатывать рекурсивно определенные предикаты над алгебраическими типами данных?

Answer 1

Не ответ, но потенциально полезный.

Я измерил, как время выполнения зависит от глубины вложенности выражения запроса:

from z3 import *
import time

List = Datatype('List')
List.declare('nil')
List.declare('cons', ('car', List), ('cdr', List))
List = List.create()

nil = List.nil
cons = List.cons

a = Const('a', List)

RightLL = Function('RightLL', List, BoolSort())

fp = Fixedpoint()
fp.declare_var(a)
fp.register_relation(RightLL)

fp.fact(RightLL(nil))
fp.rule(RightLL(cons(nil, a)), RightLL(a))
    
expr = nil
for nesting in range(20):
    start = time.time()
    result = fp.query(RightLL(expr))
    end = time.time()
    print(nesting, " ", result, " ", round(end - start, 2), "s", flush=True)
    expr = cons(nil, expr)
    

Результат:

0   sat   0.0 s
1   sat   0.02 s
2   sat   0.02 s
3   sat   0.03 s
4   sat   0.23 s
5   sat   2.71 s
6   sat   8.86 s
7   sat   37.21 s

Z3 требует экспоненциально растущего времени, чтобы ответить на Fixedpointзапрос. Если глубина вложения превышает 7, ответ не возвращается, как уже отмечалось в вопросе.

Экспоненциальный рост не является неожиданным для рекурсивно определенной древовидной задачи.