0

I'm trying to make assertions about program equivalence using z3's Fixedpoints, and I'm finding that any sort of recursion, even trivially decidable recursion, makes z3 totally choke. This z3py tutorial specifically calls out program simulation as a use case for Fixedpoints, with programs being represented by recursive data types. I feel like I must be doing something wrong.

Here's a simple example:

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 is a unary relation for trees that only extend to the right. nil only extends to the right, and if you do cons(nil, a) on a list a that only extends to the right, it continues to extend to the right. Seems like it should be trivial.

But on a modestly deep tree, the code spins indefinitely. Here's the stats after interrupting a few minutes in:

(: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)

I honestly have no idea what z3 might be trying here... Smaller lists, and lists that don't match the predicate (when the cons-on-the-left is near the top of the tree) complete quickly.

Am I doing it wrong? Or is z3 just incapable of handling recursively defined predicates over algebraic data types?

4

1 回答 1

0

不是答案，但可能会有所帮助。

我测量了运行时如何取决于查询表达式的嵌套深度：

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 的嵌套深度，不会返回问题中已经观察到的答案。

在递归定义的树状问题中，指数增长并不意外。

于 2020-09-18T11:36:31.273 回答