| ?-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.

Send feedback on this subject.