;;-------------------------------------------------------------------------
;; Utilities for WalkSAT implementation, Homework 4, CMSC 471, Fall 2009
;; (c) 2009 Marie desJardins
;;
;; Notes on representation conventions:
;;   - A "model" is a list of variable assignments, of the form
;;       ((var1 val1) (var2 val2) ...)
;;     where the "val_i" values are each T or NIL
;;   - A "clause" is any well-formed propositional Lisp-ish formula
;;     using the connectives AND, OR, and NOT; for example:
;;         (and (or (not a) b) (and (b (not c))))
;;     Note that for WalkSAT to work properly, the clauses should
;;     be in normal form; that is, they should be a single
;;     disjunction of literals (where each literal is either a
;;     variable, or "(not VAR)")
;;   - A clause list is just a list of clauses -- it is implicitly
;;     conjunctive (i.e., the clauses are ANDed together)


;; Lisp tip:
;;   (random N) where N is an integer returns a random integer in
;;     the range [0, N-1]
;;   Note that (random X) where X is a non-integer positive number returns
;;      a random real value in the range [0, X)

(defmacro random-element (l)
  "Return a random element from list L"
  `(nth (random (length ,l)) ,l))


;; Lisp tips:
;;   Note the use of the macro back-quote syntax.  By
;;     using this syntax, we can use LET* to locally bind
;;     the variables in the model (get it?  the model
;;     has the same syntax as a LET* list)
;;   LET* creates variables that are dynamic in scope rather
;;     than local in scope -- that way if there is a function
;;     call inside the LET* body, the variables will be
;;     available inside those function calls.  It's a bit
;;     of overkill here, but why not.
;;   Note also that we have constructed our clauses using
;;     Lisp syntax and connectives/functions (OR and NOT),
;;     so once we bind the variables, we can just EVAL the
;;     clause to get its truth value -- cool, huh?

(defun satisfies-one (model clause)
  "Return T if a model satisfies a single clause"
  (eval `(let* ,model
	   ,clause)))

(defun satisfies-all (model clauses)
  "Returns T if a model satisfies all clauses in a list of clauses"
  (eval `(let* ,model
	   (and . ,clauses)))
  )

(defun count-satisfies (model clauses &aux (n 0))
  "Return the number of clauses in a list of clauses satisfied by a model"
  (loop for c in clauses
	do (if (eval `(let* ,model ,c)) (incf n)))
  n)


;; Lisp tip:
;;   Check out the recursion -- basically this is FLATTEN-LIST
;;     in disgise, ripping the list apart to look for symbols
;;     and glomming them onto a list as you go.  The variable
;;     list gets passed around throughout the recursion because
;;     it seems simpler to ADJOIN one symbol at a time than to
;;     have to do a list merge on each return.

(defun clause-vars (clause &optional (vars))
  "Return a list of all variables that appear in a clause 
   (i.e., all symbols that are not connectives)"
  (cond ((null clause) vars)
	((listp clause) (clause-vars (cdr clause)
				     (clause-vars (car clause) vars)))
	((member clause '(and or not)) vars)
	;; Lisp tip: "adjoin" adds an item to a list if it is not
	;; already there
	(t (adjoin clause vars))))


(defun random-var (clause)
  "Pick a random variable from a clause"
  (let ((vars (clause-vars clause)))
    (random-element vars))
  )

(defun collect-vars (clauses &aux (vars nil))
  "Return a list of all of the variables in a list of clauses;
   uses CLAUSE-VARS as a helper"
  (loop for c in clauses
	do (setf vars (clause-vars c vars)))
  vars)


;; Lisp tip:
;;   Again I am taking advantage of the fact that the variable
;;     value assignments in the model are actually the Lisp
;;     symbols T and NIL, and using the Lisp NOT to flip their
;;     values

(defun flip (var model)
"Given a model and a variable, return a new model with the opposite
 truth value for that variable (T -> NIL; NIL -> T)"
  (loop for asst in model
	collect (if (eq (car asst) var)
		    ;; This is the variable: flip the value
		    (list (car asst) (not (second asst)))
		  asst)))