datalog.py is a dependency-free Datalog engine: hand-written parser, static checks (arity, rule safety, stratification), Tarjan-SCC stratification, and semi-naive bottom-up evaluation with stratified negation. No imports beyond the standard library.

Files

datalog.py          the engine (module + JSON/text CLI)
test_datalog.py     the verification suite — its exit code is the verdict
evidence_run.py     reproduces every number in EVIDENCE.txt
examples/reach.dl   CLI demo program
EVIDENCE.txt        captured output of the above (measured, not claimed)

Run it

python3 datalog.py examples/reach.dl --text --stats
python3 datalog.py examples/reach.dl -q unreachable      # JSON, one predicate
python3 test_datalog.py                                  # 0 = all checks pass

Language

% comment
edge(a, b).                        % fact
path(X, Y) :- edge(X, Y).          % rule
path(X, Y) :- edge(X, Z), path(Z, Y).
unreach(X) :- node(X), not reach(X).   % '!' is accepted as 'not'

Terms: ?X variable, ?_ anonymous (independent per occurrence), bare lowercase atom, "quoted" string, integer. Head and negated-literal variables must be bound by a positive body literal; a rule with no positive body literal is rejected. Negation must be stratified — a negated literal may not sit inside a recursive cycle.

Verification (this is the point of the artifact)

test_datalog.py = 40 tests, 0 failures. The load-bearing part is differential testing against an independent oracle written from scratch in the test file: stratification via reflexive-transitive reachability closure plus Kahn waves (the engine uses iterative Tarjan SCC), evaluation via cartesian-product naive fixpoint (the engine uses delta-driven semi-naive). The two share only the parser.

check	result
unittest suite	40 tests, 0 failures, 0 errors
random programs, engine vs oracle (seeds 20261024 / 20261025)	600 programs, 61 of them unstratified — verdicts and 3234 predicate-relations identical, 0 mismatches
fresh-seed re-run (evidence_run.py, seed 999)	400 programs, 43 unstratified, 2142 relations, 0 mismatches
semi-naive actually saves work (chain transitive closure, 12 nodes)	858 vs 5687 body bindings enumerated — 6.6x; at n=20, 3990 vs 47291 — 11.9x
KATs	transitive closure, non-linear same-generation recursion, stratified negation, anonymous vars in negation, zero-arity, repeated variables, order independence

Numbers above are read off EVIDENCE.txt, which evidence_run.py regenerates in one run.

Bug this suite actually caught

The first run of the differential test failed on 1 of 300 random programs: the engine derived p0(c, c) where the oracle derived nothing. Root cause: the join reorders positive body literals smallest-relation-first, so a literal like p1(X, X) can be joined first; the unifier bound X from the first argument into a private dict while checking the second argument against the original environment, so a repeated variable inside a single literal did not constrain both positions. Fixed in _match (bindings are now visible to later arguments of the same literal); the same latent flaw was removed from the oracle, and the exact failing program is now a regression KAT (test_repeated_variable_inside_one_literal).

Stated limits (not hidden)

String constants compare as written — no unescaping, so two spellings of the same escaped string are distinct terms.
- is a token only as part of an integer literal; no arithmetic or builtins.
No functors, no aggregation, no $ref-style imports.
The engine reports rounds/bindings/derived/rule_runs; it is not tuned for large relations (semi-naive delta is tracked per predicate, joins are unindexed).