Package-level declarations

A TermVisitor specialised for walking a Clause literal by literal, rather than term by term: instead of overriding TermVisitor.visitClause directly, implementors get separate hooks for the clause's head and for each body literal, further split into the negated (visitNegatedLiteral) and non-negated (visitNonNegatedLiteral) case — the very distinction the Datalog well-formedness checks in it.unibo.tuprolog.datalog are built on (see it.unibo.tuprolog.datalog.isNegated).

Whether every variable occurring in this Clause's head also occurs in at least one of its nonNegatedBodyLiterals — the Datalog requirement that a rule may not "invent" head variables that are never bound by a positive body goal. A it.unibo.tuprolog.core.Fact (empty body) vacuously satisfies this only if its head has no variables at all, since there are no non-negated body literals to bind them.

Whether every variable occurring in one of this Clause's negatedBodyLiterals also occurs in at least one of its nonNegatedBodyLiterals — the usual Datalog "safe negation" condition. It guarantees a negated literal such as not(q(Y)) is only ever checked once Y has already been bound to one of finitely many values by a positive goal earlier in the body, rather than requiring q to be enumerated over its (potentially infinite) universe of terms.

The predicate call graph of this Theory: one node per Indicator (functor/arity) that occurs as a rule head or as a body literal, and one edge per rule from its head's Indicator to each body literal's Indicator it calls — the edge weight is true for a positive call and false for a call through negation (isNegated). Facts contribute a node but no outgoing edge. Used by isNonRecursive to detect (possibly indirect, possibly negated) recursion.

Whether this Clause is function-free in the Datalog sense: no argument, anywhere in the head or in any body literal, is a compound term (a Struct with Struct.arity > 0) — only constants and variables may appear as arguments. For instance parent(X, Y) qualifies, while parent(f(X), Y) does not, because f(X) is itself a compound. Backed by the CompoundFinder visitor.

Whether this Theory belongs to the (function-free, safely-negated, non-recursive) Datalog subset of Prolog recognised by this module, i.e. whether every one of its Theory.rules satisfies hasNoCompound, allHeadVariablesInNonNegatedLiterals and allNegatedLiteralsVariablesInNonNegatedLiteralsToo, and the theory as a whole is isNonRecursive.

Whether this Struct is a negation literal, i.e. a unary not(...) or \+(...) term — the two negation predicates recognised throughout this module (see Clause.negatedBodyLiterals).

Whether this Theory's callGraph is acyclic, i.e. no predicate directly or transitively calls itself, whether through positive or negated literals. Datalog evaluation typically tolerates recursion (that is indeed one of its selling points over plain non-recursive query languages), but this module enforces a stricter, recursion-free reading — see isDatalog.

All literals of this Clause: its Clause.head (if any, i.e. if this is a Rule), followed by every goal in Clause.bodyItems, each normalised to a Struct via asLiteral.

The body literals of this Clause that are negated, i.e. for which isNegated holds.

The body literals of this Clause that are not negated, i.e. for which isNegated does not hold.

Asserts allHeadVariablesInNonNegatedLiterals.

Asserts allNegatedLiteralsVariablesInNonNegatedLiteralsToo.

Asserts hasNoCompound, i.e. that no argument of this Clause is a compound term.

Asserts isDatalog rule by rule, so that the resulting exception identifies precisely which rule and which condition (hasNoCompound, allHeadVariablesInNonNegatedLiterals or allNegatedLiteralsVariablesInNonNegatedLiteralsToo) was violated first, before finally checking ensureIsNonRecursive on the theory as a whole.

Asserts isNonRecursive.