boolean-expr[-docs]: rename cnf to dnf

diff --git a/extra/boolean-expr/boolean-expr-docs.factor b/extra/boolean-expr/boolean-expr-docs.factor
index c6f5219dc52f3669981df1a859af319f63e3ce32..5fc99dc5fd0d01a5284792d0c3c787bc927d38a4 100644 (file)
--- a/extra/boolean-expr/boolean-expr-docs.factor
+++ b/extra/boolean-expr/boolean-expr-docs.factor
@@ -9,23 +9,21 @@ ARTICLE: "boolean-expr" "Boolean expressions"
 "The " { $vocab-link "boolean-expr" } " vocab demonstrates the use of Unicode symbols in source files and multi-method dispatch."
 ;
 
-HELP: cnf
+HELP: dnf
 { $values
     { "expr" □ }
-    { "cnf" array }
+    { "dnf" array }
 }
-{ $description "Convert the " { $snippet "expr" } " to Conjuctive Normal Form (CNF), i.e. an array of subexpressions, each not containing conjunctions. See " { $url "https://en.wikipedia.org/wiki/Conjunctive_normal_form" } "." }
+{ $description "Convert the " { $snippet "expr" } " to Disjunctive Normal Form (DNF), i.e. an array of subexpressions, each not containing disjunctions. See " { $url "https://en.wikipedia.org/wiki/Disjunctive_normal_form" } "." }
 { $examples
     { $example "USING: boolean-expr prettyprint ;"
-        "X Y Z ⋀ ⋀ cnf ."
+        "X Y Z ⋀ ⋀ dnf ."
         "{ { X Y Z } }"
     }
     { $example "USING: boolean-expr prettyprint ;"
-        "X Y Z ⋁ ⋁ cnf ."
+        "X Y Z ⋁ ⋁ dnf ."
         "{ { X } { Y } { Z } }"
     }
-}
-{ $notes "Actually, looking at the exapmles above, to me it seems more like the Disjunctive Normal Form (DNF). Maybe the implementation needs to be fixed."
 } ;
 
 HELP: expr.

diff --git a/extra/boolean-expr/boolean-expr.factor b/extra/boolean-expr/boolean-expr.factor
index e65cad440cbf880caf971ecfd882d8be49d01a6a..b35cd447398c5226137b41ef4fe5c9dfe29fc3b8 100644 (file)
--- a/extra/boolean-expr/boolean-expr.factor
+++ b/extra/boolean-expr/boolean-expr.factor
@@ -50,26 +50,27 @@ METHOD: ¬ { □ } \ ¬ boa ;
 : ⊕ ( x y -- expr ) [ ⋁ ] [ ⋀ ¬ ] 2bi ⋀ ;
 : ≣ ( x y -- expr ) [ ⋀ ] [ [ ¬ ] bi@ ⋀ ] 2bi ⋁ ;
 
-GENERIC: (cnf) ( expr -- cnf )
+GENERIC: (dnf) ( expr -- dnf )
 
-METHOD: (cnf) { ⋀ } [ x>> (cnf) ] [ y>> (cnf) ] bi append ;
-METHOD: (cnf) { □ } 1array ;
+METHOD: (dnf) { ⋀ } [ x>> (dnf) ] [ y>> (dnf) ] bi append ;
+METHOD: (dnf) { □ } 1array ;
 
-GENERIC: cnf ( expr -- cnf )
+GENERIC: dnf ( expr -- dnf )
 
-METHOD: cnf { ⋁ } [ x>> cnf ] [ y>> cnf ] bi append ;
-METHOD: cnf { □ } (cnf) 1array ;
+METHOD: dnf { ⋁ } [ x>> dnf ] [ y>> dnf ] bi append ;
+METHOD: dnf { □ } (dnf) 1array ;
 
 GENERIC: satisfiable? ( expr -- ? )
 
 METHOD: satisfiable? { ⊤ } drop t ;
 METHOD: satisfiable? { ⊥ } drop f ;
 
+! See if there is a term along with its negation in the conjunction seq.
 : (satisfiable?) ( seq -- ? )
     [ \ ¬ instance? ] partition swap [ x>> ] map intersect empty? ;
 
 METHOD: satisfiable? { □ }
-    cnf [ (satisfiable?) ] any? ;
+    dnf [ (satisfiable?) ] any? ;
 
 GENERIC: (expr.) ( expr -- )