Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- (ns lab4
- (:require [clojure.test :refer :all]))
- (defn variable [name]
- {:pre [(keyword? name)]}
- (list ::var name))
- (defn variable? [expr]
- (= (first expr) ::var))
- (defn variable-name [v]
- (second v))
- (defn same-variables? [v1 v2]
- (and
- (variable? v1)
- (variable? v2)
- (= (variable-name v1)
- (variable-name v2))))
- (defn args [expr] (rest expr))
- (defn constant [val]
- {:pre [(boolean? val)]}
- (list ::const val))
- (defn constant? [expr]
- (= (first expr) ::const))
- (defn constant-value [expr]
- {:pre [(constant? expr)]}
- (second expr))
- (defn atom? [expr] (or (variable? expr) (constant? expr)))
- (defn applyToArgs [func expr]
- (cons (first expr) (map func (args expr)))
- )
- (defn negation? [expr]
- (= (first expr) ::neg))
- ; disjunction
- (defn disjunction [expr1 expr2]
- (cond
- (and (constant? expr1) (= true (constant-value expr1))) (constant true)
- (and (constant? expr1) (= false (constant-value expr1))) expr2
- (and (constant? expr2) (= true (constant-value expr2))) (constant true)
- (and (constant? expr2) (= false (constant-value expr2))) expr1
- :else (cons ::disj (list expr1 expr2))))
- (defn disjunction? [expr]
- (= (first expr) ::disj))
- (deftest disjunction_test
- (testing "disj basic"
- (let [c (disjunction (variable :x) (variable :y))]
- (is (disjunction? c))
- (is (same-variables? (first (args c)) (variable :x)))
- (is (same-variables? (second (args c)) (variable :y))))
- )
- (testing "disj with const"
- (is (same-variables? (disjunction (variable :x) (constant false)) (variable :x)))
- (is (same-variables? (disjunction (constant false) (variable :x)) (variable :x)))
- (is (= (disjunction (variable :x) (constant true)) (constant true)))
- (is (= (disjunction (constant true) (variable :x)) (constant true)))
- )
- )
- ; conjunction
- (defn conjunction [expr1 expr2]
- (cond
- (and (constant? expr1) (= true (constant-value expr1))) expr2
- (and (constant? expr1) (= false (constant-value expr1))) (constant false)
- (and (constant? expr2) (= true (constant-value expr2))) expr1
- (and (constant? expr2) (= false (constant-value expr2))) (constant false)
- (not (or (variable? expr1) (negation? expr1))) (applyToArgs (fn [expr] (conjunction expr expr2)) expr1)
- (not (or (variable? expr2) (negation? expr2))) (applyToArgs (fn [expr] (conjunction expr1 expr)) expr2)
- :else (cons ::conj (list expr1 expr2)))
- )
- (defn conjunction? [expr]
- (= (first expr) ::conj))
- (deftest conjunction_test
- (testing "conj basic"
- (let [c (conjunction (variable :x) (variable :y))]
- (is (conjunction? c))
- (is (same-variables? (first (args c)) (variable :x)))
- (is (same-variables? (second (args c)) (variable :y))))
- )
- (testing "conj with const"
- (is (= (conjunction (variable :x) (constant false)) (constant false)))
- (is (= (conjunction (constant false) (variable :x)) (constant false)))
- (is (same-variables? (conjunction (variable :x) (constant true)) (variable :x)))
- (is (same-variables? (conjunction (constant true) (variable :x)) (variable :x)))
- )
- (testing "distributive"
- (let [d1 (disjunction (variable :x) (variable :y))
- d2 (disjunction (variable :y) (variable :x))
- c (conjunction d1 d2)]
- )
- )
- )
- ; negation
- (defn negation [expr]
- (cond
- (negation? expr) (first (args expr))
- (constant? expr) (constant (not (constant-value expr)))
- (variable? expr) (list ::neg expr)
- (conjunction? expr) (disjunction (negation (first (rest expr))) (negation (second (rest expr))))
- (disjunction? expr) (conjunction (negation (first (rest expr))) (negation (second (rest expr))))
- ))
- (deftest negation_test
- (testing "negation basic"
- (let [c (negation (variable :x))]
- (is (negation? c))
- (is (same-variables? (first (args c)) (variable :x))))
- (is (same-variables? (negation (negation (variable :x))) (variable :x)))
- )
- (testing "negation with const"
- (is (= (constant-value (negation (constant true))) false))
- (is (= (constant-value (negation (constant false))) true))
- )
- )
- ; implication
- (defn implication [expr1 expr2]
- (disjunction (negation expr1) expr2))
- (deftest implication_test
- (testing "impl with const"
- (is (same-variables? (negation (implication (variable :x) (constant false))) (variable :x)))
- (is (= (implication (constant false) (variable :x)) (constant true)))
- (is (= (implication (variable :x) (constant true)) (constant true)))
- (is (same-variables? (implication (constant true) (variable :x)) (variable :x)))
- )
- )
- ; print utils
- (defn print-atom [atom]
- {:pre [(atom? atom)]}
- (if (variable? atom)
- (print (name (variable-name atom)))
- (print (constant-value atom))))
- (defn print-expr [expr]
- (cond
- (atom? expr) (print-atom expr)
- (negation? expr) (do
- (print "~")
- (print-atom (first (args expr))))
- (conjunction? expr) (do
- ;(print "(")
- (print-expr (first (args expr)))
- (print "*")
- (print-expr (second (args expr)))
- ;(print ")")
- )
- (disjunction? expr) (do
- ;(print "(")
- (print-expr (first (args expr)))
- (print " + ")
- (print-expr (second (args expr)))
- ;(print ")")
- )
- )
- )
- ; substitute
- (defn substitute [expr var const]
- {:pre [(variable? var) (constant? const)]}
- (cond
- (and (variable? expr) (same-variables? expr var)) const
- (and (variable? expr) (not (same-variables? expr var))) expr
- (constant? expr) expr
- (conjunction? expr) (conjunction (substitute (first (args expr)) var const) (substitute (second (args expr)) var const))
- (disjunction? expr) (disjunction (substitute (first (args expr)) var const) (substitute (second (args expr)) var const))
- (negation? expr) (negation (substitute (first (args expr)) var const))))
- (deftest substitute_test
- (testing "subst"
- (let [i1 (implication (variable :x) (variable :y))
- i2 (implication (variable :y) (variable :x))
- c (conjunction i1 i2)
- subsx (substitute c (variable :x) (constant false))
- subsxy (substitute subsx (variable :y) (constant false))]
- (is (= (constant-value subsxy) true))
- )
- ))
- ;(run-tests 'lab4)
- ;(let [i1 (implication (variable :x) (variable :y))
- ; i2 (implication (variable :y) (variable :x))
- ; c (conjunction i1 i2)
- ; cx (substitute c (variable :y) (constant true))
- ; dnf (substitute c (variable :z) (constant true))]
- ; (do
- ; (print-expr c)
- ; (println)
- ; (print-expr cx)
- ; (println)
- ; (print-expr dnf)
- ; ))
- ;(let [d1 (disjunction (variable :x) (variable :y))
- ; d2 (disjunction (variable :a) (variable :b))
- ; c (conjunction d1 d2)]
- ; (do
- ; ;(print-expr (applyToArgs (fn [expr] (negation expr)) d1))
- ; ;(println)
- ; (print-expr c))
- ; )
- ;(let [d1 (disjunction (negation (variable :x)) (variable :y))
- ; d2 (disjunction (negation (variable :a)) (variable :b))
- ; c (conjunction d1 d2)]
- ; (do
- ; (print-expr c)
- ; (println))
- ; )
- ;
- ;
- ;(let [i1 (implication (variable :x) (variable :y))
- ; i2 (implication (variable :y) (variable :x))
- ; c (conjunction i1 i2)]
- ; (do
- ; (print-expr c)
- ; (println)
- ; (print-expr (substitute c (variable :x) (constant false)))
- ; )
- ; )
- (let [n1 (negation (disjunction (disjunction (variable :x) (variable :y)) (variable :z)))
- d1 (disjunction (variable :a) (variable :b))
- d (disjunction n1 d1)]
- (do
- (print-expr d)
- (println)
- )
- )
- ;(let [expr (disjunction (variable :x) (variable :y))
- ; expr_withTrue (substitute expr (variable :x) (constant true))
- ; x (variable :x)
- ; x_withTrue (substitute x (variable :x) (constant true))]
- ; (do
- ; (print-expr expr)
- ; (println)
- ; (print-expr expr_withTrue)))
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement