NikolajBjorner
commented
8 years ago Thanks for the useful example. The way the datatype decision procedure performs splitting on recursive data-types is a decision procedure when the formulas are quantifier-free. For formulas with quantifiers, no termination guarantees are provided. The example exhibits a case where the procedure that builds a finite model for quantifier-free recursive data-types fails to terminate. The quantified formula keeps getting instantiated by freshly generated terms, and the instantiation causes the decision procedure to create fresh terms that cause additional instantiation. Regarding the code: you can get the sort of a theory variable without using m_find because the types are all the same within an equivalence class (assuming Z3 isn't buggy here). The more crucial part of your change is to quickly give up building models for the quantifier-free formula. This causes the discrepancies in the unit tests. It is possible that there are ways to have both termination in more such quantifier cases and also retain the ground decision procedure, but I can't say without digging in what it may be like.
smcpeak
If I give Z3 a recursive data type and a condition that is unsatisfiable for any finite instance, Z3 will go into an infinite loop during model creation, eventually timing out. The loop happens because it is trying all possible finite values, of which there are an infinite number of course. I would like Z3 to instead quickly stop and say "unknown".
I have a candidate fix for this, but it causes three tests in z3test to fail, so I know it isn't completely right.
My reduced input example is attached as rdp-min.smt2.txt:
rdp-min.smt2.txt
When I run Z3 version 4.4.1 like so:
it runs for about 2 seconds and reports "unknown".
When I add some tracing:
the timeout is clear, and near the end of .z3-trace, there is:
The above term has 43 "restOf" applications; if I let it run for 20s instead, it times out after building a list with length of about 140.
Stepping through the code in gdb, what's happening seems fairly straightforward. The prover core first thinks the formula is satisfiable, and asks each theory to help build a model. The "datatype" theory sees a term with indeterminate constructor, "(restOf theList)", and forces a case split on its constructor. The "End" case is quickly rejected, but the "Elem" case creates "(restOf (restOf theList))", which again has indeterminate constructor. When the attempt to build a model resumes, the process repeats, building longer and longer lists, until Z3 times out.
I have a candidate fix, attached as z3-rdp-changes.txt:
z3-rdp-changes.txt
With these changes, my reduced test case works:
However, these tests in z3test fail:
It would seem that I need to allow Z3 to do bounded unfolding of recursive data types, but I don't know how, so I'd appreciate feedback on whether this is a good approach, and if so, suggestions on how to add an unfolding limit.