;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Written by Norvig and Russell
;;; Converted to Scheme (and modified slightly) by Tomas Lozano-Perez (MIT)
;;;; Convert Expressions to Normal Form (Conjunctive, Implicative or Horn)
;;; This could be done much more efficiently.  Most often, a special
;;; representation is used for CNF, which eliminates the explicit ANDs
;;; and ORs.  This code is meant to be informative, not efficient.

;;;; Top-Level Functions

;;; Convert a sentence p to conjunctive normal form [p 279-280]."
;; That is, return (and (or ...) ...) where 
;; each of the conjuncts has all literal disjuncts.

(define (->cnf input)
  (define (cnf-loop p vars)
    (set! p (eliminate-implications p))
    ;; VARS is a list of universally quantified variables that P is in scope of.
    (case (op p)
      ((NOT) (let ((p2 (move-not-inwards (arg1 p))))
	       (if (literal-clause? p2) p2 (cnf-loop p2 vars))))
      ((AND) (conjunction (mappend (lambda (q) (conjuncts (cnf-loop q vars)))
				   (args p))))
      ((OR)  (merge-disjuncts (map (lambda (q) (cnf-loop q vars))
				   (args p))))
      ((ALL) (let ((new-vars (map new-variable  (mklist (arg1 p)))))
	       (cnf-loop (sublis (map cons  (mklist (arg1 p)) new-vars)
				 (arg2 p))
			 (append new-vars vars))))
      ((EXI) (cnf-loop (skolemize (arg2 p) (arg1 p) vars) vars))
      (else   p)			; p is atomic
      ))
  (define (eliminate-dups-in-disjuncts p)
    (if (literal-clause? p) 
	p
	(case (op p)
	  ((and) (cons (op p)
		       (rem-duplicates
			(map eliminate-dups-in-disjuncts (args p)) equal?)))
	  ((or) (cons (op p) 
		      (rem-duplicates (args p) equal?)))
	  (else p)))
    )
  (eliminate-dups-in-disjuncts (cnf-loop input '()))
  )

;;;; Auxiliary Functions

(define (eliminate-implications p)
  (if (literal-clause? p)
      p
      (case (op p)
	((=>)  `(or ,(arg2 p) (not ,(arg1 p))))

	;; I think this leads to more complicated expressions - TLP
	;;((<=>) `(or (and ,(arg1 p) ,(arg2 p))
	;; (and (not ,(arg1 p)) (not ,(arg2 p)))))

        ((<=>) `(and (or (not ,(arg1 p)) ,(arg2 p))
		     (or (not ,(arg2 p)) ,(arg1 p))))
	(else   (cons (op p) (map eliminate-implications (args p)))))))

;;; Given P, return ~P, but with the negation moved as far in as possible.

(define (move-not-inwards p)
  (case (op p)
    ((TRUE) 'false)
    ((FALSE) 'true)
    ((NOT) (arg1 p))
    ((AND) (disjunction (map move-not-inwards (args p))))
    ((OR)  (conjunction (map move-not-inwards (args p))))
    ((ALL) (make-exp 'EXI (arg1 p) (move-not-inwards (arg2 p))))
    ((EXI) (make-exp 'ALL (arg1 p) (move-not-inwards (arg2 p))))
    (else (make-exp 'not p))))

;;; Return a CNF expression for the disjunction.

(define (merge-disjuncts disj)
  ;; The argument is a list of disjuncts, each in CNF.
  ;; The second argument is a list of conjuncts built so far.
  (case (length disj)
    ((0) 'false)
    ((1) (first disj))
    (else
     (conjunction
      (apply-append
       (map (lambda (y)
	      (map (lambda (x)
		     (disjunction (append (disjuncts x) 
					  (disjuncts y))))
		   (conjuncts (first disj))))
	    (conjuncts (merge-disjuncts (rest disj)))))))))

;;; Within the proposition P, replace each of VARS with a skolem constant,
;;; or if OUTSIDE-VARS is non-null, a skolem function of them.
(define (skolemize p vars outside-vars)
  (sublis (map (lambda (var)
		 (cons var (if (null? outside-vars)
			       (skolem-constant var)
			       (cons (skolem-constant var) outside-vars))))
	       (mklist vars))
	  p))

;;; Return a unique skolem constant, a symbol starting with '$'

(define (skolem-constant name)
  (set! *new-variable-counter* (+ 1 *new-variable-counter*))
  (string->symbol (string-append "$"
				 (symbol->string name)
				 "_"
				 (number->string *new-variable-counter*))))

;;; Are p and q renamings of each other? (That is, expressions that differ
;;; only in variable names?)

(define (renaming? p q)
  (define (renaming-loop p q bindings)
    (cond ((eq? bindings *fail*) *fail*)
	  ((equal? p q) bindings)
	  ((and (pair? p) (pair? q))
	   (renaming-loop (rest p) (rest q)
			  (renaming-loop (first p) (first q) bindings)))
	  ((not (and (variable? p) (variable? q)))
	   *fail*)
	  ;; P and Q are both variables from here on
	  ((and (not (get-binding p bindings)) (not (get-binding q bindings)))
	   (extend-bindings p q bindings))
	  ((or (eq? (lookup p bindings) q) (eq? p (lookup q bindings)))
	   bindings)
	  (else *fail*)))
  (renaming-loop p q *no-bindings*))

;;;; Utility Predicates and Accessors

(define *logical-connectives* '(and or not => <=>))
(define *logical-quantifiers* '(all exi))

(define (atomic-clause? sentence)
  (not (or (member (op sentence) *logical-connectives*)
	   (member (op sentence) *logical-quantifiers*))))

(define (literal-clause? sentence)
  (or (atomic-clause? sentence)
      (and (eq? (op sentence) 'not) (atomic-clause? (arg1 sentence)))))

(define (negative-clause? sentence)
  (eq? (op sentence) 'not))

(define (conjunction? sentence)
  (eq? (op sentence) 'and))

(define (horn-clause? sentence)
  (and (eq? (op sentence) '=>)
       (every atomic-clause? (conjuncts (arg1 sentence)))
       (atomic-clause? (arg2 sentence))))

;;; Return a list of the conjuncts in this sentence.
(define (conjuncts sentence)
  (cond ((eq? (op sentence) 'and) (args sentence))
	((eq? sentence 'true) '())
	(else (list sentence))))

;;; Return a list of the disjuncts in this sentence.
(define (disjuncts sentence)
  (cond ((eq? (op sentence) 'or) (args sentence))
	((eq? sentence 'false) '())
	(else (list sentence))))

;;; Form a conjunction with these args."
(define (conjunction args)
  (case (length args)
    ((0) 'true)
    ((1) (first args))
    (else (cons 'and args))))

;;; Form a disjunction with these args."
(define (disjunction args)
  (case (length args)
    ((0) 'false)
    ((1) (first args))
    (else (cons 'or args))))

;;; An expression is a list consisting of a prefix operator followed by args,
;;; Or it can be a symbol, denoting an operator with no arguments.
;;; Expressions are used in Logic, and as actions for agents.

(define (make-exp op . args) (cons op args))
(define (op exp) (if (list? exp) (first exp) exp))
(define (args exp) (if (list? exp) (rest exp) '()))
(define (arg1 exp) (first (args exp)))
(define (arg2 exp) (second (args exp)))

(define (set-args! exp new-value)
  (set-cdr! exp new-value))

;;; Return (cons x y), or reuse x-y if it is equal? to (cons x y)
(define (reuse-cons x y x-y)
  (if (and (eqv? x (car x-y)) (eqv? y (cdr x-y)))
      x-y
      (cons x y)))

;;; If x is a list, return it; otherwise return a singleton list, (x).
(define (mklist x)
  (if (list? x) x (list x)))

;;; Apply fn to respective elements of list(s), and append results."

(define (mappend fn . lists)
  (apply-append (apply map fn lists)))

(define (apply-append l)
  (define (loop l ans)
    (if (null? l) ans
	(loop (cdr l) (append (car l) ans))))
  (loop l '()))


(define (every fn l)
  (cond ((null? l) #t)
	((fn (car l)) (every fn (cdr l)))
	(else #f)))

(define (sublis alist tree)
  (if (pair? tree)
      (let ((left (sublis alist (car tree)))
            (right (sublis alist (cdr tree))))
        (if (and (eq? left (car tree))
                 (eq? right (cdr tree)))
            tree
            (cons left right)))
      (let ((new (assv tree alist)))
        (if new
            (cdr new)
            tree) ) ) )

(define (rem-duplicates l test)
  (define (mem? x lst)
    (if (null? lst) #f
	(if (test x (car lst)) #t
	    (mem? x (cdr lst)))))
  (cond ((pair? l)
	 (if (mem? (car l) (cdr l))
	     (rem-duplicates (cdr l) test)
	     (cons (car l) (rem-duplicates (cdr l) test))))
	(else l)))