saddsa

#lang racket

(define (var? t)
  (symbol? t))

(define (neg? t)
  (and (list? t)
       (= 2 (length t))
       (eq? 'neg (car t))))

(define (lit? t)
  (and (list? t)
       (= 3 (length t))
       (eq? `lit (car t))))

(define (lit t)
  (list `lit #f #t))

(define (conj? t)
  (and (list? t)
       (= 3 (length t))
       (eq? 'conj (car t))))

(define (disj? t)
  (and (list? t)
       (= 3 (length t))
       (eq? '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-subf f)
  (second f))

(define (disj-left f)
  (second f))

(define (disj-rght f)
  (third f))

(define (conj-left f)
  (second f))

(define (lit-neg? f)
  (second f))

(define (lit-var f)
  (third f))

(define (conj-rght f)
  (third f))

(define (neg f)
  (list 'neg f))

(define (conj l r)
  (list 'conj l r))

(define (disj l r)
  (list 'disj l r))

(define (free-vars f)
  (define (find-list el xs)
    (if (null? xs)
        #false
        (if (eq? (car xs) el)
            #true
            (find-list el (cdr xs)))))
  (define (polacz xs ys)
    (if (null? ys)
        xs
        (if (find-list (car ys) xs)
            (polacz xs (cdr ys))
            (polacz (cons (car ys) xs) (cdr ys)))))
  (define (find-free f)
    (cond [(neg? f) (find-free (neg-subf f))]
          [(lit? f) (lit-var f)]
          [(disj? f)
                (polacz (find-free (disj-left f)) (find-free (disj-rght f)))]
          [(conj? f)
                (polacz (find-free (conj-left f)) (find-free (conj-rght f)))]
          [else (list f)]))
 (find-free f))

(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 (eval-formula f ev)
  (define (find-list el xs)
    (if (null? xs)
        0
        (if (eq? (caar xs) el)
            (second (car xs))
            (find-list el (cdr xs)))))
  (define (evaluate f)
    (cond [(var? f) (let ((res (find-list f ev)))
                         (if (number? res)
                             (error "NIE MA")
                             res))]
          [(neg? f) (if (lit? (neg-subf f))
                        (xor (lit-neg? (neg-subf f)
                             (lit-var (neg-subf))))
                        (not (evaluate (neg-subf f))))]
          [(disj? f) (or
                        (evaluate (disj-left f))
                        (evaluate (disj-rght f)))]
          [(conj? f) (and
                        (evaluate (conj-left f))
                        (evaluate (conj-rght f)))]))
  (evaluate f))

(define (falsifable-eval? f)
  (define (iter vals)
      (if (null? vals)
          false
          (if (eval-formula f (car vals))
              (iter (cdr vals))
              (car vals))))
  (iter (gen-vals (free-vars f))))

;;(free-vars (neg (disj (conj `a `b) `c)))
;;(gen-vals (free-vars (neg (disj (conj `a `b) `c))))
;;(eval-formula (neg (disj (conj `a `b) `c)) `((c #f) (b #f) (a #t)))
;;(falsifable-eval? (neg (disj (conj `a `b) `c)))
;;(falsifable-eval? (conj `p (neg `p)))
;;(falsifable-eval? (disj `p (neg `p)))

(define (nnf? f)
  (cond [(lit? f) #true]
        [(neg? f) (if (lit? (neg-subf f))
                      #true
                      #false)]
        [(disj? f) (and
                      (nnf? (disj-left f))
                      (nnf? (disj-rght f)))]
        [(conj? f) (and
                      (nnf? (conj-left f))
                      (nnf? (conj-rght f)))]))

;;(nnf? (disj (conj (lit `a) (lit `b)) (lit `c)))

(free-vars (neg (disj (conj (list `lit #t `a) `b) `c)))
;;(falsifable-eval? (neg (disj (conj (list `lit #t `a) `b) `c)))


(define (convert-to-cnf f)
  ())