datalog: bounded-successor regression test (224/224)

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).")))