% Find up to 1000 models up through size 25

assign(iterate_up_to, 25).
assign(max_models, 1000).

% The following fixes [+,-,*] as the ring of integers (mod domain_size).

set(integer_ring).

% For efficiency of the search when doing integer_ring constraints,
% it is important to have a good symbol ordering.  The ring coefficients
% (A,B,C in this case) should be first.  One could use a "lex" command
% to achieve this.  An easier way is to rely on the default ordering,
% which places upper case constants before lower case constants.
% Skolem constants are lower case, so the following gives a good ordering.

% Change operator name to @, because * is the ring product.

formulas(theory).

x @ y = (A * x) + (B * y).

(x @ e) @ x = x.
x @ (x @ y) = y.
(x @ y) @ (z @ u) = (x @ z) @ (y @ u).
((x @ x) @ x) @ x = e.

end_of_list.
