search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.16k stars 1.47k forks source link

Debugging when the fixed point solver hangs? #2473

Closed mikesol closed 5 years ago

mikesol commented 5 years ago

The following fixed-point example is copied from an Isabelle/HOL tutorial on structural induction, and I was curious to see if z3 could handle it. Z3 hangs, so it is difficult to know if it is unsolvable or if there is a bug in my code. More generally, it would be helpful to understand where/why/how the fixed-point engine is struggling and if there are reformulations that could help it succeed or if certain examples are simply too difficult. Below is the code, and thanks for your help!


def test_list_rev():
  ll = Datatype('ll')
  ll.declare('empty')
  ll.declare('cons', ('car', IntSort()), ('cdr', ll))
  ll = ll.create()
  list_app = Function('list_app', ll, ll, ll, BoolSort())
  list_rev = Function('list_rev', ll, ll, BoolSort())
  a,e,f,g,h = Consts('a e f g h', ll)
  b,c,d = Ints('b c d')

  fp = Fixedpoint()
  fp.declare_var(a,b,c,d,e,f,g,h)
  fp.register_relation(list_rev, list_app)
  fp.fact(list_app(ll.empty, e, e))
  fp.fact(list_app(e, ll.empty, e))
  fp.rule(list_app(a,e,h), [ll.cons(b, f) == a, list_app(f, e, g), ll.cons(b, g) == h])
  fp.fact(list_rev(ll.empty,ll.empty))
  fp.rule(list_rev(a,e), [ll.cons(b, f) == a, ll.cons(b, ll.empty) == g, list_rev(f, h), list_app(h, g, e)])
  assert fp.query(list_rev(a,e), list_rev(e, f), a != f) == unsat
agurfinkel commented 5 years ago

There is no easy way to debug spacer (the fp engine) from the outside. You can set verbosity to 1 -v:1 to get a little more visibility. Anything more requires a debug build and using tracing options, such as -tr:spacer_progress.

Spacer is not great for inductive data types and not great for problems that require guessing a matching invariant. In this example, it diverges iterating over lists of specific size and specific values (i.e., enumerating all integer lists of size 1, or enumerating all symbolic lists of size 1, size 2, etc.) depending on options given.

Some of these kind of problems can be solved by picking a particular induction scheme. This, however, needs to be encoded by the user explicitly. Spacer only tries to find a solution for the given predicates (list_app and list_rev in this case) and not synthesize new induction schemes.