fd-plus-prop now propagates in the four partial- and all-domain cases
(vvn, nvv, vnv, vvv) by interval reasoning:
x in [z.min - y.max .. z.max - y.min]
y in [z.min - x.max .. z.max - x.min]
z in [x.min + y.min .. x.max + y.max]
Helpers added:
fd-narrow-or-skip — common "no-domain? skip; else filter & set" path.
fd-int-floor-div / fd-int-ceil-div — integer-division wrappers because
SX `/` returns rationals; floor/ceil computed via (a - (mod a b)).
fd-times-prop gets the same treatment for positive domains. Mixed-sign
domains pass through (sound, but no narrowing).
10 new tests in clpfd-bounds.sx demonstrate domains shrinking BEFORE
labelling: x+y=10 with x in {1..10}, y in {1..3} narrows x to {7..9};
3*y=z narrows z to {3..12}; impossible bounds (x+y=100, x,y in {1..10})
return :no-subst directly. 132/132 across the clpfd test files.
Suggested next: Piece D (send-more-money + Sudoku 4x4) to validate
this against larger puzzles.
Two more arities of the naive memoization wrapper:
table-1: predicate (1-arg) tabling. Cache entry is :ok / :no.
Demonstrated with a tabled membero-as-predicate.
table-3: 3-arg (i1 i2 output) tabling. Cache key joins the two
inputs; cache value is the output value list.
Canonical demo: tabled Ackermann.
(ack-o 0 0 q) -> 1
(ack-o 2 3 q) -> 9
(ack-o 3 3 q) -> 61
A(3,3) executes A(2,..) many times, A(1,..) more, A(0,..) most. With
table-3 each (m, n) pair is computed once.
6 new tests, 644/644 cumulative.
`table-2` wraps a 2-arg (input, output) relation. On a ground input
walk, looks up the (string-encoded) cache key; on miss, runs the
relation, drains the answer stream, extracts walk*-output values from
each subst, stores them, and replays. On hit, replays the cached
values directly — no recomputation.
Cache lifetime: a single global mk-tab-cache (mutated via set!).
mk-tab-clear! resets between independent queries.
Canonical demo: tabled fib(25) = 75025 in ~5 seconds; the same naive
fib-o times out at 60s. Memoization collapses the exponential redundant
recomputation in the binary recursion.
Limitations (deferred to future SLG work): cyclic recursive calls with
the same ground key still diverge — naive memoization populates the
cache only AFTER computation completes, so a recursive call inside its
own computation can't see the in-progress entry. The brief's "tabled
patho on cyclic graphs" use case requires producer/consumer
scheduling and is left for a future iteration.
12 new tests, fib(0..20) + ground-term predicate + cache-replay
verification. 638/638 cumulative.
The previous fd-fire-store fired every constraint exactly once. That
left the propagation incomplete in chains like
fd-plus c4 1 a; fd-neq c3 a
where, on the round c4 binds, fd-plus binds a, but fd-neq c3 a was
already past — so the conflict went undetected.
New: fd-store-signature is sum-of-domain-sizes + count-of-bindings.
fd-fire-store calls fd-fire-list and recurses while the signature
strictly decreases. Reaches a fixed point or fails.
This makes N-queens via FD tractable:
4-queens -> ((2 4 1 3) (3 1 4 2)) — exactly the two solutions.
5-queens -> 10 solutions (the canonical count), in seconds.
Phase 6 marked complete in the plan: domains, fd-in, fd-eq, fd-neq,
fd-lt, fd-lte, fd-plus, fd-times, fd-distinct, fd-label, all wired
through the constraint-reactivation loop.
Two new tests, 626/626 cumulative.
Ground-cases propagator parallel to fd-plus. Division back-direction
checks (mod z x) = 0 before recovering a divisor. Edge cases:
multiplying by zero binds the product to zero; with z=0 and one
factor zero, the other factor is unconstrained.
7 tests including divisor enumeration, square-of-each, divisibility
rejection. 624/624 cumulative.
Ground-cases propagator: when at least two of {x, y, z} walk to
ground numbers, the third is derived (or checked, if also ground).
Three vars with domains: deferred — no bounds-consistency in this
iteration.
Includes a small fd-bind-or-narrow helper that handles the common
"bind a var to a target int, respecting any existing domain"
pattern shared across propagators.
7 new tests: ground/ground/ground, recover x, recover y, impossible
case, domain-check rejection, x+y=5 enumeration, large numbers.
617/617 cumulative.
(fd-distinct (list a b c ...)) imposes pairwise distinctness via O(n²)
fd-neq constraints. Each fd-neq propagates independently when any pair
becomes ground or has a domain-removable value.
Tests: empty/singleton trivially succeed; pair-distinct/equal cover
correctness; 3-perms-of-3 = 6 and 4-perms-of-4 = 24 confirm full
permutation enumeration; pigeonhole 4-of-3 fails.
7 new tests, 610/610 cumulative.
Three more constraint goals built on the same propagator-store
machinery as fd-neq:
fd-lt: x < y. Ground/ground compares; var/num filters domain;
var/var narrows x's domain to (< y-max) and y's to (> x-min).
fd-lte: ≤ variant.
fd-eq: x = y. Ground/ground checks. Var/num: requires num to be in
var's domain (or var unconstrained) before binding. Var/var: intersect
domains, narrow both, then unify the vars.
10 new tests: narrowing against ground, ordered-pair generation,
chained x<y<z determinism, domain-sharing, out-of-domain rejection.
603/603 cumulative (100/100 across the four CLP(FD) test files).
fd-neq adds a closure to the constraint store and runs it once on
post. After every label binding, fd-fire-store re-runs all stored
constraints — when one side of a fd-neq later becomes ground, the
domain of the other side has the value removed.
Propagator semantics:
(number, number) -> equal? fail : ok
(number, var) -> remove number from var's domain
(var, number) -> symmetric
(var, var) -> defer (re-fires after each label step)
Pigeonhole-fails test confirms the constraint flow ends correctly:
3 vars all-pairwise-distinct over a 2-element domain has no solutions.
7 new tests, 593/593 cumulative.
fd-in x dom-list: narrows x's domain. If x is a ground number, checks
membership; if x is a logic var, intersects existing domain (or sets
fresh) and stores via fd-set-domain. Fails if domain becomes empty.
fd-label vars: drives search by enumerating each var's domain. Each
var is unified with each value in its domain, in order, via mk-mplus
of singleton streams.
Forward: (fd-in x dom) (fd-label (list x)) iterates x over dom.
Intersection: two fd-in goals on the same var compose via dom-intersect.
Disjoint domains -> empty answer set. Ground value membership check
gates pass/fail. Composes with the rest of the miniKanren machinery —
fresh / conde / membero etc. all work alongside.
9 new tests, 586/586 cumulative.
Foundation for native CLP(FD). The substitution dict carries a reserved
"_fd" key holding a constraint store:
{:domains {var-name -> sorted-int-list}
:constraints (... pending constraints ...)}
This commit ships only the domain machinery + accessors:
fd-dom-from-list / fd-dom-range / fd-dom-empty? / fd-dom-singleton?
fd-dom-min / fd-dom-max / fd-dom-member? / fd-dom-intersect /
fd-dom-without
fd-store-of / fd-domain-of / fd-set-domain / fd-with-store
fd-set-domain returns nil when the domain becomes empty (failure),
which is the wire signal subsequent constraint goals will consume.
The constraints field is reserved for the next iteration.
26 new tests, 577/577 cumulative.
Capture the current state: 17 library files (1229 LOC), 61 test files
(4360 LOC), 551/551 tests passing. Phases 1-5 fully done; Phase 6
covered by minimal FD (ino, all-distincto) plus an intarith escape
hatch; Phase 7 documented via the cyclic-graph divergence test as
motivation for future tabling work.
The lib-guest validation experiment is conclusive: lib/minikanren/
unify.sx adds ~50 lines of local logic over lib/guest/match.sx's
~100-line kit. The kit earns its keep at roughly 3x by line count.
Classic miniKanren tests green: appendo forwards/backwards, Peano
arithmetic enumeration (pluso, *o, lto), 4-queens (both solutions),
Pythagorean triples, family-relation inference, symbolic
differentiation, pet/colour permutation puzzle, Latin square 2x2,
binary tree walker.
(take-while-o pred l result): take elements from l while pred holds,
stopping at the first element that fails. (drop-while-o pred l result):
drop matching elements, return the rest including the first non-match.
Together: (take-while p l) ⊕ (drop-while p l) = l, verified by an
end-to-end roundtrip test.
8 new tests, 546/546 cumulative.
(arith-progo start step len result): result is the list
(start, start+step, ..., start+(len-1)*step). Length 0 yields the
empty list. Negative steps and zero step are supported.
Useful for FD-style domain construction:
(arith-progo 1 1 9 dom) -> (1 2 3 4 5 6 7 8 9)
6 new tests, 538/538 cumulative.
Walks the list with a recursive count. On a head match, recurse and
add 1 via pluso-i; on no match (nafc), recurse forwarding the count.
Empty list yields 0.
6 new tests, 532/532 cumulative.
Walks the list; if the head appears in the tail (membero), drop it and
recurse; otherwise keep it and recurse. Result preserves only the
*last* occurrence of each value.
Caveat: with input like (1 1 1) the membero check succeeds with
multiplicity, so multiple (1) answers may emerge — each is shape-
identical, but the test deliberately checks every-result-is-(1) rather
than asserting answer count.
5 new tests, 526/526 cumulative.
Demonstrates conda for first-match-wins dispatch over a set of rewrite
rules: 0+x = x, x+0 = x, 0*y = 0, x*0 = 0, 1*x = x, x*1 = x, default
unchanged.
Six rules + a fall-through default, all wrapped in a single conda. The
first clause whose head succeeds commits to that rewrite. The fall-
through default ensures the relation always succeeds with at least the
unchanged input.
6 new tests, 521/521 cumulative.
(flat-mapo rel l result): each element x of l is mapped to a list via
rel x list-from-x, and all such lists are concatenated to form result.
(flat-mapo (fn (x r) (== r (list x x))) (list 1 2 3) q)
-> ((1 1 2 2 3 3))
5 new tests, 515/515 cumulative.
(enumerate-i l result): result is l with each element paired with its
0-based index. (enumerate-from-i n l result): same but starts at n.
(enumerate-i (list :a :b :c) q) -> (((0 :a) (1 :b) (2 :c)))
5 new tests, 501/501 cumulative.
(partitiono pred l yes no) — yes is the elements of l where pred
succeeds; no is the rest. Conde dispatches on each element via the
predicate goal vs nafc-of-the-predicate, threading the head through
the matching output list.
Composes with intarith / membero / etc. for any predicate-shaped goal:
(partitiono (fn (x) (lto-i x 5)) (list 1 7 2 8 3) yes no)
yes -> (1 2 3); no -> (7 8)
5 new tests, 496/496 cumulative.
Composes two appendos: (appendo a b mid) ∧ (appendo mid c r). Runs
forward (concatenate three known lists) and backward (recover any of
the three from the other two and the result).
5 new tests, 491/491 cumulative.
Drop-in fast replacement for Peano lengtho when the count fits in a
host integer. Two conde clauses: empty list -> 0; recurse, n = 1 +
length(tail). Uses pluso-i so the length walks to a native int.
5 new tests, 486/486 cumulative.
Sum and product over a list of ground integers via fold + intarith.
Empty list yields the identity (0 for sum, 1 for product). Recurse
combines the head with the recursively-computed tail value via
pluso-i / *o-i.
9 new tests, 481/481 cumulative.
Two conde clauses each: singleton -> the element; multi -> compare head
against the recursive min/max of the tail and pick. Uses lteo-i / lto-i
for the comparisons, so the input must be ground integers.
mino + maxo can run together: (fresh (mn mx) (mino l mn) (maxo l mx)
(== q (list mn mx))) recovers both.
9 new tests, 472/472 cumulative.
Three conde clauses: empty list / singleton list / two-or-more (where
the first two satisfy lteo-i and the rest is recursively sorted). Uses
ground-only integer comparison (intarith), so the input list must
walk to ground integers.
7 new tests, 463/463 cumulative.
Recursive: empty l1 trivially holds; otherwise the head is in l2 (via
membero) and the tail is a subset. Duplicates in l1 are allowed since
each is independently checked.
7 new tests, 456/456 cumulative.
Mitigation for the cyclic-graph divergence (see tests/cyclic-graph.sx).
Threads a `visited` accumulator through the recursion; each candidate
next-step is gated by `nafc (membero z visited)`. Terminates on graphs
with cycles, no Phase-7 tabling required for the simple acyclic-path
query.
Demonstrates a viable alternative to tabling for the common case where
the user wants finite path enumeration over a graph with cycles.
3 new tests, 449/449 cumulative.
Three conde clauses: empty list -> empty result; head matches x ->
skip and recurse; head differs (nafc-gated) -> keep and recurse.
Distinct from rembero, which removes only the first occurrence.
5 new tests, 446/446 cumulative.
Demo of matche dispatch + conde + recursion for tree traversal:
(matche tree
((:leaf x) (== v x))
((:node l r) (conde ((btree-walko l v)) ((btree-walko r v)))))
Test tree ((1 2) (3 (4 5))) yields all 5 leaves under run*. Also tests
membership (run 1) and absence.
4 new tests, 441/441 cumulative.
Four conso calls express the (a b . rest) -> (b a . rest) rewrite as a
purely relational constraint. Self-inverse on length-2+ lists; runs
forward (swap given input) and backward (recover original from the
swapped form). Fails on lists shorter than 2.
6 new tests, 437/437 cumulative.
(pairlisto l1 l2 pairs): pairs is the zipped list of pairs (l1[i] l2[i]).
Recurses on both l1 and l2 in lockstep, building pairs in parallel.
Runs forward, can recover l1 given l2 and pairs, can recover l2 given
l1 and pairs. Different-length lists fail.
5 new tests, 431/431 cumulative.
(iterate-no rel n x result) holds when applying the 2-arg relation rel
n times (Peano n) starting from x produces result. Base case: zero
iterations means result equals x. Recursive case: rel x mid, then
iterate-no n-1 from mid.
Generalises common chains:
succ iteration: (iterate-no succ-rel n :z q) -> n in Peano
list growth: (iterate-no cons-rel n () q) -> n-element list
4 new tests, 426/426 cumulative.
rev-acco is the standard tail-recursive reverse with an accumulator;
rev-2o starts the accumulator at the empty list. Faster than the
appendo-driven reverseo for forward queries because there is no nested
appendo per element.
Trade-off: rev-acco is asymmetric. The accumulator's initial-empty
cannot be enumerated backwards the way reverseo does, so reverseo is
still the right choice when both directions matter.
A test verifies rev-2o and reverseo agree on forward queries.
6 new tests, 422/422 cumulative.
Classic miniKanren relation. (selecto x rest l) holds when l contains
x at any position with `rest` being everything else. Direct base case
(l = (x . rest)) plus the skip-head recursion that threads the head
through to the result rest.
Run modes: enumerate every (x, rest) split; recover rest given an
element; recover an element given the rest; (and ground/all combinations).
6 new tests, 411/411 cumulative.
Composes two appendos: l = front ++ s ++ back, equivalently
(appendo front-and-s back l) and (appendo front s front-and-s).
Goal order matters: doing the (appendo ground:l) split first makes the
search finitary; the second appendo is then deterministic given
front-and-s and ground s. Reversing the order causes divergence on
failing inputs (the front search becomes unbounded).
7 new tests, 405/405 cumulative.
Two-line definitions over appendo:
(prefixo p l) ≡ ∃rest. (appendo p rest l)
(suffixo s l) ≡ ∃front. (appendo front s l)
Both enumerate all prefixes/suffixes when called with a fresh first
arg, and serve as decision relations when called with both grounded.
9 new tests, 398/398 cumulative.
Two-line definition: a list is a palindrome iff it equals its reverse.
Direct composition of reverseo + ==.
7 new tests: empty / singleton / equal pair / unequal pair /
5-element-yes / 5-element-no / strings.
389/389 cumulative.
Mirrors the structure all-distincto already uses internally: walk the
list, ensure each element is not equal to x via nafc, recurse on tail.
Useful as a constraint-style filter:
(membero x (list 1 2 3 4 5))
(not-membero x (list 2 4))
-> x in {1, 3, 5}
4 new tests, 382/382 cumulative.
repeato: produces (or recognizes) a list of n copies of a value, with n
Peano-encoded. Runs forward, backward (recover the count from a uniform
list), and bidirectionally.
concato: fold-appendo over a list-of-lists. (concato (list (list 1 2)
(list) (list 3 4 5)) q) -> ((1 2 3 4 5)).
10 new tests, 378/378 cumulative.
(tako n l prefix) — prefix is the first n elements of l.
(dropo n l suffix) — suffix is l after dropping the first n.
Both use a Peano natural for the count. Round-trip holds:
(tako n l) ⊕ (dropo n l) = l (verified by an end-to-end test)
9 new tests, 368/368 cumulative.
eveno: zero, or (s (s m)) when m is even.
oddo: one, or (s (s m)) when m is odd.
Both run forward (predicate test on a Peano number) and backward
(enumerate even / odd numbers). The two are mutually exclusive — no
number satisfies both.
12 new tests, 359/359 cumulative.
(defrel (NAME ARGS...) (CLAUSE1 ...) (CLAUSE2 ...) ...) expands to
(define NAME (fn (ARGS...) (conde (CLAUSE1 ...) (CLAUSE2 ...) ...))).
Mirrors Prolog's `name(Args) :- goals.` shape. Inherits the Zzz-on-each-
clause laziness from conde, so user relations defined via defrel
terminate on partial answers without needing manual delay. Tests
redefine membero / listo / pluso through defrel and verify equivalence.
3 new tests, 347/347 cumulative.
lasto: x is the final element of l. Direct base case (l = (x)) plus
recurse-on-cdr.
init-o: init is l without its last element. Base case for singleton:
(== init ()). Otherwise recurse, threading the head through to the
init result via conso.
Together with appendo, the round-trip init append (list last) = l
holds, which is exercised by an end-to-end test.
8 new tests, 344/344 cumulative.
tests/rdb.sx shows the library as a small Datalog engine over fact
tables. Each table is an SX list of tuples, wrapped by a relation that
does (membero (list ...) table). Queries compose selection, projection,
and joins entirely in run* / fresh / conde / membero / intarith / nafc.
Five queries: dept filter, salary > threshold, employee-project join,
intersection (engineers on a specific project), anyone on multiple
distinct projects.
5 new tests, 336/336 cumulative.
