mention how instantiation-nested predicates are treated in stratification and evaluation

This commit is contained in:
Philip Ginsbach
2023-06-20 12:17:43 +01:00
parent 0c4eb68921
commit e4e91c7ab0

View File

@@ -2046,6 +2046,8 @@ A valid stratification must include each predicate and type in the QL program th
A valid stratification must not include the same predicate in multiple layers.
Each non-abstract predicate has an associated body. For predicates inside *declared modules*, this is the predicate declaration. The body of an *instantiation-nested* predicate is the body of the *underlying nested* predicate where all references and calls have been substituted with the *instantiation-relative* entity or alias.
Formulas, variable declarations and expressions within a predicate body have a *negation polarity* that is positive, negative, or zero. Positive and negative are opposites of each other, while zero is the opposite of itself. The negation polarity of a formula or expression is then determined as follows:
- The body of a predicate is positive.