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

formulas(utils).
   ds1 = domain_size + -1.
   all x (x < ds1 -> s(x) = x+1).   %s(ds1) = ds1. %successor function
   all x (x > 0 -> p(x) = x + -1).  %p(0) = 0.     %predecessor function
   stars = 1.                       %only one star per block
end_of_list.

formulas(star_battle).
  all x all y (f(x,y) < 2).         %cells can be 0 (no star) or 1 (star)
  f(x,y1) = 1 & f(x,y2) = 1 -> y1 = y2.         %only one star per row  
  f(x1,y) = 1 & f(x2,y) = 1 -> x1 = x2.         %only one star per column  

  %no two stars can be adjacent horizontally, vertically or diagonally
  %the sum of the values adjacent to a star must be 1
  f(x,y) = 1 -> f(p(x),p(y)) + f(p(x),y) + f(p(x),s(y)) +
                f(x,p(y))    +             f(x,s(y))    +
                f(s(x),p(y)) + f(s(x),y) + f(s(x),s(y)) = 0.
end_of_list.

formulas(sample_puzzle).
  f(0,0) + f(0,1) = stars.
  f(0,2) + f(0,3) + f(0,4) + f(1,4) + f(1,3) + f(1,2) = stars.
  f(1,0) + f(1,1) + f(2,0) + f(2,1) = stars.
  f(3,0) + f(3,1) + f(3,2) + f(2,2) + f(2,3) + f(2,4) = stars.
  f(4,0) + f(4,1) + f(4,2) + f(4,3) + f(4,4) + f(3,4) + f(3,3) = stars.
end_of_list.

