set(arithmetic).
assign(domain_size,9).                  %8 arrows and an empty space
assign(max_models,1).

formulas(stars_and_arrows).
  all x all y (x < 5 & y < 5 ->  
     (f(x,y) < 2) & 
     (f(x,0) + f(x,1) + f(x,2) + f(x,3) + f(x,4) = f(x,5)) & 
     (f(0,y) + f(1,y) + f(2,y) + f(3,y) + f(4,y) = f(5,y))).

  all x all y (x > 5 | y > 5 -> f(x,y) = 0).
  f(5,5)=0.
 
  NA = 0.  L  = 1.    R = 2.   U = 3.    D = 4.
          DL  = 5.   DR = 6.  UL = 7.   UR = 8. 

  all x all y (x > 4 | y > 4 -> g(x,y) = 0).
  
  %Where is arrow, there is no star
  all x all y ((x <= 4 & y <= 4 & g(x,y) != 0) -> f(x,y) = 0). 
   
  %Each arrow points to at least one star
  g(x,y) = R  -> exists z (z > y & f(x,z) = 1). 
  g(x,y) = L  -> exists z (z < y & f(x,z) = 1).
  g(x,y) = U  -> exists z (z < x & f(z,y) = 1). 
  g(x,y) = D  -> exists z (z > x & f(z,y) = 1). 
  g(x,y) = DR -> (exists x1 exists y1 
     (x1 > x & y1 > y & (x1 + -x = y1 + -y) & f(x1,y1) = 1)). 
  g(x,y) = DL  -> (exists x1 exists y1 
     (x1 > x & y1 < y & (x1 + -x = y + -y1) & f(x1,y1) = 1)). 
  all x all y ((x > 0 & y < 4 & g(x,y) = UR) -> (exists x1 exists y1 
     (x1 < x & y1 > y & (x + -x1 = y1 + -y) & f(x1,y1) = 1))). 
  all x all y ((x > 0 & y > 4 & g(x,y) = UL) -> (exists x1 exists y1 
     (x1 < x & y1 < y & (x + -x1 = y1 + -y) & f(x1,y1) = 1))). 
end_of_list.

formulas(sample_puzzle).
  f(0,5) = 2 & f(1,5) = 2 & f(2,5) = 3 & f(3,5) = 0 & f(4,5) = 1.
  f(5,0) = 1 & f(5,1) = 2 & f(5,2) = 3 & f(5,3) = 2 & f(5,4) = 0. 

  g(0,0) = DR. g(0,1) = NA. g(0,2) = DL. g(0,3) = NA. g(0,4) = NA.
  g(1,0) = NA. g(1,1) = R.  g(1,2) = NA. g(1,3) = NA. g(1,4) = UL.  
  g(2,0) = NA. g(2,1) = NA. g(2,2) = NA. g(2,3) = NA. g(2,4) = NA.
  g(3,0) = NA. g(3,1) = U.  g(3,2) = NA. g(3,3) = NA. g(3,4) = NA.
  g(4,0) = UR. g(4,1) = NA. g(4,2) = NA. g(4,3) = UL. g(4,4) = L.
end_of_list.
