giles
caec05eb27
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 54s
New lib/datalog/strata.sx: dl-build-dep-graph (relation -> deps with :neg flag), Floyd-Warshall reachability, SCC-via-mutual-reach for non-stratifiability detection, iterative dl-compute-strata, and dl-group-rules-by-stratum. eval.sx refactor: - dl-saturate-rules! db rules — semi-naive worker over a rule subset - dl-saturate! db — stratified driver. Rejects non-stratifiable programs at saturation time, then iterates strata in order - dl-match-negation — succeeds iff inner positive match is empty Order-aware safety in dl-rule-check-safety (Phase 4) already required negation vars to be bound by a prior positive literal. Stratum dict keys are strings (SX dicts don't accept ints). Phase 6 magic sets deferred — opt-in path, semi-naive default suffices for current workloads.
232 lines
5.8 KiB
Plaintext
232 lines
5.8 KiB
Plaintext
;; lib/datalog/tests/negation.sx — stratified negation tests.
|
|
|
|
(define dl-nt-pass 0)
|
|
(define dl-nt-fail 0)
|
|
(define dl-nt-failures (list))
|
|
|
|
(define
|
|
dl-nt-deep=?
|
|
(fn
|
|
(a b)
|
|
(cond
|
|
((and (list? a) (list? b))
|
|
(and (= (len a) (len b)) (dl-nt-deq-l? a b 0)))
|
|
((and (dict? a) (dict? b))
|
|
(let ((ka (keys a)) (kb (keys b)))
|
|
(and (= (len ka) (len kb)) (dl-nt-deq-d? a b ka 0))))
|
|
((and (number? a) (number? b)) (= a b))
|
|
(else (equal? a b)))))
|
|
|
|
(define
|
|
dl-nt-deq-l?
|
|
(fn
|
|
(a b i)
|
|
(cond
|
|
((>= i (len a)) true)
|
|
((not (dl-nt-deep=? (nth a i) (nth b i))) false)
|
|
(else (dl-nt-deq-l? a b (+ i 1))))))
|
|
|
|
(define
|
|
dl-nt-deq-d?
|
|
(fn
|
|
(a b ka i)
|
|
(cond
|
|
((>= i (len ka)) true)
|
|
((let ((k (nth ka i)))
|
|
(not (dl-nt-deep=? (get a k) (get b k))))
|
|
false)
|
|
(else (dl-nt-deq-d? a b ka (+ i 1))))))
|
|
|
|
(define
|
|
dl-nt-set=?
|
|
(fn
|
|
(a b)
|
|
(and
|
|
(= (len a) (len b))
|
|
(dl-nt-subset? a b)
|
|
(dl-nt-subset? b a))))
|
|
|
|
(define
|
|
dl-nt-subset?
|
|
(fn
|
|
(xs ys)
|
|
(cond
|
|
((= (len xs) 0) true)
|
|
((not (dl-nt-contains? ys (first xs))) false)
|
|
(else (dl-nt-subset? (rest xs) ys)))))
|
|
|
|
(define
|
|
dl-nt-contains?
|
|
(fn
|
|
(xs target)
|
|
(cond
|
|
((= (len xs) 0) false)
|
|
((dl-nt-deep=? (first xs) target) true)
|
|
(else (dl-nt-contains? (rest xs) target)))))
|
|
|
|
(define
|
|
dl-nt-test!
|
|
(fn
|
|
(name got expected)
|
|
(if
|
|
(dl-nt-deep=? got expected)
|
|
(set! dl-nt-pass (+ dl-nt-pass 1))
|
|
(do
|
|
(set! dl-nt-fail (+ dl-nt-fail 1))
|
|
(append!
|
|
dl-nt-failures
|
|
(str
|
|
name
|
|
"\n expected: " expected
|
|
"\n got: " got))))))
|
|
|
|
(define
|
|
dl-nt-test-set!
|
|
(fn
|
|
(name got expected)
|
|
(if
|
|
(dl-nt-set=? got expected)
|
|
(set! dl-nt-pass (+ dl-nt-pass 1))
|
|
(do
|
|
(set! dl-nt-fail (+ dl-nt-fail 1))
|
|
(append!
|
|
dl-nt-failures
|
|
(str
|
|
name
|
|
"\n expected (set): " expected
|
|
"\n got: " got))))))
|
|
|
|
(define
|
|
dl-nt-throws?
|
|
(fn
|
|
(thunk)
|
|
(let
|
|
((threw false))
|
|
(do
|
|
(guard
|
|
(e (#t (set! threw true)))
|
|
(thunk))
|
|
threw))))
|
|
|
|
(define
|
|
dl-nt-run-all!
|
|
(fn
|
|
()
|
|
(do
|
|
;; Negation against EDB-only relation.
|
|
(dl-nt-test-set! "not against EDB"
|
|
(dl-query
|
|
(dl-program
|
|
"p(1). p(2). p(3). r(2).
|
|
q(X) :- p(X), not(r(X)).")
|
|
(list (quote q) (quote X)))
|
|
(list {:X 1} {:X 3}))
|
|
|
|
;; Negation against derived relation — needs stratification.
|
|
(dl-nt-test-set! "not against derived rel"
|
|
(dl-query
|
|
(dl-program
|
|
"p(1). p(2). p(3). s(2).
|
|
r(X) :- s(X).
|
|
q(X) :- p(X), not(r(X)).")
|
|
(list (quote q) (quote X)))
|
|
(list {:X 1} {:X 3}))
|
|
|
|
;; Two-step strata: r derives via s; q derives via not r.
|
|
(dl-nt-test-set! "two-step strata"
|
|
(dl-query
|
|
(dl-program
|
|
"node(a). node(b). node(c). node(d).
|
|
edge(a, b). edge(b, c). edge(c, a).
|
|
reach(X, Y) :- edge(X, Y).
|
|
reach(X, Z) :- edge(X, Y), reach(Y, Z).
|
|
unreachable(X) :- node(X), not(reach(a, X)).")
|
|
(list (quote unreachable) (quote X)))
|
|
(list {:X (quote d)}))
|
|
|
|
;; Combine negation with arithmetic and comparison.
|
|
(dl-nt-test-set! "negation with arithmetic"
|
|
(dl-query
|
|
(dl-program
|
|
"n(1). n(2). n(3). n(4). n(5). odd(1). odd(3). odd(5).
|
|
even(X) :- n(X), not(odd(X)).")
|
|
(list (quote even) (quote X)))
|
|
(list {:X 2} {:X 4}))
|
|
|
|
;; Empty negation result.
|
|
(dl-nt-test-set! "negation always succeeds"
|
|
(dl-query
|
|
(dl-program
|
|
"p(1). p(2). q(X) :- p(X), not(r(X)).")
|
|
(list (quote q) (quote X)))
|
|
(list {:X 1} {:X 2}))
|
|
|
|
;; Negation always fails.
|
|
(dl-nt-test-set! "negation always fails"
|
|
(dl-query
|
|
(dl-program
|
|
"p(1). p(2). r(1). r(2). q(X) :- p(X), not(r(X)).")
|
|
(list (quote q) (quote X)))
|
|
(list))
|
|
|
|
;; Stratifiability checks.
|
|
(dl-nt-test! "non-stratifiable rejected"
|
|
(dl-nt-throws?
|
|
(fn ()
|
|
(let ((db (dl-make-db)))
|
|
(do
|
|
(dl-add-rule!
|
|
db
|
|
{:head (list (quote p) (quote X))
|
|
:body (list (list (quote q) (quote X))
|
|
{:neg (list (quote r) (quote X))})})
|
|
(dl-add-rule!
|
|
db
|
|
{:head (list (quote r) (quote X))
|
|
:body (list (list (quote p) (quote X)))})
|
|
(dl-add-fact! db (list (quote q) 1))
|
|
(dl-saturate! db)))))
|
|
true)
|
|
|
|
(dl-nt-test! "stratifiable accepted"
|
|
(dl-nt-throws?
|
|
(fn ()
|
|
(dl-program
|
|
"p(1). p(2). r(2).
|
|
q(X) :- p(X), not(r(X)).")))
|
|
false)
|
|
|
|
;; Multi-stratum chain.
|
|
(dl-nt-test-set! "three-level strata"
|
|
(dl-query
|
|
(dl-program
|
|
"a(1). a(2). a(3). a(4).
|
|
b(X) :- a(X), not(c(X)).
|
|
c(X) :- d(X).
|
|
d(2).
|
|
d(4).")
|
|
(list (quote b) (quote X)))
|
|
(list {:X 1} {:X 3}))
|
|
|
|
;; Safety violation: negation refers to unbound var.
|
|
(dl-nt-test! "negation safety violation"
|
|
(dl-nt-throws?
|
|
(fn ()
|
|
(dl-program
|
|
"p(1). q(X) :- p(X), not(r(Y)).")))
|
|
true))))
|
|
|
|
(define
|
|
dl-negation-tests-run!
|
|
(fn
|
|
()
|
|
(do
|
|
(set! dl-nt-pass 0)
|
|
(set! dl-nt-fail 0)
|
|
(set! dl-nt-failures (list))
|
|
(dl-nt-run-all!)
|
|
{:passed dl-nt-pass
|
|
:failed dl-nt-fail
|
|
:total (+ dl-nt-pass dl-nt-fail)
|
|
:failures dl-nt-failures})))
|