Relaxed Safety
@relaxedSafety.The computational properties of the engine are guaranteed by safety checks (e.g. wardedness and linearity).
These conditions on the program guarantee that the evaluation will terminate computing the correct
result. In many cases where there is interaction between Skolem functions, aggregate functions and user-defined
functions, these conditions become very restrictive, and many programs are unnecessarily refused by the engine.
The engine supports a relaxed mode of operation whereby Skolem functions and existential variables are treated
separately from built-in and user-defined functions. This mode of operation is more permissive, but programs
that are accepted may not be safe in general. To trigger this mode of operation one should use the program
annotation @relaxedSafety. The following program, deemed unsafe in the default mode of operation, is
accepted with the annotation @relaxedSafety, and computes the (non-monotonic) sum aggregate on the relation a.
a(1, 2).
a(1, 3).
a(1, 4).
a(2, 2).
a(2, 4).
a_msum(X, Z) :- a(X, Y), Z = msum(Y).
a_msum_red(X, Z1) :- a_msum(X, Z1), a_msum(X, Z2), Z2 > Z1 .
a_sum(X, Z) :- a_msum(X, Z), not a_msum_red(X, Z).
@output("a_sum").
@relaxedSafety.The output of the program is:
a_sum(1, 9). a_sum(2, 6).