extra/boolean-expr/boolean-expr.factor

   1 ! Copyright (C) 2008 Slava Pestov.
   2 ! See http://factorcode.org/license.txt for BSD license.
   3 USING: accessors arrays classes kernel sequences sets
   4 io prettyprint ;
   5 FROM: multi-methods => GENERIC: METHOD: ;
   6 IN: boolean-expr
   7
   8 TUPLE: ⋀ x y ;
   9 TUPLE: ⋁ x y ;
  10 TUPLE: ¬ x ;
  11
  12 SINGLETONS: ⊤ ⊥ ;
  13
  14 SINGLETONS: P Q R S T U V W X Y Z ;
  15
  16 UNION: □ ⋀ ⋁ ¬ ⊤ ⊥ P Q R S T U V W X Y Z ;
  17
  18 GENERIC: ⋀ ( x y -- expr )
  19
  20 METHOD: ⋀ { ⊤ □ } nip ;
  21 METHOD: ⋀ { □ ⊤ } drop ;
  22 METHOD: ⋀ { ⊥ □ } drop ;
  23 METHOD: ⋀ { □ ⊥ } nip ;
  24
  25 METHOD: ⋀ { ⋁ □ } [ [ x>> ] dip ⋀ ] [ [ y>> ] dip ⋀ ] 2bi ⋁ ;
  26 METHOD: ⋀ { □ ⋁ } [ x>> ⋀ ] [ y>> ⋀ ] 2bi ⋁ ;
  27
  28 METHOD: ⋀ { □ □ } \ ⋀ boa ;
  29
  30 GENERIC: ⋁ ( x y -- expr )
  31
  32 METHOD: ⋁ { ⊤ □ } drop ;
  33 METHOD: ⋁ { □ ⊤ } nip ;
  34 METHOD: ⋁ { ⊥ □ } nip ;
  35 METHOD: ⋁ { □ ⊥ } drop ;
  36
  37 METHOD: ⋁ { □ □ } \ ⋁ boa ;
  38
  39 GENERIC: ¬ ( x -- expr )
  40
  41 METHOD: ¬ { ⊤ } drop ⊥ ;
  42 METHOD: ¬ { ⊥ } drop ⊤ ;
  43 METHOD: ¬ { ¬ } x>> ;
  44 METHOD: ¬ { ⋀ } [ x>> ¬ ] [ y>> ¬ ] bi ⋁ ;
  45 METHOD: ¬ { ⋁ } [ x>> ¬ ] [ y>> ¬ ] bi ⋀ ;
  46
  47 METHOD: ¬ { □ } \ ¬ boa ;
  48
  49 : → ( x y -- expr ) ¬ ⋀ ;
  50 : ⊕ ( x y -- expr ) [ ⋁ ] [ ⋀ ¬ ] 2bi ⋀ ;
  51 : ≣ ( x y -- expr ) [ ⋀ ] [ [ ¬ ] bi@ ⋀ ] 2bi ⋁ ;
  52
  53 GENERIC: (dnf) ( expr -- dnf )
  54
  55 METHOD: (dnf) { ⋀ } [ x>> (dnf) ] [ y>> (dnf) ] bi append ;
  56 METHOD: (dnf) { □ } 1array ;
  57
  58 GENERIC: dnf ( expr -- dnf )
  59
  60 METHOD: dnf { ⋁ } [ x>> dnf ] [ y>> dnf ] bi append ;
  61 METHOD: dnf { □ } (dnf) 1array ;
  62
  63 GENERIC: satisfiable? ( expr -- ? )
  64
  65 METHOD: satisfiable? { ⊤ } drop t ;
  66 METHOD: satisfiable? { ⊥ } drop f ;
  67
  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? ;
  71
  72 METHOD: satisfiable? { □ }
  73     dnf [ (satisfiable?) ] any? ;
  74
  75 GENERIC: (expr.) ( expr -- )
  76
  77 METHOD: (expr.) { □ } pprint ;
  78
  79 : op. ( expr -- )
  80     "(" write
  81     [ x>> (expr.) ]
  82     [ bl class-of pprint bl ]
  83     [ y>> (expr.) ]
  84     tri
  85     ")" write ;
  86
  87 METHOD: (expr.) { ⋀ } op. ;
  88 METHOD: (expr.) { ⋁ } op. ;
  89 METHOD: (expr.) { ¬ } [ class-of pprint ] [ x>> (expr.) ] bi ;
  90
  91 : expr. ( expr -- ) (expr.) nl ;