;;;
;;; Based on the CommonLisp prover written by Shaul Markovitch from Technion
;;; Translated to Scheme by Tomas Lozano-Perez, MIT
;;;

;;; Main algorithms and data structures.
;;;
;;; The main algorithm implements classic resolutions.  It starts with
;;; a clause set that contains the clauses of the axioms and the
;;; negated theorem.  It then repeatedly
;;; selects two clauses, resolves them, and add the resolvent to the
;;; clause set.  The algorithm stops when it finds an empty clause (in
;;; which case it returns T).  If there are no more candidates for unification,
;;; the algorithm returns NIL.  If the alloted resources are
;;; exhausted, the algorithm stops with no definitive answer.
;;;
;;; proof-node
;;;   A proof-node is a structure that holds one resolvent created
;;;   during the proof.  The structure consists of the clause itself,
;;;   the binding list resulted from the unification of its parent
;;;   clauses, pointers to the proof-nodes of its parent clauses, and
;;;   various flags and counters.  The proof-node that contains the
;;;   empty clause at the end of the proof process is in fact the root
;;;   of the PROOF-TREE that can be traced by following the parent
;;;   links.  The algorithm starts with a list of proof-nodes, one for
;;;   each clause of the basic clause set (of the axioms and the
;;;   negated theorem).
;;;
;;; candidate-list
;;;   The purpose of the candidate list is to save time in finding
;;;   candidates for resolution.  A candidate is a pair ((n1 i1)(n2 i2)).
;;;   The meaning of a candidate: the i1 literal of the clause of node
;;;   n1 and the i2 literal of the clause of proof-node n2 contain
;;;   complementary predicates.  It does not mean that the literals
;;;   are unifiable, but only that they are potentially unifiable.
;;;   Note that the index is 0 based.  Whenever a new resolvent is
;;;   added, the system needs to test only for new candidates
;;;   resulting from the new resolvent.
;;;
;;; predicate-hash
;;;   The purpose of the clause hash is to make the process of
;;;   finding new candidates more efficient.  This is a hash
;;;   table with an entry for each predicate name.  Each entry
;;;   contains two lists.  The first is a list of pointers to places
;;;   where the predicate apears in positive literals, the second is a
;;;   list of pointers to places where the predicate appears in a
;;;   negative literal.  A pointer is a pair.  The first element
;;;   points to a proof-node whose clause contains the literal, and
;;;   the second is an index of this literal within the clause.  When
;;;   a new clause is created, each of its literals is combined with
;;;   the appropriate list in the index to create a new list of
;;;   candidates.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;  Resolution Strategies
;;;
;;;    There are 4 built in mechanisms to control the resolutions 
;;;    process.  
;;;
;;;    candidate-filters
;;;       A veriable contains a list of function names or lambda 
;;;       expressions.  When a new candidate is generated the program
;;;       passes the candidate through all the filters, from left
;;;       to right.  For example, the set of support filter checks
;;;       that one of the candidates is from the set-of-support.
;;;       Each of the functions gets one argument - a candidate
;;;
;;;    clause-filters
;;;       Filters a newly generated clauses.
;;;       Each of the functions gets two arguments: the new clause
;;;       and the list of all proof-nodes.  For example, the uniqueness
;;;       filter tests whether the new clause already exists.
;;;
;;;    initial-clause-filters
;;;       Same as the above, but applied only during the initialization
;;;       to the axioms and negated-theorem clauses.
;;;
;;;    candidate-ordering-strategies
;;;       A list of functions used for sorting the candidates.  Each of 
;;;       the functions gets two arguments (two candidates) and returns
;;;       one of the three atoms: < > =.  The order of the strategies
;;;       determines a lexicographic order on the candidates.  The 
;;;       strategies are applied from left to right as long 
;;;       as = is returned.
;;;
;;;    All the control mechanisms are stored in a structure of type
;;;    resolution (described below).
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;; Access/Setting proof-node

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; proof-node is the main data structure.  Each of the clauses is stored
;;; in such a structure.  The parent links allow retrieval of the proof 
;;; tree.  New strategies and filters may need to add fields to this 
;;; record.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define pn-clause 1)
(define pn-parent 2)
(define pn-binding 3)
(define pn-set-of-support 4)
(define pn-depth 5)

