SHARE
TWEET

Untitled

a guest Dec 18th, 2019 74 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. ; negation
  107. (defn negation [expr]
  108.   (cond
  109.     (negation? expr) (first (args expr))
  110.     (constant? expr) (constant (not (constant-value expr)))
  111.     (variable? expr) (list ::neg expr)
  112.     (conjunction? expr) (disjunction (negation (first (rest expr))) (negation (second (rest expr))))
  113.     (disjunction? expr) (conjunction (negation (first (rest expr))) (negation (second (rest expr))))
  114.     ))
  115.  
  116. (deftest negation_test
  117.   (testing "negation basic"
  118.     (let [c (negation (variable :x))]
  119.       (is (negation? c))
  120.       (is (same-variables? (first (args c)) (variable :x))))
  121.     (is (same-variables? (negation (negation (variable :x))) (variable :x)))
  122.     )
  123.   (testing "negation with const"
  124.     (is (= (constant-value (negation (constant true))) false))
  125.     (is (= (constant-value (negation (constant false))) true))
  126.     )
  127.   )
  128.  
  129. ; implication
  130. (defn implication [expr1 expr2]
  131.   (disjunction (negation expr1) expr2))
  132.  
  133. (deftest implication_test
  134.   (testing "impl with const"
  135.     (is (same-variables? (negation (implication (variable :x) (constant false))) (variable :x)))
  136.     (is (= (implication (constant false) (variable :x)) (constant true)))
  137.     (is (= (implication (variable :x) (constant true)) (constant true)))
  138.     (is (same-variables? (implication (constant true) (variable :x)) (variable :x)))
  139.     )
  140.   )
  141.  
  142. (defn print-atom [atom]
  143.   {:pre [(atom? atom)]}
  144.   (if (variable? atom)
  145.     (print (name (variable-name atom)))
  146.     (print (constant-value atom))))
  147.  
  148. (defn print-expr [expr]
  149.   (cond
  150.     (atom? expr) (print-atom expr)
  151.     (negation? expr) (do
  152.                        (print "~")
  153.                        (print-atom (first (args expr))))
  154.     (conjunction? expr) (do
  155.                           (print "(")
  156.                           (print-expr (first (args expr)))
  157.                           (print ")*(")
  158.                           (print-expr (second (args expr)))
  159.                           (print ")")
  160.                           )
  161.     (disjunction? expr) (do
  162.                           (print-expr (first (args expr)))
  163.                           (print " + ")
  164.                           (print-expr (second (args expr))))
  165.     )
  166.   )
  167.  
  168.  
  169. (defn substitute [expr var const]
  170.   {:pre [(variable? var) (constant? const)]}
  171.   (cond
  172.     (and (variable? expr) (same-variables? expr var)) const
  173.     (and (variable? expr) (not (same-variables? expr var))) expr
  174.     (constant? expr) expr
  175.     (conjunction? expr) (conjunction (substitute (first (args expr)) var const) (substitute (second (args expr)) var const))
  176.     (disjunction? expr) (disjunction (substitute (first (args expr)) var const) (substitute (second (args expr)) var const))
  177.     (negation? expr) (negation (substitute (first (args expr)) var const))))
  178.  
  179. ;(println (negation (conjunction (variable :x) (variable :y))))
  180. ;(println (negation (disjunction (variable :x) (variable :y))))
  181. ;(println (conjunction (variable :x) (variable :b)))
  182. ;(println (disjunction (variable :x) (variable :b)))
  183.  
  184. ;(print-expr (variable :x))
  185. ;(print-expr (constant false))
  186. ;(print-expr (disjunction (conjunction (negation (variable :a)) (variable :b)) (conjunction (variable :c) (variable :d))))
  187. ;(println)
  188. ;(print (implication (disjunction (variable :x) (variable :y)) (conjunction (variable :x) (variable :y))))
  189.  
  190.  
  191. ;(run-tests 'lab4)
  192.  
  193. ;(let [i1 (implication (variable :x) (variable :y))
  194. ;      i2 (implication (variable :y) (variable :x))
  195. ;      c (conjunction i1 i2)
  196. ;      cx (substitute c (variable :y) (constant true))
  197. ;      dnf (substitute c (variable :z) (constant true))]
  198. ;  (do
  199. ;    (print-expr c)
  200. ;    (println)
  201. ;    (print-expr cx)
  202. ;    (println)
  203. ;    (print-expr dnf)
  204. ;    ))
  205.  
  206. ;(let [d1 (disjunction (variable :x) (variable :y))
  207. ;      d2 (disjunction (variable :a) (variable :b))
  208. ;      c (conjunction d1 d2)]
  209. ;  (do
  210. ;    ;(print-expr (applyToArgs (fn [expr] (negation expr)) d1))
  211. ;    ;(println)
  212. ;    (print-expr c))
  213. ;  )
  214.  
  215.  
  216. ;(let [d1 (disjunction (negation (variable :x)) (variable :y))
  217. ;      d2 (disjunction (negation (variable :y)) (variable :x))
  218. ;      c (conjunction d1 d2)]
  219. ;  (do
  220. ;    (print-expr c))
  221. ;  )
  222.  
  223.  
  224. (let [i1 (implication (variable :x) (variable :y))
  225.       i2 (implication (variable :y) (variable :x))
  226.       c (conjunction i1 i2)]
  227.   (do
  228.     (println c)
  229.     (print-expr c)
  230.     )
  231.   )
  232.  
  233. ;(let [expr (disjunction (variable :x) (variable :y))
  234. ;      expr_withTrue (substitute expr (variable :x) (constant true))
  235. ;      x (variable :x)
  236. ;      x_withTrue (substitute x (variable :x) (constant true))]
  237. ;  (do
  238. ;    (print-expr expr)
  239. ;    (println)
  240. ;    (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