DeepLog

Abstract

Added One module for N formulas. DeepLogModuleFactory.compile(*nodes) takes any number of formula ASTs and returns one module with a column per formula, in the order given. Before, N formulas meant N compile calls — N circuit factories, N knowledge compilations, and a copy of every predicate module per formula — even where they shared subformulas, atoms, or the boolean circuit they count. The engine path already had the batching (compile_to_module builds co-resident lumps and hands them to lower_circuit_nodes); the AST path now reaches the same mechanism rather than a second one. Both folds run over every root under one memo, so a subformula the roots share as an object is built once and the atoms they share are one circuit leaf; when every root constructs to a lump of one circuit they are lowered through lower_circuit_nodes, so the boundary is folded once, one knowledge compilation serves every count over that circuit, and each predicate module is evaluated once. Any other mix — roots in different algebras, a root that stayed an enumeration — is lowered root by root and composed column-wise, where a shared sub-module is built once but still evaluated once per root enclosing it: slower, never wrong. compile(node) is unchanged, output shape included. Two roots that would name the same column are refused rather than silently collapsing into one, and sharing between separately parsed formulas reaches only their atoms, since each parse interns into its own hash-cons table. deeplog.formula.ast.fold takes the optional memo its circuit-side counterpart fold_circuit already had, and is now the whole fold — the private _fold that two modules imported across package boundaries is gone. children(node) joins it as the shallow projection companion to map_children, for the walks that read children without rewriting them. deeplog.formula.circuit_node.lump_name(node) is the one spelling of the name a lump compiles under, which three sites had written by hand and two of them carried a docstring warning that drift is silent. Operators with no circuit form are now lowered as tensor operations instead of being rejected (glab #137), and an operator with no node form is compiled across rather than kept out. Which of the two applies is not configured anywhere and not asked of the algebra: an operator over operands that could not be circuit-represented (a connective or a division over a quantifier, or over two separately lowered modules) is applied to their already-reduced outputs by the new ElementwiseModule (deeplog.module.ElementwiseModule), which aligns the operands onto their symbol-union input and combines them column-wise, broadcasting a single column across the rest. This makes connectives over quantifiers compile — And(Forall x . φ, Forall y . ψ) in the LTN fuzzy setting previously raised NotImplementedError. ColumnwiseModule is the single-module dual: it evaluates one module once and applies the operator across selections of its output columns, and now names its own output columns when asked (names=) instead of always borrowing the first group's. Circuits are compiled across an operator the backend has no node for, rather than the operator being kept out of the circuit — the new deeplog.circuit.split. A semifield's divide is the standing case: knowledge compilation and Klay build their graph out of a semiring's product, sum and complement, and a quotient is none of those. So the graph is cut there: the operand subgraphs are compiled as roots of one ordinary compilation, the algebra's own operator_fns entry combines their output columns, and the region above the cut is the same circuit compiled again, bounded at the cuts, which it treats as input slots fed by those columns. A division is therefore an elementwise operation on circuits, and what sits above one is still a circuit on the backend the algebra selected — where previously everything above a division stayed symbolic to the root. Nesting needs no extra machinery: the operands are compiled by the same entry point, which cuts them in turn. Circuit.get_operator accordingly accepts every operator its algebra defines, divide included. Bounding a compile is frontier, a new optional {node_id: symbol} argument on Circuit.to_module and on the traversals the backends walk (Circuit.iter_topological / reachable_leaves / reachable_constants / flatten_chains, and Graph.iter_topological / flatten_chains beneath them): those nodes are yielded but not descended into, and they are input slots of the region above them under the given symbols. It is what makes a partition compile without being copied into a circuit of its own. Semifield (deeplog.Semifield) — a Semiring whose product is invertible, so divide is defined. PROBABILITY and LOGPROBABILITY are now semifields. The algebra declares the quotient and says nothing about what compiles it — no backend walk has a node for one, so it is cut (deeplog.circuit.split) — and the denominator floor that keeps impossible evidence finite lives on the algebra rather than on the module performing the division, and log-space division is subtraction, floored at finfo.min rather than at the linear floor transported through log — the two representations have different floors by design, since log space exists to hold probabilities far below the linear one, and clamping a log denominator at log(tiny) (-87.3 in float32) silently corrupts any program with more than ~126 independent facts. The floor is derived from the operands' dtype (torch.finfo(dtype).tiny) rather than pinned: for a numerator in [0, 1] that is the smallest denominator the dtype can divide by without overflowing, whereas the 1e-12 it replaces was a float32 constant that stores as exactly zero in float16 — the clamp was a silent no-op there and impossible evidence came back as inf/nan. There is no floor setting: DEFAULT_DIVISION_EPS, DEFAULT_RATIO_EPS and the eps argument of Semifield are all removed. An algebra whose division differs at all supplies the whole division_fn, which subsumes a one-scalar knob and cannot silently disagree with it — eps alongside division_fn was a representable state in which eps was ignored. In float32 the floor relaxes from 1e-12 to 1.18e-38, so a denominator between the two is no longer clamped. Scalar posterior recognition: P(q | e) = E[q∧e] / E[e] compiles as a divide of two expectation aggregations. Division is an operator of the probability Semifield like any other, so it becomes an ordinary circuit node; no backend walk has a node for a quotient, so deeplog.circuit.split cuts the graph there and applies the algebra's divide across the compiled columns (denominator clamped away from zero, so impossible evidence stays finite). recognize_posterior rewrites divide(WMC, WMC) into divide(expectation, expectation) when both operands are expectations/canonical weighted model counts and the denominator evidence is a conjunct of the numerator q ∧ e; it runs ahead of recognize_expectation in DEFAULT_PASSES. Like every other pass it is recognition-only — a divide it does not recognize is left alone and still lowers, as a plain division of its two operands. Probability domain only for now. Numeric-constant facts (0.6 :: fact) are now baked into the PySDD-compiled arithmetic circuit, matching the MV-SDD backend: a boolean leaf whose EngineResult.labels entry is a numeric constant is pre-filled rather than left a runtime input, so a program of only numeric facts compiles to a module with no inputs (only neural-network-backed labels stay inputs). A fully-baked, input-less module is callable bare (module()): ModuleCircuit evaluates a single constant row when handed no tensors, and a WrappedModule pre-hook synthesises the empty (1, 0) batch channel. to_module accepts its roots as a single {name: node} mapping, the shape multi-root producers (grounder proofs, engine result formulas) already have, alongside the existing positional CircuitNodes with names. The mapping form forbids names and takes its output order from insertion order, exactly as the positional form does; a mapping mixed with other positional roots raises. Naming the same node twice now raises Duplicate root instead of silently collapsing the two outputs into one. to_dict(tensors, shape) — the read-out counterpart of shape validation. It splits a module's result along its symbolic shape into a {Symbol: tensor} mapping with the batch dimension preserved, so to_dict(module(x), module.get_output_shape()) reads a module's outputs by name instead of by index. The result is a SymbolDict, a plain dict whose repr prints pretty symbols and formats scalars compactly, so interactive readouts stay legible. Raises ShapeMismatchException when the tensors do not conform to shape, and ValueError when shape names the same symbol twice. Exported from the top-level package. DeepProbLog conditional queries: a program's :- body. integrity constraints now condition every query on evidence, so Solver.get_query_result returns the posterior P(q | e) = E[q∧e] / E[e] instead of the prior P(q). A constraint :- body reads as "body must not hold" (the operator dual of the ?- q query directive), so positive evidence is written :- not(e). and negative evidence :- e.. The engine builds the shared evidence e = ⋀ᵢ ¬(bodyᵢ) on the same source circuit as the query proofs — so each numerator q∧e and the denominator e co-reside and share leaves — and carries it on the new EngineResult.evidence field; compile_to_module transforms numerators and the shared denominator in one batched WMC pass, lowers all of them in one knowledge compilation, and divides with the new PosteriorModule (deeplog.module.PosteriorModule), so the shared circuit and the predicate modules feeding it are evaluated once for all answers rather than once per answer. Conditional and unconditional results have the same shape — one SymTensor with a column per query answer — so adding a constraint to a program does not reshape its result. With no cons