;;; Reflect Connect (6x6)

;;; components

(role red)
(role blue)

(base (step 1))
(<= (base (step ?n)) (stepcount ?m ?n))

(<= (base (control ?r)) (role ?r))

(<= (base (captured ?r ?n))
	(role ?r)
	(number ?n))

(<= (base (cell ?x ?y ?c))
	(lowindex ?x)
	(lowindex ?y)
	(color ?c)
	(distinct ?x 6))

(<= (base (cell ?x ?y ?c))
	(lowindex ?x)
	(lowindex ?y)
	(color ?c)
	(distinct ?y 6))

(<= (base (cell ?x ?y ?c))
	(hiindex ?x)
	(hiindex ?y)
	(color ?c)
	(distinct ?x 6))

(<= (base (cell ?x ?y ?c))
	(hiindex ?x)
	(hiindex ?y)
	(color ?c)
	(distinct ?y 6))


;;; input

(<= (input ?r (move ?x1 ?y1 ?x2 ?y2))
	(role ?r)
	(adjacent ?x1 ?y1 ?x2 ?y2))

(<= (input ?r (move ?x1 ?y1 ?x2 ?y2))
	(role ?r)
	(diagonal ?x1 ?y1 ?x2 ?y2))

(<= (input ?r (move ?x1 ?y1 ?x2 ?y2))
	(role ?r)
	(reflectto ?x1 ?x2)
	(reflectto ?y1 ?y2))

(<= (input ?r noop) (role ?r))


;;; init

(init (step 1))
(init (control red))
(init (captured red 0))
(init (captured blue 0))

(init (cell 1 1 red))
(init (cell 2 1 red))
(init (cell 3 1 red))
(init (cell 4 1 red))
(init (cell 5 1 red))
(init (cell 1 2 red))
(init (cell 2 2 red))
(init (cell 3 2 red))
(init (cell 4 2 red))
(init (cell 1 3 red))
(init (cell 2 3 red))
(init (cell 3 3 red))
(init (cell 1 4 red))
(init (cell 2 4 red))
(init (cell 1 5 red))

(init (cell 7 11 blue))
(init (cell 8 11 blue))
(init (cell 9 11 blue))
(init (cell 10 11 blue))
(init (cell 11 11 blue))
(init (cell 8 10 blue))
(init (cell 9 10 blue))
(init (cell 10 10 blue))
(init (cell 11 10 blue))
(init (cell 9 9 blue))
(init (cell 10 9 blue))
(init (cell 11 9 blue))
(init (cell 10 8 blue))
(init (cell 11 8 blue))
(init (cell 11 7 blue))

(init (cell 1 6 blank))
(init (cell 2 6 blank))
(init (cell 3 6 blank))
(init (cell 4 6 blank))
(init (cell 5 6 blank))
(init (cell 2 5 blank))
(init (cell 3 5 blank))
(init (cell 4 5 blank))
(init (cell 5 5 blank))
(init (cell 6 5 blank))
(init (cell 3 4 blank))
(init (cell 4 4 blank))
(init (cell 5 4 blank))
(init (cell 6 4 blank))
(init (cell 4 3 blank))
(init (cell 5 3 blank))
(init (cell 6 3 blank))
(init (cell 5 2 blank))
(init (cell 6 2 blank))
(init (cell 6 1 blank))
(init (cell 6 11 blank))
(init (cell 6 10 blank))
(init (cell 7 10 blank))
(init (cell 6 9 blank))
(init (cell 7 9 blank))
(init (cell 8 9 blank))
(init (cell 6 8 blank))
(init (cell 7 8 blank))
(init (cell 8 8 blank))
(init (cell 9 8 blank))
(init (cell 6 7 blank))
(init (cell 7 7 blank))
(init (cell 8 7 blank))
(init (cell 9 7 blank))
(init (cell 10 7 blank))
(init (cell 7 6 blank))
(init (cell 8 6 blank))
(init (cell 9 6 blank))
(init (cell 10 6 blank))
(init (cell 11 6 blank))


