(defun neg (literal) (* -1 literal))

(defun false-literal (assignment literal)
  (member (neg literal) assignment))

(defun one-not-false-literal (assignment clause)
  (cond
   ((atom clause) nil)
   ((false-literal assignment (car clause))
    (one-not-false-literal assignment (cdr clause)))
   (t
    clause)))

(defun two-not-false-literals (assignment clause)
  (cond
   ((atom clause) nil)
   ((false-literal assignment (car clause))
    (two-not-false-literals assignment (cdr clause)))
   (t
    (cons (car clause)
          (one-not-false-literal assignment (cdr clause))))))

(defun get-unit (formula assignment) 
  (if (atom formula)
    (mv nil nil)
    (let ((reduced-clause (two-not-false-literals assignment (car formula))))
      (cond ((not reduced-clause) (mv (car formula) nil))
            ((and (car reduced-clause)
                  (not (cdr reduced-clause))
                  (not (member (car reduced-clause) assignment)))
             (mv (car formula) (car reduced-clause)))
            (t (get-unit (cdr formula) assignment))))))

(defun all-lits (formula)
  (if (atom formula)
    nil
    (append (car formula) (all-lits (cdr formula)))))

(defthm reduced-clause-implies-member-car-reduced-clause
        (implies (two-not-false-literals assignment clause)
                 (member (car (two-not-false-literals assignment clause))
                         clause)))

(defthm member-append-member-or
        (iff (member x (append y z))
             (or (member x y)
                 (member x z))))

(defthm get-unit-returns-member-of-all-lits
  (implies (cadr (get-unit formula assignment))
           (member (cadr (get-unit formula assignment))
                   (all-lits formula))))

(defthm new-element-reduces-difference
        (implies (and (member e y) 
                      (not (member e x)))
                 (< (len (set-difference-equal y (cons e x))) 
                    (len (set-difference-equal y x)))))

(defun remove-literal (clause literal)
  (cond ((atom clause) clause)
        ((eql (car clause) literal) (cdr clause))
        (t (cons (car clause) (remove-literal (cdr clause) literal)))))

(defun resolve (clause resolvent literal)
  (union-equal (remove-literal clause literal) 
               (remove-literal resolvent (neg literal))))

(defun unit-under-assignment (assignment clause)
  (and (car (two-not-false-literals assignment clause))
       (not (cdr (two-not-false-literals assignment clause)))))

(defun implications-or-resolvent (formula assignment implications) 
  (declare (xargs :measure (nfix (len (set-difference-equal (all-lits formula) implications)))
                  :hints (("Subgoal 1"
                           :use ((:instance 
                                  new-element-reduces-difference
                                  (y (all-lits formula))
                                  (x implications)
                                  (e (mv-nth 1 (get-unit formula (append assignment
                                                                         implications))))))
                           ))))
  (mv-let (clause literal)
          (get-unit formula (append assignment implications))
          (if (not literal) ; end recursion
            (if clause
              (mv nil clause)
              (mv implications nil))
            (mv-let (more-implications resolvent)
                    (implications-or-resolvent formula assignment 
                                               (cons literal implications))
                    (if more-implications
                      (mv more-implications nil)
                      (if (or (unit-under-assignment assignment resolvent)
                              (not (member (neg literal) resolvent)))
                        (mv nil resolvent)
                        (mv nil (resolve clause resolvent literal))))))))

(defun get-decision (heuristics assignment)
  (if (atom heuristics)
    nil
    (if (or (member (car heuristics) assignment)
            (member (neg (car heuristics)) assignment))
      (get-decision (cdr heuristics) assignment)
      (list (car heuristics)))))
           
(defthm get-decision-returns-not-member-assignment
  (implies (get-decision heuristics assignment)
           (not (member (car (get-decision heuristics assignment)) 
                        assignment))))

(defthm cons-subsetp-lemma
        (implies (subsetp x lst)
                 (subsetp x (cons y lst))))

; requires cons-subsetp-lemma and append-subsetp-lemma
(defthm decision-subsetp-of-implications
        (implies (car (implications-or-resolvent formula assignment decision))
                 (subsetp decision
                          (car (implications-or-resolvent formula assignment decision)))))

(defthm subsetp-car-member
        (implies (and (consp x)
                      (subsetp x y))
                 (member (car x) y)))

; requires subsetp-car-member
(defthm car-get-decision-member-car-implications
        (implies (and (consp d)
                      (car (implications-or-resolvent f a d)))
                 (member (car d) (car (implications-or-resolvent f a d)))))

(defthm member-not-member-reduce-set-difference
        (implies (and (member (car g) h)
                      (member (car g) i)
                      (not (member (car g) a)))
                 (< (len (set-difference-equal h (append a i)))
                    (len (set-difference-equal h a)))))

