How to define a simple Boolean term rewriter properly in Symbolics?

General Usage
,
1

We know that a & a = a holds for a Boolean variable a. However, this rule is missing in SymbolicUtils.jl.

julia> using SymbolicUtils

julia> r = @rule ~x & ~x => ~x
~x & ~x => ~x

julia> @syms a::Bool b::Bool
(a, b)

julia> simplify(a & a; rewriter=r)
a

julia> simplify(a & a & a; rewriter=r)
(a & a) & a

julia> simplify((a & a) & b; rewriter=r)
(a & a) & b

julia>  simplify(a & a & a & a; rewriter=r)
((a & a) & a) & a

I do not understand why a & a & a or (a & a) & b does not work. I am new to Symbolics in Julia. Any help is appreciated.

2 Likes
2 
using SymbolicUtils, SymbolicUtils.Rewriters
r = Postwalk(Chain([@rule ~x & ~x => ~x]))
@syms a::Bool b::Bool
r(a & a) # a
r(a & a & a) # a
r((a & a) & b) # a & b
r(a & a & a & a) # a
1 Like