#|
 Copyright © 2018 by Pete Manolios 
 CS 4820 Fall 2018. Pete Manolios.

 Homework 6.
 Due: 11/6 (Midnight)

 For this assignment, work in groups of 2-3. Send me exactly one
 solution per team and make sure to follow the submission instructions
 on the course Web page. In particular, make sure that the subject of
 your email submission is "CS 4820 HWK 6".

 The group members are:

 ... (put the names of the group members here)
 
 To make sure that we are all on the same page, download and build the
 latest version of SBCL. See
 http://www.sbcl.org/platform-table.html. It is OK to use the git
 version or an existing binary.

 The download and build the latest version of ACL2. See
 https://github.com/acl2/acl2/, use the testing branch and use the
 version of sbcl you just built. Here you have to use the latest
 version of ACL2, since it includes the latest ACL2s books.

 Certify the ACL2s books. In the books/acl2s subdirectory 
 of the acl2 installation, certify the books with 

 cert.pl *.lisp

 Read http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=BUILD____PRELIMINARIES 
 and  http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=BUILD____CERT.PL

 Now, create an ACL2s executable. When you execute the code in this
 file, that's the executable to use.
 
 Next, install quicklisp. See https://www.quicklisp.org/beta/. 

 As mentioned at the beginning of the semester, the code we will write
 is in Lisp. You can find the common lisp manual online in various
 formats by searching for "common lisp manual."

 Other references that you might find useful and are available online
 include
 
 - Common Lisp: A Gentle Introduction to Symbolic Computation by David
   Touretzky
 - ANSI Common Lisp by Paul Graham
 
|#


(set-ignore-ok t)

;; This gets us to raw lisp.
:q

#| 
 The point of the next two forms is that we can use ACL2s from within
 lisp. That will be useful to check that your code works.
|#

(defun acl2s-last-result ()
  (let ((state *the-live-state*))
    (@ result)))

