;;;; -*-  Mode: LISP; Syntax: Common-Lisp; Base: 10                    -*-
;;;; ---------------------------------------------------------------------
;;;; File name: clause.lsp
;;;;    System: FIRE
;;;;    Author: Jesse Alama
;;;;   Created: November 25, 2001
;;;;   Purpose: Define operators for operating on sets of terms
;;;; ---------------------------------------------------------------------
;;;;  Modified: Wednesday, February 5, 2003 at 09:50:34 by forbus

(in-package :fire)

#|
A clause is a set of terms (see term.lsp)
|#

(defun remove-term (clause term)
  (remove term clause))

(defun negate-terms (clause)
  (mapcar #'negate-term clause))

(defun make-clause-from-term (term)
  (list term))

(defun terms-w/-operator+polarity (clause operator polarity)
  (select #'(lambda (term)
	      (term-has-operator-and-polarity? term operator polarity))
	  clause))

(defun clause-literals (clause)
  (mapcar #'car clause))

(defun uniquify-variables-for-clauses (clauses)
  (mapcar #'uniquify-variables-for-clause clauses))

(defun uniquify-variables-for-clause (clause)
  (let ((vars (remove-duplicates (tree-select #'variable? clause)))
	(new-subst '()))
    (dolist (var vars)
      (push (cons var (intern (gensym "?") :data)) new-subst))
    (apply-substitution new-subst clause)))

(defun equal-clauses? (c1 c2)
  (sets-equal? c1 c2 :test #'equal-terms?))