artdag: miniKanren CLP(FD) scheduler (schedule.sx) + 15 tests
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 40s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 40s
lib/artdag/schedule.sx on lib/minikanren: slot var per node, fd-lt per edge, fd-label search. schedule-asap (smallest-first labeling) agrees exactly with plan.sx greedy Kahn waves (cross-validated); schedules enumerates all valid schedules; schedules-capped filters to <=cap per slot; schedule-valid? independent dep check. Adds a 'schedule' suite to conformance.sh loading the minikanren CLP(FD) stack. Completes the optional Phase 3/7 miniKanren box. schedule 15/15, total 213/213. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
@@ -13,7 +13,7 @@ if [ ! -x "$SX_SERVER" ]; then
|
|||||||
exit 1
|
exit 1
|
||||||
fi
|
fi
|
||||||
|
|
||||||
SUITES=(dag analyze plan execute optimize fed cost serialize stats fault maude-optimize)
|
SUITES=(dag analyze plan execute optimize fed cost serialize stats fault maude-optimize schedule)
|
||||||
|
|
||||||
OUT_JSON="lib/artdag/scoreboard.json"
|
OUT_JSON="lib/artdag/scoreboard.json"
|
||||||
OUT_MD="lib/artdag/scoreboard.md"
|
OUT_MD="lib/artdag/scoreboard.md"
|
||||||
@@ -25,6 +25,27 @@ run_suite() {
|
|||||||
TMP=$(mktemp)
|
TMP=$(mktemp)
|
||||||
local MAUDE_LOADS=""
|
local MAUDE_LOADS=""
|
||||||
local BRIDGE_LOAD=""
|
local BRIDGE_LOAD=""
|
||||||
|
local MK_LOADS=""
|
||||||
|
local SCHED_LOAD=""
|
||||||
|
if [ "$suite" = "schedule" ]; then
|
||||||
|
MK_LOADS='(load "lib/guest/match.sx")
|
||||||
|
(load "lib/minikanren/unify.sx")
|
||||||
|
(load "lib/minikanren/stream.sx")
|
||||||
|
(load "lib/minikanren/goals.sx")
|
||||||
|
(load "lib/minikanren/fresh.sx")
|
||||||
|
(load "lib/minikanren/conde.sx")
|
||||||
|
(load "lib/minikanren/run.sx")
|
||||||
|
(load "lib/minikanren/relations.sx")
|
||||||
|
(load "lib/minikanren/project.sx")
|
||||||
|
(load "lib/minikanren/diseq.sx")
|
||||||
|
(load "lib/minikanren/intarith.sx")
|
||||||
|
(load "lib/minikanren/matche.sx")
|
||||||
|
(load "lib/minikanren/defrel.sx")
|
||||||
|
(load "lib/minikanren/nafc.sx")
|
||||||
|
(load "lib/minikanren/fd.sx")
|
||||||
|
(load "lib/minikanren/clpfd.sx")'
|
||||||
|
SCHED_LOAD='(load "lib/artdag/schedule.sx")'
|
||||||
|
fi
|
||||||
if [ "$suite" = "maude-optimize" ]; then
|
if [ "$suite" = "maude-optimize" ]; then
|
||||||
MAUDE_LOADS='(load "lib/guest/lex.sx")
|
MAUDE_LOADS='(load "lib/guest/lex.sx")
|
||||||
(load "lib/guest/pratt.sx")
|
(load "lib/guest/pratt.sx")
|
||||||
@@ -64,6 +85,7 @@ run_suite() {
|
|||||||
(load "lib/persist/kv.sx")
|
(load "lib/persist/kv.sx")
|
||||||
(load "lib/persist/api.sx")
|
(load "lib/persist/api.sx")
|
||||||
${MAUDE_LOADS}
|
${MAUDE_LOADS}
|
||||||
|
${MK_LOADS}
|
||||||
(load "lib/artdag/dag.sx")
|
(load "lib/artdag/dag.sx")
|
||||||
(load "lib/artdag/analyze.sx")
|
(load "lib/artdag/analyze.sx")
|
||||||
(load "lib/artdag/plan.sx")
|
(load "lib/artdag/plan.sx")
|
||||||
@@ -76,6 +98,7 @@ ${MAUDE_LOADS}
|
|||||||
(load "lib/artdag/fault.sx")
|
(load "lib/artdag/fault.sx")
|
||||||
(load "lib/artdag/api.sx")
|
(load "lib/artdag/api.sx")
|
||||||
${BRIDGE_LOAD}
|
${BRIDGE_LOAD}
|
||||||
|
${SCHED_LOAD}
|
||||||
(epoch 2)
|
(epoch 2)
|
||||||
(eval "(define artdag-test-pass 0)")
|
(eval "(define artdag-test-pass 0)")
|
||||||
(eval "(define artdag-test-fail 0)")
|
(eval "(define artdag-test-fail 0)")
|
||||||
|
|||||||
139
lib/artdag/schedule.sx
Normal file
139
lib/artdag/schedule.sx
Normal file
@@ -0,0 +1,139 @@
|
|||||||
|
; lib/artdag/schedule.sx — relational scheduling on lib/minikanren CLP(FD).
|
||||||
|
; Each node gets a slot var in [1..max-slots]; every edge (input->node) imposes
|
||||||
|
; `fd-lt slot(input) slot(node)`. `fd-label` searches the finite domains; a solution
|
||||||
|
; is a {node-id -> slot} assignment respecting all dependencies. Grouping by slot
|
||||||
|
; gives parallel batches (plan.sx's batch shape). Labeling picks smallest slots
|
||||||
|
; first, so the FIRST solution is the ASAP leveling — it agrees with plan.sx's greedy
|
||||||
|
; Kahn waves; the relational extra is enumerating EVERY valid schedule. The
|
||||||
|
; parallelism cap is a cardinality property, enforced by filtering labeled solutions
|
||||||
|
; (the FD core handles precedence only). lib/minikanren is a READ-ONLY consumed
|
||||||
|
; substrate: make-var, fd-in, fd-lt, fd-label, mk-conj, reify, stream-take, empty-s.
|
||||||
|
|
||||||
|
(define
|
||||||
|
artdag/range1
|
||||||
|
(fn (n) (map (fn (i) (+ i 1)) (range 0 n))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
artdag/-zip-assoc
|
||||||
|
(fn
|
||||||
|
(ids vals)
|
||||||
|
(reduce
|
||||||
|
(fn (m p) (assoc m (first p) (nth p 1)))
|
||||||
|
{}
|
||||||
|
(zip ids vals))))
|
||||||
|
|
||||||
|
; build the constraint goal + the ordered slot vars for a dag over domain 1..maxslots.
|
||||||
|
(define
|
||||||
|
artdag/sched-goal-and-vars
|
||||||
|
(fn
|
||||||
|
(dag maxslots)
|
||||||
|
(let
|
||||||
|
((ids (artdag/dag-order dag)))
|
||||||
|
(let
|
||||||
|
((vars (map (fn (id) (make-var)) ids)))
|
||||||
|
(let
|
||||||
|
((id->var (artdag/-zip-assoc ids vars))
|
||||||
|
(dom (artdag/range1 maxslots)))
|
||||||
|
(let
|
||||||
|
((in-goals (map (fn (v) (fd-in v dom)) vars))
|
||||||
|
(lt-goals
|
||||||
|
(reduce
|
||||||
|
(fn
|
||||||
|
(acc id)
|
||||||
|
(concat
|
||||||
|
acc
|
||||||
|
(map
|
||||||
|
(fn
|
||||||
|
(inp)
|
||||||
|
(fd-lt (get id->var inp) (get id->var id)))
|
||||||
|
(artdag/node-inputs (artdag/dag-get dag id)))))
|
||||||
|
(list)
|
||||||
|
ids)))
|
||||||
|
{:goal (apply mk-conj (concat in-goals lt-goals (list (fd-label vars)))) :vars vars :ids ids}))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
artdag/-sched-solutions
|
||||||
|
(fn
|
||||||
|
(g limit)
|
||||||
|
(map
|
||||||
|
(fn (sol) (artdag/-zip-assoc (get g :ids) sol))
|
||||||
|
(map
|
||||||
|
(fn (s) (reify (get g :vars) s))
|
||||||
|
(stream-take limit ((get g :goal) empty-s))))))
|
||||||
|
|
||||||
|
; all valid dependency-respecting slot assignments within 1..maxslots.
|
||||||
|
(define
|
||||||
|
artdag/schedules
|
||||||
|
(fn
|
||||||
|
(dag maxslots)
|
||||||
|
(artdag/-sched-solutions
|
||||||
|
(artdag/sched-goal-and-vars dag maxslots)
|
||||||
|
-1)))
|
||||||
|
|
||||||
|
; one valid assignment (ASAP within the bound), or nil if maxslots is too small.
|
||||||
|
(define
|
||||||
|
artdag/schedule
|
||||||
|
(fn
|
||||||
|
(dag maxslots)
|
||||||
|
(let
|
||||||
|
((ss (artdag/-sched-solutions (artdag/sched-goal-and-vars dag maxslots) 1)))
|
||||||
|
(if (empty? ss) nil (first ss)))))
|
||||||
|
|
||||||
|
; ASAP schedule: node-count slots are always sufficient (a linear chain is the worst
|
||||||
|
; case), and smallest-first labeling yields the tightest leveling.
|
||||||
|
(define
|
||||||
|
artdag/schedule-asap
|
||||||
|
(fn (dag) (artdag/schedule dag (artdag/node-count dag))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
artdag/schedule-makespan
|
||||||
|
(fn
|
||||||
|
(assignment)
|
||||||
|
(reduce
|
||||||
|
(fn (m id) (max m (get assignment id)))
|
||||||
|
0
|
||||||
|
(keys assignment))))
|
||||||
|
|
||||||
|
; group node-ids by slot (ascending), each batch id-sorted for determinism.
|
||||||
|
(define
|
||||||
|
artdag/schedule->batches
|
||||||
|
(fn
|
||||||
|
(dag assignment)
|
||||||
|
(let
|
||||||
|
((mx (artdag/schedule-makespan assignment)))
|
||||||
|
(filter
|
||||||
|
(fn (b) (not (empty? b)))
|
||||||
|
(map
|
||||||
|
(fn
|
||||||
|
(slot)
|
||||||
|
(artdag/sort-strings
|
||||||
|
(filter
|
||||||
|
(fn (id) (= (get assignment id) slot))
|
||||||
|
(keys assignment))))
|
||||||
|
(artdag/range1 mx))))))
|
||||||
|
|
||||||
|
; independent check: every input is scheduled strictly before its consumer.
|
||||||
|
(define
|
||||||
|
artdag/schedule-valid?
|
||||||
|
(fn
|
||||||
|
(dag assignment)
|
||||||
|
(every?
|
||||||
|
(fn
|
||||||
|
(id)
|
||||||
|
(every?
|
||||||
|
(fn (inp) (< (get assignment inp) (get assignment id)))
|
||||||
|
(artdag/node-inputs (artdag/dag-get dag id))))
|
||||||
|
(artdag/dag-order dag))))
|
||||||
|
|
||||||
|
; schedules whose every slot holds <= cap nodes (parallelism cap as a post-filter).
|
||||||
|
(define
|
||||||
|
artdag/schedules-capped
|
||||||
|
(fn
|
||||||
|
(dag maxslots cap)
|
||||||
|
(filter
|
||||||
|
(fn
|
||||||
|
(asn)
|
||||||
|
(every?
|
||||||
|
(fn (b) (<= (len b) cap))
|
||||||
|
(artdag/schedule->batches dag asn)))
|
||||||
|
(artdag/schedules dag maxslots))))
|
||||||
@@ -10,9 +10,10 @@
|
|||||||
"serialize": {"pass": 13, "fail": 0},
|
"serialize": {"pass": 13, "fail": 0},
|
||||||
"stats": {"pass": 12, "fail": 0},
|
"stats": {"pass": 12, "fail": 0},
|
||||||
"fault": {"pass": 14, "fail": 0},
|
"fault": {"pass": 14, "fail": 0},
|
||||||
"maude-optimize": {"pass": 40, "fail": 0}
|
"maude-optimize": {"pass": 40, "fail": 0},
|
||||||
|
"schedule": {"pass": 15, "fail": 0}
|
||||||
},
|
},
|
||||||
"total_pass": 198,
|
"total_pass": 213,
|
||||||
"total_fail": 0,
|
"total_fail": 0,
|
||||||
"total": 198
|
"total": 213
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -15,4 +15,5 @@ _Generated by `lib/artdag/conformance.sh`_
|
|||||||
| stats | 12 | 0 | 12 |
|
| stats | 12 | 0 | 12 |
|
||||||
| fault | 14 | 0 | 14 |
|
| fault | 14 | 0 | 14 |
|
||||||
| maude-optimize | 40 | 0 | 40 |
|
| maude-optimize | 40 | 0 | 40 |
|
||||||
| **Total** | **198** | **0** | **198** |
|
| schedule | 15 | 0 | 15 |
|
||||||
|
| **Total** | **213** | **0** | **213** |
|
||||||
|
|||||||
127
lib/artdag/tests/schedule.sx
Normal file
127
lib/artdag/tests/schedule.sx
Normal file
@@ -0,0 +1,127 @@
|
|||||||
|
; Phase 3/7 (optional) — relational scheduling on lib/minikanren CLP(FD).
|
||||||
|
; Each node gets a slot var; edges impose fd-lt; fd-label searches. The ASAP solution
|
||||||
|
; agrees with plan.sx's greedy Kahn waves; enumerating all solutions is the extra.
|
||||||
|
|
||||||
|
; ---- linear chain a -> b -> c: exactly one minimal schedule ----
|
||||||
|
|
||||||
|
(define
|
||||||
|
sc-chain
|
||||||
|
(artdag/build
|
||||||
|
(list
|
||||||
|
(list "a" "src" (list) {})
|
||||||
|
(list "b" "blur" (list "a") {:radius 1})
|
||||||
|
(list "c" "blur" (list "b") {:radius 2}))))
|
||||||
|
(define sc-chain-a (artdag/dag-id sc-chain "a"))
|
||||||
|
(define sc-chain-b (artdag/dag-id sc-chain "b"))
|
||||||
|
(define sc-chain-c (artdag/dag-id sc-chain "c"))
|
||||||
|
(define sc-chain-asap (artdag/schedule-asap sc-chain))
|
||||||
|
|
||||||
|
(artdag-test "chain: ASAP schedule exists" (nil? sc-chain-asap) false)
|
||||||
|
|
||||||
|
(artdag-test
|
||||||
|
"chain: slots are strictly increasing along the chain"
|
||||||
|
(list
|
||||||
|
(get sc-chain-asap sc-chain-a)
|
||||||
|
(get sc-chain-asap sc-chain-b)
|
||||||
|
(get sc-chain-asap sc-chain-c))
|
||||||
|
(list 1 2 3))
|
||||||
|
|
||||||
|
(artdag-test
|
||||||
|
"chain: makespan equals chain length"
|
||||||
|
(artdag/schedule-makespan sc-chain-asap)
|
||||||
|
3)
|
||||||
|
|
||||||
|
(artdag-test
|
||||||
|
"chain: exactly one schedule when slots = node count (no slack)"
|
||||||
|
(len (artdag/schedules sc-chain 3))
|
||||||
|
1)
|
||||||
|
|
||||||
|
(artdag-test
|
||||||
|
"chain: ASAP batches are one node per slot"
|
||||||
|
(map len (artdag/schedule->batches sc-chain sc-chain-asap))
|
||||||
|
(list 1 1 1))
|
||||||
|
|
||||||
|
(artdag-test
|
||||||
|
"chain: ASAP schedule is valid (deps respected)"
|
||||||
|
(artdag/schedule-valid? sc-chain sc-chain-asap)
|
||||||
|
true)
|
||||||
|
|
||||||
|
; ---- diamond a -> b,c -> d: b and c are parallel ----
|
||||||
|
|
||||||
|
(define
|
||||||
|
sc-dia
|
||||||
|
(artdag/build
|
||||||
|
(list
|
||||||
|
(list "a" "src" (list) {})
|
||||||
|
(list "b" "blur" (list "a") {:radius 1})
|
||||||
|
(list "c" "bright" (list "a") {:radius 1})
|
||||||
|
(list "d" "over" (list "b" "c") {} true))))
|
||||||
|
(define sc-dia-asap (artdag/schedule-asap sc-dia))
|
||||||
|
|
||||||
|
(artdag-test
|
||||||
|
"diamond: ASAP makespan is 3 (a | b,c | d)"
|
||||||
|
(artdag/schedule-makespan sc-dia-asap)
|
||||||
|
3)
|
||||||
|
|
||||||
|
(artdag-test
|
||||||
|
"diamond: ASAP batch sizes are 1,2,1"
|
||||||
|
(map len (artdag/schedule->batches sc-dia sc-dia-asap))
|
||||||
|
(list 1 2 1))
|
||||||
|
|
||||||
|
(artdag-test
|
||||||
|
"diamond: FD ASAP batches agree with plan.sx greedy waves"
|
||||||
|
(=
|
||||||
|
(artdag/schedule->batches sc-dia sc-dia-asap)
|
||||||
|
(map artdag/sort-strings (artdag/plan sc-dia 0)))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(artdag-test
|
||||||
|
"diamond: every enumerated schedule is valid"
|
||||||
|
(every?
|
||||||
|
(fn (asn) (artdag/schedule-valid? sc-dia asn))
|
||||||
|
(artdag/schedules sc-dia 4))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(artdag-test
|
||||||
|
"diamond: b and c share a slot in the ASAP schedule"
|
||||||
|
(=
|
||||||
|
(get sc-dia-asap (artdag/dag-id sc-dia "b"))
|
||||||
|
(get sc-dia-asap (artdag/dag-id sc-dia "c")))
|
||||||
|
true)
|
||||||
|
|
||||||
|
; ---- parallelism cap: filter schedules to <= cap nodes per slot ----
|
||||||
|
|
||||||
|
(artdag-test
|
||||||
|
"cap 1: the ASAP (b,c parallel) schedule is excluded, serial ones remain"
|
||||||
|
(every?
|
||||||
|
(fn
|
||||||
|
(asn)
|
||||||
|
(every?
|
||||||
|
(fn (b) (<= (len b) 1))
|
||||||
|
(artdag/schedule->batches sc-dia asn)))
|
||||||
|
(artdag/schedules-capped sc-dia 4 1))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(artdag-test
|
||||||
|
"cap 1: at least one serial schedule exists within 4 slots"
|
||||||
|
(> (len (artdag/schedules-capped sc-dia 4 1)) 0)
|
||||||
|
true)
|
||||||
|
|
||||||
|
(artdag-test
|
||||||
|
"cap 2: admits the parallel ASAP schedule"
|
||||||
|
(if
|
||||||
|
(some
|
||||||
|
(fn (shape) (= shape (list 1 2 1)))
|
||||||
|
(map
|
||||||
|
(fn (asn) (map len (artdag/schedule->batches sc-dia asn)))
|
||||||
|
(artdag/schedules-capped sc-dia 4 2)))
|
||||||
|
true
|
||||||
|
false)
|
||||||
|
true)
|
||||||
|
|
||||||
|
; ---- unsatisfiable: too few slots for the chain ----
|
||||||
|
|
||||||
|
(artdag-test
|
||||||
|
"chain: no schedule when slots < chain length"
|
||||||
|
(nil? (artdag/schedule sc-chain 2))
|
||||||
|
true)
|
||||||
@@ -31,14 +31,21 @@ edges.
|
|||||||
|
|
||||||
## Status (rolling)
|
## Status (rolling)
|
||||||
|
|
||||||
`bash lib/artdag/conformance.sh` → **198/198** (11 suites: dag, analyze, plan, execute, optimize, fed, cost, serialize, stats, fault, maude-optimize)
|
`bash lib/artdag/conformance.sh` → **213/213** (12 suites: dag, analyze, plan, execute, optimize, fed, cost, serialize, stats, fault, maude-optimize, schedule)
|
||||||
|
|
||||||
Base roadmap (Phases 1–6) COMPLETE + Phase 7 (maude rule-based optimization) COMPLETE
|
Base roadmap (Phases 1–6) COMPLETE + Phase 7 (maude rule-based optimization) COMPLETE
|
||||||
(only optional miniKanren scheduling remains). Now hardening only.
|
(only optional miniKanren scheduling remains). Now hardening only.
|
||||||
|
|
||||||
## Integration / merge status (2026-06-28)
|
## Integration / merge status (2026-06-28)
|
||||||
|
|
||||||
**READY TO MERGE `loops/artdag` → `architecture`.** `origin/architecture`'s `lib/artdag/`
|
**MERGED to architecture (Phase 7) at `b0d845bb`** — local `architecture` now carries
|
||||||
|
`lib/maude` + artdag Phase 7, conformance green there (198/198 at merge time). The merge
|
||||||
|
was clean/additive; `architecture` itself was NOT pushed (pushing it triggers a large dev
|
||||||
|
reload — a deliberate separate call). **NOTE: re-merge needed** — `loops/artdag` has since
|
||||||
|
added `lib/artdag/schedule.sx` (miniKanren CLP(FD) scheduler, 213/213), not yet on
|
||||||
|
architecture.
|
||||||
|
|
||||||
|
(Historical, for the Phase 7 merge above:) `origin/architecture`'s `lib/artdag/`
|
||||||
is stale — it predates the maude-bridge, so it is missing ALL of Phase 7
|
is stale — it predates the maude-bridge, so it is missing ALL of Phase 7
|
||||||
(`maude-bridge.sx` + `optimize-rules.sx` both absent). `loops/artdag` is 9 commits ahead
|
(`maude-bridge.sx` + `optimize-rules.sx` both absent). `loops/artdag` is 9 commits ahead
|
||||||
of `origin/architecture` (the Phase 7 chain `657d8061..4a02a9c4` + the architecture-merge
|
of `origin/architecture` (the Phase 7 chain `657d8061..4a02a9c4` + the architecture-merge
|
||||||
@@ -122,7 +129,10 @@ lib/artdag/optimize.sx lib/artdag/federation.sx
|
|||||||
nodes have all deps satisfied → run in parallel); respect a max-parallelism limit
|
nodes have all deps satisfied → run in parallel); respect a max-parallelism limit
|
||||||
- [x] plan over the *dirty* subset only (incremental plan)
|
- [x] plan over the *dirty* subset only (incremental plan)
|
||||||
- [x] `lib/artdag/tests/plan.sx` — batch correctness, parallelism cap, dirty-only plan
|
- [x] `lib/artdag/tests/plan.sx` — batch correctness, parallelism cap, dirty-only plan
|
||||||
- [ ] (optional/later) miniKanren constraint scheduling — flag, don't block on it
|
- [x] miniKanren constraint scheduling — `lib/artdag/schedule.sx` on lib/minikanren
|
||||||
|
CLP(FD): slot var per node, `fd-lt` per edge, `fd-label` search; ASAP solution agrees
|
||||||
|
with the greedy Kahn waves above, plus full schedule enumeration + parallelism-cap
|
||||||
|
filter (Phase 3 + Phase 7 optional box)
|
||||||
|
|
||||||
## Phase 4 — Execute (incremental + memoized)
|
## Phase 4 — Execute (incremental + memoized)
|
||||||
|
|
||||||
@@ -209,6 +219,23 @@ be an op token.
|
|||||||
|
|
||||||
## Progress log
|
## Progress log
|
||||||
|
|
||||||
|
- **2026-06-28 Phase 3/7 — miniKanren CLP(FD) scheduler** (schedule suite 15/15, total
|
||||||
|
213/213). `lib/artdag/schedule.sx` on `lib/minikanren` (read-only substrate): each node
|
||||||
|
gets a slot var in `[1..max-slots]`, every edge `(input->node)` imposes `fd-lt
|
||||||
|
slot(input) slot(node)`, `fd-label` searches the finite domains. A solution is a
|
||||||
|
`{node-id -> slot}` assignment respecting all dependencies; `schedule->batches` groups by
|
||||||
|
slot into parallel waves. Smallest-first labeling makes `schedule-asap` the tightest
|
||||||
|
leveling — and it **agrees exactly with `plan.sx`'s greedy Kahn waves** (cross-validated
|
||||||
|
in the suite: FD batches == `artdag/plan dag 0`). The relational extra over the greedy
|
||||||
|
planner: `schedules` enumerates EVERY valid schedule, and `schedules-capped` filters to
|
||||||
|
`<= cap` nodes per slot (cardinality is a post-filter; the FD core handles precedence).
|
||||||
|
`schedule-valid?` independently checks deps; unsatisfiable bounds return nil. Substrate
|
||||||
|
load deps: `lib/guest/match.sx` (the kit: `mk-var`) before the minikanren stack, then
|
||||||
|
`fd.sx`+`clpfd.sx`. Built functionally (`make-var`/`mk-conj`/`reify`/`stream-take`/
|
||||||
|
`empty-s`) since the node count is runtime data, not macro-time. Gotcha: `artdag/member?`
|
||||||
|
uses `equal?` (representation-sensitive) — membership of `map`-built lists must compare
|
||||||
|
with `=`, not `member?`.
|
||||||
|
|
||||||
- **2026-06-19 Phase 7 — confluence gate is non-vacuous** (maude-optimize 40/40, total
|
- **2026-06-19 Phase 7 — confluence gate is non-vacuous** (maude-optimize 40/40, total
|
||||||
198/198). Added a regression proving `mau/confluent?` actually discriminates: the
|
198/198). Added a regression proving `mau/confluent?` actually discriminates: the
|
||||||
Peano-arithmetic variant of the same laws (`0 + N = N`, `s M + N = s(M+N)` instead of
|
Peano-arithmetic variant of the same laws (`0 + N = N`, `s M + N = s(M+N)` instead of
|
||||||
|
|||||||
Reference in New Issue
Block a user