From: Alexander Ilin <alex.ilin@protonmail.com>
Date: Tue, 4 Jan 2022 00:11:58 +0000 (+0100)
Subject: boolean-expr: add some more expression simplification rules
X-Git-Tag: 0.99~1959
X-Git-Url: https://gitweb.factorcode.org/gitweb.cgi?p=factor.git;a=commitdiff_plain;h=96cf63731d12b06ad17d9f9cfd4091a26d53684e

boolean-expr: add some more expression simplification rules

Add some tests and comments.
---

diff --git a/extra/boolean-expr/boolean-expr-tests.factor b/extra/boolean-expr/boolean-expr-tests.factor
new file mode 100644
index 0000000000..8f99a69821
--- /dev/null
+++ b/extra/boolean-expr/boolean-expr-tests.factor
@@ -0,0 +1,16 @@
+! 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
diff --git a/extra/boolean-expr/boolean-expr.factor b/extra/boolean-expr/boolean-expr.factor
index 0f8c5b1091..9959e93333 100644
--- a/extra/boolean-expr/boolean-expr.factor
+++ b/extra/boolean-expr/boolean-expr.factor
@@ -2,7 +2,7 @@
 ! 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 ;
@@ -22,10 +22,15 @@ METHOD: ⋀ { □ ⊤ } drop ;
 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 )
 
@@ -34,7 +39,9 @@ METHOD: ⋁ { □ ⊤ } nip ;
 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 )