;;; legal

(<= (legal ?r (move ?x1 ?y1 ?x2 ?y2))
	(true (control ?r))
	(true (cell ?x1 ?y1 ?r))
	(adjacent ?x1 ?y1 ?x2 ?y2)
	(true (cell ?x2 ?y2 blank)))

(<= (legal ?r (move ?x1 ?y1 ?x2 ?y2))
	(true (control ?r))
	(role ?r2)
	(distinct ?r ?r2)
	(true (cell ?x1 ?y1 ?r))
	(adjacent ?x1 ?y1 ?x2 ?y2)
	(true (cell ?x2 ?y2 ?r2))
	(not (true (captured ?r 3))))

(<= (legal ?r (move ?x1 ?y1 ?x2 ?y2))
	(true (control ?r))
	(true (cell ?x1 ?y1 ?r))
	(diagonal ?x1 ?y1 ?x2 ?y2)
	(true (cell ?x2 ?y2 blank)))

(<= (legal ?r (move ?x1 ?y1 ?x2 ?y2))
	(true (control ?r))
	(role ?r2)
	(distinct ?r ?r2)
	(true (cell ?x1 ?y1 ?r))
	(diagonal ?x1 ?y1 ?x2 ?y2)
	(true (cell ?x2 ?y2 ?r2))
	(not (true (captured ?r 3))))

(<= (legal ?r (move ?x1 ?y1 ?x2 ?y2))
	(true (control ?r))
	(true (cell ?x1 ?y1 ?r))
	(reflectto ?x1 ?x2)
	(reflectto ?y1 ?y2)
	(true (cell ?x2 ?y2 blank)))

(<= (legal ?r noop)
	(role ?r)
	(not (true (control ?r))))


;;; next

(<= (next (step ?n))
	(stepcount ?m ?n)
	(true (step ?m)))

(<= (next (control red))
	(true (control blue)))

(<= (next (control blue))
	(true (control red)))

;;; no capture occurs
(<= (next (captured ?r ?n))
	(true (captured ?r ?n))
	(does ?r (move ?x1 ?y1 ?x2 ?y2))
	(true (cell ?x2 ?y2 blank)))

;;; opponent piece captured
(<= (next (captured ?r ?n))
	(does ?r (move ?x1 ?y1 ?x2 ?y2))
	(true (cell ?x2 ?y2 ?r2))
	(distinct ?r2 blank)
	(true (captured ?r ?m))
	(captureadd ?m ?n))

;;; not r's turn
(<= (next (captured ?r ?n))
	(true (captured ?r ?n))
	(not (true (control ?r))))

;; move to cell(x,y)
(<= (next (cell ?x ?y ?r))
	(does ?r (move ?x0 ?y0 ?x ?y)))

;; move away from cell(x,y)
(<= (next (cell ?x ?y blank))
	(true (cell ?x ?y ?r))
	(does ?r (move ?x ?y ?x2 ?y2)))

;; move does not involve cell(x,y)
(<= (next (cell ?x ?y ?r))
	(true (cell ?x ?y ?r))
	(does ?r2 (move ?x1 ?y1 ?x2 ?y2))
	(distinct ?x ?x1)
	(distinct ?x ?x2))

(<= (next (cell ?x ?y ?r))
	(true (cell ?x ?y ?r))
	(does ?r2 (move ?x1 ?y1 ?x2 ?y2))
	(distinct ?x ?x1)
	(distinct ?y ?y2))

(<= (next (cell ?x ?y ?r))
	(true (cell ?x ?y ?r))
	(does ?r2 (move ?x1 ?y1 ?x2 ?y2))
	(distinct ?y ?y1)
	(distinct ?x ?x2))

