Leonid Ryzhyk
2013-11-03
When running Reduce on the following input:
load redlog; rlset pasf; phi := ex(x, cong(x+1, z, 16)); rlqe (phi);
I obtain this result:
15*z + 14 ~16~ 0 or 15*z + 13 ~16~ 0 or 15*z + 11 ~16~ 0 or 15*z + 8 ~16~ 0 or 15*z + 7 ~16~ 0 or 15*z + 4 ~16~ 0 or 15*z + 2 ~16~ 0 or 15*z + 1 ~16~ 0 or 5*z + 4 ~16~ 0 or 5*z + 3 ~16~ 0 or 5*z + 2 ~16~ 0 or 5*z + 1 ~16~ 0 or 3*z + 2 ~16~ 0 or 3*z + 1 ~16~ 0 or z + 1 ~16~ 0 or z ~16~ 0
which is obviously correct; however I was hoping that Redlog would be able to simplify it all the way to "true". Is there a way to achieve this, e.g., by using a different encoding of the problem?
Thanks!
Leonid
Thomas Sturm
2013-11-04
Unfortunately, the simplifier is not very good.
If you suspect that it is true, you can directly ask for it, like:
rlqe all(z, phi);
More conveniently you could go
rlqe rlall phi;
where rlall() is the universal closure, i.e. all remaining variables are universally quantified.
Best,
Thomas
Leonid Ryzhyk
2013-11-05
Thanks for the explanation!
Leonid