aboutsummaryrefslogtreecommitdiff
path: root/Semestr 2/racket/lista5/skrr
diff options
context:
space:
mode:
authorFranciszek Malinka <franciszek.malinka@gmail.com>2021-02-25 14:42:55 +0100
committerFranciszek Malinka <franciszek.malinka@gmail.com>2021-02-25 14:42:55 +0100
commit9477dbe667f250ecd23f8fc0d56b942191526421 (patch)
treea4b50c9a726f415f835f5311c11c5d66e95f688c /Semestr 2/racket/lista5/skrr
parent1968c1e590077bd51844eacfac722d7963848cb8 (diff)
Stare semestry, niepoukladane
Diffstat (limited to 'Semestr 2/racket/lista5/skrr')
-rw-r--r--Semestr 2/racket/lista5/skrr/solution.bak135
-rw-r--r--Semestr 2/racket/lista5/skrr/solution.rkt88
2 files changed, 223 insertions, 0 deletions
diff --git a/Semestr 2/racket/lista5/skrr/solution.bak b/Semestr 2/racket/lista5/skrr/solution.bak
new file mode 100644
index 0000000..72c7f36
--- /dev/null
+++ b/Semestr 2/racket/lista5/skrr/solution.bak
@@ -0,0 +1,135 @@
+#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
new file mode 100644
index 0000000..e8efbc9
--- /dev/null
+++ b/Semestr 2/racket/lista5/skrr/solution.rkt
@@ -0,0 +1,88 @@
+#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