;; DDKB (Domain Dependent Knowledge Base)
;; for puzzles with INC-3 (increment by mod 3) function
;; and only EQual and NotEqual predicates

(in-package "USER")

;; true iff EXP-1 is equal to EXP-2 in the P-LIST
(defun test-EQ (exp-1 exp-2 p-list)
  (cond ((equal exp-1 exp-2))
	((eq (car exp-1) (car exp-2))  ; every function is safe over equal
	 (test-EQ (cdr exp-1) (cdr exp-2) p-list))
	((or (cdr exp-1) (cdr exp-2)) nil)
	; exp-1 and exp-2 have only one element
	((go-thru-eqs 'EQ (car exp-1) (car exp-2) p-list))))

;; true iff EXP-1 is NOT equal to EXP-2 in the P-LIST
(defun test-NE (exp-1 exp-2 p-list)
  (cond ((and (eq (car exp-1) 'inc-3) (eq (car exp-2) 'inc-3))
	 ; both exp start with INC-3
	 (test-NE (cdr exp-1) (cdr exp-2) p-list))
	((eq (car exp-1) 'inc-3) (test-EQ (cdr exp-1) exp-2 p-list))
	((eq (car exp-2) 'inc-3) (test-EQ exp-1 (cdr exp-2) p-list))
	; Now, exp-1 and exp-2 have one member each.
	((go-thru-eqs 'NE (car exp-1) (car exp-2) p-list))))

;; Simplification for INC-3 function
(defun simplify (exp p-list)
  (cond ((and (eq (car exp) 'inc-3)
	      (eq (cadr exp) 'inc-3)
	      (eq (caddr exp) 'inc-3))
	 (simplify (cdddr exp) p-list))
	(t exp)))