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