| ?- sat(X + Y). sat(X=\=_A*Y#Y)
illustrates three facts. First, any accumulated constraints affecting
the top-level variables are displayed floundered
goals, since the query is not true for all X
and
Y
. Secondly, accumulated constraints are displayed as
sat(
V=:=
Expr)
or sat(
V=\=
Expr)
where V is a variable and Expr is a "polynomial",
i.e. an exclusive or of conjunctions of variables and
constants. Thirdly, _A
had to be introduced as an artificial
variable, since Y
cannot be expressed as a function of
X
. That is, X + Y
is true iff there exists an _A
such that X=\=_A*Y#Y
. Let's check it!
| ?- taut(_A ^ (X=\=_A*Y#Y) =:= X + Y, T). T = 1
verifies the above answer. Notice that the formula in this query is a tautology, and so it is entailed by an empty set of constraints.