! Copyright (C) 2008 Slava Pestov. ! See http://factorcode.org/license.txt for BSD license. USING: accessors arrays classes kernel sequences sets io prettyprint multi-methods ; IN: boolean-expr ! Demonstrates the use of Unicode symbols in source files, and ! multi-method dispatch. TUPLE: ⋀ x y ; TUPLE: ⋁ x y ; TUPLE: ¬ x ; SINGLETONS: ⊤ ⊥ ; SINGLETONS: P Q R S T U V W X Y Z ; UNION: □ ⋀ ⋁ ¬ ⊤ ⊥ P Q R S T U V W X Y Z ; GENERIC: ⋀ ( x y -- expr ) METHOD: ⋀ { ⊤ □ } nip ; METHOD: ⋀ { □ ⊤ } drop ; METHOD: ⋀ { ⊥ □ } drop ; METHOD: ⋀ { □ ⊥ } nip ; METHOD: ⋀ { ⋁ □ } [ [ x>> ] dip ⋀ ] [ [ y>> ] dip ⋀ ] 2bi ⋁ ; METHOD: ⋀ { □ ⋁ } [ x>> ⋀ ] [ y>> ⋀ ] 2bi ⋁ ; METHOD: ⋀ { □ □ } \ ⋀ boa ; GENERIC: ⋁ ( x y -- expr ) METHOD: ⋁ { ⊤ □ } drop ; METHOD: ⋁ { □ ⊤ } nip ; METHOD: ⋁ { ⊥ □ } nip ; METHOD: ⋁ { □ ⊥ } drop ; METHOD: ⋁ { □ □ } \ ⋁ boa ; GENERIC: ¬ ( x -- expr ) METHOD: ¬ { ⊤ } drop ⊥ ; METHOD: ¬ { ⊥ } drop ⊤ ; METHOD: ¬ { ⋀ } [ x>> ¬ ] [ y>> ¬ ] bi ⋁ ; METHOD: ¬ { ⋁ } [ x>> ¬ ] [ y>> ¬ ] bi ⋀ ; METHOD: ¬ { □ } \ ¬ boa ; : → ( x y -- expr ) ¬ ⋀ ; : ⊕ ( x y -- expr ) [ ⋁ ] [ ⋀ ¬ ] 2bi ⋀ ; : ≣ ( x y -- expr ) [ ⋀ ] [ [ ¬ ] bi@ ⋀ ] 2bi ⋁ ; GENERIC: (cnf) ( expr -- cnf ) METHOD: (cnf) { ⋀ } [ x>> (cnf) ] [ y>> (cnf) ] bi append ; METHOD: (cnf) { □ } 1array ; GENERIC: cnf ( expr -- cnf ) METHOD: cnf { ⋁ } [ x>> cnf ] [ y>> cnf ] bi append ; METHOD: cnf { □ } (cnf) 1array ; GENERIC: satisfiable? ( expr -- ? ) METHOD: satisfiable? { ⊤ } drop t ; METHOD: satisfiable? { ⊥ } drop f ; : partition ( seq quot -- left right ) [ [ not ] compose filter ] [ filter ] 2bi ; inline : (satisfiable?) ( seq -- ? ) [ \ ¬ instance? ] partition [ x>> ] map intersect empty? ; METHOD: satisfiable? { □ } cnf [ (satisfiable?) ] any? ; GENERIC: (expr.) ( expr -- ) METHOD: (expr.) { □ } pprint ; : op. ( expr -- ) "(" write [ x>> (expr.) ] [ bl class pprint bl ] [ y>> (expr.) ] tri ")" write ; METHOD: (expr.) { ⋀ } op. ; METHOD: (expr.) { ⋁ } op. ; METHOD: (expr.) { ¬ } [ class pprint ] [ x>> (expr.) ] bi ; : expr. ( expr -- ) (expr.) nl ;