From c5fcf7179a83ef65c86c6a4a390029149e518649 Mon Sep 17 00:00:00 2001
From: Franciszek Malinka <franciszek.malinka@gmail.com>
Date: Tue, 5 Oct 2021 21:49:54 +0200
Subject: Duzy commit ze smieciami

---
 Semestr 2/racket/lista5/skrr/solution.bak | 135 ------------------------------
 Semestr 2/racket/lista5/skrr/solution.rkt |  88 -------------------
 2 files changed, 223 deletions(-)
 delete mode 100644 Semestr 2/racket/lista5/skrr/solution.bak
 delete mode 100644 Semestr 2/racket/lista5/skrr/solution.rkt

(limited to 'Semestr 2/racket/lista5/skrr')

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
-- 
cgit v1.2.3