(<= (next (cell ?x ?y ?r))
	(true (cell ?x ?y ?r))
	(does ?r2 (move ?x1 ?y1 ?x2 ?y2))
	(distinct ?y ?y1)
	(distinct ?y ?y2))


;;; goal

(<= (goal ?r 50) 
	(role ?r)
	(advantage 0 ?r))

(<= (goal ?r 70) 
	(role ?r)
	(advantage 1 ?r))

(<= (goal ?r 30)
	(role ?r)
	(role ?r2)
	(distinct ?r ?r2)
	(advantage 1 ?r2))

(<= (goal ?r 80) 
	(role ?r)
	(advantage 2 ?r))

(<= (goal ?r 20)
	(role ?r)
	(role ?r2)
	(distinct ?r ?r2)
	(advantage 2 ?r2))

(<= (goal ?r 90) 
	(role ?r)
	(advantage 3 ?r))

(<= (goal ?r 10)
	(role ?r)
	(role ?r2)
	(distinct ?r ?r2)
	(advantage 3 ?r2))

(<= (goal ?r 100) 
	(role ?r)
	(advantage 4 ?r))

(<= (goal ?r 0)
	(role ?r)
	(role ?r2)
	(distinct ?r ?r2)
	(advantage 4 ?r2))


;;; terminal

(<= terminal (align 4 ?r))

(<= terminal (true (step 40)))


;;; views

(<= (advantage 0 ?r)
	(alignnum ?n)
	(maxalign ?n ?r)
	(role ?r2)
	(distinct ?r ?r2)
	(maxalign ?n ?r2))

(<= (advantage 1 ?r)
	(alignnum ?n)
	(maxalign ?n ?r)
	(advantagesucc ?m ?n)
	(role ?r2)
	(distinct ?r ?r2)
	(maxalign ?m ?r2))

(<= (advantage 2 ?r)
	(alignnum ?n)
	(maxalign ?n ?r)
	(advantagesucc ?m2 ?n)
	(advantagesucc ?m1 ?m2)
	(role ?r2)
	(distinct ?r ?r2)
	(maxalign ?m1 ?r2))

(<= (advantage 3 ?r)
	(alignnum ?n)
	(maxalign ?n ?r)
	(advantagesucc ?m3 ?n)
	(advantagesucc ?m2 ?m3)
	(advantagesucc ?m1 ?m2)
	(role ?r2)
	(distinct ?r ?r2)
	(maxalign ?m1 ?r2))

(<= (advantage 4 ?r)
	(maxalign 4 ?r)
	(role ?r2)
	(distinct ?r ?r2)
	(maxalign 0 ?r2))

(<= (maxalign 0 ?r)
	(role ?r)
	(not (align 1 ?r)))

(<= (maxalign 1 ?r)
	(role ?r)
	(align 1 ?r)
	(not (align 2 ?r)))

(<= (maxalign 2 ?r)
	(role ?r)
	(align 2 ?r)
	(not (align 3 ?r)))

(<= (maxalign 3 ?r)
	(role ?r)
	(align 3 ?r)
	(not (align 4 ?r)))

(<= (maxalign 4 ?r) 
	(role ?r)
	(align 4 ?r))

(<= (align 1 red)
	(true (cell ?x ?y red))
	(hiindex ?x)
	(hiindex ?y))

(<= (align 1 blue)
	(true (cell ?x ?y blue))
	(lowindex ?x)
	(lowindex ?y))

;; vertical lines
(<= (align 2 red)
	(true (cell ?x ?y1 red))
	(hiindex ?x)
	(hiindex ?y1)
	(succ ?y1 ?y2)
	(true (cell ?x ?y2 red)))

(<= (align 2 blue)
	(true (cell ?x ?y2 blue))
	(lowindex ?x)
	(lowindex ?y2)
	(succ ?y1 ?y2)
	(true (cell ?x ?y1 blue)))

