MP5

#lang racket
(define (var? t)
  (symbol? t))
(define (neg? t)
  (and (list? t)
       (= 2 (length t))
       (eq? (quote neg) (car t))))
(define (conj? t)
  (and (list? t)
       (= 3 (length t))
       (eq? (quote conj) (car t))))
(define (disj? t)
  (and (list? t)
       (= 3 (length t))
       (eq? (quote disj) (car t))))

(define (prop? f)
  (or (var? f)
      (and (neg? f)
           (prop? (neg-subf f)))
      (and (disj? f)
           (prop? (disj-left f))
           (prop? (disj-rght f)))
      (and (conj? f)
           (prop? (conj-left f))
           (prop? (conj-rght f)))))

(define (neg t)
  (list (quote neg) t))
(define neg-subf second)

(define (disj p q)
  (list (quote disj) p q))
(define disj-left cadr)
(define disj-rght caddr)

(define (conj p q)
  (list (quote conj) p q))
(define conj-left cadr)
(define conj-rght caddr)

(define (free-vars fs)
  (define (iter f fs)
    (cond [(neg? f)  (iter (neg-subf f)   fs)]
          [(disj? f) (iter (disj-left f) (iter (disj-rght f) fs))]
          [(conj? f) (iter (conj-left f) (iter (conj-rght f) fs))]
          [(var? f)  (append (list f) fs) ]))
  (remove-duplicates (iter fs null)))

( define ( gen-vals xs )
   (if ( null? xs )
       ( list null )
       ( let*
            ((vss (gen-vals (cdr xs)))
             (x (car xs))
             (vst (map (lambda (vs) (cons (list x true) vs)) vss))
             (vsf (map (lambda (vs) (cons (list x false) vs)) vss)))
          (append vst vsf))))

(define (check x vs)
  (cond [(null? vs) (error "Nie ma wartościowania dla podanej zmiennej")]
        [(eq? x (caar vs)) (cadar vs)]
        [else (check x (cdr vs))]))

(define (eval-formula f vs)
  (cond [(neg? f)  (not (eval-formula (neg-subf f) vs))]
        [(disj? f) (or  (eval-formula (disj-left f) vs) (eval-formula (disj-rght f) vs))]
        [(conj? f) (and (eval-formula (conj-left f) vs) (eval-formula (conj-rght f) vs))]
        [(var? f)  (check f vs)]))

(define (falsifiable-eval? f)
  (define (helper vs)
    (cond ((null? vs) false)
          ((eval-formula f (car vs)) (helper (cdr vs)))
          (else (car vs))))
  (helper (gen-vals (free-vars f))))

;; literał
(define (lit var bool)
  (list 'lit var bool))
(define lit-bool third)
(define lit-var second)
(define (lit? l)
  (and (= 3 (length l))
       (eq? (first l) 'lit)
       (var? (second l))
       (boolean? (third l))))

(define (nnf-lit? f)
  (cond [(disj? f) (and (nnf-lit? (disj-left f))
                        (nnf-lit? (disj-rght f)))]
        [(conj? f) (and (nnf-lit? (conj-left f))
                        (nnf-lit? (conj-rght f)))]
        [else (lit? f)]))

(define (eval-formula-lit f vs)
  (cond [(disj? f) (or  (eval-formula-lit (disj-left f) vs) (eval-formula-lit (disj-rght f) vs))]
        [(conj? f) (and (eval-formula-lit (conj-left f) vs) (eval-formula-lit (conj-rght f) vs))]
        [(lit? f)  (eq? (lit-bool f) (check (lit-var f) vs))]))

(define (free-vars-lit f)
  (define (iter f fs)
    (cond [(disj? f) (iter (disj-left f) (iter (disj-rght f) fs))]
          [(conj? f) (iter (conj-left f) (iter (conj-rght f) fs))]
          [(lit? f)  (append (list (lit-var f)) fs)]))
  (remove-duplicates (iter f null)))

(define (falsifiable-eval-lit? f)
  (define (helper vs)
    (cond ((null? vs) false)
          ((eval-formula-lit f (car vs)) (helper (cdr vs)))
          (else (car vs))))
  (helper (gen-vals (free-vars-lit f))))

(define (nnf? f)
  (cond [(neg? f) (var? (neg-subf f))]
        [(disj? f) (and (nnf? (disj-left f))
                        (nnf? (disj-rght f)))]
        [(conj? f) (and (nnf? (conj-left f))
                        (nnf? (conj-rght f)))]
        [else (var? f)]))


(define (neg-nnf f)
  (cond [(var? f)  (lit f false)]
        [(neg? f)  (convert-to-nnf (neg-subf f))]
        [(disj? f) (conj (neg-nnf (disj-left f))
                         (neg-nnf (disj-rght f)))]
        [(conj? f) (disj (neg-nnf (conj-left f))
                         (neg-nnf (conj-rght f)))]))

(define (convert-to-nnf f)
  (cond [(var? f)  (lit f true)]
        [(neg? f)  (neg-nnf (neg-subf f))]
        [(disj? f) (disj (convert-to-nnf (disj-left f))
                         (convert-to-nnf (disj-rght f)))]
        [(conj? f) (conj (convert-to-nnf (conj-left f))
                         (convert-to-nnf (conj-rght f)))]))