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/solution.rkt | 140 +++++++++++++++++++++++++++++++++++
 1 file changed, 140 insertions(+)
 create mode 100644 semestr-2/racket/lista5/solution.rkt

(limited to 'semestr-2/racket/lista5/solution.rkt')

diff --git a/semestr-2/racket/lista5/solution.rkt b/semestr-2/racket/lista5/solution.rkt
new file mode 100644
index 0000000..67964d8
--- /dev/null
+++ b/semestr-2/racket/lista5/solution.rkt
@@ -0,0 +1,140 @@
+#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
-- 
cgit v1.2.3