z3/doc/design_recfuns.md

Design for handling recursive functions

Main source of inspiration is [Sutter, Köksal & Kuncak 2011], as implemented in Leon, but the main differences is that we should unroll function definitions directly from the inside of Z3, in a backtracking way. Termination and fairness are ensured by iterative-deepening on the maximum number of unrollings in a given branch.

Unfolding

The idea is that every function definition f(x1…xn) := rhs[x1…xn] is compiled into:

• a list of cases A_f_i[x1…xn] => f(x1…xn) = rhs_i[x1…xn]. When A_f_i[t1…tn] becomes true in the model, f(t1…tn) is said to be unfolded and the clause A_f_i[t1…tn] => f(t1…tn) = rhs_i[t1…tn] is added as an auxiliary clause.
• a list of constraints Γ_f_i[x1…xn] <=> A_f_i[x1…xn] that states when A_f_i[x1…xn] should be true, depending on inputs x1…xn. For every term f(t1…tn) present in congruence closure, we immediately add all the Γ_f_i[t1…tn] <=> A_f_i[t1…tn] as auxiliary clauses (maybe during internalization of f(t1…tn)?).

where each A_f_i[x1…xn] is a special new predicate representing the given case of f, and rhs_i does not contain any ite. We assume pattern matching has been compiled to ite beforehand.

For example, fact(n) := if n<2 then 1 else n * fact(n-1) is compiled into:

• A_fact_0[n] => fact(n) = 1
• A_fact_1[n] => fact(n) = n * fact(n-1)
• A_fact_0[n] <=> n < 2
• A_fact_1[n] <=> ¬(n < 2)

The 2 first clauses are only added when A_fact_0[t] is true (respectively A_fact_1[t] is true). The 2 other clauses are added as soon as fact(t) is internalized.

Termination

To ensure termination, we define variables:

• unfold_depth: int
• current_max_unfold_depth: int
• global_max_unfold_depth: int

and a special literal [max_depth=$n] for each n:int. Solving is done under the local assumption [max_depth=$current_max_unfold_depth] (this should be handled in some outer loop, e.g. in a custom tactic).

Whenever A_f_i[t1…tn] becomes true (for any f), we increment unfold_depth. If unfold_depth > current_max_unfold_depth, then the conflict clause [max_depth=$current_max_unfold_depth] => Γ => false where Γ is the conjunction of all A_f_i[t1…tn] true in the trail.

For non-recursive functions, we don't have to increment unfold_depth. Some other functions that are known

If the solver answers "SAT", we have a model. Otherwise, if [max_depth=$current_max_unfold_depth] is part of the unsat-core, then we increase current_max_unfold_depth. If current_max_unfold_depth == global_max_unfold_depth then we report "UNKNOWN" (reached global depth limit), otherwise we can try to solve() again with the new assumption (higher depth limit).

Tactic

there should be a parametrized tactic funrec(t, n) where t is the tactic used to solve (under assumption that depth is limited to current_max_unfold_depth) and n is an integer that is assigned to global_max_unfold_depth.

This way, to try and find models for a problem with recursive functions + LIA, one could use something like (funrec (then simplify dl smt) 100).

Expected benefits

This addition to Z3 would bring many benefits compared to current alternatives (Leon, quantifiers, …)

• should be very fast and lightweight (compared to Leon or quantifiers). In particular, every function call is very lightweight even compared to Leon (no need for full model building, followed by unsat core extraction)
• possibility of answering "SAT" for any QF_* fragment + recursive functions
• makes define-funs-rec a first-class citizen of the language, usable to model user-defined theories or to analyze functional programs directly

Optimizations

• maybe C_f_i literals should never be decided on (they can always be propagated). Even stronger: they should not be part of conflicts? (i.e. tune conflict resolution to always resolve these literals away, disregarding their level)