2018-01-21 17:09:58 -05:00
|
|
|
|
! Copyright (C) 2008 Slava Pestov.
|
|
|
|
|
! See http://factorcode.org/license.txt for BSD license.
|
|
|
|
|
USING: accessors arrays classes kernel sequences sets
|
2018-01-21 17:12:20 -05:00
|
|
|
|
io prettyprint ;
|
|
|
|
|
FROM: multi-methods => GENERIC: METHOD: ;
|
2018-01-21 17:09:58 -05:00
|
|
|
|
IN: boolean-expr
|
|
|
|
|
|
|
|
|
|
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 ⋁ ;
|
|
|
|
|
|
2018-01-21 21:11:10 -05:00
|
|
|
|
GENERIC: (dnf) ( expr -- dnf )
|
2018-01-21 17:09:58 -05:00
|
|
|
|
|
2018-01-21 21:11:10 -05:00
|
|
|
|
METHOD: (dnf) { ⋀ } [ x>> (dnf) ] [ y>> (dnf) ] bi append ;
|
|
|
|
|
METHOD: (dnf) { □ } 1array ;
|
2018-01-21 17:09:58 -05:00
|
|
|
|
|
2018-01-21 21:11:10 -05:00
|
|
|
|
GENERIC: dnf ( expr -- dnf )
|
2018-01-21 17:09:58 -05:00
|
|
|
|
|
2018-01-21 21:11:10 -05:00
|
|
|
|
METHOD: dnf { ⋁ } [ x>> dnf ] [ y>> dnf ] bi append ;
|
|
|
|
|
METHOD: dnf { □ } (dnf) 1array ;
|
2018-01-21 17:09:58 -05:00
|
|
|
|
|
|
|
|
|
GENERIC: satisfiable? ( expr -- ? )
|
|
|
|
|
|
|
|
|
|
METHOD: satisfiable? { ⊤ } drop t ;
|
|
|
|
|
METHOD: satisfiable? { ⊥ } drop f ;
|
|
|
|
|
|
2018-01-21 21:11:10 -05:00
|
|
|
|
! See if there is a term along with its negation in the conjunction seq.
|
2018-01-21 17:09:58 -05:00
|
|
|
|
: (satisfiable?) ( seq -- ? )
|
2018-01-21 21:12:32 -05:00
|
|
|
|
[ ¬? ] partition swap [ x>> ] map intersect empty? ;
|
2018-01-21 17:09:58 -05:00
|
|
|
|
|
|
|
|
|
METHOD: satisfiable? { □ }
|
2018-01-21 21:11:10 -05:00
|
|
|
|
dnf [ (satisfiable?) ] any? ;
|
2018-01-21 17:09:58 -05:00
|
|
|
|
|
|
|
|
|
GENERIC: (expr.) ( expr -- )
|
|
|
|
|
|
|
|
|
|
METHOD: (expr.) { □ } pprint ;
|
|
|
|
|
|
|
|
|
|
: op. ( expr -- )
|
|
|
|
|
"(" write
|
|
|
|
|
[ x>> (expr.) ]
|
2018-01-21 17:11:11 -05:00
|
|
|
|
[ bl class-of pprint bl ]
|
2018-01-21 17:09:58 -05:00
|
|
|
|
[ y>> (expr.) ]
|
|
|
|
|
tri
|
|
|
|
|
")" write ;
|
|
|
|
|
|
|
|
|
|
METHOD: (expr.) { ⋀ } op. ;
|
|
|
|
|
METHOD: (expr.) { ⋁ } op. ;
|
2018-01-21 17:11:11 -05:00
|
|
|
|
METHOD: (expr.) { ¬ } [ class-of pprint ] [ x>> (expr.) ] bi ;
|
2018-01-21 17:09:58 -05:00
|
|
|
|
|
|
|
|
|
: expr. ( expr -- ) (expr.) nl ;
|