;;;This files contains functions useful for the HW4 problem
;;;to write a program to check if a propositional formula is valid
;;;


;;; Well-formed formula checker
;;;
;;; The function  (well_formed x) checks if x is a well-formed
;;; boolean infix Boolean formula and outputs t if it is and nil
;;; otherwise
;;;
;;; Example use:
;;; >(well_formed '(A AND (B OR C)))
;;; t

(defun well_formed (x)
"Check if x is a well-formed boolean formula" 
	(if (atom x) t 
		(if (or (neg_well_formed x)
		        (and_well_formed x)
		        (or_well_formed x)
		    )
		t
		nil
		)
		 
	) 
)

;
; Auxiliary Functions
;

(defun neg_well_formed (x)
"check if x's is the negation of a well-formed formula"
	(if (and (eql (first x) 'NOT)
	         (well_formed (second x))
		 (null (third x))
	    )
	  t
	  nil
	)
)

(defun and_well_formed (x)
"check if x's is the and of well-formed formulas"
	(if (and (well_formed (first x) )
	         (eql (second x) 'AND)		 
		 (well_formed (third x))
		 (null (fourth x))
	    )
	 t
	 nil
	)
)

(defun or_well_formed (x)
"check if x's is the or of well-formed formulas"
	(if (and (well_formed (first x) )
	         (eql (second x) 'OR)
		 (well_formed (third x))
		 (null (fourth x))
	    )
	 t
	 nil
	)
)

;;;
;;; var_assign
;;;
;;; a variable assignment structure
;;;
(defstruct var_assign  
	(name 'x)       ;name of variable
	(value nil)	;its value
)

;;;
;;; (ext_var x)
;;;
;;; extracts variables from a well-formed formula x 
;;;
;;; If a variable occurs more than once it will be extracted more than once
;;; this can potentially make your code slower
;;;
;;; Example use:
;;; >(ext_var '(A AND B))
;;; (#S(VAR_ASSIGN NAME A VALUE NIL) #S(VAR_ASSIGN NAME B VALUE NIL))

(defun ext_var (x)
"extracts variables from a well-formed formula x into an all nil
 truth assignment"
	(if (atom x) (list (make-var_assign :name x))
	    (prog ( (f (first x))
		    (s (second x))
		    (th (third x))
		  )
	          (if (eql f 'NOT) (return (ext_var s)))
	          (if (or (eql s 'AND)
			  (eql s 'OR)
			) 
			(return
				(append 
					(ext_var f)
					(ext_var th)
				)
			)
		  )
		  (return nil)
	     )
	)		
)

;;;
;;; (next_assign a)
;;;
;;; if a is a truth assignment computes lex next truth assign
;;;
;;; Example use:
;;; >(next_assign '(#S(VAR_ASSIGN NAME A VALUE NIL) #S(VAR_ASSIGN NAME B VALUE 
;;; NIL)))
;;; (#S(VAR_ASSIGN NAME A VALUE T) #S(VAR_ASSIGN NAME B VALUE NIL))

(defun next_assign (a)
" computes lexicographically next truth assignment after a	
"
	(if (or (eql a nil) (atom a)) nil
	   (prog ( (name (var_assign-name (first a)))
		   (value (var_assign-value (first a)))
		   (r (rest a))	
		 )
	   	(if (eql value nil )
			(return (cons (make-var_assign :name name :value t) r))
			(return (cons (make-var_assign :name name :value nil)
					(next_assign r)
				)
			)
		)
	   )  
  	)
)

;;;
;;; (at_value at assign)
;;;
;;; returns the value assigned to at in assign if it is assigned 
;;; otherwise nil
;;;
;;; If at assigned more than once in assign only first assignment used
;;;
;;; Example use:
;;; >(setf c (ext_var '(A AND B)))
;;; >(at_value 'A c)
;;; nil
;;; >(setf c (next_assign c))
;;; >(at_value 'A c)
;;; T

(defun at_value (at assign)
"returns the value assigned to the atom at in the truth assignment assign
if it exists. Otherwise returns nil"
	(if (or (not (atom at))
		(atom assign)
		(null assign)	
	     ) 
		nil
		(prog 	( (f (first assign))
			)
	  		(if (not (var_assign-p f)) (return nil))
	  		(if (eql at (var_assign-name f)) 
				(return (var_assign-value f)))
	  		(return (at_value at (rest assign)))
		)
	)
)
	
;;;
;;; (form_value formula assign)
;;;
;;; returns t or nil depending on whether assign is a satisfying 
;;; assignment for formula
;;;
;;;; your code here

;;;
;;; (valid fmla)
;;;
;;; return t if fmla is a valid formula; nil otherwise
;;;
;;; your code here