(defun acl2s-query (q)
  (let ((state *the-live-state*))
    (ld `((mv-let
           (erp val state)
           (trans-eval ',q 'acl2s-query state t)
           (assign result (list erp (cdr val))))))
    (acl2s-last-result)))

#|

 Here are some examples you can try to see how acl2s-query works.

 (acl2s-query '(+ 1 2))
 (acl2s-query '(thm (iff (implies p q)
                         (or (not p) q))))
|#

#|

 Next, we need to load some software libraries using quicklisp.  For
 example, the trivia library provides pattern matching
 capabilities. Search for "match" below. You can see the online
 documentation for the other software libraries.

|#

(load "~/quicklisp/setup.lisp")
(ql:quickload :trivia)
(ql:quickload :cl-ppcre)
(ql:quickload :let-plus)
(setf ppcre:*allow-named-registers* t)

#|
 
 We now define our own package.

|#

(defpackage :tp (:use :cl :trivia :ppcre :let-plus :acl2 :acl2s))
(in-package :tp)

;; We import acl2s-query into our package.

(import 'acl2::acl2s-query)

#|
 
 We have a list of the propositional operators and information about
 them. 

 :arity can be a positive integer or - (meaning arbitrary arity) If
 :arity is -, there must be an identity and the function must be
 associative and commutative.

 If :identity is non-nil, then the operator has the indicated
 identity. 
 
 An operator is idempotent iff :idem is t.

 If :sink is not -, then it must be the case that (op ... sink ...) =
 sink, e.g., (and ... nil ...) = nil.

 FYI: it is common for global variables to be enclosed in *'s. 

|# 

(defparameter *p-ops*
  '((and     :arity - :identity t   :idem t   :sink nil)
    (or      :arity - :identity nil :idem t   :sink t)
    (not     :arity 1 :identity -   :idem nil :sink -)
    (implies :arity 2 :identity -   :idem nil :sink -)
    (iff     :arity - :identity t   :idem nil :sink -)
    (if      :arity 3 :identity -   :idem nil :sink -)))

#|

 mapcar is like map. See the common lisp manual.

|#

(defparameter *p-funs* (mapcar #'car *p-ops*))

#|

 See the definition of member in the common lisp manual.  Notice that
 there are different types of equality, including =, eql, eq, equal
 and equals. We need to be careful, so we'll just use equal and we'll
 define functions that are similar to the ACL2s functions we're
 familiar with.

|# 

(defun in (a x)
  (member a x :test #'equal))

(defmacro len (l) `(length ,l))

(defun p-funp (x)
  (in x *p-funs*))

(defun get-alist (k l)
  (cdr (assoc k l :test #'equal)))

(defun get-key (k l)
  (cadr (member k l :test #'equal)))

(defun remove-dups (l)
  (remove-duplicates l :test #'equal))

(defmacro == (x y) `(equal ,x ,y))
(defmacro != (x y) `(not (equal ,x ,y)))

(defun pfun-argsp (pop args)
  (and (in pop *p-funs*)
       (let ((arity (get-key :arity (get-alist pop *p-ops*))))
         (and (or (eql arity '-)
                  (= (len args) arity))
              (every #'p-formulap args)))))

(defun pfun-formulap (f)
  (and (consp f)
       (pfun-argsp (car f) (cdr f))))

#|
 
 Here is the definition of a propositional formula. 
 
|#

(defun p-formulap (f)
  (match f
    ((type boolean) t)
    ((type symbol) t)
    ((list* pop args)
     (if (p-funp pop)
         (pfun-argsp pop args)
       t))
    (_ nil)))

#|
 
 Notice that in addition to propositional variables, we allow atoms
 such as (foo x). 

 Here are some assertions (see the common lisp manual).
 
|#

(assert (p-formulap '(and)))
(assert (p-formulap '(and x y z)))
(assert (p-formulap '(and t nil)))
(assert (not (p-formulap '(implies x t nil))))
(assert (p-formulap 'q))
(assert (p-formulap '(implies (foo x) (bar y))))
(assert (p-formulap '(iff p q r s t)))
(assert (not (p-formulap '(if p q r t))))

#|

 The propositional skeleton is what remains when we remove
 non-variable atoms.

|#

(defun p-skeleton-args (args amap acc)
  (if (endp args)
      (values (reverse acc) amap)
    (multiple-value-bind (na namap)
        (p-skeleton- (car args) amap)
      (p-skeleton-args (cdr args) namap (cons na acc)))))

(defun p-skeleton- (f amap)
  (match f
    ((type symbol) (values f amap))
    ((list* pop args)
     (if (p-funp pop)
         (multiple-value-bind (nargs namap)
             (p-skeleton-args args amap nil)
             (values (cons pop nargs) namap))
       (let ((geta (get-alist f amap)))
         (if geta
             (values geta amap)
           (let ((gen (gentemp "P")))
             (values gen (acons f gen amap)))))))
    (_ (error "Not a p-formula"))))

(defun p-skeleton (f)
  (p-skeleton- f nil))

#|

 Here are some examples you can try.

(p-skeleton
 '(or p q r s))

(p-skeleton
 '(iff q r))

(p-skeleton
 '(or p (iff q r)))

(p-skeleton
 '(or p (iff q r) (and p q p) (if p (and p q) (or p q))))

(p-skeleton
 '(iff p p q (foo t nil) (foo t nil) (or p q)))

(p-skeleton
 '(iff p p q (foo t r) (foo s nil) (or p q)))

(p-skeleton
 '(or (foo a (g a c)) (g a c) (not (foo a (g a c)))))

|#

#|

 Next we have some utilities for converting propositional formulas to
 ACL2 formulas.

|#

(defun to-acl2 (f)
  (let ((s (p-skeleton f)))
    (match s
      ((type symbol) (intern (symbol-name f) "ACL2"))
      ((list 'not x)
       `(acl2::not ,(to-acl2 x)))
      ((list* 'or args)
       `(acl2::or ,@(mapcar #'to-acl2 args)))
      ((list* 'and args)
       `(acl2::and ,@(mapcar #'to-acl2 args)))
      ((list 'implies p q)
       `(acl2::implies ,(to-acl2 p) ,(to-acl2 q)))
      ((list 'iff) t)
      ((list 'iff p) (to-acl2 p))
      ((list* 'iff args)
       (acl2::xxxjoin 'acl2::iff
                      (mapcar #'to-acl2 args))))))

(defun pvars- (f)
  (match f
    ((type boolean) nil)
    ((type symbol) (list f))
    ((list 'not x)
     (pvars- x))
    ((list* 'or args)
     (reduce #'append (mapcar #'pvars- args)))
    ((list* 'and args)
     (reduce #'append (mapcar #'pvars- args)))
    ((list 'implies p q)
     (append (pvars- p) (pvars- q)))
    ((list* 'iff args)
     (reduce #'append (mapcar #'pvars- args)))))

(defun pvars (f) (remove-dups (pvars- f)))

(pvars '(and t (iff nil) (iff t nil t nil) p q))
(pvars '(iff p p q (foo t r) (foo s nil) (or p q)))

(defun boolean-hyps (l)
  (cons 'acl2::and
        (mapcar #'(lambda (x) `(acl2::booleanp ,x))
                (mapcar #'to-acl2 l))))

(boolean-hyps '(p q r))

(defun acl2s-check-equal (f g)
  (let* ((iff `(iff ,f ,g))
	 (pvars (pvars iff))
	 (aiff (to-acl2 iff))
         (af (second aiff))
         (ag (third aiff))
         (bhyps (boolean-hyps pvars)))
    (acl2s-query
     `(acl2::thm (acl2::implies ,bhyps (acl2::iff ,af ,ag))))))

;; And some simple examples.
(acl2s-check-equal 'p 'p)
(acl2s-check-equal 'p 'q)

; Here is how to check if the query succeeded
(assert (== (caadr (acl2s-check-equal 'p 'p)) nil))

; So, here's a useful function
(defun assert-acl2s-equal (f g)
  (assert (== (caadr (acl2s-check-equal f g)) nil)))

(assert-acl2s-equal 'p 'p)

; This will lead to an error (so comment it out after trying it).
; In sbcl :top get you out of the debugger.
(assert-acl2s-equal 'p 'q)

; Here is how we can use ACL2 to check our code.
(let* ((x '(or (foo a (g a c)) (g a c) (not (foo a (g a c))))))
  (assert-acl2s-equal x t))

(let* ((x '(or (foo a (g a c)) (g a c) (not (foo a (g a c)))))
       (sx (p-skeleton x)))
  (assert-acl2s-equal sx t))


#|
 
 Question 1. (25 pts)

 Define function, p-simplify that given a propositional formula
 returns an equivalent propositional formula with the following
 properties. 

 A. The skeleton of the returned formula is either a constant or does
 not include any constants. For example:

 (and p t (foo t nil) q) should be simplified to (and p (foo t nil) q)
 (and p t (foo t b) nil) should be simplified to nil

 B. Flatten expressions, e.g.:

 (and p q (and r s) (or u v)) is not flat, but this is
 (and p q r s (or u v))

 A formula of the form (op ...) where op is a Boolean operator applied
 to 0 or 1 arguments is not flat. For example, replace (and) with t. A
 formula of the form (op ... (op ...)) where op is a Boolean operator
 is not flat. For example, replace (and p q (and r s)) with (and p q r s).  

 C. If there is Boolean constant s s.t. If (op ... s ...) = s, then we
 say that s is a sink of op. For example t is a sink of or. A formula
 is sink-free if no such subformulas remain. The returned formula
 should be sink-free.

 D. Simplify your formulas so that no subexpressions of the following
 form remain
 
 (not (not f))

 E. Simplify formulas so that no subexpressions of the form

 (op ... p ... q ...)

 where p, q are equal literals or  p = (not q) or q = (not p).

 For example
 
 (or x y (foo a b) z (not (foo a b)) w) should be simplified to 

 t 

|#

(defun p-simplify (f) ...)

#|
 
 Question 2. (10 pts)

 Test your definition with assert-acl2s-equal using at least 10
 propositional formulas that include non-variable atoms, all of the
 operators, deeply nested formulas, etc.

|#


#|

 Question 3. (15 pts)

 Define nnf, a function that given a propositional formula, something
 that satisfies p-formulap, puts it into negation normal form (NNF).

 The propositional skeleton of the resulting formula cannot contain any
 of the following propositional connectives: implies, iff, if.

 Notice that

 (or (foo (if a b)) (not p))

 is in NNF because (foo (if a b))) is an atom and the skeleton is
 something like:

 (or p1 (not p))

 Test nnf using with assert-acl2s-equal using at least 10
 propositional formulas.

|#

(defun nnf (f) ...)

#|

 Question 4. (25 pts)

 Define tseitin, a function that given a propositional formula,
 something that satisfies p-formulap, applies the tseitin
 transformation to generate a CNF formula that is equi-satisfiable.

 Remember that you have to deal with atoms such as

 (foo (if a b))

 You should simplify the formula first, using p-simplify, but you
 should *not* start by applying NNF, as that may cause a blow-up.

 Test tseitin using with assert-acl2s-equal using at least 10
 propositional formulas.

|#

(defun tseitin (f) ...)

#|

 Question 5. (25 pts)

 Define DP, a function that given a propositional formula in CNF,
 applies the Davis-Putnam algorithm to determine if the formula is
 satisfiable.

 Remember that you have to deal with atoms such as

 (foo (if a b))

 If the formula is sat, DP returns 'sat and a satisfying assignment: an
 alist mapping each atom in the formula to t/nil. Use values to return
 multiple values.

 If it is usat, return 'unsat.

 Test DPP using with assert-acl2s-equal using at least 10
 propositional formulas.

|#

(defun dp (f) ...)

#|

 Question 6. Extra Credit (25 pts)

 Define DPLL, a function that given a propositional formula in CNF,
 applies the DPLL algorithm to determine if the formula is
 satisfiable.

 Remember that you have to deal with atoms such as

 (foo (if a b))

 If the formula is sat, DPLL returns 'sat and a satisfying assignment:
 an alist mapping each atom in the formula to t/nil. Use values to
 return multiple values.

 If it is usat, return 'unsat.

 Test DPLL using with assert-acl2s-equal using at least 10
 propositional formulas.

|#

(defun dpll (f) ...)