diff --git a/lib/datalog/scoreboard.json b/lib/datalog/scoreboard.json index 8b9218d9..9692afe3 100644 --- a/lib/datalog/scoreboard.json +++ b/lib/datalog/scoreboard.json @@ -1,14 +1,14 @@ { "lang": "datalog", - "total_passed": 223, + "total_passed": 224, "total_failed": 0, - "total": 223, + "total": 224, "suites": [ {"name":"tokenize","passed":26,"failed":0,"total":26}, {"name":"parse","passed":18,"failed":0,"total":18}, {"name":"unify","passed":28,"failed":0,"total":28}, {"name":"eval","passed":30,"failed":0,"total":30}, - {"name":"builtins","passed":19,"failed":0,"total":19}, + {"name":"builtins","passed":20,"failed":0,"total":20}, {"name":"semi_naive","passed":8,"failed":0,"total":8}, {"name":"negation","passed":10,"failed":0,"total":10}, {"name":"aggregates","passed":19,"failed":0,"total":19}, @@ -16,5 +16,5 @@ {"name":"magic","passed":24,"failed":0,"total":24}, {"name":"demo","passed":21,"failed":0,"total":21} ], - "generated": "2026-05-08T10:33:34+00:00" + "generated": "2026-05-08T10:36:02+00:00" } diff --git a/lib/datalog/scoreboard.md b/lib/datalog/scoreboard.md index ebeab7d4..7810f66a 100644 --- a/lib/datalog/scoreboard.md +++ b/lib/datalog/scoreboard.md @@ -1,6 +1,6 @@ # datalog scoreboard -**223 / 223 passing** (0 failure(s)). +**224 / 224 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| @@ -8,7 +8,7 @@ | parse | 18 | 18 | ok | | unify | 28 | 28 | ok | | eval | 30 | 30 | ok | -| builtins | 19 | 19 | ok | +| builtins | 20 | 20 | ok | | semi_naive | 8 | 8 | ok | | negation | 10 | 10 | ok | | aggregates | 19 | 19 | ok | diff --git a/lib/datalog/tests/builtins.sx b/lib/datalog/tests/builtins.sx index f5136134..840b30af 100644 --- a/lib/datalog/tests/builtins.sx +++ b/lib/datalog/tests/builtins.sx @@ -179,6 +179,17 @@ ((db (dl-program "n(0). n(1). n(2). n(3). n(4). n(5). n(6). n(7). n(8). n(9).\n big(X) :- n(X), >=(X, 5)."))) (do (dl-saturate! db) (len (dl-relation db "big")))) 5) + ;; Bounded successor: a recursive rule with a comparison + ;; guard terminates because the Herbrand base is effectively + ;; bounded. + (dl-bt-test-set! "bounded successor" + (dl-query + (dl-program + "nat(0). + nat(Y) :- nat(X), is(Y, +(X, 1)), <(Y, 5).") + (list (quote nat) (quote X))) + (list {:X 0} {:X 1} {:X 2} {:X 3} {:X 4})) + (dl-bt-test! "unsafe — comparison without binder" (dl-bt-throws? (fn () (dl-program "p(X) :- <(X, 5).")))