steve
/
factor
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

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

factor-shell
Alexander Iljin 2018-01-22 03:11:10 +01:00
parent 1b41bf3cfa
commit f0f2214448
2 changed files with 13 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
extra/boolean-expr/boolean-expr-docs.factor
View File

@ -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.

15
extra/boolean-expr/boolean-expr.factor
View File

@ -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 -- )