#### 32.2.3 Example 3

| ?- `[user].`
| `adder(X, Y, Sum, Cin, Cout) :-`
`sat(Sum =:= card([1,3],[X,Y,Cin])),`
`sat(Cout =:= card([2-3],[X,Y,Cin])).`
| `^D`
% consulted user in module user, 0 msec 424 bytes
| ?- `adder(x, y, Sum, cin, Cout).`
sat(Sum=:=cin#x#y),
sat(Cout=:=x*cin#x*y#y*cin)
| ?- `adder(x, y, Sum, 0, Cout).`
sat(Sum=:=x#y),
sat(Cout=:=x*y)
| ?- `adder(X, Y, 0, Cin, 1), labeling([X,Y,Cin]).`
Cin = 0,
X = 1,
Y = 1 ? `;`
Cin = 1,
X = 0,
Y = 1 ? `;`
Cin = 1,
X = 1,
Y = 0 ? `;`

illustrates the use of cardinality constraints and models a one-bit
adder circuit. The first query illustrates how representing the
input signals by symbolic constants forces the output signals to be
displayed as functions of the inputs and not vice versa. The second
query computes the simplified functions obtained by setting
carry-in to 0. The third query asks for particular input values
satisfying sum and carry-out being 0 and 1, respectively.