(ns test0.core
  (:gen-class) 
  (:require [clojure.test :as test]))


(defn constant
  "
   Constructor for constant. Creates a boolean constant expression.
   It accepts a value of either 0 or 1.
  "
  [value]
  {:pre [(or (= value 0) (= value 1))]}
  (list ::const value))

(defn constant?
  "
    Check if expr is constant. 
    Returns true if the expression is a constant.
  "
  [expr]
  (= (first expr) ::const))

(defn constant-value
  "
    Get constant value. 
    Returns the boolean value (0 or 1) of the constant expression.
  "
  [expr]
  {:pre [(constant? expr)]}
  (second expr))

(defn same-constants?
  "
    Check if two constant expressions are equal.
    It returns true if both expressions are constants 
    and have the same boolean value (0 or 1).
  "
  [const1 const2]
  (and
   (constant? const1)
   (constant? const2)
   (= (constant-value const1)
      (constant-value const2))))

(defn variable
  "
    Constructor for variable. 
    Creates a boolean variable expression with a given name.
    The name must be a keyword.   
  "
  [name]
  {:pre [(keyword? name)]}
  (list ::var name))

(defn variable?
  "
    Check if expr is variable. 
    Returns true if the expression is a variable.   
  "
  [expr]
  (= (first expr) ::var))

(defn variable-name
  "
    Get variable name. 
    Returns the name of the variable in string format.   
  " 
  [var]
  (second var))

(defn same-variables?
  "
    Check if two variables are the same. 
    Returns true if both expressions are variables and have the same name.
 "
  [var1 var2]
  (and
   (variable? var1)
   (variable? var2)
   (= (variable-name var1)
      (variable-name var2))))

(defn AND
  "
    Constructor for conjunction (&). 
    Creates a conjunction expression with one or more arguments.
    If only one argument is provided, it is returned as is.   
  "
  [expr & rest]
  (if (empty? rest)
    expr
    (cons ::and (cons expr rest))))

(defn AND?
  "
    Check if expression is conjunction. 
    Returns true if the expression is a conjunction. 
  "
  [expr]
  (= (first expr) ::and))

(defn OR
  "
    Constructor for disjunction (|). 
    Creates a disjunction expression with one or more arguments.
    If only one argument is provided, it is returned as is.   
  "
  [expr & rest]
  (if (empty? rest)
    expr
    (cons ::or (cons expr rest))))

(defn OR?
  "
    Check if expression is disjunction. 
    Returns true if the expression is a disjunction. 
  "
  [expr]
  (= (first expr) ::or))

(defn NOT
  "
    Constructor for negation (~). 
    Creates a negation expression for a given expression.   
  "
  [expr]
  (list ::not expr))

(defn NOT?
  "
    Check if expression is negation. 
    Returns true if the expression is a negation.     
  "
  [expr]
  (= (first expr) ::not))

(defn IMPL
  "
    Constructor for implication (->). 
    Creates an implication expression (expr1 -> expr2).  
  "
  [expr1 expr2]
  (list ::impl expr1 expr2))

(defn IMPL?
  "
    Check if expression is implication. 
    Returns true if the expression is an implication.  
  "
  [expr]
  (= (first expr) ::impl))

(defn same-type?
  "
    Check that expr1 and expr2 are of the same type. 
    Returns true if both expressions share the same type.    
  "
  [expr1 expr2]
  (= (first expr1) (first expr2)))

(defn args
  "
    Get arguments of operation. 
    Returns a list of the arguments for the given operation expression.    
  "
  [expr]
  (rest expr))

(defn merge-same-pred-args
  "
    Merge expressions with the same logical operator.
    This function recursively combines arguments of the same type 
    within a logical expression while keeping constants and variables intact.
    and x (and a b) c)) = (and x a b c)
  "
  [expr]
  (if (or (constant? expr) (variable? expr))
    (list expr)
    (->> (args expr)
         (mapcat #(if (same-type? expr %)
                    (merge-same-pred-args %)
                    (list %))))))