(<= (align 3 red)
	(true (cell ?x ?y1 red))
	(hiindex ?x)
	(hiindex ?y1)
	(succ ?y1 ?y2)
	(succ ?y2 ?y3)
	(true (cell ?x ?y2 red))
	(true (cell ?x ?y3 red)))

(<= (align 3 blue)
	(true (cell ?x ?y3 blue))
	(lowindex ?x)
	(lowindex ?y3)
	(succ ?y2 ?y3)
	(succ ?y1 ?y2)
	(true (cell ?x ?y2 blue))
	(true (cell ?x ?y1 blue)))

(<= (align 4 red)
	(true (cell ?x ?y1 red))
	(hiindex ?x)
	(hiindex ?y1)
	(succ ?y1 ?y2)
	(succ ?y2 ?y3)
	(succ ?y3 ?y4)
	(true (cell ?x ?y2 red))
	(true (cell ?x ?y3 red))
	(true (cell ?x ?y4 red)))

(<= (align 4 blue)
	(true (cell ?x ?y4 blue))
	(lowindex ?x)
	(lowindex ?y4)
	(succ ?y3 ?y4)
	(succ ?y2 ?y3)
	(succ ?y1 ?y2)
	(true (cell ?x ?y3 blue))
	(true (cell ?x ?y2 blue))
	(true (cell ?x ?y1 blue)))


;; horizontal lines
(<= (align 2 red)
	(true (cell ?x1 ?y red))
	(hiindex ?x1)
	(hiindex ?y)
	(succ ?x1 ?x2)
	(true (cell ?x2 ?y red)))

(<= (align 2 blue)
	(true (cell ?x2 ?y blue))
	(lowindex ?x2)
	(lowindex ?y)
	(succ ?x1 ?x2)
	(true (cell ?x1 ?y blue)))

(<= (align 3 red)
	(true (cell ?x1 ?y red))
	(hiindex ?x1)
	(hiindex ?y)
	(succ ?x1 ?x2)
	(succ ?x2 ?x3)
	(true (cell ?x2 ?y red))
	(true (cell ?x3 ?y red)))

(<= (align 3 blue)
	(true (cell ?x3 ?y blue))
	(lowindex ?x3)
	(lowindex ?y)
	(succ ?x2 ?x3)
	(succ ?x1 ?x2)
	(true (cell ?x2 ?y blue))
	(true (cell ?x1 ?y blue)))

(<= (align 4 red)
	(true (cell ?x1 ?y red))
	(hiindex ?x1)
	(hiindex ?y)
	(succ ?x1 ?x2)
	(succ ?x2 ?x3)
	(succ ?x3 ?x4)
	(true (cell ?x2 ?y red))
	(true (cell ?x3 ?y red))
	(true (cell ?x4 ?y red)))

(<= (align 4 blue)
	(true (cell ?x4 ?y blue))
	(lowindex ?x4)
	(lowindex ?y)
	(succ ?x3 ?x4)
	(succ ?x2 ?x3)
	(succ ?x1 ?x2)
	(true (cell ?x3 ?y blue))
	(true (cell ?x2 ?y blue))
	(true (cell ?x1 ?y blue)))


;; diagonal lines
(<= (align 2 red)
	(true (cell ?x1 ?y1 red))
	(hiindex ?x1)
	(hiindex ?y1)
	(succ ?x1 ?x2)
	(succ ?y1 ?y2)
	(true (cell ?x2 ?y2 red)))

(<= (align 2 red)
	(true (cell ?x1 ?y2 red))
	(hiindex ?x1)
	(succ ?x1 ?x2)
	(hiindex ?y2)
	(succ ?y1 ?y2)
	(hiindex ?y1)
	(true (cell ?x2 ?y1 red)))

(<= (align 3 red)
	(true (cell ?x1 ?y1 red))
	(hiindex ?x1)
	(hiindex ?y1)
	(succ ?x1 ?x2)
	(succ ?x2 ?x3)
	(succ ?y1 ?y2)
	(succ ?y2 ?y3)
	(true (cell ?x2 ?y2 red))
	(true (cell ?x3 ?y3 red)))

