set(arithmetic).
assign(domain_size,6). 
assign(max_models,-1).

formulas(utils).
  con = domain_size/2.
  ds1 = domain_size + -1.
  all x (x < ds1 -> s(x) = x+1) & s(ds1) = 5.         %succesor function
end_of_list.

formulas(3_in_a_row_with_two_functions).
 all x all y (w(x,y)<= 1) & (b(x,y)<= 1). %white/blue are true/false only
 all x all y (w(x,y) = 1 ->  b(x,y) = 0). %cells can only have a colour
 all x all y (w(x,y) = 1  |  b(x,y) = 1). %cells need to have a colour

 %number(white cells) = number(blue cells) = 3 on each row/column (con=3)
 all x w(x,0) + w(x,1) + w(x,2) + w(x,3) + w(x,4) + w(x,5) = con.
 all y w(0,y) + w(1,y) + w(2,y) + w(3,y) + w(4,y) + w(5,y) = con.

 %cannot have 3 of a kind in a row (con=3)
 all x all y (y <= con -> -(w(x,y)=1 & w(x,s(y))=1 & w(x,s(s(y)))=1) &
                          -(b(x,y)=1 & b(x,s(y))=1 & b(x,s(s(y)))=1)).

 %cannot have 3 of a kind in a column (con=3)
 all x all y (x <= con -> -(w(x,y)=1 & w(s(x),y)=1 & w(s(s(x)),y)=1) &
                          -(b(x,y)=1 & b(s(x),y)=1 & b(s(s(x)),y)=1)). 
end_of_list.

formulas(sample_puzzle).
  b(0,4)=1 & b(1,0)=1 & b(1,4)=1 & b(4,0)=1 & b(5,0)=1.
  w(0,1)=1 & w(3,5)=1 & w(4,5)=1.
end_of_list.
