tur/backtrack-dfs
depth-first search driver over the backtracking trail.
dfs-succeed
(dfs-succeed :)
the goal with exactly one solution and no bindings.
A goal that calls `k` once and propagates its verdict.
(dfs-solve (dfs-succeed) (fn [] true)) ; => 1
Since: SX2
dfs-fail
(dfs-fail :)
the goal with no solutions.
A goal that never calls `k` and reports exhaustion.
(dfs-solve (dfs-fail) (fn [] true)) ; => 0
Since: SX2
dfs-and
(dfs-and [^fat g1 : (fn [(fn [])
conjunction: g2 runs inside each solution of g1.
| g1 | the outer goal | |
| g2 | the inner goal, tried under each of g1's solutions |
The conjoined goal.
(dfs-and (dfs-set x 1) (dfs-set y 2)) ; one solution: x=1, y=2
Since: SX2
dfs-or
(dfs-or [^fat g1 : (fn [(fn [])
disjunction: g1's alternatives fully exhausted, then g2's.
| g1 | tried first, depth-first | |
| g2 | tried after g1 is exhausted |
The disjoined goal.
(dfs-or (dfs-set x 1) (dfs-set x 2)) ; two solutions
Since: SX2
dfs-guard
(dfs-guard [^fat pred : (fn [])
succeed with no bindings iff `pred` holds NOW.
| pred | evaluated when the search reaches this goal |
A goal with one solution when pred is true, none otherwise.
(dfs-and (dfs-choose-int x 1 3)
(dfs-guard (fn [] (> (bt-get x) 1)))) ; x=2, x=3
Since: SX2
dfs-set
(dfs-set [c : BtCell v : int] :)
bind a trailed cell to a value.
| c | the cell | |
| v | the value |
A goal with one solution (the binding) or none (refused write).
Since: SX2
dfs-choose-go
(dfs-choose-go [c : BtCell lo : int hi : int ^fat k : (fn [])
internal: try binding c to each of lo..hi in order.
dfs-choose-int
(dfs-choose-int [c : BtCell lo : int hi : int] :)
nondeterministically bind `c` to an integer in [lo, hi].
| c | the cell to bind | |
| lo | first candidate (inclusive) | |
| hi | last candidate (inclusive) |
A goal with up to (hi - lo + 1) solutions.
(dfs-choose-int x 1 8) ; x = 1, then 2, ... then 8
Since: SX2
dfs-solve
(dfs-solve [^fat goal : (fn [(fn [])
run a goal depth-first; count solutions.
| goal | the goal to run | |
| on-solution | reifier + continuation verdict, run per solution |
The number of solutions on-solution saw.
(dfs-solve (dfs-choose-int x 1 3)
(fn [] (do (println (bt-get x)) true))) ; prints 1 2 3 => 3
Carries `#fx{Bt}`: this is the entry point that actually runs the search
and so brackets, writes and unwinds the trail. The goal CONSTRUCTORS above
(`dfs-set`, `dfs-choose-int`, ...) do not carry it -- they only build a
closure, and the trail is touched when that closure runs, which is here.
Since: SX2