--- /dev/null
+! Copyright (C) 2022 Alexander Ilin.
+! See http://factorcode.org/license.txt for BSD license.
+USING: boolean-expr literals tools.test ;
+IN: boolean-expr.tests
+
+${ P ¬ Q ⋀ } [ P ¬ P Q ⋁ ⋀ ] unit-test
+${ P ¬ Q ⋀ } [ P ¬ Q P ⋁ ⋀ ] unit-test
+${ P Q ⋀ } [ P P ¬ Q ⋁ ⋀ ] unit-test
+${ P Q ⋀ } [ P Q P ¬ ⋁ ⋀ ] unit-test
+
+! The following tests can't pass because only the distributivity of ∧ over ∨ is
+! implemented, but not the other way around, to prevent infinite loops.
+! ${ P ¬ Q ⋀ } [ P ¬ P Q ⋀ ⋁ ] unit-test
+! ${ Q P ¬ ⋀ } [ P ¬ Q P ⋀ ⋁ ] unit-test
+! ${ P Q ⋀ } [ P P ¬ Q ⋀ ⋁ ] unit-test
+! ${ P Q ⋀ } [ P Q P ¬ ⋀ ⋁ ] unit-test
! See http://factorcode.org/license.txt for BSD license.
USING: accessors arrays classes kernel sequences sets
io prettyprint ;
-FROM: multi-methods => GENERIC: METHOD: ;
+FROM: multi-methods => GENERIC: METHOD: method ;
IN: boolean-expr
TUPLE: ⋀ x y ;
METHOD: ⋀ { ⊥ □ } drop ;
METHOD: ⋀ { □ ⊥ } nip ;
+! Implement only distributivity of ∧ over ∨, but not ∨ over ∧ to avoid
+! infinite looping. This makes sure that internally we always use DNF.
METHOD: ⋀ { ⋁ □ } [ [ x>> ] dip ⋀ ] [ [ y>> ] dip ⋀ ] 2bi ⋁ ;
METHOD: ⋀ { □ ⋁ } [ x>> ⋀ ] [ y>> ⋀ ] 2bi ⋁ ;
-METHOD: ⋀ { □ □ } \ ⋀ boa ;
+METHOD: ⋀ { ¬ ⋁ } { □ ⋁ } \ ⋀ method execute( x y -- expr ) ;
+METHOD: ⋀ { ¬ □ } 2dup swap x>> = [ 2drop ⊥ ] [ \ ⋀ boa ] if ;
+METHOD: ⋀ { □ ¬ } 2dup x>> = [ 2drop ⊥ ] [ \ ⋀ boa ] if ;
+METHOD: ⋀ { □ □ } 2dup = [ drop ] [ \ ⋀ boa ] if ;
GENERIC: ⋁ ( x y -- expr )
METHOD: ⋁ { ⊥ □ } nip ;
METHOD: ⋁ { □ ⊥ } drop ;
-METHOD: ⋁ { □ □ } \ ⋁ boa ;
+METHOD: ⋁ { ¬ □ } 2dup swap x>> = [ 2drop ⊤ ] [ \ ⋁ boa ] if ;
+METHOD: ⋁ { □ ¬ } 2dup x>> = [ 2drop ⊤ ] [ \ ⋁ boa ] if ;
+METHOD: ⋁ { □ □ } 2dup = [ drop ] [ \ ⋁ boa ] if ;
GENERIC: ¬ ( x -- expr )