; requires member-not-member-reduce-set-difference
(defthm get-decision-and-implication-reduce-set-difference
        (implies (and (get-decision h a)
                      (car (implications-or-resolvent f a (get-decision h a))))
                 (and  (member (car (get-decision h a)) h)
                       (member (car (get-decision h a)) (car (implications-or-resolvent f a (get-decision h a))))
                       (not (member (car (get-decision h a)) a))
                       (< (len (set-difference-equal h (append a (car (implications-or-resolvent f a (get-decision h a))))))
                          (len (set-difference-equal h a))))))

(defun assign-rec (formula heuristics assignment) ; return (solution, conflict)
  (declare (xargs :measure (nfix (len (set-difference-equal heuristics assignment)))))
  (let ((decision (get-decision heuristics assignment)))
    (if (not decision) 
      (mv assignment nil) ; found a solution -> satisfiable
      (mv-let (implications resolvent)
              (implications-or-resolvent formula assignment decision)
              (if implications
                (assign-rec formula heuristics (append assignment implications))
                (mv nil resolvent))))))

(defun solution-or-resolvent (formula heuristics)
  (mv-let (assignment resolvent)
          (implications-or-resolvent formula nil nil)
          (if resolvent
            (mv nil nil) ; found refutation -> unsatisfiable
            (assign-rec formula heuristics assignment))))

(defun heuristics-init (formula)
  (all-lits formula))          

(skip-proofs
(defun cdcl-rec (formula heuristics)  ; returns solution or unsatisfiable
;  (declare (xargs :measure (nfix (len (set-difference-equal power-set(formula) formula)))))
  (mv-let (solution resolvent)
          (solution-or-resolvent formula heuristics)
          (cond (resolvent (cdcl-rec (cons resolvent formula) heuristics))
                (solution solution)   ; found solution
                (t 'unsatisfiable)))) ; found refutation
)

(defun cdcl (formula)
  (cdcl-rec formula (heuristics-init formula)))

(implications-or-resolvent  '((1 4)(3 -4 -5)(-3 -2 -4)) '(5 2) '(-1))

(implications-or-resolvent  '((-1 -3 5 17 18)
                              (1 -8 10)
                              (2 -4 -10)
                              (-2 -7 12)
                              (-3 5 -18 -19)
                              (3 10)
                              (-5 10)
                              (6 -11 -12)
                              (7 -11 13))
                            '(-6 8 -13 19 4 -17) 
                            '(11))

;(ld "~/Desktop/sat75lisp/uf75-020.cnf" :ld-pre-eval-print t)

(cdcl '((1 2)(-1 2)(1 -2)(-1 -2)))

(cdcl '((4 -18 19)
        (3 18 -5)
        (-5 -8 -15)
        (-20 7 -16)
        (10 -13 -7)
        (-12 -9 17)
        (17 19 5)
        (-16 9 15)
        (11 -5 -14)
        (18 -10 13)
        (-3 11 12)
        (-6 -17 -8)
        (-18 14 1)
        (-19 -15 10)
        (12 18 -19)
        (-8 4 7)
        (-8 -9 4)
        (7 17 -15)
        (12 -7 -14)
        (-10 -11 8)
        (2 -15 -11)
        (9 6 1)
        (-11 20 -17)
        (9 -15 13)
        (12 -7 -17)
        (-18 -2 20)
        (20 12 4)
        (19 11 14)
        (-16 18 -4)
        (-1 -17 -19)
        (-13 15 10)
        (-12 -14 -13)
        (12 -14 -7)
        (-7 16 10)
        (6 10 7)
        (20 14 -16)
        (-19 17 11)
        (-7 1 -20)
        (-5 12 15)
        (-4 -9 -13)
        (12 -11 -7)
        (-5 19 -8)
        (1 16 17)
        (20 -14 -15)
        (13 -4 10)
        (14 7 10)
        (-5 9 20)
        (10 1 -19)
        (-16 -15 -1)
        (16 3 -11)
        (-15 -10 4)
        (4 -15 -3)
        (-10 -16 11)
        (-8 12 -5)
        (14 -6 12)
        (1 6 11)
        (-13 -5 -1)
        (-7 -2 12)
        (1 -20 19)
        (-2 -13 -8)
        (15 18 4)
        (-11 14 9)
        (-6 -15 -2)
        (5 -12 -15)
        (-6 17 5)
        (-13 5 -19)
        (20 -1 14)
        (9 -17 15)
        (-5 19 -18)
        (-12 8 -10)
        (-18 14 -4)
        (15 -9 13)
        (9 -5 -1)
        (10 -19 -14)
        (20 9 4)
        (-9 -2 19)
        (-5 13 -17)
        (2 -10 -18)
        (-18 3 11)
        (7 -9 17)
        (-15 -6 -3)
        (-2 3 -13)
        (12 3 -2)
        (-2 -3 17)
        (20 -15 -16)
        (-5 -17 -19)
        (-20 -18 11)
        (-9 1 -5)
        (-19 9 17)
        (12 -2 17)
        (4 -16 -5)))