SHARE
TWEET

Untitled

a guest Dec 19th, 2019 46 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. (ns lab4
  2.   (:require [clojure.test :refer :all]))
  3.  
  4. (defn variable [name]
  5.   {:pre [(keyword? name)]}
  6.   (list ::var name))
  7.  
  8. (defn variable? [expr]
  9.   (= (first expr) ::var))
  10.  
  11. (defn variable-name [v]
  12.   (second v))
  13.  
  14. (defn same-variables? [v1 v2]
  15.   (and
  16.     (variable? v1)
  17.     (variable? v2)
  18.     (= (variable-name v1)
  19.        (variable-name v2))))
  20.  
  21. (defn args [expr] (rest expr))
  22.  
  23. (defn constant [val]
  24.   {:pre [(boolean? val)]}
  25.   (list ::const val))
  26.  
  27. (defn constant? [expr]
  28.   (= (first expr) ::const))
  29.  
  30. (defn constant-value [expr]
  31.   {:pre [(constant? expr)]}
  32.   (second expr))
  33.  
  34. (defn atom? [expr] (or (variable? expr) (constant? expr)))
  35.  
  36. (defn applyToArgs [func expr]
  37.   (cons (first expr) (map func (args expr)))
  38.   )
  39.  
  40. (defn negation? [expr]
  41.   (= (first expr) ::neg))
  42.  
  43. ; disjunction
  44. (defn disjunction [expr1 expr2]
  45.   (cond
  46.     (and (constant? expr1) (= true (constant-value expr1))) (constant true)
  47.     (and (constant? expr1) (= false (constant-value expr1))) expr2
  48.     (and (constant? expr2) (= true (constant-value expr2))) (constant true)
  49.     (and (constant? expr2) (= false (constant-value expr2))) expr1
  50.     :else (cons ::disj (list expr1 expr2))))
  51.  
  52. (defn disjunction? [expr]
  53.   (= (first expr) ::disj))
  54.  
  55. (deftest disjunction_test
  56.   (testing "disj basic"
  57.     (let [c (disjunction (variable :x) (variable :y))]
  58.       (is (disjunction? c))
  59.       (is (same-variables? (first (args c)) (variable :x)))
  60.       (is (same-variables? (second (args c)) (variable :y))))
  61.     )
  62.   (testing "disj with const"
  63.     (is (same-variables? (disjunction (variable :x) (constant false)) (variable :x)))
  64.     (is (same-variables? (disjunction (constant false) (variable :x)) (variable :x)))
  65.     (is (= (disjunction (variable :x) (constant true)) (constant true)))
  66.     (is (= (disjunction (constant true) (variable :x)) (constant true)))
  67.     )
  68.   )
  69.  
  70. ; conjunction
  71. (defn conjunction [expr1 expr2]
  72.   (cond
  73.     (and (constant? expr1) (= true (constant-value expr1))) expr2
  74.     (and (constant? expr1) (= false (constant-value expr1))) (constant false)
  75.     (and (constant? expr2) (= true (constant-value expr2))) expr1
  76.     (and (constant? expr2) (= false (constant-value expr2))) (constant false)
  77.     (not (or (variable? expr1) (negation? expr1))) (applyToArgs (fn [expr] (conjunction expr expr2)) expr1)
  78.     (not (or (variable? expr2) (negation? expr2))) (applyToArgs (fn [expr] (conjunction expr1 expr)) expr2)
  79.     :else (cons ::conj (list expr1 expr2)))
  80.   )
  81.  
  82. (defn conjunction? [expr]
  83.   (= (first expr) ::conj))
  84.  
  85. (deftest conjunction_test
  86.   (testing "conj basic"
  87.     (let [c (conjunction (variable :x) (variable :y))]
  88.       (is (conjunction? c))
  89.       (is (same-variables? (first (args c)) (variable :x)))
  90.       (is (same-variables? (second (args c)) (variable :y))))
  91.     )
  92.   (testing "conj with const"
  93.     (is (= (conjunction (variable :x) (constant false)) (constant false)))
  94.     (is (= (conjunction (constant false) (variable :x)) (constant false)))
  95.     (is (same-variables? (conjunction (variable :x) (constant true)) (variable :x)))
  96.     (is (same-variables? (conjunction (constant true) (variable :x)) (variable :x)))
  97.     )
  98.   (testing "distributive"
  99.     (let [d1 (disjunction (variable :x) (variable :y))
  100.           d2 (disjunction (variable :y) (variable :x))
  101.           c (conjunction d1 d2)]
  102.       )
  103.  
  104.     )
  105.   )
  106.  
  107. ; negation
  108. (defn negation [expr]
  109.   (cond
  110.     (negation? expr) (first (args expr))
  111.     (constant? expr) (constant (not (constant-value expr)))
  112.     (variable? expr) (list ::neg expr)
  113.     (conjunction? expr) (disjunction (negation (first (rest expr))) (negation (second (rest expr))))
  114.     (disjunction? expr) (conjunction (negation (first (rest expr))) (negation (second (rest expr))))
  115.     ))
  116.  
  117. (deftest negation_test
  118.   (testing "negation basic"
  119.     (let [c (negation (variable :x))]
  120.       (is (negation? c))
  121.       (is (same-variables? (first (args c)) (variable :x))))
  122.     (is (same-variables? (negation (negation (variable :x))) (variable :x)))
  123.     )
  124.   (testing "negation with const"
  125.     (is (= (constant-value (negation (constant true))) false))
  126.     (is (= (constant-value (negation (constant false))) true))
  127.     )
  128.   )
  129.  
  130. ; implication
  131. (defn implication [expr1 expr2]
  132.   (disjunction (negation expr1) expr2))
  133.  
  134. (deftest implication_test
  135.   (testing "impl with const"
  136.     (is (same-variables? (negation (implication (variable :x) (constant false))) (variable :x)))
  137.     (is (= (implication (constant false) (variable :x)) (constant true)))
  138.     (is (= (implication (variable :x) (constant true)) (constant true)))
  139.     (is (same-variables? (implication (constant true) (variable :x)) (variable :x)))
  140.     )
  141.   )
  142.  
  143. ; print utils
  144. (defn print-atom [atom]
  145.   {:pre [(atom? atom)]}
  146.   (if (variable? atom)
  147.     (print (name (variable-name atom)))
  148.     (print (constant-value atom))))
  149.  
  150. (defn print-expr [expr]
  151.   (cond
  152.     (atom? expr) (print-atom expr)
  153.     (negation? expr) (do
  154.                        (print "~")
  155.                        (print-atom (first (args expr))))
  156.     (conjunction? expr) (do
  157.                           ;(print "(")
  158.                           (print-expr (first (args expr)))
  159.                           (print "*")
  160.                           (print-expr (second (args expr)))
  161.                           ;(print ")")
  162.                           )
  163.     (disjunction? expr) (do
  164.                           ;(print "(")
  165.                           (print-expr (first (args expr)))
  166.                           (print " + ")
  167.                           (print-expr (second (args expr)))
  168.                           ;(print ")")
  169.                           )
  170.     )
  171.   )
  172.  
  173. ; substitute
  174. (defn substitute [expr var const]
  175.   {:pre [(variable? var) (constant? const)]}
  176.   (cond
  177.     (and (variable? expr) (same-variables? expr var)) const
  178.     (and (variable? expr) (not (same-variables? expr var))) expr
  179.     (constant? expr) expr
  180.     (conjunction? expr) (conjunction (substitute (first (args expr)) var const) (substitute (second (args expr)) var const))
  181.     (disjunction? expr) (disjunction (substitute (first (args expr)) var const) (substitute (second (args expr)) var const))
  182.     (negation? expr) (negation (substitute (first (args expr)) var const))))
  183.  
  184. (deftest substitute_test
  185.   (testing "subst"
  186.     (let [i1 (implication (variable :x) (variable :y))
  187.           i2 (implication (variable :y) (variable :x))
  188.           c (conjunction i1 i2)
  189.           subsx (substitute c (variable :x) (constant false))
  190.           subsxy (substitute subsx (variable :y) (constant false))]
  191.       (is (= (constant-value subsxy) true))
  192.       )
  193.     ))
  194.  
  195.  
  196. ;(run-tests 'lab4)
  197.  
  198. ;(let [i1 (implication (variable :x) (variable :y))
  199. ;      i2 (implication (variable :y) (variable :x))
  200. ;      c (conjunction i1 i2)
  201. ;      cx (substitute c (variable :y) (constant true))
  202. ;      dnf (substitute c (variable :z) (constant true))]
  203. ;  (do
  204. ;    (print-expr c)
  205. ;    (println)
  206. ;    (print-expr cx)
  207. ;    (println)
  208. ;    (print-expr dnf)
  209. ;    ))
  210.  
  211. ;(let [d1 (disjunction (variable :x) (variable :y))
  212. ;      d2 (disjunction (variable :a) (variable :b))
  213. ;      c (conjunction d1 d2)]
  214. ;  (do
  215. ;    ;(print-expr (applyToArgs (fn [expr] (negation expr)) d1))
  216. ;    ;(println)
  217. ;    (print-expr c))
  218. ;  )
  219.  
  220.  
  221. ;(let [d1 (disjunction (negation (variable :x)) (variable :y))
  222. ;      d2 (disjunction (negation (variable :a)) (variable :b))
  223. ;      c (conjunction d1 d2)]
  224. ;  (do
  225. ;    (print-expr c)
  226. ;    (println))
  227. ;  )
  228. ;
  229. ;
  230. ;(let [i1 (implication (variable :x) (variable :y))
  231. ;      i2 (implication (variable :y) (variable :x))
  232. ;      c (conjunction i1 i2)]
  233. ;  (do
  234. ;    (print-expr c)
  235. ;    (println)
  236. ;    (print-expr (substitute c (variable :x) (constant false)))
  237. ;    )
  238. ;  )
  239.  
  240. (let [n1 (negation (disjunction (disjunction (variable :x) (variable :y)) (variable :z)))
  241.       d1 (disjunction (variable :a) (variable :b))
  242.       d (disjunction n1 d1)]
  243.   (do
  244.     (print-expr d)
  245.     (println)
  246.     )
  247.   )
  248.  
  249.  
  250.  
  251. ;(let [expr (disjunction (variable :x) (variable :y))
  252. ;      expr_withTrue (substitute expr (variable :x) (constant true))
  253. ;      x (variable :x)
  254. ;      x_withTrue (substitute x (variable :x) (constant true))]
  255. ;  (do
  256. ;    (print-expr expr)
  257. ;    (println)
  258. ;    (print-expr expr_withTrue)))
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
Top