design document for handling recursive functions

doc/design_recfuns.md

@@ -0,0 +1,85 @@
+# 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