#lang racket
(require rackunit)
(require rackunit/text-ui)

;; Autor: Michał Zobniów
;; Data : 29.03.2019
;; Filip Sieczkowski pomógł mi ze zrozumieniem treści zadania 2

;; procedury pomocnicze
(define (tagged-tuple? tag len x)
  (and (list? x)
       (=   len (length x))
       (eq? tag (car x))))

(define (tagged-list? tag x)
  (and (pair? x)
       (eq? tag (car x))
       (list? (cdr x))))

;; reprezentacja formuł w CNFie
;; zmienne
(define (var? x)
  (symbol? x))

(define (var x)
  x)

(define (var-name x)
  x)

(define (var<? x y)
  (symbol<? x y))

;; literały
(define (lit pol var)
  (list 'lit pol var))

(define (pos x)
  (lit true (var x)))

(define (neg x)
  (lit false (var x)))

(define (lit? x)
  (and (tagged-tuple? 'lit 3 x)
       (boolean? (second x))
       (var? (third x))))

(define (lit-pol l)
  (second l))

(define (lit-var l)
  (third l))

;; klauzule
(define (clause? c)
  (and (tagged-list? 'clause c)
       (andmap lit? (cdr c))))

(define (clause . lits)
  (cons 'clause lits))

(define (clause-lits c)
  (cdr c))

(define (cnf? f)
  (and (tagged-list? 'cnf f)
       (andmap clause? (cdr f))))

(define (cnf . clauses)
  (cons 'cnf clauses))

(define (cnf-clauses f)
  (cdr f))

;; definicja rezolucyjnych drzew wyprowadzenia
(define (axiom? p)
  (tagged-tuple? 'axiom 2 p))

(define (axiom c)
  (list 'axiom c))

(define (axiom-clause a)
  (second a))

(define (res? p)
  (tagged-tuple? 'resolve 4 p))

(define (res x pf-pos pf-neg)
  (list 'resolve x pf-pos pf-neg))

(define (res-var p)
  (second p))
(define (res-proof-pos p)
  (third p))
(define (res-proof-neg p)
  (fourth p))

(define (proof? p)
  (if
   (or (and (axiom? p)
            (clause? (axiom-clause p)))
       (and (res? p)
            (var? (res-var p))
            (proof? (res-proof-pos p))
            (proof? (res-proof-neg p))))
   #t
   #f))

;;Procedury pomocnicze do szukania klauzuli i literałów;;
(define (find-clause cla prop-cnf)
  (if (eq? (cdr prop-cnf) null)
      #f
      (let ([l (cadr prop-cnf)])
        (if (equal? cla l)
            #t
            (find-clause cla (cdr prop-cnf))))))

(define (find-lit lit clause)
  (if (eq? (cdr clause) null)
      #f
      (let ([l (cadr clause)])
        (if (equal? lit l)
            #t
            (find-lit lit (cdr clause))))))


(define (proof-result pf prop-cnf)
  (if (axiom? pf)
      (if (null? (clause-lits (axiom-clause pf)))
          (axiom-clause pf)
          #f)
      (cond
        ;;Jeżeli prawe i lewe poddrzewo jest axiomem
        ((and (axiom? (res-proof-pos pf))
              (axiom? (res-proof-neg pf)))

         (let ([pos (axiom-clause (res-proof-pos pf))]
               [neg (axiom-clause (res-proof-neg pf))])
           ;;Sprawdzam czy klauzule należą do zbioru klauzli
           (if (and (find-clause pos prop-cnf)(find-clause neg prop-cnf))
               (let (
                     [lit-pos (lit #t (res-var pf))]
                     [lit-neg (lit #f (res-var pf))])
                 ;;Sprawdzam czy literały należą do klauzuli
                 (if (and (find-lit lit-pos pos) (find-lit lit-neg neg))
                     ;;Tworze wynik
                     (cons 'clause (remove-duplicates (append (filter (λ(x) (not (equal? lit-pos x))) (cdr pos))
                                                              (filter (λ(x) (not (equal? lit-neg x))) (cdr neg)))))
                     #f))
               #f))
         )

        ;;Jeżeli lewe poddrzewo jest axiomem, a prawe rezolwenta
        ((and (axiom? (res-proof-pos pf))
              (res? (res-proof-neg pf)))
         ;;res-neg wynik prawego poddrzewa
         ;;axiom-neg axiom prawego poddrzewa
         (let* ([res-neg (proof-result (res-proof-neg pf) prop-cnf)]
                [axiom-neg (axiom res-neg)]
                [new-res (res (res-var pf) (res-proof-pos pf) axiom-neg)])
           (proof-result new-res (cons 'cnf  (cons res-neg (cdr prop-cnf))))))

        ;;Jeżeli prawe poddrzewo jest axiomem, a lewe rezolwenta
        ((and (res? (res-proof-pos pf))
              (axiom? (res-proof-neg pf)))
         ;;res-pos wynik lewego poddrzewa
         ;;axiom-neg axiom lewego poddrzewa
         (let* ([res-pos (proof-result (res-proof-pos pf) prop-cnf)]
                [axiom-pos (axiom res-pos)]
                [new-res (res (res-var pf) axiom-pos (res-proof-neg pf))])
           (proof-result new-res (cons 'cnf  (cons res-pos (cdr prop-cnf))))))

        ;;Jeżeli oba drzewa są rezolwentami
        ((and (res? (res-proof-pos pf))
              (res? (res-proof-neg pf)))
         ;;res-pos wynik lewego poddrzewa
         ;;axiom-neg axiom lewego poddrzewa
         ;;res-neg wynik prawego poddrzewa
         ;;axiom-neg axiom prawego poddrzewa
         (let* ([res-neg (proof-result (res-proof-neg pf) prop-cnf)]
                [res-pos (proof-result (res-proof-pos pf) prop-cnf)]
                [axiom-pos (axiom res-pos)]
                [axiom-neg (axiom res-neg)]
                [new-res (res (res-var pf) axiom-pos axiom-neg)])
           (proof-result new-res (cons 'cnf (cons res-neg (cons res-pos (cdr prop-cnf)))))))
        )))


(define (check-proof? pf prop)
  (let ((c (proof-result pf prop)))
    (and (clause? c)
         (null? (clause-lits c)))))

;; XXX: Zestaw testów do zadania pierwszego

(define proof-checking-tests
  (test-suite "proof-checking-tests"

              ;;Test z pliku PDF
              (test-case "proof-checking-test-1"
                         (let* ([C1 (clause (lit #t 'p) (lit #t 'q))]
                                [C2 (clause (lit #f 'p) (lit #t 'q))]
                                [C3 (clause (lit #f 'q) (lit #t 'r))]
                                [C4 (clause (lit #f 'q) (lit #f 'r))]
                                [prop-cnf (cnf C1 C2 C3 C4)]
                                [A1 (axiom C1)]
                                [A2 (axiom C2)]
                                [A3 (axiom C3)]
                                [A4 (axiom C4)]
                                [pf (res 'q
                                         (res 'p A1 A2)
                                         (res 'r A3 A4))])
                           (check-eq? (check-proof? pf prop-cnf) #t)))

              ;;Test z Whitebooka Zadanie 125
              (test-case "proof-checking-test-2"
                         (let* ([C1 (clause (lit #f 'p)(lit #t 'q))]
                                [C2 (clause (lit #f 'p)(lit #f 'r)(lit #t 's))]
                                [C3 (clause (lit #f 'q)(lit #t 'r))]
                                [C4 (clause (lit #t 'p))]
                                [C5 (clause (lit #f 's))]
                                [prop-cnf (cnf C1 C2 C3 C4 C5)]
                                [A1 (axiom C1)]
                                [A2 (axiom C2)]
                                [A3 (axiom C3)]
                                [A4 (axiom C4)]
                                [A5 (axiom C5)]
                                [pf (res 'p
                                         A4
                                         (res 's
                                              (res 'r
                                                   (res 'q A1 A3)
                                                   A2)
                                              A5))])
                           (check-eq? (check-proof? pf prop-cnf) #t)))

              ;;Według (proof?) pojedynczy axiom też jest poprawnym dowodem ale wiemy że zbiór złozony z jednej klauzuli niepustej jest spełnialny
              (test-case "proof-checking-test-3"
                         (let* ([C1 (clause (lit #f 'p)(lit #t 'q))]
                                [prop-cnf (cnf C1)]
                                [A1 (axiom C1)]
                                [pf A1])
                           (check-eq? (check-proof? pf prop-cnf) #f)))

              ;;Podobnie jak w test3 tylko że teraz klauzula jest pusta
              (test-case "proof-checking-test-4"
                         (let* ([C1 (clause)]
                                [prop-cnf (cnf C1)]
                                [A1 (axiom C1)]
                                [pf A1])
                           (check-eq? (check-proof? pf prop-cnf) #t)))))


;; testy procedur pomocniczych
(define find-lit-and-find-clause-tests
  (test-suite "find-lit-and-find-clause-tests"

              (test-case "find-clause-test"
                         (let* ([C1 (clause (lit #t 'p) (lit #t 'q))]
                                [C2 (clause (lit #f 'p) (lit #t 'q))]
                                [C3 (clause (lit #f 'q) (lit #t 'r))]
                                [C4 (clause (lit #f 'q) (lit #f 'r))]
                                [prop-cnf (cnf C1 C2 C3 C4)])
                           (check-eq?
                            (and (eq? (find-clause C1 prop-cnf) #t)
                                 (eq? (find-clause C2 prop-cnf) #t)
                                 (eq? (find-clause C3 prop-cnf) #t)
                                 (eq? (find-clause C4 prop-cnf) #t))
                            #t)))

              (test-case "find-lit-test"
                         (let* ([L1 (lit #t 'p)]
                                [L2 (lit #t 'q)]
                                [L3 (lit #t 'z)]
                                [L4 (lit #t 'r)]
                                [C1 (clause L1 L2 L3 L4)])
                           (check-eq?
                            (and (eq? (find-lit L1 C1) #t)
                                 (eq? (find-lit L2 C1) #t)
                                 (eq? (find-lit L3 C1) #t)
                                 (eq? (find-lit L4 C1) #t))
                            #t)))))

(run-tests find-lit-and-find-clause-tests)
(run-tests proof-checking-tests)


;; Wewnętrzna reprezentacja klauzul

(define (sorted? ord? xs)
  (or (null? xs)
      (null? (cdr xs))
      (and (ord? (car xs)
                 (cadr xs))
           (sorted? ord? (cdr xs)))))

(define (sorted-varlist? xs)
  (and (andmap var? xs)
       (sorted? var<? xs)))

(define (res-clause pos neg pf)
  (list 'res-clause pos neg pf))

(define (res-clause-pos rc)
  (second rc))
(define (res-clause-neg rc)
  (third rc))
(define (res-clause-proof rc)
  (fourth rc))

(define (res-clause? p)
  (and (tagged-tuple? 'res-clause 4 p)
       (sorted-varlist? (second p))
       (sorted-varlist? (third  p))
       (proof? (fourth p))))

;; implementacja zbiorów / kolejek klauzul do przetworzenia

(define clause-set-empty
  '(stop () ()))

(define (clause-set-add rc rc-set)
  (define (eq-cl? sc)
    (and (equal? (res-clause-pos rc)
                 (res-clause-pos sc))
         (equal? (res-clause-neg rc)
                 (res-clause-neg sc))))
  (define (add-to-stopped sset)
    (let ((procd  (cadr  sset))
          (toproc (caddr sset)))
      (cond
        [(null? procd) (list 'stop (list rc) '())]
        [(or (memf eq-cl? procd)
             (memf eq-cl? toproc))
         sset]
        [else (list 'stop procd (cons rc toproc))])))
  (define (add-to-running rset)
    (let ((pd  (second rset))
          (tp  (third  rset))
          (cc  (fourth rset))
          (rst (fifth  rset)))
      (if (or (memf eq-cl? pd)
              (memf eq-cl? tp)
              (eq-cl? cc)
              (memf eq-cl? rst))
          rset
          (list 'run pd tp cc (cons rc rst)))))
  (if (eq? 'stop (car rc-set))
      (add-to-stopped rc-set)
      (add-to-running rc-set)))

(define (clause-set-done? rc-set)
  (and (eq? 'stop (car rc-set))
       (null? (caddr rc-set))))

(define (clause-set-next-pair rc-set)
  (define (aux rset)
    (let* ((pd  (second rset))
           (tp  (third  rset))
           (nc  (car tp))
           (rtp (cdr tp))
           (cc  (fourth rset))
           (rst (fifth  rset))
           (ns  (if (null? rtp)
                    (list 'stop (cons cc (cons nc pd)) rst)
                    (list 'run  (cons nc pd) rtp cc rst))))
      (cons cc (cons nc ns))))
  (if (eq? 'stop (car rc-set))
      (let ((pd (second rc-set))
            (tp (third  rc-set)))
        (aux (list 'run '() pd (car tp) (cdr tp))))
      (aux rc-set)))

(define (clause-set-done->clause-list rc-set)
  (and (clause-set-done? rc-set)
       (cadr rc-set)))

;; konwersja z reprezentacji wejściowej na wewnętrzną

(define (clause->res-clause cl)
  (let ((pos (filter-map (lambda (l) (and (lit-pol l) (lit-var l)))
                         (clause-lits cl)))
        (neg (filter-map (lambda (l) (and (not (lit-pol l)) (lit-var l)))
                         (clause-lits cl)))
        (pf  (axiom cl)))
    (res-clause (sort pos var<?) (sort neg var<?) pf)))

;; tu zdefiniuj procedury pomocnicze, jeśli potrzebujesz

;;;;; MERGE SORT ;;;;;

;; Mój Merge sort z zadania z List 3 ;;
(define (split xs)
  (define (iter acc ys)
    (if (<= (length ys) (/ (length xs) 2))
        (cons acc (list ys))
        (iter (append acc (list (car ys))) (cdr ys))))
  (if (< (length xs) 2)
      xs
      (iter null xs)))

(define (merge xs ys)
  (define (iter xs ys acc)
    (cond [(null? xs) (append acc ys)]
          [(null? ys) (append acc xs)]
          [(var<? (car xs) (car ys))(iter (cdr xs) ys (append acc (list (car xs))))]
          [else (iter xs (cdr ys) (append acc (list (car ys))))]))
  (iter xs ys null))

(define (merge-sort xs)
  (if (< (length xs) 1)
      xs
      (if (= 1 (length xs))
          xs
          (let ([ys (split xs)])
            (merge (merge-sort (car ys)) (merge-sort (car (cdr ys))))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;szukam var w liscie varów
(define (find-var var var-list)
  (if (null? var-list)
      #f
      (let ([var-from-var-list (car var-list)])
        (if (equal? var var-from-var-list)
            var
            (find-var var (cdr var-list))))))

;;wybieram var do rezolucji
(define (choose-var pos-vars neg-vars)
  (if (null? pos-vars)
      #f
      (let* ([pos-var (car pos-vars)]
             [neg-var (find-var pos-var neg-vars)])
        (if (equal? neg-var #f)
            (choose-var (cdr pos-vars) neg-vars)
            pos-var))))

(define (rc-trivial? rc)
  (let* ([rc-pos (res-clause-pos rc)]
         [rc-neg (res-clause-neg rc)]
         [var (choose-var rc-pos rc-neg)])
    (if (equal? var #f)
        #f
        #t)))

(define (rc-resolve rc1 rc2)
  (let* ([pos-vars-rc1 (res-clause-pos rc1)]
         [neg-vars-rc1 (res-clause-neg rc1)]
         [pos-vars-rc2 (res-clause-pos rc2)]
         [neg-vars-rc2 (res-clause-neg rc2)]
         ;;szukam vara dla którego mogę zrobić rezolucje
         [res1 (choose-var pos-vars-rc1 neg-vars-rc2)]
         [res2 (choose-var pos-vars-rc2 neg-vars-rc1)])
    (cond ((not (equal? res1 #f))
           ;;rezolucja i budowanie res-clause
           (let* ([proof-rc1 (res-clause-proof rc1)]
                  [proof-rc2 (res-clause-proof rc2)]
                  [ready-pos-vars-rc1 (filter (λ(x) (not (equal? res1 x))) pos-vars-rc1)]
                  [ready-neg-vars-rc2 (filter (λ(x) (not (equal? res1 x))) neg-vars-rc2)]
                  [new-pos-vars (merge-sort (remove-duplicates (append ready-pos-vars-rc1 pos-vars-rc2)))]
                  [new-neg-vars (merge-sort (remove-duplicates (append neg-vars-rc1 ready-neg-vars-rc2)))]
                  [new-proof (res res1 proof-rc1 proof-rc2)])
             (res-clause new-pos-vars new-neg-vars new-proof)))
          ((not (equal? res2 #f))
           ;;rezolucja i budowanie res-clause
           (let* ([proof-rc1 (res-clause-proof rc1)]
                  [proof-rc2 (res-clause-proof rc2)]
                  [ready-neg-vars-rc1 (filter (λ(x) (not (equal? res2 x))) neg-vars-rc1)]
                  [ready-pos-vars-rc2 (filter (λ(x) (not (equal? res2 x))) pos-vars-rc2)]
                  [new-pos-vars (merge-sort (remove-duplicates (append ready-pos-vars-rc2 pos-vars-rc1)))]
                  [new-neg-vars (merge-sort (remove-duplicates (append neg-vars-rc2 ready-neg-vars-rc1)))]
                  [new-proof (res res2 proof-rc2 proof-rc1)])
             (res-clause new-pos-vars new-neg-vars new-proof)))
          (else #f))))


(define (fixed-point op start)
  (let ((new (op start)))
    (if (eq? new false)
        start
        (fixed-point op new))))

(define (cnf->clause-set f)
  (define (aux cl rc-set)
    (clause-set-add (clause->res-clause cl) rc-set))
  (foldl aux clause-set-empty (cnf-clauses f)))

(define (get-empty-proof rc-set)
  (define (rc-empty? c)
    (and (null? (res-clause-pos c))
         (null? (res-clause-neg c))))
  (let* ((rcs (clause-set-done->clause-list rc-set))
         (empty-or-false (findf rc-empty? rcs)))
    (and empty-or-false
         (res-clause-proof empty-or-false))))

(define (improve rc-set)
  (if (clause-set-done? rc-set)
      false
      (let* ((triple (clause-set-next-pair rc-set))
             (c1     (car  triple))
             (c2     (cadr triple))
             (rc-set (cddr triple))
             (c-or-f (rc-resolve c1 c2)))
        (if (and c-or-f (not (rc-trivial? c-or-f)))
            (clause-set-add c-or-f rc-set)
            rc-set))))

(define (prove cnf-form)
  (let* ((clauses (cnf->clause-set cnf-form))
         (sat-clauses (fixed-point improve clauses))
         (pf-or-false (get-empty-proof sat-clauses)))
    (if (eq? pf-or-false false)
        'sat
        (list 'unsat pf-or-false))))

;; XXX: Zestaw testów do zadania drugiego



(define prove-tests
  (test-suite "prove-tests"
              ;;Testuje za pomocą zadania 1

              ;; Test z pdf z zadania 1
              (test-case "prove-test-1"
                         (let* ([C1 (clause (lit #f 'p) (lit #t 'q))]
                                [C2 (clause (lit #t 'p) (lit #t 'q))]
                                [C3 (clause (lit #f 'q) (lit #t 'r))]
                                [C4 (clause (lit #f 'q) (lit #f 'r))]
                                [prop-cnf (cnf C1 C2 C3 C4)])
                           (check-equal? (check-proof? (cadr (prove prop-cnf)) prop-cnf)  #t)))

              ;; Zadanie 125 Whitebook (ma rozwiązanie)
              (test-case "prove-test-2"
                         (let* ([C1 (clause (lit #f 'p)(lit #t 'q))]
                                [C2 (clause (lit #f 'p)(lit #f 'r)(lit #t 's))]
                                [C3 (clause (lit #f 'q)(lit #t 'r))]
                                [C4 (clause (lit #t 'p))]
                                [C5 (clause (lit #f 's))]
                                [prop-cnf (cnf C1 C2 C3 C4 C5)])
                           (check-equal? (check-proof? (cadr (prove prop-cnf)) prop-cnf)  #t)))

              ;; Zadanie 126 Whitebook (ma rozwiązanie)
              (test-case "prove-test-3"
                         (let* ([C1 (clause (lit #t 'p) (lit #t 'r))]
                                [C2 (clause (lit #f 'r) (lit #f 's))]
                                [C3 (clause (lit #t 'q) (lit #t 's))]
                                [C4 (clause (lit #t 'q) (lit #t 'r))]
                                [C5 (clause (lit #f 'p) (lit #f 'q))]
                                [C6 (clause (lit #t 's) (lit #t 'p))]
                                [prop-cnf (cnf C1 C2 C3 C4 C5 C6)])
                           (check-equal? (check-proof? (cadr (prove prop-cnf)) prop-cnf)  #t)))
              ;; Przykład który nie ma rozwiązania
              (test-case "prove-test-3"
                         (let* ([C1 (clause (lit #t 'p) (lit #t 'r))]
                                [prop-cnf (cnf C1)])
                           (check-equal? (prove prop-cnf) 'sat)))))


(define rc-trivial?-tests
  (test-suite "rc-trivial?-tests"

              ;;Nietrywialna klauzula
              (test-case "prove-test-1"
                         (let* ([C1 (clause (lit #t 'p) (lit #t 'q))]
                                [C1-new (clause->res-clause C1)])
                           (check-equal? (rc-trivial? C1-new) #f)))

              ;;Trywialna klauzula
              (test-case "prove-test-2"
                         (let* ([C1 (clause (lit #t 'p) (lit #f 'p))]
                                [C1-new (clause->res-clause C1)])
                           (check-equal? (rc-trivial? C1-new) #t)))

              ;;Pusta klauzula
              (test-case "prove-test-3"
                         (let* ([C1 (clause)]
                                [C1-new (clause->res-clause C1)])
                           (check-equal? (rc-trivial? C1-new) #f)))))

(define rc-resolve-tests
  (test-suite "rc-resolve-tests"

              (test-case "rc-resolve-test-1"
                         (let* ([C1 (clause (lit #t 'p) (lit #t 'q))]
                                [C2 (clause (lit #f 'p) (lit #t 'q))]
                                [C1-new (clause->res-clause C1)]
                                [C2-new (clause->res-clause C2)])
                           (check-equal? (res-clause? (rc-resolve C1-new C2-new)) #t)))

              (test-case "rc-resolve-test-2"
                         (let* ([C1 (clause (lit #f 'p) (lit #f 'q))]
                                [C2 (clause (lit #t 's) (lit #t 'p))]
                                [C1-new (clause->res-clause C1)]
                                [C2-new (clause->res-clause C2)])
                           (check-equal? (res-clause? (rc-resolve C1-new C2-new)) #t)))))

;;Testy Procedur Pomocniczych
(define choose-var-and-find-var-tests
  (test-suite " choose-var-and-find-var-tests"

              (test-case "choose-var-test1"
                         (let* ([pos-vars (list 'p 'r 'q)]
                                [neg-vars (list 's 'z 'q)])
                           (check-equal? (choose-var pos-vars neg-vars) 'q)))

              (test-case "choose-var-test1"
                         (let* ([pos-vars (list 'p 'r 't)]
                                [neg-vars (list 's 'z 'q)])
                           (check-equal? (choose-var pos-vars neg-vars) #f)))

              (test-case "find-var-test1"
                         (let* ([var 'q]
                                [vars (list 's 'z 'q)])
                           (check-equal? (find-var var vars) 'q)))

              (test-case "find-var-test1"
                         (let* ([var 't]
                                [vars (list 's 'z 'q)])
                           (check-equal? (find-var var vars) #f)))))

(run-tests prove-tests)
(run-tests rc-trivial?-tests)
(run-tests rc-resolve-tests)
(run-tests choose-var-and-find-var-tests)