(<= (align 3 red)
	(true (cell ?x1 ?y3 red))
	(hiindex ?x1)
	(succ ?x1 ?x2)
	(succ ?x2 ?x3)
	(hiindex ?y3)
	(succ ?y2 ?y3)
	(hiindex ?y2)
	(succ ?y1 ?y2)
	(hiindex ?y1)
	(true (cell ?x2 ?y2 red))
	(true (cell ?x3 ?y1 red)))

(<= (align 4 red)
	(true (cell ?x1 ?y1 red))
	(hiindex ?x1)
	(hiindex ?y1)
	(succ ?x1 ?x2)
	(succ ?x2 ?x3)
	(succ ?x3 ?x4)
	(succ ?y1 ?y2)
	(succ ?y2 ?y3)
	(succ ?y3 ?y4)
	(true (cell ?x2 ?y2 red))
	(true (cell ?x3 ?y3 red))
	(true (cell ?x4 ?y4 red)))

(<= (align 4 red)
	(true (cell ?x1 ?y4 red))
	(hiindex ?x1)
	(succ ?x1 ?x2)
	(succ ?x2 ?x3)
	(succ ?x3 ?x4)
	(hiindex ?y4)
	(succ ?y3 ?y4)
	(hiindex ?y3)
	(succ ?y2 ?y3)
	(hiindex ?y2)
	(succ ?y1 ?y2)
	(hiindex ?y1)
	(true (cell ?x2 ?y3 red))
	(true (cell ?x3 ?y2 red))
	(true (cell ?x4 ?y1 red)))

(<= (align 2 blue)
	(true (cell ?x2 ?y2 blue))
	(lowindex ?x2)
	(lowindex ?y2)
	(succ ?x1 ?x2)
	(succ ?y1 ?y2)
	(true (cell ?x1 ?y1 blue)))

(<= (align 2 blue)
	(true (cell ?x1 ?y2 blue))
	(lowindex ?y2)
	(succ ?y1 ?y2)
	(lowindex ?x1)
	(succ ?x1 ?x2)
	(lowindex ?x2)
	(true (cell ?x2 ?y1 blue)))

(<= (align 3 blue)
	(true (cell ?x3 ?y3 blue))
	(lowindex ?x3)
	(lowindex ?y3)
	(succ ?x2 ?x3)
	(succ ?y2 ?y3)
	(true (cell ?x2 ?y2 blue))
	(succ ?x1 ?x2)
	(succ ?y1 ?y2)
	(true (cell ?x1 ?y1 blue)))

(<= (align 3 blue)
	(true (cell ?x1 ?y3 blue))
	(lowindex ?y3)
	(succ ?y2 ?y3)
	(succ ?y1 ?y2)
	(lowindex ?x1)
	(succ ?x1 ?x2)
	(lowindex ?x2)
	(succ ?x2 ?x3)
	(lowindex ?x3)
	(true (cell ?x2 ?y2 blue))
	(true (cell ?x3 ?y1 blue)))

(<= (align 4 blue)
	(true (cell ?x4 ?y4 blue))
	(lowindex ?x4)
	(lowindex ?y4)
	(succ ?x3 ?x4)
	(succ ?y3 ?y4)
	(true (cell ?x3 ?y3 blue))
	(succ ?x2 ?x3)
	(succ ?y2 ?y3)
	(true (cell ?x2 ?y2 blue))
	(succ ?x1 ?x2)
	(succ ?y1 ?y2)
	(true (cell ?x1 ?y1 blue)))

(<= (align 4 blue)
	(true (cell ?x1 ?y4 blue))
	(lowindex ?y4)
	(succ ?y3 ?y4)
	(succ ?y2 ?y3)
	(succ ?y1 ?y2)
	(lowindex ?x1)
	(succ ?x1 ?x2)
	(lowindex ?x2)
	(succ ?x2 ?x3)
	(lowindex ?x3)
	(succ ?x3 ?x4)
	(lowindex ?x4)
	(true (cell ?x2 ?y3 blue))
	(true (cell ?x3 ?y2 blue))
	(true (cell ?x4 ?y1 blue)))