(define (proof-node-clause pn) (vector-ref pn pn-clause))
(define (proof-node-parent pn) (vector-ref pn pn-parent))
(define (proof-node-binding pn) (vector-ref pn pn-binding))
(define (proof-node-set-of-support pn) (vector-ref pn pn-set-of-support))
(define (proof-node-depth pn) (vector-ref pn pn-depth))

(define (set-proof-node-clause! pn val) (vector-set! pn pn-clause val) pn)
(define (set-proof-node-parent! pn val) (vector-set! pn pn-parent val) pn)
(define (set-proof-node-binding! pn val) (vector-set! pn pn-binding val) pn)
(define (set-proof-node-set-of-support! pn val) (vector-set! pn pn-set-of-support val) pn)
(define (set-proof-node-depth! pn val) (vector-set! pn pn-depth val) pn)

(define (make-proof-node clause)	; the clause is required, other stuff can be added later
  (let ((pn (make-vector 6)))
    (vector-set! pn 0 'proof-node)
    (set-proof-node-clause! pn clause)
    (set-proof-node-depth! pn 0)
    (set-proof-node-parent! pn #f)
    (set-proof-node-binding! pn *no-bindings*)
    (set-proof-node-set-of-support! pn #f)
    pn))

(define (make-proof-node-all clause parent binding s-o-s depth)	
  (let ((pn (make-proof-node clause)))
    (set-proof-node-parent! pn parent)
    (set-proof-node-binding! pn binding)
    (set-proof-node-set-of-support! pn s-o-s)
    (set-proof-node-depth! pn depth)
    pn))

;;; Access/Setting proof-result

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; proof-result
;;;    A structure used for returning the proof results.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define pr-answer 1)
(define pr-n-res 2)
(define pr-proof 3)

(define (proof-result-answer pr) (vector-ref pr pr-answer))
(define (proof-result-n-resolutions pr) (vector-ref pr pr-n-res))
(define (proof-result-proof pr) (vector-ref pr pr-proof))

(define (set-proof-result-answer! pr val) (vector-set! pr pr-answer val) pr)
(define (set-proof-result-n-resolutions! pr val) (vector-set! pr pr-n-res val) pr)
(define (set-proof-result-proof! pr val) (vector-set! pr pr-proof val) pr)

(define (make-proof-result-all answer n-res proof)
  (let ((pr (make-vector 4)))
    (vector-set! pr 0 'proof-result)
    (set-proof-result-answer! pr answer)
    (set-proof-result-n-resolutions! pr n-res)
    (set-proof-result-proof! pr proof)
    pr))

;;; Candidates and literals

;;;   A candidate is a pair ((n1 i1)(n2 i2)).  The meaning of a
;;;   candidate: the i1 literal of the clause of node n1 and the i2
;;;   literal of the clause of proof-node n2 contain complementary
;;;   predicates (not necessarily unifiable).

(define candidate-pn1 caar)
(define candidate-pn2 caadr)
(define candidate-i1 cadar)
(define candidate-i2 cadadr)
(define make-candidate list)		; takes two literal refs
(define make-literal-ref list)		; takes pn and index

;;; Some parameters

;;; The maximum number of resolutions allowed for proving one theorem
(define *resource-limit* 10000)

;;; When non-#f, the prover displays each unification attempt
(define *trace-prover* #t)

;;; When non-#f, shows a dot for every *show-progress* resolutions
(define *show-progress* 20)

;;; A variable used to hold the axioms after reading them
(define *axioms* '())

;;; Hash table for preds

(define (make-predicate-hash-entry) (list '() '()))
(define (predicate-hash-entry-pos entry) (car entry))
(define (predicate-hash-entry-neg entry) (cadr entry))
(define (set-predicate-hash-entry-pos! entry val) 
  (set-car! entry val))
(define (set-predicate-hash-entry-neg! entry val) 
  (set-car! (cdr entry) val))
(define (add-predicate-hash-entry-pos! entry val) 
  (set-car! entry (cons val (car entry))))
(define (add-predicate-hash-entry-neg! entry val) 
  (set-car! (cdr entry) (cons val (cadr entry))))

;;; Reads a file and returns the set of axioms listed in the file in CNF.
;;; The axioms are also stored in the global var *axioms*.
(define (read-axioms file)
  (define (loop)
    (let ((new (read)))
      (if (eof-object? new)
	  '()
	  (cons new (loop)))))
  (let ((axioms (reverse (with-input-from-file file loop))))
    (set! *axioms* (convert-to-cnf (conjunction axioms)))
    *axioms*))

(define (add-axioms axioms)
  (set! *axioms* (append (convert-to-cnf (conjunction axioms)) *axioms*)))

;;; The main user function.  Gets the theorem and axioms and calls the 
;;; theorem prover.  The axioms are assumed to be in cnf.  
;;; The theorem is a prefix lisp expression, for example
;;; (EXI (?X ?Y) (AND (MOTHER ?X ?Y)(NOT (MOTHER ?Y ?X))))
;;; The function returns #t if a proof was found, #f if there is no  proof, 
;;; and the symbol GAVE-UP if the alloted resources are exhausted.

(define (prove theorem . ans-vars)
  (let ((pr (theorem-prover theorem *axioms* ans-vars)))
    (proof-result-answer pr)))

(define (theorem-prover theorem axiom-clauses ans-vars)
  (let* ((theorem-clauses (convert-to-cnf 
			   ;; add the answer predicate
			   `(or (ans ,@ans-vars) (not ,theorem))))
	 (theorem-nodes (map (lambda (c)
			       (set-proof-node-set-of-support!
				(make-proof-node c) #t))
			     theorem-clauses))
	 (axiom-nodes (map make-proof-node axiom-clauses))
	 (proof-nodes (append theorem-nodes axiom-nodes))
	 (predicate-hash (make-predicate-hash))
	 (candidates '()))
    ;; The following code initializes the candidate list.  It takes each
    ;; clause in the axioms+theorem clauses and merges its resolution
    ;; candidate with the the candidate list using the candidate ordering
    ;; strategies to determine the sort order.
    (set! proof-nodes (filter (lambda (pn) (apply-initial-clause-filters
					    (proof-node-clause pn) proof-nodes))
			      proof-nodes))
    (for-each 
     (lambda (pn)
       (set! candidates (add-to-candidates pn candidates predicate-hash)))
     proof-nodes)
    ;; The main loop.  Keeps popping candidates from the candidate list,
    ;; unifying them and adding the new clauses.
    (theorem-prover-loop 1 proof-nodes candidates predicate-hash)))

(define (theorem-prover-loop n-resolutions proof-nodes candidates predicate-hash)
  (cond ((> n-resolutions *resource-limit*)
	 (make-proof-result-all 'gave-up n-resolutions #f))
	((null? candidates)
	 (make-proof-result-all #f n-resolutions #f))
	(else
	 (let ((cand (first candidates)))
	   (set! candidates (cdr candidates))
	   (let ((binding (unify-cand cand)))
	     (cond (binding
		    (if *trace-prover*
			(begin 
			  (display-cand cand)
			  (display* "  Unification result: " binding)))
		    ;; Unification was successful. A new clause is
		    ;; generated, and its variables are renamed.
		    
		    (let* ((clause (subst-bindings binding (resolve-cand cand)))
			   (vars-in-clause (variables-in clause))
			   (renaming
			    (if (null? vars-in-clause)
				*no-bindings*
				(map (lambda (var) 
				       (make-binding var (new-variable var #t)))
				     (variables-in clause))))
			   (new-clause (subst-bindings renaming clause)))
		      (cond ((apply-clause-filters new-clause proof-nodes)
			     ;; The clause filters allow us to filter out
			     ;; newly generated clauses.
			     (let ((resolvant
				    (make-resolvant new-clause cand 
						    (merge-bindings renaming binding))))
			       (if *trace-prover*
				   (display* "  New Clause: " (proof-node-clause resolvant)))
			       (if (contradiction? (proof-node-clause resolvant))
				   (make-proof-result-all
				    (if (null? (proof-node-clause resolvant))
					#t 
					(first (proof-node-clause resolvant)))
				    n-resolutions resolvant)
				   (apply 
				    theorem-prover-loop
				    (list
				     (+ 1 n-resolutions)
				     (cons resolvant proof-nodes)
				     (add-to-candidates resolvant candidates predicate-hash)
				     predicate-hash)))))
			    (else
			     (if *trace-prover*
				 (display* "  Clause " new-clause " was filtered out."))
			     (theorem-prover-loop
			      (+ 1 n-resolutions) proof-nodes candidates predicate-hash)
			     ))))
		   (else
		    ;;(if *trace-prover*
		    ;;(display* "Unification attempt failed"))
		    (theorem-prover-loop
		     (+ 1 n-resolutions) proof-nodes candidates predicate-hash)))))
	 )))

(define (contradiction? clause)
  ;; null? will work without ans predicate
  (or (null? clause)
      (and (null? (rest clause))	; length=1
	   (eq? (get-predicate-name (first clause)) 'ans))))

(define (make-resolvant new-clause cand binding)
  (make-proof-node-all
   new-clause
   cand
   binding
   (or (proof-node-set-of-support (candidate-pn1 cand))
       (proof-node-set-of-support (candidate-pn2 cand)))
   (+ 1
      (max (proof-node-depth (candidate-pn1 cand))
	   (proof-node-depth (candidate-pn2 cand))))))

(define (add-to-candidates resolvant candidates predicate-hash)
  (let ((new
	 #|
	 (merge! (sort! (get-clause-candidates resolvant
					       predicate-hash)
			candidate-ordering)
		 candidates
		 candidate-ordering)
	 |#
	 (sort (append (get-clause-candidates resolvant
					      predicate-hash)
		       candidates)
	       candidate-ordering)
	 ))
    (update-predicate-hash resolvant predicate-hash)
    new))

(define (display-cand cand)
  (display* "Unifying: \n  Literal "
	    (candidate-i1 cand)
	    " of "
	    (proof-node-clause (candidate-pn1 cand))
	    "\n  Literal "
	    (candidate-i2 cand)
	    " of "
	    (proof-node-clause (candidate-pn2 cand))))
			
;;; This function is somewhat redundant.  Its main purpose is to
;;; correct several problems with the cnf returned by Norvig's program"

(define (convert-to-cnf p)
  (filtered-map 
   tautology-filter
   (lambda (x) (rename-variables x #t))
   (let ((cnf (->cnf p)))		; Call Norvig's program
     (cond ((literal-clause? cnf)
	    (list (list cnf)))
	   ((eq? (first cnf) 'or)
	    (list (rest cnf)))
	   (else 
	    (map (lambda (c)
		   (cond ((literal-clause? c) (list c))
			 ((eq? (first c) 'or) (rest c))
			 (else c)))
		 (if (eq? (first cnf) 'and)
		     (rest cnf)
		     cnf)))))))

;;; This function gets a new clause and the current predicate hash
;;; and updates the entries for the predicate symbols appearing in the
;;; clause.  The predicate hash is a hash table where the keys are
;;; the predicate names.  For each predicate, the entry contains two
;;; list.  The first has pointers to positive literals and the second
;;; to negative literals.  A pointer is a pair.  The first element
;;; points to the clause proof node and the second is the index of the
;;; literal in the clause.

(define (update-predicate-hash proof-node hash)
  (define (loop literals literal-index)
    (if (null? literals) 
	#f
	(let* ((literal (first literals))
	       (predicate-name (get-predicate-name literal))
	       (hash-entry (or (predicate-hash-lookup hash predicate-name)
			       (make-predicate-hash-entry))))
	  (if (negative-literal? literal)
	      (add-predicate-hash-entry-neg! 
	       hash-entry
	       (make-literal-ref proof-node literal-index))
	      (add-predicate-hash-entry-pos! 
	       hash-entry
	       (make-literal-ref proof-node literal-index)))
	  (predicate-hash-insert hash predicate-name hash-entry)
	  (loop (rest literals) (+ 1 literal-index) ))))
  (loop (proof-node-clause proof-node) 0))

;;; Returns the predicate symbol of a literal.

(define (get-predicate-name literal)
  (if (negative-literal? literal)
      (first (second literal))
      (first literal)))

(define (negative-literal? literal)
  (eq? (first literal) 'not))

;;; Returns all the resolution candidates that were added by adding
;;; the new clause to the clause database.  For each positive literal
;;; in the new clause, the new candidates are all the clauses
;;; where the literal predicate appears as a negative literal.
;;; This list is readily available in the predicate hash.
;;; The same is done for a new negative literal.  The new candidates
;;; are filtered by the literal filters of the current resolution
;;; strategy.

(define (get-clause-candidates proof-node predicate-hash)
  (define (loop literals index1)
    (if (null? literals)
	'()
	(let* ((literal1 (first literals))
	       (predicate-name (get-predicate-name literal1))
	       (hash-entry (or (predicate-hash-lookup predicate-hash predicate-name)
			       (make-predicate-hash-entry))))

	  (append 
	   ;; the elements of a hash entry are lists of literal-refs (proof-node index)
	   (inner-loop (if (negative-literal? literal1)
			   (predicate-hash-entry-pos hash-entry)
			   (predicate-hash-entry-neg hash-entry))
		       index1)
	   (loop (rest literals) (+ index1 1))))))  
  (define (inner-loop literal-refs index1)
    (if (null? literal-refs)
	'()
	(let ((cand (make-candidate
		     (make-literal-ref proof-node index1) 
		     (first literal-refs))))
	  (if (apply-candidate-filters cand)
	      (cons cand (inner-loop (rest literal-refs) index1))
	      (inner-loop (rest literal-refs) index1)))))
      
  (loop (proof-node-clause proof-node) 0))

;;; This is the actual resolution procedure.  The candidate contains
;;; pointers to the two clauses and literals that were successfully
;;; unified.  The function collects  the union of literals of the two
;;; clauses except the two that were unified.

(define (resolve-cand cand)
  (define (loop literals res-index index ans)
    (if (null? literals)
	ans
	(if (and (not (= index res-index))
		 (not (member (first literals) ans)))
	    (loop (rest literals) res-index (+ index 1) 
		  (cons (copy-tree (first literals)) ans))
	    (loop (rest literals) res-index (+ index 1) ans))))
  (reverse
   (loop (proof-node-clause (candidate-pn2 cand)) (candidate-i2 cand) 0 
	 (loop (proof-node-clause (candidate-pn1 cand)) (candidate-i1 cand) 0 '()))))

;;; A candidate is a pair.  Each element is a pair.  The first element
;;; is a pointer to the proof-node of a clause and the second is an
;;; index of aliteral in that clause.  This function extracts the two
;;; literals and tries to unify them

(define (unify-cand cand)
  (unify (without-not
	  (list-ref (proof-node-clause (candidate-pn1 cand))
		    (candidate-i1 cand)))
	 (without-not
	  (list-ref (proof-node-clause (candidate-pn2 cand))
		    (candidate-i2 cand)))))

(define (without-not exp) (if (eq? (first exp) 'not) (second exp) exp))

;; returns elements of vals
(define (filter test vals)
  (cond ((null? vals) '())
	((test (car vals))
	 (cons (car vals) (filter test (cdr vals))))
	(else
	 (filter test (cdr vals)))))

;; returns output of fn applied to vals
(define (filtered-map test fn vals)
  (cond ((null? vals) '())
	((test (car vals))
	 (cons (fn (car vals)) (filtered-map test fn (cdr vals))))
	(else
	 (filtered-map test fn (cdr vals)))))

(define (cl-member? entry l key test)
  (cond ((null? l) #f)
	((test entry (key (car l))) l)
	(else (cl-member? entry (cdr l) key test))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Resolution strategies
;;;   General explanations are at the header
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Resolution - a structure that determines the resolution strategy
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define st-name 1)
(define cand-order 2)
(define cand-filter 3)
(define clause-filter 4)
(define init-clause-filter 5)

(define (resolution-strategy-name res)
  (vector-ref res st-name))
(define (resolution-candidate-ordering-strategies res)
  (vector-ref res cand-order))
(define (resolution-candidate-filters res)
  (vector-ref res cand-filter))
(define (resolution-clause-filters res)
  (vector-ref res clause-filter))
(define (resolution-initial-clause-filters res)
  (vector-ref res init-clause-filter))

(define (set-resolution-strategy-name! res val)
  (vector-set! res st-name val))
(define (set-resolution-candidate-ordering-strategies! res val)
  (vector-set! res cand-order val))
(define (set-resolution-candidate-filters! res val)
  (vector-set! res cand-filter val))
(define (set-resolution-clause-filters! res val)
  (vector-set! res clause-filter val))
(define (set-resolution-initial-clause-filters! res val)
  (vector-set! res init-clause-filter val))

(define (make-resolution name)
  (let ((res (make-vector 6)))
    (vector-set! res 0 'resolution)
    (set-resolution-strategy-name! res name)
    ;;A list of functions used to impose a lexicographic order over
    ;;the set of candidate
    (set-resolution-candidate-ordering-strategies! 
     res (list trivial-ordering))
    ;;A list of filter functions to filter out resolution candidate
    (set-resolution-candidate-filters! 
     res (list trivial-candidate-filter))
    ;;A list of filter functions to filter out a new resolvent
    (set-resolution-clause-filters!
     res (list trivial-clause-filter))
    ;;A list of filter functions to filter out clauses in the initial
    ;;set.
    (set-resolution-initial-clause-filters!
     res (list trivial-clause-filter))
    res
    ))

(define (make-resolution-all 
	 name cand-order cand-filter clause-filter init-clause-filter)
  (let ((res (make-resolution name)))
    ;;A list of functions used to impose a lexicographic order over
    ;;the set of candidate
    (if cand-order
	(set-resolution-candidate-ordering-strategies! 
	 res cand-order))
    ;;A list of filter functions to filter out resolution candidate
    (if cand-filter 
	(set-resolution-candidate-filters! 
	 res cand-filter))
    ;;A list of filter functions to filter out a new resolvent
    (if clause-filter
	(set-resolution-clause-filters! 
	 res clause-filter))
    ;;A list of filter functions to filter out clauses in the initial
    ;;set.
    (if init-clause-filter
	(set-resolution-initial-clause-filters! 
	 res init-clause-filter))
    res
    ))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;  candidate-ordering
;;;   The candidate ordering routine orders the candidates in lexicographic
;;;   order according to the list *candidate-ordering-strategies*.
;;;   The first strategy in the list is the most significant.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define (candidate-ordering cand1 cand2) 
  (define (order c1 c2 strategies)
    (cond ((null? strategies) #t)
	  (else
	   (case ((first strategies) c1 c2)
	     ((<) #t)
	     ((>) #f)
	     ((=) (order c1 c2 (rest strategies)))))))
  (order cand1 cand2 (resolution-candidate-ordering-strategies
		      *current-resolution-strategy*)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;  Candidate ordering strategies
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
	 
;;; A candidate ordering strategy.  Prefers pairs whose minimal clause 
;;; length is shorter

(define (shortest-min-clause cand1 cand2)
  (let ((min1 (min (length (proof-node-clause (candidate-pn1 cand1)))
		   (length (proof-node-clause (candidate-pn2 cand1)))))
	(min2 (min (length (proof-node-clause (candidate-pn1 cand2)))
		   (length (proof-node-clause (candidate-pn2 cand2))))))
    (numeric-relation min1 min2)))

(define (numeric-relation n1 n2)
  (cond ((< n1 n2) '<)((> n1 n2) '>)(else '=)))

;;; A candidate ordering strategy.  Prefers pairs whose sum of clause 
;;; length is shorter

(define (shortest-sum cand1 cand2)
  (let ((sum1 (+ (length (proof-node-clause (candidate-pn1 cand1)))
		 (length (proof-node-clause (candidate-pn2 cand1)))))
	(sum2 (+ (length (proof-node-clause (candidate-pn1 cand2)))
		 (length (proof-node-clause (candidate-pn2 cand2))))))
    (numeric-relation sum1 sum2)))


;;; A trivial ordering function.  It should be used when, during the 
;;; experimentation we need to test the prover with no ordering functions.

(define (trivial-ordering cand1 cand2) #t)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;  Candidate filtering
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define (apply-candidate-filters cand)
  (define (loop filters)
    (cond ((null? filters) #t)
	  (((car filters) cand) (loop (rest filters)))
	  (else #f)))
  (loop (resolution-candidate-filters *current-resolution-strategy*))
  )
   
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;  Candidate filtering strategies
;;;    To add a strategy define the function according to the example 
;;;    below. 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
   
;;; Set of support strategy.  One of the candidate clauses should be a 
;;; descendant of the set of support (the theorem negation)

(define (setofsupport-filter cand)
  (or (proof-node-set-of-support (candidate-pn1 cand))
      (proof-node-set-of-support (candidate-pn2 cand))))

(define (trivial-candidate-filter cand) 
 #t)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;  Clause filtering
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define (apply-clause-filters clause proof-nodes)
  (define (loop filters)
    (cond ((null? filters) #t)
	  (((car filters) clause proof-nodes) (loop (rest filters)))
	  (else #f)))
  (loop (resolution-clause-filters *current-resolution-strategy*))
  )
   
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;  clause filtering strategies
;;;    To add a strategy define the function according to the example 
;;;    below.  
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
   
;;; This filter makes sure that we don't add duplicate clauses.   It looks as 
;;; if it is always worthwhile to keep this filter.  Note however that the 
;;; cost of the test is high and proportional to the number of clauses

(define (uniqueness-filter clause proof-nodes)
  (not (cl-member? clause proof-nodes 
		   proof-node-clause	; key
		   literal-set-equivalence ; test
		   )))

(define (literal-set-equivalence set1 set2)
  (define (subset? s1 s2 test)
    (define (loop set)
      (cond ((null? set) #t)
	    ((cl-member? (car set) set2 identity renaming?) 
	     (loop (cdr set)))
	    (else #f)))
    (loop s1))
  (and (= (length set1) (length set2))
       (subset? set1 set2 renaming?)))

(define (tautology-filter clause . opt)
  (define (loop literals)
    (cond ((null? literals) #t)
	  ((and (negative-literal? (first literals))
		(member (second (first literals)) clause))
	   #f)
	  (else (loop (rest literals)))))
  (loop clause))
  
;;; A trivial filter that always returns T.  Should be used when testing 
;;; the system without cadidate filtering

(define (trivial-clause-filter clause nodes) 
    #t)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;  Initial clause filtering
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define (apply-initial-clause-filters clause proof-nodes)
  (define (loop filters)
    (cond ((null? filters) #t)
	  (((car filters) clause proof-nodes) (loop (rest filters)))
	  (else #f)))
  (loop (resolution-initial-clause-filters *current-resolution-strategy*))
  )
   
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;  initial clause filtering strategies
;;;    To add a strategy define the function according to the example 
;;;    below.  
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
   

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Resolutions strategies.
;;;   A resolution strategy is created by filling in the fields of
;;;   the resolution record.  Below a few examples of such
;;;   combinations are given.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define *default-resolution-strategy*
  (make-resolution-all
   'default
   (list shortest-min-clause shortest-sum)
   (list setofsupport-filter)
   (list tautology-filter uniqueness-filter)
   #f
   ))

(define *setofsupport-strategy*
  (make-resolution-all
   'set-of-support
   #f
   (list setofsupport-filter)
   (list tautology-filter uniqueness-filter)
   #f
   ))

(define *shortest-min-shortest-sum-strategy*
  (make-resolution-all
   'shortest-min-shortest-sum
   (list shortest-min-clause shortest-sum)
   #f
   (list tautology-filter uniqueness-filter)
   #f
   ))

(define *shortest-min-clause-strategy*
  (make-resolution-all
   'shortest-min-clause
   (list shortest-min-clause)
   #f
   (list tautology-filter uniqueness-filter)
   #f
   ))

;;; This seems to be the best strategy
(define *current-resolution-strategy* *shortest-min-shortest-sum-strategy*)


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Test functions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define (prove theorem vars)
  (let ((answer (theorem-prover theorem *axioms* vars)))
    (print-proof answer)
    answer
    ))

(define (compare-strategies strategies theorem vars)
  (map (lambda (strategy)
	 (list (resolution-strategy-name strategy)
	       (fluid-let ((*current-resolution-strategy* strategy))
		 (let ((answer (theorem-prover theorem *axioms* vars)))
		   (print-proof answer)
		   answer
		   ))))
       strategies))

(define (print-proof pr)
  (let ((step 1)
	(step-for-clause '()))
    (define (print-clause cl)
      (let ((entry (if (list? cl) (first cl) cl))
	    (index (if (list? cl) (second cl) #f)))
	(display* "(" step ") " 
		  ;; provenance of clause
		  (if (proof-node-parent entry)
		      (map (lambda (clp)
			     (cdr (assoc clp step-for-clause)))
			   (proof-node-parent entry))
		      (if (assoc 'ans (proof-node-clause entry))
			  '(negated-goal)
			  '(axiom))))
	(set! step-for-clause
	      (cons (cons cl step) step-for-clause))
	(set! step (+ 1 step))
	(pretty-print (proof-node-clause entry)) 
	(let ((bindings (proof-node-binding entry)))
	  (or (eq? bindings *no-bindings*)
	      (begin
		(display "(unifier: ") 
		(pretty-print bindings)
		(display ")"))))
	(newline)
	))
    (define (collect-axioms cl)
      (if cl
	  (let ((entry (if (list? cl) (first cl) cl)))
	    (if (proof-node-parent entry)
		(for-each collect-axioms (proof-node-parent entry))
		(or (assoc cl step-for-clause) 
		    (print-clause cl))))))
    (define (print-proof-loop cl)
      (if cl
	  (let ((entry (if (list? cl) (first cl) cl)))
	    (if (proof-node-parent entry)
		(do ((x (proof-node-parent entry) (cdr x)))
		    ((null? x))
		  (print-proof-loop (car x))))
	    (or (assoc cl step-for-clause) 
		(print-clause cl))
	    ))
      )
    (display* "Search for proof attempted: " 
	      (proof-result-n-resolutions pr) " resolutions.")
    (display* "Proof result is: " (proof-result-answer pr))
    (collect-axioms (proof-result-proof pr))
    (print-proof-loop (proof-result-proof pr))
    (newline)
    ))

(define (test)
  (read-axioms "test1.lgc")
  (compare-strategies (list *default-resolution-strategy*
		            *shortest-min-shortest-sum-strategy*
			    *shortest-min-clause-strategy*
			    )
		      '(mother ?mom yzhak)
		      '(?mom)))

(define *t:silent* #f)                  ; if we want no output, set to #f

(define (display* . l)
  ;; Print the list of arguments
  (cond (*t:silent* #f)
        (else
         (for-each display l)
         (newline))))