#lang racket

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

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

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

(define (disj? t)
  (and (list? t)
       (= (length t) 3)
       (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-right f)))
      (and (conj? f)
           (prop? (conj-left f))
           (prop? (conj-right f)))))

(define (neg p)
  (list 'neg p))

(define (conj p q)
  (list 'conj p q))

(define (disj p q)
  (list 'disj p q))

(define (neg-subf f)
  (cadr f))

(define (disj-left f)
  (cadr f))

(define (disj-right f)
  (caddr f))

(define (conj-left f)
  (cadr f))

(define (conj-right f)
  (caddr f))

(define (free-vars f)
  (define (fv f t)
    (cond [(neg? f) (fv (neg-subf f) t)]
          [(disj? f) (fv (disj-right f) (fv (disj-left f) t))]
          [(conj? f) (fv (conj-right f) (fv (conj-left f) t))]
          [else (remove-duplicates(append t (list f)))]))
  (fv f null))

; (free-vars (neg (disj 'a (conj 'a (neg (conj 'b (disj 9 11)))))))



( 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 xs vals)
  (define (val? x v)
    (if (null? v)
        (error "błąd")
        (if (eq? (caar v) x)
            (cadar v)
            (val? x (cdr v)))))
  (cond
         ((var? xs) (val? xs vals))
         ((neg? xs) (not (eval-formula (neg-subf xs) vals)))
         ((disj? xs) (or (eval-formula (disj-left xs) vals)(eval-formula(disj-right xs) vals)))
         ((conj? xs) (and (eval-formula(conj-left xs) vals (eval-formula(conj-right xs) vals))))))