;; specifies adjacency without considering low/hi indices
(<= (adjacent ?x1 ?y ?x2 ?y)
	(index ?y)
	(succ ?x1 ?x2))

(<= (adjacent ?x1 ?y ?x2 ?y)
	(index ?y)
	(succ ?x2 ?x1))

(<= (adjacent ?x ?y1 ?x ?y2)
	(index ?x)
	(succ ?y1 ?y2))

(<= (adjacent ?x ?y1 ?x ?y2)
	(index ?x)
	(succ ?y2 ?y1))

;; specifies diagonality without considering low/hi indices
(<= (diagonal ?x1 ?y1 ?x2 ?y2)
	(succ ?x1 ?x2)
	(succ ?y1 ?y2))

(<= (diagonal ?x1 ?y1 ?x2 ?y2)
	(succ ?x2 ?x1)
	(succ ?y1 ?y2))

(<= (diagonal ?x1 ?y1 ?x2 ?y2)
	(succ ?x1 ?x2)
	(succ ?y2 ?y1))

(<= (diagonal ?x1 ?y1 ?x2 ?y2)
	(succ ?x2 ?x1)
	(succ ?y2 ?y1))

(<= (index ?n) (lowindex ?n))

(<= (index ?n) (hiindex ?n))


;;; data

(number 0)
(number 1)
(number 2)
(number 3)

(alignnum 0)
(alignnum 1)
(alignnum 2)
(alignnum 3)
(alignnum 4)

(captureadd 0 1)
(captureadd 1 2)
(captureadd 2 3)

(color red)
(color blue)
(color blank)

(lowindex 1)
(lowindex 2)
(lowindex 3)
(lowindex 4)
(lowindex 5)
(lowindex 6)
(hiindex 6)
(hiindex 7)
(hiindex 8)
(hiindex 9)
(hiindex 10)
(hiindex 11)

(succ 1 2)
(succ 2 3)
(succ 3 4)
(succ 4 5)
(succ 5 6)
(succ 6 7)
(succ 7 8)
(succ 8 9)
(succ 9 10)
(succ 10 11)

(advantagesucc 0 1)
(advantagesucc 1 2)
(advantagesucc 2 3)
(advantagesucc 3 4)

(reflectto 1 11)
(reflectto 11 1)
(reflectto 2 10)
(reflectto 10 2)
(reflectto 3 9)
(reflectto 9 3)
(reflectto 4 8)
(reflectto 8 4)
(reflectto 5 7)
(reflectto 7 5)
(reflectto 6 6)

(stepcount 1 2)
(stepcount 2 3)
(stepcount 3 4)
(stepcount 4 5)
(stepcount 5 6)
(stepcount 6 7)
(stepcount 7 8)
(stepcount 8 9)
(stepcount 9 10)
(stepcount 10 11)
(stepcount 11 12)
(stepcount 12 13)
(stepcount 13 14)
(stepcount 14 15)
(stepcount 15 16)
(stepcount 16 17)
(stepcount 17 18)
(stepcount 18 19)
(stepcount 19 20)
(stepcount 20 21)
(stepcount 21 22)
(stepcount 22 23)
(stepcount 23 24)
(stepcount 24 25)
(stepcount 25 26)
(stepcount 26 27)
(stepcount 27 28)
(stepcount 28 29)
(stepcount 29 30)
(stepcount 30 31)
(stepcount 31 32)
(stepcount 32 33)
(stepcount 33 34)
(stepcount 34 35)
(stepcount 35 36)
(stepcount 36 37)
(stepcount 37 38)
(stepcount 38 39)
(stepcount 39 40)