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: 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 ! 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 ⋁ ;
  29
  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 ;
  34
  35 GENERIC: ⋁ ( x y -- expr )
  36
  37 METHOD: ⋁ { ⊤ □ } drop ;
  38 METHOD: ⋁ { □ ⊤ } nip ;
  39 METHOD: ⋁ { ⊥ □ } nip ;
  40 METHOD: ⋁ { □ ⊥ } drop ;
  41
  42 METHOD: ⋁ { ¬ □ } 2dup swap x>> = [ 2drop ⊤ ] [ \ ⋁ boa ] if ;
  43 METHOD: ⋁ { □ ¬ } 2dup      x>> = [ 2drop ⊤ ] [ \ ⋁ boa ] if ;
  44 METHOD: ⋁ { □ □ } 2dup = [ drop ] [ \ ⋁ boa ] if ;
  45
  46 GENERIC: ¬ ( x -- expr )
  47
  48 METHOD: ¬ { ⊤ } drop ⊥ ;
  49 METHOD: ¬ { ⊥ } drop ⊤ ;
  50 METHOD: ¬ { ¬ } x>> ;
  51 METHOD: ¬ { ⋀ } [ x>> ¬ ] [ y>> ¬ ] bi ⋁ ;
  52 METHOD: ¬ { ⋁ } [ x>> ¬ ] [ y>> ¬ ] bi ⋀ ;
  53
  54 METHOD: ¬ { □ } \ ¬ boa ;
  55
  56 : → ( x y -- expr ) swap ¬ ⋁ ;
  57 : ⊕ ( x y -- expr ) [ ⋁ ] [ ⋀ ¬ ] 2bi ⋀ ;
  58 : ≣ ( x y -- expr ) [ ⋀ ] [ [ ¬ ] bi@ ⋀ ] 2bi ⋁ ;
  59
  60 GENERIC: (dnf) ( expr -- dnf )
  61
  62 METHOD: (dnf) { ⋀ } [ x>> (dnf) ] [ y>> (dnf) ] bi append ;
  63 METHOD: (dnf) { □ } 1array ;
  64
  65 GENERIC: dnf ( expr -- dnf )
  66
  67 METHOD: dnf { ⋁ } [ x>> dnf ] [ y>> dnf ] bi append ;
  68 METHOD: dnf { □ } (dnf) 1array ;
  69
  70 GENERIC: satisfiable? ( expr -- ? )
  71
  72 METHOD: satisfiable? { ⊤ } drop t ;
  73 METHOD: satisfiable? { ⊥ } drop f ;
  74
  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? ;
  78
  79 METHOD: satisfiable? { □ }
  80     dnf [ (satisfiable?) ] any? ;
  81
  82 GENERIC: (expr.) ( expr -- )
  83
  84 METHOD: (expr.) { □ } pprint ;
  85
  86 : op. ( expr -- )
  87     "(" write
  88     [ x>> (expr.) ]
  89     [ bl class-of pprint bl ]
  90     [ y>> (expr.) ]
  91     tri
  92     ")" write ;
  93
  94 METHOD: (expr.) { ⋀ } op. ;
  95 METHOD: (expr.) { ⋁ } op. ;
  96 METHOD: (expr.) { ¬ } [ class-of pprint ] [ x>> (expr.) ] bi ;
  97
  98 : expr. ( expr -- ) (expr.) nl ;