diff options
Diffstat (limited to 'Semestr 2/racket/lista5')
21 files changed, 0 insertions, 1104 deletions
diff --git a/Semestr 2/racket/lista5/compiled/drracket/errortrace/prop_rkt.dep b/Semestr 2/racket/lista5/compiled/drracket/errortrace/prop_rkt.dep deleted file mode 100644 index 6e0cfbb..0000000 --- a/Semestr 2/racket/lista5/compiled/drracket/errortrace/prop_rkt.dep +++ /dev/null @@ -1 +0,0 @@ -("7.6" racket ("f0a57e86828cdab35eaad454d5deb80353172518" . "8314027ed4c1c6fd9c412af77103e94790e59dd2") (collects #"errortrace" #"errortrace-key.rkt") (collects #"racket" #"main.rkt") (collects #"racket" #"runtime-config.rkt")) diff --git a/Semestr 2/racket/lista5/compiled/drracket/errortrace/prop_rkt.zo b/Semestr 2/racket/lista5/compiled/drracket/errortrace/prop_rkt.zo Binary files differdeleted file mode 100644 index 748fec9..0000000 --- a/Semestr 2/racket/lista5/compiled/drracket/errortrace/prop_rkt.zo +++ /dev/null diff --git a/Semestr 2/racket/lista5/compiled/drracket/errortrace/props_rkt.dep b/Semestr 2/racket/lista5/compiled/drracket/errortrace/props_rkt.dep deleted file mode 100644 index 0926afc..0000000 --- a/Semestr 2/racket/lista5/compiled/drracket/errortrace/props_rkt.dep +++ /dev/null @@ -1 +0,0 @@ -("7.6" racket ("e0347fa7e89f59bc97c197db02b440f666222428" . "8314027ed4c1c6fd9c412af77103e94790e59dd2") (collects #"errortrace" #"errortrace-key.rkt") (collects #"racket" #"main.rkt") (collects #"racket" #"runtime-config.rkt")) diff --git a/Semestr 2/racket/lista5/compiled/drracket/errortrace/props_rkt.zo b/Semestr 2/racket/lista5/compiled/drracket/errortrace/props_rkt.zo Binary files differdeleted file mode 100644 index eccc7f7..0000000 --- a/Semestr 2/racket/lista5/compiled/drracket/errortrace/props_rkt.zo +++ /dev/null diff --git a/Semestr 2/racket/lista5/compiled/drracket/errortrace/solution_rkt.dep b/Semestr 2/racket/lista5/compiled/drracket/errortrace/solution_rkt.dep deleted file mode 100644 index 9810b4c..0000000 --- a/Semestr 2/racket/lista5/compiled/drracket/errortrace/solution_rkt.dep +++ /dev/null @@ -1 +0,0 @@ -("7.6" racket ("ae3a6974cdd4582f480927d9968aad2f495b7fc4" . "33b0c09c14dce6a2115d810ac3d0f25a9dce3205") #"C:\\Users\\franc\\Documents\\lista5\\props.rkt" (collects #"errortrace" #"errortrace-key.rkt") (collects #"racket" #"main.rkt") (collects #"racket" #"runtime-config.rkt")) diff --git a/Semestr 2/racket/lista5/compiled/drracket/errortrace/solution_rkt.zo b/Semestr 2/racket/lista5/compiled/drracket/errortrace/solution_rkt.zo Binary files differdeleted file mode 100644 index ca1ab20..0000000 --- a/Semestr 2/racket/lista5/compiled/drracket/errortrace/solution_rkt.zo +++ /dev/null diff --git a/Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.dep b/Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.dep deleted file mode 100644 index 0926afc..0000000 --- a/Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.dep +++ /dev/null @@ -1 +0,0 @@ -("7.6" racket ("e0347fa7e89f59bc97c197db02b440f666222428" . "8314027ed4c1c6fd9c412af77103e94790e59dd2") (collects #"errortrace" #"errortrace-key.rkt") (collects #"racket" #"main.rkt") (collects #"racket" #"runtime-config.rkt")) diff --git a/Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.zo b/Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.zo Binary files differdeleted file mode 100644 index eccc7f7..0000000 --- a/Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.zo +++ /dev/null diff --git a/Semestr 2/racket/lista5/julita/props.rkt b/Semestr 2/racket/lista5/julita/props.rkt deleted file mode 100644 index 204b108..0000000 --- a/Semestr 2/racket/lista5/julita/props.rkt +++ /dev/null @@ -1,52 +0,0 @@ -#lang racket - -(provide conj conj-left conj-right conj? - disj disj-left disj-right disj? - neg neg-subf neg? - var?) - - -(define (conj p q) - (list 'conj p q)) - -(define (conj-left f) - (second f)) - -(define (conj-right f) - (third f)) - -(define (conj? t) - (and (list? t) - (= 3 (length t)) - (eq? 'conj (car t)))) - - -(define (disj p q) - (list 'disj p q)) - -(define (disj-left f) - (second f)) - -(define (disj-right f) - (third f)) - -(define (disj? t) - (and (list? t) - (= 3 (length t)) - (eq? 'disj (car t)))) - - -(define (neg x) - (list 'neg x)) - -(define (neg-subf x) - (second x)) - -(define (neg? t) - (and (list? t) - (= 2 (length t)) - (eq? 'neg (car t)))) - - -(define (var? t) - (symbol? t)) diff --git a/Semestr 2/racket/lista5/julita/solution.bak b/Semestr 2/racket/lista5/julita/solution.bak deleted file mode 100644 index b3dda94..0000000 --- a/Semestr 2/racket/lista5/julita/solution.bak +++ /dev/null @@ -1,164 +0,0 @@ -#lang racket - -;;Praca grupowa: -;;Dawid Holewa -;;Julita Osman -;;Aleksandra Stępniewska - -(require "props.rkt") -(provide falsifiable-cnf?) - -;Ponieważ formuła w cnf to konjunkcja klauzul -;a klauzula to alternatywa literałów -;to formuła w tej postaci jest tautologią -;wtedy i tylko wtedy gdy -;wszystkie klauzule w niej występujace sa zawsze prawdziwe (też są tautologiami) -;w przeciwnym razie, formulę taką da się zanegować; -;zatem nasz pomysł polega na tym, aby -;1)sprawdzic czy formula jest tautologia -;2)jesli tak to zwracamy fałsz -;3)wpp. pierwsza z klauzul, która nie jest tautologia -;(zatem jest mozliwa do zanegowania i jednocześnie neguje cała formułe w cnf) -;"przesuwamy" na początek listy reprezentującej cnf - -;dodatkowo to czy klauzula jest tautologią nie musimy sprawdzać wykonując wartościowanie -;możemy skorzystać z własności alternatywy -;klauzula bedzię zawsze pawdziwa tylko jeśli conajmniej jedna ze zmiennych występuje jednoczesnie ze swoją negacją - -;Falsifiable, która sprawdza każde wartościowania -;sprawdza 2^(ilosc zmiennych w całym wyrażeniu) wartosciowań, -;podczas gdy -;falsifiable, która opiera się na strukturze cnf -;przechodzi po cnf, aż do napotkania pierwszej -;mozliwej do zanegowania klauzuli -;zatem w najroszym przypadku przejdziemy po całym cnf -;ale zawsze wartosciowania negujacego formule szukamy tylko dla jedenej klauzuli -;zauważmy,ze jeśli formuła jest tautologią to oszczędzamy bardzo dużo czasu nie rozpartując wszystkich wartosciowań, tylko wypisujac odrazu falsz - -;Ta druga jest więc efektywniejsza - -(define (lit? f);; a lub ~a - (or (var? f) ;;a - (and (neg? f);;~a - (var? (neg-subf f))))) - -(define (lit-pos v) - v) - -(define (lit-neg v) - (neg v)) - -(define (lit-var l) ;;a-->a ~a-->a - (if (var? l) - l - (neg-subf l))) - -(define (lit-pos? l) - (var? l)) - -(define (to-nnf f) - (cond - [(var? f) (lit-pos f)] - [(neg? f) (to-nnf-neg (neg-subf f))] - [(conj? f) (conj (to-nnf (conj-left f)) - (to-nnf (conj-right f)))] - [(disj? f) (disj (to-nnf (disj-left f)) - (to-nnf (disj-right f)))])) - -(define (to-nnf-neg f) - (cond - [(var? f) (lit-neg f)] - [(neg? f) (to-nnf (neg-subf f))] - [(conj? f) (disj (to-nnf-neg (conj-left f)) - (to-nnf-neg (conj-right f)))] - [(disj? f) (conj (to-nnf-neg (disj-left f)) - (to-nnf-neg (disj-right f)))])) - -(define (mk-cnf xss) - (cons 'cnf xss)) - -(define (clause? f) - (and (list? f) - (andmap lit? f))) - -(define (cnf? f) - (and (pair? f) - (eq? 'cnf (car f)) - (list? (cdr f)) - (andmap clause? (cdr f)))) - -(define (to-cnf f) - (define (join xss yss) - (apply append (map (lambda (xs) (map (lambda (ys) (append xs ys)) yss)) xss))) - - (define (go f) - (cond - [(lit? f) (list (list f))] - [(conj? f) (append (go (conj-left f)) - (go (conj-right f)))] - [(disj? f) (join (go (disj-left f)) - (go (disj-right f)))])) - (mk-cnf (go f))) - - -(define (contain-both-literals? claus) - (define (aux to-check) - (cond [(empty? to-check) #f] - [(neg? (car to-check)) - (if (memq (neg-subf (car to-check)) claus) - #t - (aux (cdr to-check)))] - [else (aux (cdr to-check))])) - (aux claus)) - - -;; sprawdza czy ktorakolwiek z klauzul z listy reprezentujacej cnf -;; zawiera chociaz jedną parę zmiennej i jej negacji -;; zwraca liste pusta jesli cnf jest tautologia -;; zwraca liste z pierwsza klauzule nie bedaca tautologia "przesunieta" na poczatek (possible-to-neg) -(define (has-both big-set) - (define (possible-to-neg big-set x) ;;przesuwa x-ty element listy big-set na poczatek - (define x-ty (list-ref big-set x)) - (append (list x-ty) (remove x-ty big-set))) - (define (aux iter big-set) - (if (= iter (length big-set)) - '() - (if (contain-both-literals? (list-ref big-set iter)) ;;sprawdzamy czy iter klauzula cnf ma wystapienie a i ~a jednoczesnie - (aux (+ iter 1) big-set) - (possible-to-neg big-set iter)))) - (aux 0 (cdr big-set))) ;;(cdr big-set) bo to cnf czyli pierwszy element listy to edykieta 'cnf - - -(define (falsifiable-cnf? t) - (define tt (to-cnf (to-nnf t))) - (define f (has-both tt)) - (if (empty? f) - #f - (find-valuation f))) - - -(define (valuate f sigma) - (define (insigma-proc lista result) - (cond [(null? lista) result] - [(insigma-proc (cdr lista) (append result (list (lit-var(caar lista)))))])) - ;; insigma ---> lista zmiennych z wartosciowania pierwszej klauzuli: - (define insigma (insigma-proc sigma '())) - (define (aux insigma otherclause sigma) - (cond [(null? otherclause) sigma] - [(if (memq (lit-var (car otherclause)) insigma) - (aux insigma (cdr otherclause) sigma) - (if(neg? (car otherclause)) - (aux (append insigma (list(car otherclause))) - (cdr otherclause) - (append sigma (list(list (lit-var(car otherclause)) 1)))) - (aux (append insigma (list(car otherclause))) - (cdr otherclause) - (append sigma (list(list (car otherclause) 0))))))])) - (if (empty? f) - sigma - (valuate (cdr f) - (aux insigma (car f) sigma)))) - -(define (find-valuation f) - (valuate f '())) - diff --git a/Semestr 2/racket/lista5/julita/solution.rkt b/Semestr 2/racket/lista5/julita/solution.rkt deleted file mode 100644 index da87bf9..0000000 --- a/Semestr 2/racket/lista5/julita/solution.rkt +++ /dev/null @@ -1,164 +0,0 @@ -#lang racket - -;;Praca grupowa: -;;Dawid Holewa -;;Julita Osman -;;Aleksandra Stępniewska - -(require "props.rkt") -(provide falsifiable-cnf?) - -;Ponieważ formuła w cnf to konjunkcja klauzul -;a klauzula to alternatywa literałów -;to formuła w tej postaci jest tautologią -;wtedy i tylko wtedy gdy -;wszystkie klauzule w niej występujace sa zawsze prawdziwe (też są tautologiami) -;w przeciwnym razie, formulę taką da się zanegować; -;zatem nasz pomysł polega na tym, aby -;1)sprawdzic czy formula jest tautologia -;2)jesli tak to zwracamy fałsz -;3)wpp. pierwsza z klauzul, która nie jest tautologia -;(zatem jest mozliwa do zanegowania i jednocześnie neguje cała formułe w cnf) -;"przesuwamy" na początek listy reprezentującej cnf - -;dodatkowo to czy klauzula jest tautologią nie musimy sprawdzać wykonując wartościowanie -;możemy skorzystać z własności alternatywy -;klauzula bedzię zawsze pawdziwa tylko jeśli conajmniej jedna ze zmiennych występuje jednoczesnie ze swoją negacją - -;Falsifiable, która sprawdza każde wartościowania -;sprawdza 2^(ilosc zmiennych w całym wyrażeniu) wartosciowań, -;podczas gdy -;falsifiable, która opiera się na strukturze cnf -;przechodzi po cnf, aż do napotkania pierwszej -;mozliwej do zanegowania klauzuli -;zatem w najroszym przypadku przejdziemy po całym cnf -;ale zawsze wartosciowania negujacego formule szukamy tylko dla jedenej klauzuli -;zauważmy,ze jeśli formuła jest tautologią to oszczędzamy bardzo dużo czasu nie rozpartując wszystkich wartosciowań, tylko wypisujac odrazu falsz - -;Ta druga jest więc efektywniejsza - -(define (lit? f);; a lub ~a - (or (var? f) ;;a - (and (neg? f);;~a - (var? (neg-subf f))))) - -(define (lit-pos v) - v) - -(define (lit-neg v) - (neg v)) - -(define (lit-var l) ;;a-->a ~a-->a - (if (var? l) - l - (neg-subf l))) - -(define (lit-pos? l) - (var? l)) - -(define (to-nnf f) - (cond - [(var? f) (lit-pos f)] - [(neg? f) (to-nnf-neg (neg-subf f))] - [(conj? f) (conj (to-nnf (conj-left f)) - (to-nnf (conj-right f)))] - [(disj? f) (disj (to-nnf (disj-left f)) - (to-nnf (disj-right f)))])) - -(define (to-nnf-neg f) - (cond - [(var? f) (lit-neg f)] - [(neg? f) (to-nnf (neg-subf f))] - [(conj? f) (disj (to-nnf-neg (conj-left f)) - (to-nnf-neg (conj-right f)))] - [(disj? f) (conj (to-nnf-neg (disj-left f)) - (to-nnf-neg (disj-right f)))])) - -(define (mk-cnf xss) - (cons 'cnf xss)) - -(define (clause? f) - (and (list? f) - (andmap lit? f))) - -(define (cnf? f) - (and (pair? f) - (eq? 'cnf (car f)) - (list? (cdr f)) - (andmap clause? (cdr f)))) - -(define (to-cnf f) - (define (join xss yss) - (apply append (map (lambda (xs) (map (lambda (ys) (append xs ys)) yss)) xss))) - - (define (go f) - (cond - [(lit? f) (list (list f))] - [(conj? f) (append (go (conj-left f)) - (go (conj-right f)))] - [(disj? f) (join (go (disj-left f)) - (go (disj-right f)))])) - (mk-cnf (go f))) - - -(define (contain-both-literals? claus) - (define (aux to-check) - (cond [(empty? to-check) #f] - [(neg? (car to-check)) - (if (memq (neg-subf (car to-check)) claus) - #t - (aux (cdr to-check)))] - [else (aux (cdr to-check))])) - (aux claus)) - - -;; sprawdza czy ktorakolwiek z klauzul z listy reprezentujacej cnf -;; zawiera chociaz jedną parę zmiennej i jej negacji -;; zwraca liste pusta jesli cnf jest tautologia -;; zwraca liste z pierwsza klauzule nie bedaca tautologia "przesunieta" na poczatek (possible-to-neg) -(define (has-both big-set) - (define (possible-to-neg big-set x) ;;przesuwa x-ty element listy big-set na poczatek - (define x-ty (list-ref big-set x)) - (append (list x-ty) (remove x-ty big-set))) - (define (aux iter big-set) - (if (= iter (length big-set)) - '() - (if (contain-both-literals? (list-ref big-set iter)) ;;sprawdzamy czy iter klauzula cnf ma wystapienie a i ~a jednoczesnie - (aux (+ iter 1) big-set) - (possible-to-neg big-set iter)))) - (aux 0 (cdr big-set))) ;;(cdr big-set) bo to cnf czyli pierwszy element listy to edykieta 'cnf - - -(define (falsifiable-cnf? t) - (define tt (to-cnf (to-nnf t))) - (define f (has-both tt)) - (if (empty? f) - #f - (find-valuation f))) - - -(define (valuate f sigma) - (define (insigma-proc lista result) - (cond [(null? lista) result] - [(insigma-proc (cdr lista) (append result (list (lit-var(caar lista)))))])) - ;; insigma ---> lista zmiennych z wartosciowania pierwszej klauzuli: - (define insigma (insigma-proc sigma '())) - (define (aux insigma otherclause sigma) - (cond [(null? otherclause) sigma] - [(if (memq (lit-var (car otherclause)) insigma) - (aux insigma (cdr otherclause) sigma) - (if(neg? (car otherclause)) - (aux (append insigma (list(car otherclause))) - (cdr otherclause) - (append sigma (list(list (lit-var(car otherclause)) true)))) - (aux (append insigma (list(car otherclause))) - (cdr otherclause) - (append sigma (list(list (car otherclause) false))))))])) - (if (empty? f) - sigma - (valuate (cdr f) - (aux insigma (car f) sigma)))) - -(define (find-valuation f) - (valuate f '())) - diff --git a/Semestr 2/racket/lista5/prop.rkt b/Semestr 2/racket/lista5/prop.rkt deleted file mode 100644 index 6f1f7b4..0000000 --- a/Semestr 2/racket/lista5/prop.rkt +++ /dev/null @@ -1 +0,0 @@ -#lang racket diff --git a/Semestr 2/racket/lista5/props.bak b/Semestr 2/racket/lista5/props.bak deleted file mode 100644 index 1a5659a..0000000 --- a/Semestr 2/racket/lista5/props.bak +++ /dev/null @@ -1,71 +0,0 @@ -#lang racket - -(provide var? - neg? - conj? - disj? - conj - disj - neg - conj-left - conj-right - disj-right - disj-left - neg-subf) -; (require "solution.rkt") - -(define (var? t) (symbol? t)) - -(define (neg? t) - (and (list? t) - (= 2 (length t)) - (eq? 'neg (car 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 (lit? t) - (or (var? t) - (and (neg? t) - (var? (neg-subf t))))) - -(define (conj left right) - (list 'conj left right)) - -(define (disj left right) - (list 'disj left right)) - -(define (neg f) - (list 'neg f)) - -(define (conj-left f) - (if (conj? f) - (cadr f) - (error "Złe dane ze znacznikiem -- CONJ-LEFT" f))) - -(define (conj-right f) - (if (conj? f) - (caddr f) - (error "Złe dane ze znacznikiem -- CONJ-RIGHT" f))) - -(define (disj-left f) - (if (disj? f) - (cadr f) - (error "Złe dane ze znacznikiem -- DISJ-LEFT" f))) - -(define (disj-right f) - (if (disj? f) - (caddr f) - (error "Złe dane ze znacznikiem -- DISJ-RIGHT" f))) - -(define (neg-subf f) - (if (neg? f) - (cadr f) - (error "Złe dane ze znacznikiem -- NEG-FORM" f))) diff --git a/Semestr 2/racket/lista5/props.rkt b/Semestr 2/racket/lista5/props.rkt deleted file mode 100644 index 204b108..0000000 --- a/Semestr 2/racket/lista5/props.rkt +++ /dev/null @@ -1,52 +0,0 @@ -#lang racket - -(provide conj conj-left conj-right conj? - disj disj-left disj-right disj? - neg neg-subf neg? - var?) - - -(define (conj p q) - (list 'conj p q)) - -(define (conj-left f) - (second f)) - -(define (conj-right f) - (third f)) - -(define (conj? t) - (and (list? t) - (= 3 (length t)) - (eq? 'conj (car t)))) - - -(define (disj p q) - (list 'disj p q)) - -(define (disj-left f) - (second f)) - -(define (disj-right f) - (third f)) - -(define (disj? t) - (and (list? t) - (= 3 (length t)) - (eq? 'disj (car t)))) - - -(define (neg x) - (list 'neg x)) - -(define (neg-subf x) - (second x)) - -(define (neg? t) - (and (list? t) - (= 2 (length t)) - (eq? 'neg (car t)))) - - -(define (var? t) - (symbol? t)) diff --git a/Semestr 2/racket/lista5/skrr/solution.bak b/Semestr 2/racket/lista5/skrr/solution.bak deleted file mode 100644 index 72c7f36..0000000 --- a/Semestr 2/racket/lista5/skrr/solution.bak +++ /dev/null @@ -1,135 +0,0 @@ -#lang racket - -(provide falsifiable-cnf?) -(require "props.rkt") - -(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 (lit-var f) - (cond [(var? f) f] - [(neg? f) (neg-subf f)] - [else (error "Złe dane ze znacznikiem -- LIT-VAR" f)])) - -(define (free-vars f) - (cond [(null? f) null] - [(var? f) (list f)] - [(neg? f) (free-vars (neg-subf f))] - [(conj? f) (append (free-vars (conj-left f)) - (free-vars (conj-right f)))] - [(disj? f) (append (free-vars (disj-left f)) - (free-vars (disj-right f)))] - [else (error "Zła formula -- FREE-VARS" f)])) - -(define (gen-vals xs) - (if (null? xs) - (list null) - (let* - ((vss (gen-vals (cdr xs))) - (x (car xs)) - (vst (map (λ (vs) (cons (list x true) vs)) vss)) - (vsf (map (λ (vs) (cons (list x false) vs)) vss))) - (append vst vsf)))) - -(define (eval-formula f evaluation) - (cond [(var? f) - (let ((val (assoc f evaluation))) - (if (not val) - (error "Zmienna wolna nie wystepuje w wartościowaniu -- EVAL-FORMULA" f evaluation) - (cadr val)))] - [(neg? f) (not (eval-formula (neg-subf f) evaluation))] - [(disj? f) (or (eval-formula (disj-left f) evaluation) - (eval-formula (disj-right f) evaluation))] - [(conj? f) (and (eval-formula (conj-left f) evaluation) - (eval-formula (conj-right f) evaluation))] - [else (error "Zła formuła -- EVAL-FORMULA" f evaluation)])) - -(define (falsifiable-eval? f) - (let* ((evaluations (gen-vals (free-vars f))) - (results (map (λ (evaluation) (eval-formula f evaluation)) evaluations))) - (ormap false? results))) - -(define (nff? f) - (cond [(lit? f) true] - [(neg? f) false] - [(conj? f) (and (nff? (conj-left f)) - (nff? (conj-right f)))] - [(disj? f) (and (nff? (disj-left f)) - (nff? (disj-right f)))] - [else (error "Zła formuła -- NFF?" f)])) - -(define (convert-to-nnf f) - (cond [(lit? f) f] - [(neg? f) (convert-negation (neg-subf f))] - [(conj? f) (conj (convert-to-nnf (conj-left f)) - (convert-to-nnf (conj-right f)))] - [(disj? f) (disj (convert-to-nnf (disj-left f)) - (convert-to-nnf (disj-right f)))] - [else (error "Zła formuła -- CONVERT" f)])) - -(define (convert-negation f) - (cond [(lit? f) - (if (var? f) - (neg f) - (neg-subf f))] - [(neg? f) (convert-to-nnf (neg-subf f))] - [(conj? f) (disj (convert-negation (conj-left f)) - (convert-negation (conj-right f)))] - [(disj? f) (conj (convert-negation (disj-left f)) - (convert-negation (disj-right f)))] - [else (error "Zła formuła -- CONVERT-NEGATION" f)])) - -(define (clause? x) - (and (list? x) - (andmap lit? x))) - -(define (clause-empty? x) - (and (clause? x) - (null? x))) - -(define (cnf? x) - (and (list? x) - (andmap clause? x))) - -(define (flatmap proc seq) - (foldl append null (map proc seq))) - -(define (convert-to-cnf f) - (define (convert f) - (cond [(lit? f) (list (list f))] - [(conj? f) (append (convert-to-cnf (conj-left f)) - (convert-to-cnf (conj-right f)))] - [(disj? f) - (let ((clause-left (convert-to-cnf (disj-left f))) - (clause-right (convert-to-cnf (disj-right f)))) - (flatmap (λ (clause) - (map (λ (clause2) - (append clause2 clause)) clause-left)) - clause-right))])) - (convert (convert-to-nnf f))) - -(define (falsifiable-clause? clause) - (cond [(clause-empty? clause) true] - [(lit? (findf (λ (l) (equal? - l - (convert-to-nnf (neg (car clause))))) - clause)) false] - [else (falsifiable-clause? (cdr clause))])) - -(define (falsifiable-cnf? f) - (define (neg-value lit) - (if (var? lit) - (list lit false) - (list (neg-subf lit) true))) - (ormap (λ (clause) (if (falsifiable-clause? clause) - (map neg-value clause) - false)) - (convert-to-cnf f)))
\ No newline at end of file diff --git a/Semestr 2/racket/lista5/skrr/solution.rkt b/Semestr 2/racket/lista5/skrr/solution.rkt deleted file mode 100644 index e8efbc9..0000000 --- a/Semestr 2/racket/lista5/skrr/solution.rkt +++ /dev/null @@ -1,88 +0,0 @@ -#lang racket - -(require "props.rkt") -(provide falsifiable-cnf?) - -(define (lit? f) - (or (var? f) - (and (neg? f) - (var? (neg-subf f))))) - -(define (lit-pos v) - v) - -(define (lit-neg v) - (neg v)) - -(define (lit-var l) - (if (var? l) - l - (neg-subf l))) - -(define (lit-pos? l) - (var? l)) - -(define (to-nnf f) - (cond - [(var? f) (lit-pos f)] - [(neg? f) (to-nnf-neg (neg-subf f))] - [(conj? f) (conj (to-nnf (conj-left f)) - (to-nnf (conj-right f)))] - [(disj? f) (disj (to-nnf (disj-left f)) - (to-nnf (disj-right f)))])) - -(define (to-nnf-neg f) - (cond - [(var? f) (lit-neg f)] - [(neg? f) (to-nnf (neg-subf f))] - [(conj? f) (disj (to-nnf-neg (conj-left f)) - (to-nnf-neg (conj-right f)))] - [(disj? f) (conj (to-nnf-neg (disj-left f)) - (to-nnf-neg (disj-right f)))])) - -(define (mk-cnf xss) - (cons 'cnf xss)) - -(define (clause? f) - (and (list? f) - (andmap lit? f))) - -(define (cnf? f) - (and (pair? f) - (eq? 'cnf (car f)) - (list? (cdr f)) - (andmap clause? (cdr f)))) - -(define (to-cnf f) - (define (join xss yss) - (apply append (map (lambda (xs) (map (lambda (ys) (append xs ys)) yss)) xss))) - (define (go f) - (cond - [(lit? f) (list (list f))] - [(conj? f) (append (go (conj-left f)) - (go (conj-right f)))] - [(disj? f) (join (go (disj-left f)) - (go (disj-right f)))])) - (mk-cnf (go f))) - -(define (clause-empty? x) - (and (clause? x) - (null? x))) - -(define (falsifiable-clause? clause) - (cond [(clause-empty? clause) true] - [(lit? (findf (λ (l) (equal? - l - (to-nnf (neg (car clause))))) - clause)) false] - [else (falsifiable-clause? (cdr clause))])) - -(define (falsifiable-cnf? f) - (define (neg-value lit) - (if (var? lit) - (list lit false) - (list (neg-subf lit) true))) - (ormap (λ (clause) (if (falsifiable-clause? clause) - (map neg-value clause) - false)) - (convert-to-cnf f)))
\ No newline at end of file diff --git a/Semestr 2/racket/lista5/sol2.rkt b/Semestr 2/racket/lista5/sol2.rkt deleted file mode 100644 index d037472..0000000 --- a/Semestr 2/racket/lista5/sol2.rkt +++ /dev/null @@ -1,90 +0,0 @@ -#lang racket -(provide falsifiable-cnf?) (require "props.rkt") - - -(define (falsifiable-cnf? p) - ;literał - (define (lit? p) - (or (var? p) - (and (neg? p) (var? (neg-subf p))) - )) - - (define (lit-pos? p) - (if (lit? p) - (var? p) - (error "not a literal" p) - )) - - (define (lit-var p) - (cond - [(not (lit? p)) (error "not a literal" p)] - [(lit-pos? p) p] - [else (neg-subf p)] - )) - - (define (contr p) - (if (lit? p) - (if (neg? p) (neg-subf p) (neg p)) - (error "not a literal" p) - )) - - ;konwertowanie - (define (convert-to-cnf p) - (define (convert-to-nnf p) - (cond - [(lit? p) p] - [(and (neg? p) (conj? (neg-subf p))) - (let ((A (neg-subf p))) - (disj (convert-to-nnf (neg (conj-left A))) (convert-to-nnf (neg (conj-right A)))))] - [(and (neg? p) (disj? (neg-subf p))) - (let ((A (neg-subf p))) - (conj (convert-to-nnf (neg (disj-left A))) (convert-to-nnf (neg (disj-right A)))))] - [(and (neg? p) (neg? (neg-subf p))) (convert-to-nnf (neg-subf (neg-subf p)))] - [(conj? p) (conj (convert-to-nnf (conj-right p)) (convert-to-nnf (conj-left p)))] - [(disj? p) (disj (convert-to-nnf (disj-right p)) (convert-to-nnf (disj-left p)))] - [else (error "not a proposition" p)])) - - (define (flatmap proc seq) - (foldr append null (map proc seq))) - - (define (merge a b) - (flatmap (lambda (c) (map (lambda (c2) (append c c2)) b)) a)) - - (define (convert p) - (cond - [(lit? p) (list (list p))] - [(conj? p) (append (convert (conj-left p)) (convert (conj-right p)))] - [(disj? p) (let* ((L (convert (disj-left p))) (R (convert (disj-right p)))) - (merge L R))] - [else (error "it should never be here" p)] - )) - - (map (lambda (c) (remove-duplicates c)) (convert (convert-to-nnf p)))) - - ;prawdziwa funkcja - (define cnf (convert-to-cnf p)) - - (define (falsifiable-clause? c) - (cond - [(null? c) #t] - [(eq? #f (member (contr (car c)) c)) (falsifiable-clause? (cdr c))] - [else #f] - )) - - (define (falsified-clause c) - (if (null? c) - null - (cons (list (lit-var (car c)) (not (lit-pos? (car c)))) (falsified-clause (cdr c))) - )) - - (define (falsified-val p) - (cond - [(null? p) false] - [(falsifiable-clause? (car p)) (falsified-clause (car p))] - [else (falsified-val (cdr p))] - ) - ) - (falsified-val cnf)) - - -;złożoność wykładnicza tak jak falsible-eval ale często w praktyce szybsza jak nie ma za dużo alternatyw.
\ No newline at end of file diff --git a/Semestr 2/racket/lista5/solution.bak b/Semestr 2/racket/lista5/solution.bak deleted file mode 100644 index 72c7f36..0000000 --- a/Semestr 2/racket/lista5/solution.bak +++ /dev/null @@ -1,135 +0,0 @@ -#lang racket - -(provide falsifiable-cnf?) -(require "props.rkt") - -(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 (lit-var f) - (cond [(var? f) f] - [(neg? f) (neg-subf f)] - [else (error "Złe dane ze znacznikiem -- LIT-VAR" f)])) - -(define (free-vars f) - (cond [(null? f) null] - [(var? f) (list f)] - [(neg? f) (free-vars (neg-subf f))] - [(conj? f) (append (free-vars (conj-left f)) - (free-vars (conj-right f)))] - [(disj? f) (append (free-vars (disj-left f)) - (free-vars (disj-right f)))] - [else (error "Zła formula -- FREE-VARS" f)])) - -(define (gen-vals xs) - (if (null? xs) - (list null) - (let* - ((vss (gen-vals (cdr xs))) - (x (car xs)) - (vst (map (λ (vs) (cons (list x true) vs)) vss)) - (vsf (map (λ (vs) (cons (list x false) vs)) vss))) - (append vst vsf)))) - -(define (eval-formula f evaluation) - (cond [(var? f) - (let ((val (assoc f evaluation))) - (if (not val) - (error "Zmienna wolna nie wystepuje w wartościowaniu -- EVAL-FORMULA" f evaluation) - (cadr val)))] - [(neg? f) (not (eval-formula (neg-subf f) evaluation))] - [(disj? f) (or (eval-formula (disj-left f) evaluation) - (eval-formula (disj-right f) evaluation))] - [(conj? f) (and (eval-formula (conj-left f) evaluation) - (eval-formula (conj-right f) evaluation))] - [else (error "Zła formuła -- EVAL-FORMULA" f evaluation)])) - -(define (falsifiable-eval? f) - (let* ((evaluations (gen-vals (free-vars f))) - (results (map (λ (evaluation) (eval-formula f evaluation)) evaluations))) - (ormap false? results))) - -(define (nff? f) - (cond [(lit? f) true] - [(neg? f) false] - [(conj? f) (and (nff? (conj-left f)) - (nff? (conj-right f)))] - [(disj? f) (and (nff? (disj-left f)) - (nff? (disj-right f)))] - [else (error "Zła formuła -- NFF?" f)])) - -(define (convert-to-nnf f) - (cond [(lit? f) f] - [(neg? f) (convert-negation (neg-subf f))] - [(conj? f) (conj (convert-to-nnf (conj-left f)) - (convert-to-nnf (conj-right f)))] - [(disj? f) (disj (convert-to-nnf (disj-left f)) - (convert-to-nnf (disj-right f)))] - [else (error "Zła formuła -- CONVERT" f)])) - -(define (convert-negation f) - (cond [(lit? f) - (if (var? f) - (neg f) - (neg-subf f))] - [(neg? f) (convert-to-nnf (neg-subf f))] - [(conj? f) (disj (convert-negation (conj-left f)) - (convert-negation (conj-right f)))] - [(disj? f) (conj (convert-negation (disj-left f)) - (convert-negation (disj-right f)))] - [else (error "Zła formuła -- CONVERT-NEGATION" f)])) - -(define (clause? x) - (and (list? x) - (andmap lit? x))) - -(define (clause-empty? x) - (and (clause? x) - (null? x))) - -(define (cnf? x) - (and (list? x) - (andmap clause? x))) - -(define (flatmap proc seq) - (foldl append null (map proc seq))) - -(define (convert-to-cnf f) - (define (convert f) - (cond [(lit? f) (list (list f))] - [(conj? f) (append (convert-to-cnf (conj-left f)) - (convert-to-cnf (conj-right f)))] - [(disj? f) - (let ((clause-left (convert-to-cnf (disj-left f))) - (clause-right (convert-to-cnf (disj-right f)))) - (flatmap (λ (clause) - (map (λ (clause2) - (append clause2 clause)) clause-left)) - clause-right))])) - (convert (convert-to-nnf f))) - -(define (falsifiable-clause? clause) - (cond [(clause-empty? clause) true] - [(lit? (findf (λ (l) (equal? - l - (convert-to-nnf (neg (car clause))))) - clause)) false] - [else (falsifiable-clause? (cdr clause))])) - -(define (falsifiable-cnf? f) - (define (neg-value lit) - (if (var? lit) - (list lit false) - (list (neg-subf lit) true))) - (ormap (λ (clause) (if (falsifiable-clause? clause) - (map neg-value clause) - false)) - (convert-to-cnf f)))
\ No newline at end of file diff --git a/Semestr 2/racket/lista5/solution.rkt b/Semestr 2/racket/lista5/solution.rkt deleted file mode 100644 index 67964d8..0000000 --- a/Semestr 2/racket/lista5/solution.rkt +++ /dev/null @@ -1,140 +0,0 @@ -#lang racket - -(provide falsifiable-cnf?) -(require "props.rkt") - -(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 (lit? t) - (or (var? t) - (and (neg? t) - (var? (neg-subf t))))) - -(define (lit-var f) - (cond [(var? f) f] - [(neg? f) (neg-subf f)] - [else (error "Złe dane ze znacznikiem -- LIT-VAR" f)])) - -(define (free-vars f) - (cond [(null? f) null] - [(var? f) (list f)] - [(neg? f) (free-vars (neg-subf f))] - [(conj? f) (append (free-vars (conj-left f)) - (free-vars (conj-right f)))] - [(disj? f) (append (free-vars (disj-left f)) - (free-vars (disj-right f)))] - [else (error "Zła formula -- FREE-VARS" f)])) - -(define (gen-vals xs) - (if (null? xs) - (list null) - (let* - ((vss (gen-vals (cdr xs))) - (x (car xs)) - (vst (map (λ (vs) (cons (list x true) vs)) vss)) - (vsf (map (λ (vs) (cons (list x false) vs)) vss))) - (append vst vsf)))) - -(define (eval-formula f evaluation) - (cond [(var? f) - (let ((val (assoc f evaluation))) - (if (not val) - (error "Zmienna wolna nie wystepuje w wartościowaniu -- EVAL-FORMULA" f evaluation) - (cadr val)))] - [(neg? f) (not (eval-formula (neg-subf f) evaluation))] - [(disj? f) (or (eval-formula (disj-left f) evaluation) - (eval-formula (disj-right f) evaluation))] - [(conj? f) (and (eval-formula (conj-left f) evaluation) - (eval-formula (conj-right f) evaluation))] - [else (error "Zła formuła -- EVAL-FORMULA" f evaluation)])) - -(define (falsifiable-eval? f) - (let* ((evaluations (gen-vals (free-vars f))) - (results (map (λ (evaluation) (eval-formula f evaluation)) evaluations))) - (ormap false? results))) - -(define (nff? f) - (cond [(lit? f) true] - [(neg? f) false] - [(conj? f) (and (nff? (conj-left f)) - (nff? (conj-right f)))] - [(disj? f) (and (nff? (disj-left f)) - (nff? (disj-right f)))] - [else (error "Zła formuła -- NFF?" f)])) - -(define (convert-to-nnf f) - (cond [(lit? f) f] - [(neg? f) (convert-negation (neg-subf f))] - [(conj? f) (conj (convert-to-nnf (conj-left f)) - (convert-to-nnf (conj-right f)))] - [(disj? f) (disj (convert-to-nnf (disj-left f)) - (convert-to-nnf (disj-right f)))] - [else (error "Zła formuła -- CONVERT" f)])) - -(define (convert-negation f) - (cond [(lit? f) - (if (var? f) - (neg f) - (neg-subf f))] - [(neg? f) (convert-to-nnf (neg-subf f))] - [(conj? f) (disj (convert-negation (conj-left f)) - (convert-negation (conj-right f)))] - [(disj? f) (conj (convert-negation (disj-left f)) - (convert-negation (disj-right f)))] - [else (error "Zła formuła -- CONVERT-NEGATION" f)])) - -(define (clause? x) - (and (list? x) - (andmap lit? x))) - -(define (clause-empty? x) - (and (clause? x) - (null? x))) - -(define (cnf? x) - (and (list? x) - (andmap clause? x))) - -(define (flatmap proc seq) - (foldl append null (map proc seq))) - -(define (convert-to-cnf f) - (define (convert f) - (cond [(lit? f) (list (list f))] - [(conj? f) (append (convert-to-cnf (conj-left f)) - (convert-to-cnf (conj-right f)))] - [(disj? f) - (let ((clause-left (convert-to-cnf (disj-left f))) - (clause-right (convert-to-cnf (disj-right f)))) - (flatmap (λ (clause) - (map (λ (clause2) - (append clause2 clause)) clause-left)) - clause-right))])) - (map (lambda (clause) (remove-duplicates clause)) (convert (convert-to-nnf f)))) - -(define (falsifiable-clause? clause) - (cond [(clause-empty? clause) true] - [(lit? (findf (λ (l) (equal? - l - (convert-to-nnf (neg (car clause))))) - clause)) false] - [else (falsifiable-clause? (cdr clause))])) - -(define (falsifiable-cnf? f) - (define (neg-value lit) - (if (var? lit) - (list lit false) - (list (neg-subf lit) true))) - (ormap (λ (clause) (if (falsifiable-clause? clause) - (map neg-value clause) - false)) - (convert-to-cnf f)))
\ No newline at end of file diff --git a/Semestr 2/racket/lista5/xd.bak b/Semestr 2/racket/lista5/xd.bak deleted file mode 100644 index d814e10..0000000 --- a/Semestr 2/racket/lista5/xd.bak +++ /dev/null @@ -1,4 +0,0 @@ -#lang racket - -(require "solution.rkt") - diff --git a/Semestr 2/racket/lista5/xd.rkt b/Semestr 2/racket/lista5/xd.rkt deleted file mode 100644 index 64ce78c..0000000 --- a/Semestr 2/racket/lista5/xd.rkt +++ /dev/null @@ -1,4 +0,0 @@ -#lang racket - -(require "solution.rkt") -(require "props.rkt") |