(defn find-same-const
  "
    Search for at least one instance of a constant within an expression.
    This function checks the arguments of the expression to determine 
    if the specified constant is present, returning true if found.
    if '5' in '(or x (const 5) (const 10))'
  "
  [expr const]
  (some #(same-constants? const %) (args expr)))

(defn same-not-variable?
  "
    Compare whether expr is the negation of variable
    (variable = A, expr = ~A) -> true
  "
  [variable expr]
  (if (NOT? expr)
    (same-variables? variable (second expr))
    false))

(defn find-same-not-variable
  "
    Find at least one negation of a variable in an expression.
    This function checks the arguments of an expression for the presence of a
    negative version of the given variable.
    if 'x' in '(and (not x) (or y z)))'
  "
  [expr variable]
  (some #(same-not-variable? variable %) (args expr)))

(defn return-all-except-const
  "
    Return all arguments of the expression except the specified constant.
    This function filters the arguments, excluding those that match the specified constant.
    expr = (or a (const 5) b (const 10))
    const = 5
    return = (a b (const 10))
  "
  [expr const]
  (filter #(not (same-constants? const %)) (args expr)))

(defn to-basics
  "
    Function to express all logical operations using conjunction, disjunction, and negation.
    This function transforms logical expressions into their equivalent forms based on basic operations.
  "
  [expr]
  (let [first-arg (first (args expr)),
        second-arg (second (args expr))]
    (cond
      (OR? expr) (apply OR (map #(to-basics %) (args expr)))
      (AND? expr) (apply AND (map #(to-basics %) (args expr)))
      (NOT? expr) (NOT (to-basics first-arg))
      (IMPL? expr) (OR (NOT (to-basics first-arg)) (to-basics second-arg))
      :else expr)))

(defn de-morgan-rule
  "
    A function for replacing negation signs based on De Morgan's rules
    ~(A | ... | B) = ~A & ... & ~B
    ~(A & ... & B) = ~A | ... | ~B
    ~(~A) = A
    ~0 = 1
    ~1 = 0
  "
  [expr]
  (let [not-expr (first (args expr))]
    (cond
      (OR? expr) (apply OR (map #(de-morgan-rule %) (args expr)))
      (AND? expr) (apply AND (map #(de-morgan-rule %) (args expr)))
      (NOT? expr) (cond
                    (constant? not-expr) (if (zero? (constant-value not-expr)) (constant 1) (constant 0))
                    (NOT? not-expr) (de-morgan-rule (first (args not-expr)))
                    (OR? not-expr) (apply AND (map #(de-morgan-rule (NOT %)) (args not-expr)))
                    (AND? not-expr) (apply OR (map #(de-morgan-rule (NOT %)) (args not-expr)))
                    :else expr)
      :else expr)))
  

(defn distributivity-rule
  "
    Function for expanding parentheses by distributivity
    A & (B | C) = A & B | A & C
    A | (B & C) = (A | B) & (A | C)
  "
  [expr]
  (let [first-arg (first (args expr)),
        second-arg (second (args expr))]
    (cond
      (AND? expr) (cond
                    (OR? first-arg) (OR (distributivity-rule (AND second-arg (first (args first-arg))))
                                        (distributivity-rule (AND second-arg (second (args first-arg)))))
                    (OR? second-arg) (OR (distributivity-rule (AND first-arg (first (args second-arg))))
                                         (distributivity-rule (AND first-arg (second (args second-arg)))))
                    :else expr)
      (OR? expr) (cond
                   (AND? first-arg) (AND (distributivity-rule (OR second-arg (first (args first-arg))))
                                         (distributivity-rule (OR second-arg (second (args first-arg)))))
                   (AND? second-arg) (AND (distributivity-rule (OR first-arg (first (args second-arg))))
                                          (distributivity-rule (OR first-arg (second (args second-arg)))))
                   :else expr)
      :else expr)))

(defn simplify-same-preds
  "
    Function for simplifying nested expressions with one logical operation  
    A & (B & C) = A & B & C  
    A | (B | C) = A | B | C
  "
  [expr]
  (if (or (OR? expr) (AND? expr))
    (cons (first expr) (map #(simplify-same-preds %) (merge-same-pred-args expr)))
    expr))

(defn idempotention-rule
  "
    Function for applying idempotency of conjunction and disjunction  
    A & A = A  
    A | A = A
  "
  [expr]
  (cond
    (AND? expr) (apply AND (map #(idempotention-rule %) (distinct (args expr))))
    (OR? expr) (apply OR (map #(idempotention-rule %) (distinct (args expr))))
    (NOT? expr) (NOT (idempotention-rule (first (args expr))))
    :else expr))

(defn eliminate-negation-matching
  "
    Function for replacing expressions according to rules:
    A & ~A = 0
    A | ~A = 1
  "
  [expr]
  (cond
    (AND? expr) (cond
                  (some #(true? %) (map #(find-same-not-variable expr %) (args expr))) (constant 0)
                  :else (apply AND (map #(eliminate-negation-matching %) (args expr))))
    (OR? expr) (cond
                 (some #(true? %) (map #(find-same-not-variable expr %) (args expr))) (constant 1)
                 :else (apply OR (map #(eliminate-negation-matching %) (args expr))))
    :else expr))

(defn eliminate-constant-domination
  "
    Function for replacing expressions according to rules:  
    A & 0 = 0  
    A & 1 = A  
    A | 0 = A  
    A | 1 = 1
  "
  [expr]
  (cond
       (AND? expr) (cond
                     (find-same-const expr (constant 0)) (constant 0)
                     (find-same-const expr (constant 1)) (eliminate-constant-domination (apply AND (return-all-except-const expr (constant 1))))
                     :else (apply AND (map #(eliminate-constant-domination %) (args expr))))
       (OR? expr) (cond
                    (find-same-const expr (constant 1)) (constant 1)
                    (find-same-const expr (constant 0)) (eliminate-constant-domination (apply OR (return-all-except-const expr (constant 0))))
                    :else (apply OR (map #(eliminate-constant-domination %) (args expr))))
       :else expr))

(defn dnf
  "
    Function to construct the Disjunctive Normal Form (DNF) of the expression expr.
    This function applies a series of transformations to the expression in order to
    convert it into its DNF representation by utilizing logical equivalences and simplifications.
    (and a (or (not b) c)) -> (or (and a (not b)) (and a c))
  "
  [expr]
  (->> expr
       (to-basics)                    ; Convert logical operations to basic AND, OR, and NOT forms.
       (de-morgan-rule)               ; Apply De Morgan's rule to transform negations.
       (distributivity-rule)          ; Use distributivity to reorganize the expression into disjunctive components.
       (simplify-same-preds)          ; Simplify expressions with identical predicates.
       (idempotention-rule)           ; Apply idempotent laws to eliminate redundant operations.
       (eliminate-negation-matching)   ; Remove negations that match certain expressions.
       (eliminate-constant-domination))) ; Remove constants that dominate the logical expression.

(defn substitution
  "
    Function to substitute constant values in the expression expr.
    It takes either an expression to return unchanged or 
    an expression and a map of variable substitutions.
    (+ x y) ; {'x 5, 'y 10} => (5 + 10)
  "
  ([expr] expr)
  ([expr vars]
   (cond
     (constant? expr) expr
     (variable? expr) (let [var-name (variable-name expr)]
                        (if (contains? vars var-name)
                          (constant (get vars var-name))
                          expr))
     :else (cons (first expr) (map #(substitution % vars) (args expr))))))

(test/deftest dnf-test
  (test/testing "Tests for dnf"
    
    ;; Simple logical operations
    (println "dnf(x) = x")
    (test/is (= (dnf (variable :x)) (variable :x)))
    (println "dnf(1) = 1")            
    (test/is (= (dnf (constant 1)) (constant 1))) 
    (println "dnf(0) = 0")
    (test/is (= (dnf (constant 0)) (constant 0))) 

    (println "dnf(x & y) = x & y")
    (test/is (= (dnf (AND (variable :x) (variable :y))) 
                 (AND (variable :x) (variable :y)))) 

    (println "dnf(x | y) = x | y")
    (test/is (= (dnf (OR (variable :x) (variable :y))) 
                 (OR (variable :x) (variable :y)))) 

    ;; Tests with constants
    (println "dnf(1 & x) = x")
    (test/is (= (dnf (AND (constant 1) (variable :x))) 
                 (variable :x))) 
                
    (println "dnf(0 & x) = 0")
    (test/is (= (dnf (AND (constant 0) (variable :x))) 
                 (constant 0))) 
                
    (println "dnf(1 | y) = 1")
    (test/is (= (dnf (OR (constant 1) (variable :y))) 
                 (constant 1))) 
                
    (println "dnf(0 | y) = y")
    (test/is (= (dnf (OR (constant 0) (variable :y))) 
                 (variable :y))) 

    ;; Tests with complex expressions
    (println "dnf(x -> y) = ~x | y")
    (test/is (= (dnf (IMPL (variable :x) (variable :y))) 
                 (OR (NOT (variable :x)) (variable :y)))) 
                
    (println "dnf( ~((~x | y) | ~(y -> z) )) = (x & ~y) | (x & ~y & z)")
    (test/is (= (dnf (NOT (OR (OR (NOT (variable :x)) (variable :y)) (NOT (IMPL (variable :y) (variable :z))))))
                 (OR (AND (variable :x) (NOT (variable :y))) (AND (variable :x) (NOT (variable :y)) (variable :z)))))
    
    (println "dnf((~(x) -> ~(y)) -> ((y & z) -> (~(x) & z))) = (~y) | (~z) | (~x & z) | (~x)")
    (test/is (= (dnf (IMPL (IMPL (NOT (variable :x)) (NOT (variable :y))) 
                             (IMPL (AND (variable :y) (variable :z)) 
                                   (AND (NOT (variable :x)) (variable :z)))))
                 (OR (NOT (variable :y)) (NOT (variable :z)) 
                     (AND (NOT (variable :x)) (variable :z)) (NOT (variable :x)))))
                
    (println "dnf(x | (y -> (y & x))) = x | ~y | (y & x)")
    (test/is (= (dnf (OR (variable :x) (IMPL (variable :y) (AND (variable :y) (variable :x)))))
                 (OR (variable :x) (NOT (variable :y)) (AND (variable :y) (variable :x)))))

    ;; Tests with substitution and transformations
    (test/testing "substitution-test"
                  
      (println "dnf(x -> y ) = {x=1} = 1 -> y = ~1 | y = y")           
      (test/is (= 
                (eliminate-constant-domination (dnf (substitution (IMPL (variable :x) (variable :y)) {:x 1})))
                (variable :y))) 
                  
      (println "dnf(~((~x | y) | ~(y -> z))) = {x=0;y=1} = (~((1 | 1) | ~(1 -> z))) = ~(1 | 0) = 0")  
      (test/is (= 
                (eliminate-constant-domination (dnf (substitution (NOT (OR (OR (NOT (variable :x)) (variable :y)) 
                                                                (NOT (IMPL (variable :y) (variable :z))))) 
                                              {:x 0, :y 1})))
                (constant 0))) 
                  
      (println "dnf((~((~x | y) | ~(y -> z)))) = {z=0} = (~((~x | y) | ~y )) = ~((~x | (y | ~y))) = ~1")
      (test/is (= 
                (eliminate-constant-domination (dnf (substitution (NOT (OR (OR (NOT (variable :x)) (variable :y)) 
                                                                 (NOT (IMPL (variable :y) (variable :z))))) 
                                              {:z 0})))
                (AND (variable :x) (NOT (variable :y))))) 
                  
      (println "dnf((x | (y -> (y & x)))) = {x=0} = (0 | ~y) = ~y")
      (test/is (= 
                (eliminate-constant-domination (dnf (substitution (OR (variable :x) 
                                                                      (IMPL (variable :y) 
                                                                            (AND (variable :y) 
                                                                                 (variable :x)))) 
                                                {:x 0})))
                (NOT (variable :y))))))) 

(defn -main
  "main for running tests"
  [& args]
  (test/run-tests 'test0.core)) 

(-main)

Найдите функцию substitution у вас в программе
This is my teacher question.What I need to answer.Explain me english language please.