1 ! Copyright (C) 2008 Slava Pestov.
2 ! See http://factorcode.org/license.txt for BSD license.
3 USING: accessors arrays classes kernel sequences sets
5 FROM: multi-methods => GENERIC: METHOD: ;
14 SINGLETONS: P Q R S T U V W X Y Z ;
16 UNION: □ ⋀ ⋁ ¬ ⊤ ⊥ P Q R S T U V W X Y Z ;
18 GENERIC: ⋀ ( x y -- expr )
20 METHOD: ⋀ { ⊤ □ } nip ;
21 METHOD: ⋀ { □ ⊤ } drop ;
22 METHOD: ⋀ { ⊥ □ } drop ;
23 METHOD: ⋀ { □ ⊥ } nip ;
25 METHOD: ⋀ { ⋁ □ } [ [ x>> ] dip ⋀ ] [ [ y>> ] dip ⋀ ] 2bi ⋁ ;
26 METHOD: ⋀ { □ ⋁ } [ x>> ⋀ ] [ y>> ⋀ ] 2bi ⋁ ;
28 METHOD: ⋀ { □ □ } \ ⋀ boa ;
30 GENERIC: ⋁ ( x y -- expr )
32 METHOD: ⋁ { ⊤ □ } drop ;
33 METHOD: ⋁ { □ ⊤ } nip ;
34 METHOD: ⋁ { ⊥ □ } nip ;
35 METHOD: ⋁ { □ ⊥ } drop ;
37 METHOD: ⋁ { □ □ } \ ⋁ boa ;
39 GENERIC: ¬ ( x -- expr )
41 METHOD: ¬ { ⊤ } drop ⊥ ;
42 METHOD: ¬ { ⊥ } drop ⊤ ;
44 METHOD: ¬ { ⋀ } [ x>> ¬ ] [ y>> ¬ ] bi ⋁ ;
45 METHOD: ¬ { ⋁ } [ x>> ¬ ] [ y>> ¬ ] bi ⋀ ;
47 METHOD: ¬ { □ } \ ¬ boa ;
49 : → ( x y -- expr ) ¬ ⋀ ;
50 : ⊕ ( x y -- expr ) [ ⋁ ] [ ⋀ ¬ ] 2bi ⋀ ;
51 : ≣ ( x y -- expr ) [ ⋀ ] [ [ ¬ ] bi@ ⋀ ] 2bi ⋁ ;
53 GENERIC: (dnf) ( expr -- dnf )
55 METHOD: (dnf) { ⋀ } [ x>> (dnf) ] [ y>> (dnf) ] bi append ;
56 METHOD: (dnf) { □ } 1array ;
58 GENERIC: dnf ( expr -- dnf )
60 METHOD: dnf { ⋁ } [ x>> dnf ] [ y>> dnf ] bi append ;
61 METHOD: dnf { □ } (dnf) 1array ;
63 GENERIC: satisfiable? ( expr -- ? )
65 METHOD: satisfiable? { ⊤ } drop t ;
66 METHOD: satisfiable? { ⊥ } drop f ;
68 ! See if there is a term along with its negation in the conjunction seq.
69 : (satisfiable?) ( seq -- ? )
70 [ ¬? ] partition swap [ x>> ] map intersect empty? ;
72 METHOD: satisfiable? { □ }
73 dnf [ (satisfiable?) ] any? ;
75 GENERIC: (expr.) ( expr -- )
77 METHOD: (expr.) { □ } pprint ;
82 [ bl class-of pprint bl ]
87 METHOD: (expr.) { ⋀ } op. ;
88 METHOD: (expr.) { ⋁ } op. ;
89 METHOD: (expr.) { ¬ } [ class-of pprint ] [ x>> (expr.) ] bi ;
91 : expr. ( expr -- ) (expr.) nl ;