Add division and modulo operators to Zen

[alberdingk-thijm]

From what I can tell, Zen currently lacks an implementation for / or %. Would these be possible to add? Happy to take a stab at doing so myself.

[rabeckett]

Hey Tim, Zen does currently lack an implementation for / and % operators. It does have multiplication. These operations would probably only make sense for the SMT backend and not the BDD backend but I can add them.

[alberdingk-thijm]

If it helps, my specific use case was wanting to be able to use BigInteger.IsEven on a Zen<BigInteger>, which didn't seem feasible just using multiplication since I would need to existentially quantify some n such that exists n. 2 * n = k to check that k is even.

[rabeckett]

If you want % and / for unbounded integers with BigInteger then even SMT solvers will not be able to help in most cases as it involves non-linear arithmetic and is, in general, undecidable. See this post: https://stackoverflow.com/questions/66781172/modular-arithmetic-using-z3 for example.

I can add these operations, but they may not be very useful for you.

[alberdingk-thijm]

Oh, whoops, right. Sounds like we don't need to bother then!