Symbolics.jl - failing to simplify N-over-1 rational literals within expression

General Usage
,
1

Hi,

I am currently trying to write some custom simplification rules throughout different stages of a symbolic manipulation process.

One thing I noticed is that no matter how I try, I can’t come up with a rule that cancels literal rationals of the form n//1 where n is a literal int. Later in the simplification process, the presence of this rational causes some breaking bugs (integer overflows during trying to apply some of the base rewrite rules), so I unfortunately need ot deal with this issue.

From reading the src files, it seems that this could be solved via using is_literal_number() and the ::() match predicate in @rules as in the docs.

I have however failed to write a function like this. The bellow example illustrates my attempt.

A minimal reproducible example is:

using Symbolics
using SymbolicUtils: Chain, is_literal_number

@syms x

examp = x//1 + 3//1 + 2*x//1
sim_examp = simplify(examp)
#(3//1) + 3x

#sanity check, via custom rule. We don't expect this to work...
rw = @rule ~x//1 => ~x 
sim_examp2 = simplify(examp, rewriter = Chain([rw]))
#(3//1) + 3x

rw_literal = @rule ~x::(λ -> (is_literal_number(λ) && isa(λ,Rational) && (denominator(λ) == 1))) => numerator(~x)

sim_examp3 = simplify(examp, rewriter = Symbolics.Postwalk(rw_literal))
#(3//1) + 3x

#yet....
sim_examp4 = rw_literal(3//1)
# 3 (!!!!!)


#sanity check...
cprint(x) = println(x," : ", is_literal_number(x), " : ", isa(x,Rational) && denominator(x) == 1)
trick = SymbolicUtils.Postwalk(cprint) #this walks the expression and prints the predicate 
trick(examp)
#=
3//1 : true : true - ?
3 : true : false
x : false : false
3x : false : false
(3//1) + 3x : false : false
=#

I am especially confused why the rewrites fails to match into the literal (despite the subexpression meeting the predicate, as seen in the above Postwalk() debug).

Any help is greatly appreciated - I am new to SymbolicUtils.jl and CAS in general :slight_smile: .

2

After some digging around in the base simplify rules, it seems that this issue can be partially resolved by wrapping the Postwalk() rewriter in Passthrough() to allow for the rw_literal()operations being applied “up” the graph.

#...
examp = x//1 + 3//1 + 2*x//1
f(λ) = (is_literal_number(λ) && isa(λ,Rational) && (denominator(λ) == 1))
rw_literal = @rule ~x::(λ -> f(λ)) => numerator(~x)
#In this case, Chain() also works
remove_trivials = PassThrough(Postwalk(RestartedChain([rw_literal])))

remove_trivials(examp)
#3 + 3x

However, this fails for complicated cases. My understanding is that in these cases Fixpoint() is preferred, but I can’t get it to work.

An example of this method failing on a more complicated expression:

@syms x, y, z

examp2 = y*z*(((1//1) + (2//1)*sqrt(x^2 + y^2 + z^2))^4)
remove_trivials(examp2)

#y*z*(((1//1) + (2//1)*sqrt(x^2 + y^2 + z^2))^4)
3

Open an issue if this is still the case. I think we just fixed a similar issue this week.

1 Like
4

Will check, unfortunately I might only be able to do it on Saturday.

On a slightly related note, when trying to write custom rewriters/simplifers, is there a prefered way of integrating them on top of the default_simplifer()? I don’t believe any of the Chains() that make it up get exported, so is it prefered to directly copy and mutate it instead?

5

Yeah I don’t think it’s all exported public API, but maybe it should be

1 Like