Experiments with solving non-linear formulas that involve modulo

[parno]

Here's a small experiment @yizhou7 and I recently tried. We took a number of simple lemmas from Dafny's standard library related to modulus operations, and we encoded them directly into SMT (using Z3's Python API).

Here's a rough summary of the properties involved (see the attached Python script for more details):

Lemma	Property
FundamentalDivMod	x == d * (x / d) + (x % d)
SmallMod	x < m ==> x % m == x
ModBasics	m % m == 0 && (x % m) % m == x % m && 0 <= x % m < m
ModDecreases	x % m <= x
ModIsZero	0 < x && x % m == 0 ==> x >= m
ModMultiplesBasic	(x * m) % m == 0
MultipleVanish	(b + m) % m == b % m && (b - m) % m == b % m
MultiplesVanish	(b + m * a) % m == b % m && ...
ModSubtraction	x % d - y % d == (x - y) % d
AddModNoop	((x % m) + y) % m == (x + y) % m
SubModNoopRight	(x - (y % m)) % m == (x - y) % m
ModNegNeg	x % d == (x * (1 - d)) % d
LemmaMulModNoopRight	x * (y % m) % m == (x * y) % m

With Z3, we experimented with three preludes:

1. Simply add (set-logic NIA), so that Z3 only thinks about non-linear arithmetic
2. The standard Verus prelude of SMT options, which among other things, defaults to using the NL arith.solver number 2, which relies on a simplex-based solver. We also explicitly enable NL arith (unlike Verus which disables it).
3. The standard Verus prelude of SMT options, with NL arith.solver set to 6, which is a new lra solver. Again, we explicitly enable NL arith (unlike Verus which disables it).

Since CVC5 doesn't support any of the Verus standard SMT options, for CVC5, we experimented with:

1. Simply add (set-logic NIA), so that CVC5 only thinks about non-linear arithmetic
2. Add (set-logic ALL), so that CVC5 can think about any theory it prefers.

Here are the results for Z3. Note that there's one case that Arith 2 solves and Arith 6 fails on (ModMultiplesBasic),
and vice versa for ModSubtraction.

Lemma	NL_only	Verus, Arith 2	Verus, Arith 6
FundamentalDivMod	True	True	True
SmallMod	True	True	True
ModDecreases	True	True	True
ModIsZero	True	True	True
ModMultiplesBasic	False	True	False
ModBasics	True	True	True
MultipleVanish	False	False	False
MultiplesVanish	False	False	False
ModSubtraction	True	False	True
AddModNoop	False	False	False
SubModNoopRight	False	False	False
ModNegNeg	False	False	False
LemmaMulModNoopRight	False	False	False

Here are the results for CVC5. Note that it's able to get MultipleVanish in both modes, MultiplesVanish in NIA mode, and ModNegNeg in both.

Lemma	All Logics	NIA Logic
FundamentalDivMod	True	True
SmallMod	True	True
ModDecreases	True	True
ModIsZero	True	True
ModMultiplesBasic	True	True
ModBasics	True	True
MultipleVanish	True	True
MultiplesVanish	False	True
ModSubtraction	False	False
AddModNoop	False	False
SubModNoopRight	False	False
ModNegNeg	True	True
LemmaMulModNoopRight	False	False

A related observation is that the SMT-COMP non-linear arithmetic files appear to have no queries that depend non-trivially on modulo operations, so what we're seeing here may be symptomatic of that absence.

@yizhou7 is working on trying these lemmas in our Singular mode. We expect all of the properties that don't involve inequalities to be trivial for it to solve, but stay tuned for more details.

[parno]

Here's an updated table that combines Z3, CVC5, and our Singular encoding. It's interesting to note how Singular's successes are quite complementary to the Z3 results.

Lemma	Z3 NL_only	Z3 Verus, Arith 2	Z3 Verus, Arith 6	CVC All Logics	CVC NIA Logic	Singular
FundamentalDivMod	Success	Success	Success	Success	Success
SmallMod	Success	Success	Success	Success	Success
ModDecreases	Success	Success	Success	Success	Success
ModIsZero	Success	Success	Success	Success	Success
ModMultiplesBasic		Success		Success	Success	Success
ModBasics	Success	Success	Success	Success	Success
MultipleVanish				Success	Success	Success
MultiplesVanish					Success	Success
ModSubtraction	Success		Success
AddModNoop						Success
SubModNoopRight						Success
ModNegNeg				Success	Success	Success
LemmaMulModNoopRight						Success