task4

(ns task4.core)

;порождение константы
(defn constant [num]
  {:pre [(or (= num 1) (= num 0))]}
  (list ::const num))

;проверка типа для константы
(defn constant? [c]
  (= (first c) ::const))

;взятие значения константы
(defn constant-value [c]
  (second c))

;порождение переменной
(defn variable [name]
  {:pre [(keyword? name)]}
  (list ::var name))

;проверка типа для переменной
(defn variable? [v]
  (= (first v) ::var))

;взятие имени переменной
(defn variable-name [v]
  (second v))

;проверка двух переменных на равенство
(defn same-variables? [v1 v2]
  (and
    (variable? v1)
    (variable? v2)
    (= (variable-name v1)
       (variable-name v2))))

;порождение конъюкции
(defn && [expr & rest]
  (if (empty? rest)
    expr
    (cons ::conj (cons expr rest))))

;проверка типа для конъюкции
(defn &&? [expr]
  (= ::conj (first expr)))

;порождение дизъюнкции
(defn || [expr & rest]
  (if (empty? rest)
    expr
    (cons ::disj (cons expr rest))))

;проверка типа для дизъюнкции
(defn ||? [expr]
  (= ::disj (first expr)))

;порождение импликации
(defn -> [expr & rest]
  (if (empty? rest)
    expr
    (cons ::impl (cons expr rest))))

;проверка типа для импликации
(defn ->? [expr]
  (= ::impl (first expr)))

;порождение отрицания
(defn neg [expr]
  (if (= ::neg (first expr))
    (rest expr)
    (cons ::neg expr)))

;проверка типа для отрицания выражения
(defn neg? [expr]
  (= ::neg (first expr)))

;взятие аргументов выражения
(defn args [expr]
  (rest expr))

;проверка типа для отрицания переменной
(defn neg-variable? [expr]
  (and (= ::neg (first expr)) (variable? (args expr))))

;подстановка значения вместо переменной
(defn sub-val [expr v val]
  {:pre [(and (variable? v) (or (= val 0) (= val 1)))]}
  (let [sub-rules (list
                    [(fn [expr] (same-variables? expr v))
                     (fn [_] (constant val))]
                    [(fn [expr] (not (or (constant? expr) (variable? expr))))
                     (fn [expr] (cons (first expr) (map (fn [x] (sub-val x v val)) (args expr))))]
                    [(fn [_] true) (fn [expr] expr)])]
    ((some (fn [rule]
             (if ((first rule) expr)
               (second rule)
               false))
           sub-rules)
     expr)))

;элиминация импликации
(defn impl-elim [expr]
  (let [elim-rules (list
                     [->? (fn [expr] (||
                                       (neg (impl-elim (first (args expr))))
                                       (impl-elim (second (args expr)))))]
                     [neg? (fn [expr] (neg (impl-elim (args expr))))]
                     [(fn [expr] (not (or (constant? expr) (variable? expr) (neg-variable? expr))))
                      (fn [expr] (cons (first expr) (map impl-elim (args expr))))]
                     [(fn [_] true) (fn [expr] expr)])]
    ((some (fn [rule]
             (if ((first rule) expr)
               (second rule)
               false))
           elim-rules)
     expr)))

;применение законов де Моргана для раскрытия отрицаний
(defn de-morgans-laws [expr]
  (let [de-morgans-rules (list
                           [(fn [expr] (and (neg? expr) (not (variable? (args expr)))))
                            (fn [expr] (cond
                                         (||? (args expr))
                                         (&& (de-morgans-laws (neg (first (args (args expr)))))
                                             (de-morgans-laws (neg (second (args (args expr))))))
                                         (&&? (args expr))
                                         (|| (de-morgans-laws (neg (first (args (args expr)))))
                                             (de-morgans-laws (neg (second (args (args expr))))))
                                         true (neg (de-morgans-laws (args expr)))))]
                           [(fn [expr] (not (or (constant? expr)
                                                (variable? expr)
                                                (variable? (args expr)))))
                            (fn [expr] (cons (first expr) (map de-morgans-laws (args expr))))]
                           [(fn [_] true) (fn [expr] expr)])]
    ((some (fn [rule]
             (if ((first rule) expr)
               (second rule)
               false))
           de-morgans-rules)
     expr)))

;вспомогательная функция:
;проверка наличия дизъюнкции в выражении
(defn no-disj [expr]
  (cond
    (or (variable? expr) (neg-variable? expr)) true
    (||? expr) false
    true (every? no-disj (args expr))))

