Dear All,

I would like to ask, if it would be possible to use Symbolics to simplify Boolean rules. For example

```
using Symbolics
x = SymbolicUtils.Sym{Real}(:x)
simplify((x > 1) & (x > 2))
```

should return `(x > 1)`

?

Or am I doing something wrong?

Thanks a lot for help in advance.

1 Like

The problem is, that I do it wrongly. I need to teach Symbolics the rules

```
using Symbolics, SymbolicUtils
x = SymbolicUtils.Sym{Real}(:x)
simplify((x > 1) & (x > 2))
INEQUALITY_RULES = [
@rule (~x > ~a) & (~x > ~b) => ~x > max(~a, ~b)
@rule (~x >= ~a) & (~x >= ~b) => ~x >= max(~a, ~b)
@rule (~x > ~a) | (~x > ~b) => ~x > min(~a, ~b)
@rule (~x >= ~a) | (~x >= ~b) => ~x >= min(~a, ~b)
@rule (~x < ~a) & (~x < ~b) => ~x < min(~a, ~b)
@rule (~x <= ~a) & (~x <= ~b) => ~x <= min(~a, ~b)
@rule (~x < ~a) | (~x < ~b) => ~x < max(~a, ~b)
@rule (~x <= ~a) | (~x <= ~b) => ~x <= max(~a, ~b)
]
inequality_simplifier() = SymbolicUtils.Chain(INEQUALITY_RULES)
```

and with that it works like a charm

```
julia> simplify((x > 1) & (x > 2), rewriter = inequality_simplifier())
x > 2
```

2 Likes

Still, I admit that I failing a bit. I am interested in simplifying logic rules

```
x1 = SymbolicUtils.Sym{Real}(:x1)
x2 = SymbolicUtils.Sym{Real}(:x2)
s = (((!(x1 >= 1.46) & !(x2 >= 1.4)) & !(x1 >= 1.42)) & !(x2 >= 1.42)) & (x2 <= -1.42)
```

But I am totally failing.

I have extended the rules

```
INEQUALITY_RULES = [
@rule (~x > ~a) & (~x > ~b) => ~x > max(~a, ~b)
@rule (~x >= ~a) & (~x > ~b) => ~x >= max(~a, ~b)
@rule (~x > ~a) | (~x > ~b) => ~x > min(~a, ~b)
@rule (~x >= ~a) | (~x >= ~b) => ~x >= min(~a, ~b)
@rule (~x >= ~a) | (~x > ~b) => ~x >= min(~a, ~b)
@rule (~x < ~a) & (~x < ~b) => ~x < min(~a, ~b)
@rule (~x <= ~a) & (~x <= ~b) => ~x <= min(~a, ~b)
@rule (~x < ~a) | (~x < ~b) => ~x < max(~a, ~b)
@rule (~x <= ~a) | (~x <= ~b) => ~x <= max(~a, ~b)
@rule !(~x < ~a) => ~x >= ~a
@rule !(~x > ~a) => ~x <= ~a
@rule !(~x <= ~a) => ~x > ~a
@rule !(~x >= ~a) => ~x < ~a
@acrule (~x & ~y) & ~z => ~x & (~y & ~z)
]
inequality_simplifier() = SymbolicUtils.Chain(INEQUALITY_RULES)
function extended_simplifier()
SymbolicUtils.Chain([inequality_simplifier(), SymbolicUtils.serial_expand_simplifier])
end
s = ((x1 < 1.42) & (x2 < 1.42) & (x2 <= -1.42))
simplify(s, rewriter = extended_simplifier())
```

but this runs forever. The solution should be trivial to `x1 < 1.42 & x2 <= -1.42`

. Any help is appreciated.

Open an issue. We should add these to the rule set, but you do need to make sure it’s a terminating set.

Thanks Chris,

I have created an even simpler MWE and put it to the issue

I guess in that MWE example, the e-graph should saturate.

Best wishes,

Tomas

2 Likes