From fba22d2facf66409602ca82d7a8477db1226de3d Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 6 Nov 2017 15:32:02 +0100 Subject: [PATCH] design document for handling recursive functions --- doc/design_recfuns.md | 85 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 85 insertions(+) create mode 100644 doc/design_recfuns.md diff --git a/doc/design_recfuns.md b/doc/design_recfuns.md new file mode 100644 index 000000000..9dbe5c874 --- /dev/null +++ b/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