Modular arithmetic using z3

Question

I'm trying to prove statements such as the following:

(assert (=
    (mod i n)
    (mod j n)))

(assert (> n 0))
    
(assert (not (=
    (mod (+ i 1) n)
    (mod (+ j 1) n))))

(check-sat)
(get-model)

Others are:

• (((i % n) + j) % n) == ((i + j) % n)
• ((i - n + 1) % n) == ((i + 1) % n)
• ((((a - 1) % n) + 1) % n) == (a % n)

But z3 does not seem to terminate when proving these statements. Are they beyond the power of z3/smt solvers?

If it is the only way I would not mind doing more explicit proof steps, but these rules seem so elementary I would not know where to begin. Even when using induction I quickly run into cases (like the initial example) that I would expect to be true, but which do not seem to be provable with z3.

I am using z3 4.8.6, for what it's worth. Can anyone shed some light on this why this is hard, or maybe point me in the direction of papers/z3 flags that make this feasible?

Answer 1

Long answer short, yes. These sorts of properties are too difficult for SMT solvers to handle. They essentially involve non-linear integer arithmetic, for which there is no decision procedure. The solver has a bunch of built-in heuristics that may or may not answer your query; but more often then not it'll go into an infinite loop as you no doubt observed.

See this answer for details: How does Z3 handle non-linear integer arithmetic?

What you can do

If you want to stick to a pure push-button solution, there isn't really much you can do. In certain cases, the following line helps:

(check-sat-using (and-then qfnra-nlsat smt))

This uses the theory of reals to solve your query (NRA: non-linear real arithmetic-which happens to be decidable), and then sees if the solution is actually integer. Obviously, that does not always work. In particular, any operation like mod will be difficult to deal with using this strategy.

In practice, I recommend proving specific instances of your property instead. That is, run a bunch of cases, fixing n each time:

(assert (= n 10))

then

(assert (= n 27))

etc. Obviously, this will not prove it for all n, but in a practical system if you pick your values of n carefully, you can weed out a lot of non-theorems this way.

If you really want to prove this for all n, then use a theorem prover instead. Obviously that won't be push-button, but that's the state of the art. There are many choices here: Isabelle, HOL, HOL-Light, ACL2, Coq, Lean, .. to name a few. Note that most of these theorem provers have built in tactics that utilize SMT solvers under the hood to discharge many of the sub-goals. So, you kind of have the best of both worlds, though of course the proof itself requires manual decomposition in such systems.