;;
;; Test push/pop based on the N-queens problems
;; using QF_IDL constraints
;;

(define x0::int)
(define x1::int)
(define x2::int)
(define x3::int)
(define x4::int)
(define x5::int)
(define x6::int)


;; x0 is intended to be zero: bounds on (x1 - x0)  ... (x6 - x0)
(assert (and (<= 0 (- x1 x0)) (<= (- x1 x0) 5)
	     (<= 0 (- x2 x0)) (<= (- x2 x0) 5)
	     (<= 0 (- x3 x0)) (<= (- x3 x0) 5)
             (<= 0 (- x4 x0)) (<= (- x4 x0) 5)
	     (<= 0 (- x5 x0)) (<= (- x5 x0) 5)
	     (<= 0 (- x6 x0)) (<= (- x6 x0) 5)))

;; First check should be SAT (easy)
(echo "FIRST CHECK: sat expected\n")
(check)
(show-model)

;; Constraints for the simple variant of N-queens
(push)

(assert (distinct (- x1 x0) (- x2 x0) (- x3 x0) (- x4 x0) (- x5 x0) (- x6 x0)))

(echo "\n\nSECOND CHECK: sat expected\n")
(check)
(show-model)

(assert (and (/= (- x1 x2) 1) (/= (- x1 x2) -1)))
(assert (and (/= (- x1 x3) 2) (/= (- x1 x3) -2)))
(assert (and (/= (- x1 x4) 3) (/= (- x1 x4) -3)))
(assert (and (/= (- x1 x5) 4) (/= (- x1 x5) -4)))
(assert (and (/= (- x1 x6) 5) (/= (- x1 x6) -5)))
(assert (and (/= (- x2 x3) 1) (/= (- x2 x3) -1)))
(assert (and (/= (- x2 x4) 2) (/= (- x2 x4) -2)))
(assert (and (/= (- x2 x5) 3) (/= (- x2 x5) -3)))
(assert (and (/= (- x2 x6) 4) (/= (- x2 x6) -4)))
(assert (and (/= (- x3 x4) 1) (/= (- x3 x4) -1)))
(assert (and (/= (- x3 x5) 2) (/= (- x3 x5) -2)))
(assert (and (/= (- x3 x6) 3) (/= (- x3 x6) -3)))
(assert (and (/= (- x4 x5) 1) (/= (- x4 x5) -1)))
(assert (and (/= (- x4 x6) 2) (/= (- x4 x6) -2)))
(assert (and (/= (- x5 x6) 1) (/= (- x5 x6) -1)))


;; Check should be SAT
(echo "\n\nTHIRD CHECK: sat expected\n")
(check)
(show-model)


;; Constraints for super queen (N-queens + knights moves)

(push)

(assert (and (/= (- x1 x2) 2) (/= (- x1 x2) -2)))
(assert (and (/= (- x1 x3) 1) (/= (- x1 x3) -1)))
(assert (and (/= (- x2 x3) 2) (/= (- x2 x3) -2)))
(assert (and (/= (- x2 x4) 1) (/= (- x2 x4) -1)))
(assert (and (/= (- x3 x4) 2) (/= (- x3 x4) -2)))
(assert (and (/= (- x3 x5) 1) (/= (- x3 x5) -1)))
(assert (and (/= (- x4 x5) 2) (/= (- x4 x5) -2)))
(assert (and (/= (- x4 x6) 1) (/= (- x4 x6) -1)))
(assert (and (/= (- x5 x6) 2) (/= (- x5 x6) -2)))

(echo "\n\nFOURTH CHECK: unsat expected\n")
(check) ;; should be unsat

;; Backtrack 
(pop)

(echo "\n\nFIFTH CHECK: sat expected\n")
(check)
(show-model)

;; Constraints for the toroidal N-queens
(push)

(assert (and (/= (- x1 x2) 5) (/= (- x1 x2) -5)))
(assert (and (/= (- x1 x3) 4) (/= (- x1 x3) -4)))
(assert (and (/= (- x1 x5) 2) (/= (- x1 x5) -2)))
(assert (and (/= (- x1 x6) 1) (/= (- x1 x6) -1)))
(assert (and (/= (- x2 x3) 5) (/= (- x2 x3) -5)))
(assert (and (/= (- x2 x4) 4) (/= (- x2 x4) -4)))
(assert (and (/= (- x2 x6) 2) (/= (- x2 x6) -2)))
(assert (and (/= (- x3 x4) 5) (/= (- x3 x4) -5)))
(assert (and (/= (- x3 x5) 4) (/= (- x3 x5) -4)))
(assert (and (/= (- x4 x5) 5) (/= (- x4 x5) -5)))
(assert (and (/= (- x4 x6) 4) (/= (- x4 x6) -4)))
(assert (and (/= (- x5 x6) 5) (/= (- x5 x6) -5)))


(echo "SIXTH CHECK: unsat expected\n")
(check) ;; should be unsat


;; Backtrack
(pop)

;; Recheck the N-queens. Should still be sat
(echo "\nSEVENTH CHECK: sat expected\n")
(check)
(show-model)

;; Remove all
(pop)

;; Empty check: sat
(echo "\nLAST CHECK: sat expected\n")
(check)
(show-model)