Native C++ Datalog

Lotus provides a native, strongly typed C++17 Datalog runtime under lib/Solvers/Datalog (implementation) and include/Solvers/Datalog (headers). The template API lowers rules to a type-erased semantic IR, then compiles relation dependencies into an SCC-ordered execution plan.

The runtime supports positive recursion, conditions, head expressions, distinct-aware greedy join planning, specialized full and partial runtime indexes, stratified aggregation and negation, lattice relations, and bulk-synchronous parallel evaluation.

#include "Solvers/Datalog/Core/Program.h"

using namespace lotus::datalog;

context ctx;
auto edge = ctx.relation<int, int>("edge");
auto path = ctx.relation<int, int>("path");
auto x = ctx.var<int>("x");
auto y = ctx.var<int>("y");
auto z = ctx.var<int>("z");

program p(ctx);
p.rule(path(x, y), edge(x, y));
p.rule(path(x, z), path(x, y) && edge(y, z));

edge.insert(1, 2);
edge.insert(2, 3);
auto compiled = p.compile();
ExecutionOptions options;
options.worker_count = 4;
RunStatus status = compiled.run(options);

Core/Program.h is the entry point for the native C++ API. Lower-level APIs are exposed through focused headers under Core, Runtime, and Semantic; there is no catch-all umbrella header.

The aggregate API provides collecting, streaming, and reducible factories. Reducible aggregators run with worker-local state. The lattice library includes minimum, maximum, set-union, dual, product, bounded-set, and constant-propagation values.

The current semantic and architecture reference is maintained in lib/Solvers/Datalog/README.md.

Command-line engine

lotus-datalog is the engine entry point for non-C++ clients. Native Datalog, Z3 fixedpoint input, and JSON all lower to the same type-erased Semantic IR; the runtime does not contain format-specific execution paths.

./build/bin/lotus-datalog schema > transitive-closure.json
./build/bin/lotus-datalog validate transitive-closure.json
./build/bin/lotus-datalog run transitive-closure.json --workers 4 --pretty
./build/bin/lotus-datalog schema | ./build/bin/lotus-datalog run -
./build/bin/lotus-datalog run tools/solver/datalog/examples/transitive_closure.dl
./build/bin/lotus-datalog run tools/solver/datalog/examples/z3_fixedpoint.smt2

The .dl frontend covers the portable engine semantics: typed set and lattice relations, inline facts, nullary predicates, multiple heads, positive rules, stratified negation, filters and expressions, and the built-in aggregates. The Z3 frontend supports the finite relational intersection: bit-vector or finite-domain sorts, relation and variable declarations, Horn rules, conjunction, stratified relation negation, and whole-relation queries. Format is detected automatically or chosen with --format auto|json|datalog|z3.

The reusable frontend API is declared in include/Solvers/Datalog/Frontend/Frontend.h and implemented by the LotusDatalogFrontend library under lib/Solvers/Datalog/Frontend. JSON, Lotus Datalog, Z3, and dispatch live in separate translation units and produce a source-aware FrontendIR which lowers directly to SemanticProgram without a JSON round trip. SourceUnit/executeInputs compose declarations, facts, and rules from multiple files; declarations may follow their uses. Native .include uses an injected SourceResolver so the library never chooses filesystem policy. The CLI contains no parser implementation and supplies a relative-path resolver. Output rows are sorted deterministically, making it suitable for future Python differential and performance harnesses. The complete syntax is documented in tools/solver/datalog/README.md.