(use srfi-1) ; delete, remove, any, delete-duplicates

;; resolution

(define (find-resolvents forms1 forms2)
  (append-crossmap
    (lambda (form1 form2)
      (let ((binds (unify/binds '() form1 (negated form2))))
	(if binds (list (list binds form1 form2)) '())))
    forms1 forms2))

(define (construct-resolution binds resolvent1 resolvent2 forms1 forms2)
  (clean-covered
    (fill-template
      (list->disjunction
	(append (delete resolvent1 forms1) (delete resolvent2 forms2)))   
      (fill-binds binds))))

(define (resolve form1 form2)
  (let* ((forms1 (disjuncts form1))
	 (forms2 (disjuncts (rewrite-variables form2)))
	 (resolvents (find-resolvents forms1 forms2)))
    (map (lambda (resolvent)
	   (construct-resolution (car resolvent)
				 (cadr resolvent) (caddr resolvent)
				 forms1 forms2))
	 resolvents)))

;; resolution in theories

(define (new-theory) '())

(define (theory-directly-covers? theory clause)
  (any (lambda (c)
	 (and (clause-covers? c clause)
	      (<= (length (disjuncts c)) (length (disjuncts clause)))))
       theory))

(define (theory-expand theory1 theory2)
  (let ((cleaned (remove (lambda (c) (theory-directly-covers? theory2 c))
			 theory1)))
    (if (null? cleaned) theory2
      (let* ((cleaned2 (remove (lambda (c) (theory-directly-covers? cleaned c))
			       theory2))
	     (base (append cleaned cleaned2))
	     (new (delete-duplicates (append-crossmap resolve cleaned base))))
	(theory-expand new base)))))

(define (theory-resolve theory) (theory-expand theory '()))

(define (theory-inconsistent? theory)
  (theory-directly-covers? (theory-resolve theory) '(or)))

(define (theory-incompatible? theory clause)
  (let ((resolved (theory-expand (conjuncts clause) theory)))
    (theory-directly-covers? resolved '(or))))

(define (theory-covers? theory clause)
  (theory-incompatible? theory (proposition-negated clause)))

;; minimal theory operations

(define (theory-cleanup theory)
  (cleanup-by-partial-order clause-covers? theory))