;применение свойства дистрибутивности
(defn distributive-pr [expr]
  (let [distr-rules (list
                      [&&? (fn [expr] (cond
                                        (||? (first (args expr)))
                                        (distributive-pr (||
                                                           (distributive-pr
                                                             (&&
                                                               (first (args (first (args expr))))
                                                               (second (args expr))))
                                                           (distributive-pr
                                                             (&&
                                                               (second (args (first (args expr))))
                                                               (second (args expr))))))
                                        (||? (second (args expr)))
                                        (distributive-pr (||
                                                           (distributive-pr
                                                             (&&
                                                               (first (args expr))
                                                               (first (args (second (args expr))))))
                                                           (distributive-pr
                                                             (&&
                                                               (first (args expr))
                                                               (second (args (second (args expr))))))))
                                        true (if (no-disj expr)
                                               expr
                                               (distributive-pr
                                                 (cons (first expr)
                                                       (map distributive-pr (args expr)))))))]
                      [(fn [expr] (not (or (constant? expr) (variable? expr) (neg-variable? expr))))
                       (fn [expr] (cons (first expr) (map distributive-pr (args expr))))]
                      [(fn [_] true) (fn [expr] expr)])]
    ((some (fn [rule]
             (if ((first rule) expr)
               (second rule)
               false))
           distr-rules)
     expr)))

;вспомогательная функция:
;раскрытие скобок по свойству ассоциативности для связки conn1 и применение к аргументам связки conn2
(defn associativity-pr1 [args conn1 conn2]
  (apply conn2 (reverse (reduce
                          (fn [acc arg] (if (conn1 arg)
                                          (concat acc (rest arg)) (conj acc arg)))
                          '()
                          args))))

;применение свойства ассоциативности
(defn associativity-pr [expr]
  (let [assoc-rules (list
                      [||? (fn [expr] (apply || (args (associativity-pr1
                                                        (map associativity-pr (args expr))
                                                        ||?
                                                        ||))))]
                      [&&? (fn [expr] (apply && (args (associativity-pr1
                                                        (map associativity-pr (args expr))
                                                        &&?
                                                        &&))))]
                      [(fn [expr] (not (or (constant? expr) (variable? expr) (neg-variable? expr))))
                       (fn [expr] (cons (first expr) (map associativity-pr (args expr))))]
                      [(fn [_] true) (fn [expr] expr)])]
    ((some (fn [rule]
             (if ((first rule) expr)
               (second rule)
               false))
           assoc-rules)
     expr)))

;применение свойства идемпотентности
(defn idempotence-pr [expr]
  (let [idemp-rules (list
                      [||? (fn [expr] (apply || (map idempotence-pr (distinct (args expr)))))]
                      [&&? (fn [expr] (apply && (map idempotence-pr (distinct (args expr)))))]
                      [(fn [expr] (not (or (constant? expr) (variable? expr) (neg-variable? expr))))
                       (fn [expr] (cons (first expr) (map idempotence-pr (args expr))))]
                      [(fn [_] true) (fn [expr] expr)])]
    ((some (fn [rule]
             (if ((first rule) expr)
               (second rule)
               false))
           idemp-rules)
     expr)))

;вспомогательная функция:
;провека того, что одно выражение есть отрицание второго
(defn neg-exprs? [expr]
  (if (or (variable? expr) (neg-variable? expr))
    false
    (some (fn [x] (some (fn [y] (or (= y (neg x)) (= x (neg y)))) expr)) expr)))

;замена тождественно истинных подформул на константу 1, а тождественно ложных на константу 0
(defn taut-contr-elim [expr]
  (let [taut-contr-elim-rules (list
                                [||? (fn [expr] (if (neg-exprs? (args expr))
                                                  (constant 1)
                                                  (apply || (map taut-contr-elim (args expr)))))]
                                [&&? (fn [expr] (if (neg-exprs? (args expr))
                                                  (constant 0)
                                                  (apply && (map taut-contr-elim (args expr)))))]
                                [(fn [expr] (not (or (constant? expr) (variable? expr) (neg-variable? expr))))
                                 (fn [expr] (cons (first expr) (map taut-contr-elim (args expr))))]
                                [(fn [_] true) (fn [expr] expr)])]
    ((some (fn [rule]
             (if ((first rule) expr)
               (second rule)
               false))
           taut-contr-elim-rules)
     expr)))

;приведение к ДНФ
(defn transform-to-dnf [expr]
  (taut-contr-elim
    (idempotence-pr
    (associativity-pr
      (distributive-pr
        (de-morgans-laws
          (impl-elim expr)))))))

--------------------------------

(variable :x) == x
(&& (variable :x3) (variable :x2) (variable :x1)) == x_3 & x_2 & x_1
(&& (neg (variable :x3)) (variable :x4)) == (not x_3) v x_4
(&& (variable :x1) (|| (variable :x3) (variable :x4) (variable :x6) (variable :x5)) (variable :x2)) == x_1 & (x_3 v x_4 v x_6 v x_5 v x_2)

;таким образом генерируешь формулы ИВ и потом их подставляешь в функции (вместо аргумента expr)