Feature request: API for "a = b (mod m)" for a fixed "m"

[cheshire]

Hi,

Is it possible to request an API

Z3_mk_equal_modulo(Z3_ast a, Z3_ast b, long m), where a and b are integers, and m is a constant?
It's a linear constraint, both when it's positive: \exists k . a = b + k * m and
when it's negative: \exists k, d . a = b + k * m + d /\ d != 0 /\ d < m.

It's difficult for us to do this outside of the solver, as if we introduce the existential quantifier explicitly, it might become a difficult constraint under negation.
Currently we encode this as ((a - b) / m) * m = (a - b), which I think is suboptimal and non-linear.

[NikolajBjorner]

What about the encoding: (a - b) mod m = 0?
The linear arithmetic decision procedures should pick this up as linear when m is a constant.

[cheshire]

@NikolajBjorner Seems to be much slower in practice than the divisibility encoding.
Although for divisibility encoding we have the problem that Z3 sometimes decides to re-encode the whole thing as a bitvector, even though we explicitly ask for integers.
I'm generating the following test problem:

Choose three random primes prime1, prime2, prime3.
Solve in integers:

a > 1
b > 1
c > 1
a + 1 = b (mod prime1)
b = c (mod prime2)
a = c (mod prime3)

[cheshire]

Actually, disregard the comment about the wrong sort, that was my mistake.

[NikolajBjorner]

I created a test according to your example with three primes and also a formulation using fresh quotient variables. One observation is that Z3 uses different tactics for these formulations. Thus, it could be that you are seeing different behavior because the modulus terms are not recognized by certain tactics. Try to run your example with /v:10 and see if this is the case.