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: 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 ! Implement only distributivity of ∧ over ∨, but not ∨ over ∧ to avoid
26 ! infinite looping. This makes sure that internally we always use DNF.
27 METHOD: ⋀ { ⋁ □ } [ [ x>> ] dip ⋀ ] [ [ y>> ] dip ⋀ ] 2bi ⋁ ;
28 METHOD: ⋀ { □ ⋁ } [ x>> ⋀ ] [ y>> ⋀ ] 2bi ⋁ ;
30 METHOD: ⋀ { ¬ ⋁ } { □ ⋁ } \ ⋀ method execute( x y -- expr ) ;
31 METHOD: ⋀ { ¬ □ } 2dup swap x>> = [ 2drop ⊥ ] [ \ ⋀ boa ] if ;
32 METHOD: ⋀ { □ ¬ } 2dup x>> = [ 2drop ⊥ ] [ \ ⋀ boa ] if ;
33 METHOD: ⋀ { □ □ } 2dup = [ drop ] [ \ ⋀ boa ] if ;
35 GENERIC: ⋁ ( x y -- expr )
37 METHOD: ⋁ { ⊤ □ } drop ;
38 METHOD: ⋁ { □ ⊤ } nip ;
39 METHOD: ⋁ { ⊥ □ } nip ;
40 METHOD: ⋁ { □ ⊥ } drop ;
42 METHOD: ⋁ { ¬ □ } 2dup swap x>> = [ 2drop ⊤ ] [ \ ⋁ boa ] if ;
43 METHOD: ⋁ { □ ¬ } 2dup x>> = [ 2drop ⊤ ] [ \ ⋁ boa ] if ;
44 METHOD: ⋁ { □ □ } 2dup = [ drop ] [ \ ⋁ boa ] if ;
46 GENERIC: ¬ ( x -- expr )
48 METHOD: ¬ { ⊤ } drop ⊥ ;
49 METHOD: ¬ { ⊥ } drop ⊤ ;
51 METHOD: ¬ { ⋀ } [ x>> ¬ ] [ y>> ¬ ] bi ⋁ ;
52 METHOD: ¬ { ⋁ } [ x>> ¬ ] [ y>> ¬ ] bi ⋀ ;
54 METHOD: ¬ { □ } \ ¬ boa ;
56 : → ( x y -- expr ) swap ¬ ⋁ ;
57 : ⊕ ( x y -- expr ) [ ⋁ ] [ ⋀ ¬ ] 2bi ⋀ ;
58 : ≣ ( x y -- expr ) [ ⋀ ] [ [ ¬ ] bi@ ⋀ ] 2bi ⋁ ;
60 GENERIC: (dnf) ( expr -- dnf )
62 METHOD: (dnf) { ⋀ } [ x>> (dnf) ] [ y>> (dnf) ] bi append ;
63 METHOD: (dnf) { □ } 1array ;
65 GENERIC: dnf ( expr -- dnf )
67 METHOD: dnf { ⋁ } [ x>> dnf ] [ y>> dnf ] bi append ;
68 METHOD: dnf { □ } (dnf) 1array ;
70 GENERIC: satisfiable? ( expr -- ? )
72 METHOD: satisfiable? { ⊤ } drop t ;
73 METHOD: satisfiable? { ⊥ } drop f ;
75 ! See if there is a term along with its negation in the conjunction seq.
76 : (satisfiable?) ( seq -- ? )
77 [ ¬? ] partition swap [ x>> ] map intersect empty? ;
79 METHOD: satisfiable? { □ }
80 dnf [ (satisfiable?) ] any? ;
82 GENERIC: (expr.) ( expr -- )
84 METHOD: (expr.) { □ } pprint ;
89 [ bl class-of pprint bl ]
94 METHOD: (expr.) { ⋀ } op. ;
95 METHOD: (expr.) { ⋁ } op. ;
96 METHOD: (expr.) { ¬ } [ class-of pprint ] [ x>> (expr.) ] bi ;
98 : expr. ( expr -- ) (expr.) nl ;