Specifying modular arithmetic conditions in Z3

Question

How do I specify a modular artithmetic condition such as

f1 := (b[0]*2^0 + b[1]*2^1 + b[2]*2^2 + b[3]*2^3 + b[4]*2^4 ≡ 1 (mod 5)) ∨ 
      (b[0]*2^0 + b[1]*2^1 + b[2]*2^2 + b[3]*2^3 + b[4]*2^4 ≡ 2 (mod 5)) ∨
      (b[0]*2^0 + b[1]*2^1 + b[2]*2^2 + b[3]*2^3 + b[4]*2^4 ≡ 3 (mod 5)) ∨
      (b[0]*2^0 + b[1]*2^1 + b[2]*2^2 + b[3]*2^3 + b[4]*2^4 ≡ 4 (mod 5));

f2 := (b[0]*2^0 + b[1]*2^1 + b[2]*2^2 + b[3]*2^3 + b[4]*2^4 ≡ 1 (mod 7)) ∨
      (b[0]*2^0 + b[1]*2^1 + b[2]*2^2 + b[3]*2^3 + b[4]*2^4 ≡ 2 (mod 7)) ∨
      (b[0]*2^0 + b[1]*2^1 + b[2]*2^2 + b[3]*2^3 + b[4]*2^4 ≡ 3 (mod 7)) ∨
      (b[0]*2^0 + b[1]*2^1 + b[2]*2^2 + b[3]*2^3 + b[4]*2^4 ≡ 4 (mod 7)) ∨
      (b[0]*2^0 + b[1]*2^1 + b[2]*2^2 + b[3]*2^3 + b[4]*2^4 ≡ 5 (mod 7)) ∨
      (b[0]*2^0 + b[1]*2^1 + b[2]*2^2 + b[3]*2^3 + b[4]*2^4 ≡ 6 (mod 7));

F := f1 ∧ f2;

in Z3 SMT Solver?

In the above example

• ≡ is modular equivalence,
• (mod p) denotes modular arithmetic relative to p,
• "+","*" denote modular arithmetic operations addition and multiplication respectively,
• ∨ is the logical-or (disjunction) and
• ∧ is the logical-and (conjunction)
• b[] is an array of bits i.e., belongs to the set {0,1}
• 2^0, 2^1, ...., 2^4 are powers of 2

Z3 C# .NET API preferred. If not, any equivalent Z3 formulation is fine.

Answer 1

Using Z3 .net API

    internal class Z3Demo : Context
    {
        public Z3Demo() :
            // This example needs model generation turned on.
            base(new Dictionary<string, string>() { { "model", "true" } })
        { 
        }
        public void Show()
        {
            void o(string s) { Console.WriteLine(s); }

            Microsoft.Z3.Global.ToggleWarningMessages(true);

            o($"Z3 Version: {Microsoft.Z3.Version.FullVersion}");
           
            //  local helper to create int constants
            IntExpr Int(int val) { return MkInt(val); }

            var b = new BoolExpr[5];
            for (int i = 0; i < b.Length; i++)
            {
                b[i] = MkBoolConst($"b{i}");
            }

            var operands = new IntExpr[5];            
            for (int i = 0; i < b.Length; i++)
            {
                operands[i] = (IntExpr)MkITE(b[i], Int(1 << i), Int(0));
            }

            var sum = (IntExpr)MkAdd(operands);
            var sum5 = MkMod(sum, Int(5));
            var sum7 = MkMod(sum, Int(7));
            var f1 = MkNot(MkEq(sum5, Int(0)));
            var f2 = MkNot(MkEq(sum7, Int(0)));
            var F = MkAnd(f1, f2);

            var solver = MkSolver();
            solver.Assert(F);

            if (solver.Check() == Status.SATISFIABLE)
            {
                o("Solution found:");

                for (int i = 0; i < b.Length; i++)
                {
                    o($"b{i} = {solver.Model.Evaluate(b[i])}");
                }

                o("");
                o($"{F}");
            }
            else
            {
                o("No solution found");
            }           
        }
    }

Resulting output

Z3 Version: Z3 4.12.0.0
Solution found:
b0 = true
b1 = false
b2 = false
b3 = false
b4 = false

(let ((a!1 (+ (ite b0 1 0) (ite b1 2 0) (ite b2 4 0) (ite b3 8 0) (ite b4 16 0))))
  (and (not (= (mod a!1 5) 0)) (not (= (mod a!1 7) 0))))

---

Using z3py Z3 Python API

    from z3 import *
    
    #  create array of Boolean decision variables
    b = [Bool(f'b{i}') for i in range(5)]
    sum = Sum([b[i] * (2 ** i) for i in range(5)])
    sum5 = sum % 5
    sum7 = sum % 7
    # f1 = Or(sum5 == 1, sum5 == 2, sum5 == 3, sum5 == 4)
    f1 = (sum5 != 0)
    # f2 = Or(sum7 == 1, sum7 == 2, sum7 == 3, sum7 == 4, sum7 == 5, sum7 == 6)
    f2 = (sum7 != 0)
    F = And(f1, f2)
    
    s = Solver()
    s.add(F)
    
    print(s.check())
    print(s.model())
    
    print(s.sexpr)

Resulting output

sat
[b2 = False, b3 = False, b1 = True, b4 = False, b0 = False]
<bound method Solver.sexpr of [And((If(b0, 1, 0) +
      If(b1, 2, 0) +
      If(b2, 4, 0) +
      If(b3, 8, 0) +
      If(b4, 16, 0))%
     5 !=
     0,
     (If(b0, 1, 0) +
      If(b1, 2, 0) +
      If(b2, 4, 0) +
      If(b3, 8, 0) +
      If(b4, 16, 0))%
     7 !=
     0)]>

For integer rather than Boolean variables, the result is:

sat
[b1 = 1, b4 = 0, b0 = 0, b2 = 1, b3 = 0]
<bound method Solver.sexpr of [And((b0*1 + b1*2 + b2*4 + b3*8 + b4*16)%5 != 0,
     (b0*1 + b1*2 + b2*4 + b3*8 + b4*16)%7 != 0),
 b0 >= 0,
 b0 <= 1,
 b1 >= 0,
 b1 <= 1,
 b2 >= 0,
 b2 <= 1,
 b3 >= 0,
 b3 <= 1,
 b4 >= 0,
 b4 <= 1]>

Answer 2

Looks like there's some "mental" optimizations you can do here. Note that SMT solvers are very good at bit-vector reasoning. Looks like your b is simply a 5-bit bit-vector. The expression:

b[0]*2^0 + b[1]*2^1 + b[2]*2^2 + b[3]*2^3 + b[4]*2^4

is precisely equivalent to b, when you interpret b[i] as the i'th bit of the bit-vector, 0 being the least-significant. So, instead of "blasting" it like this, simply let the solver handle it internally. You'll have easier time coding, and the solver can use custom tricks to make it go faster.

With this in mind, your f1 says b isn't divisible by 5, and your f2 says it's not divisible by 7. So, you're looking for all 5-bit bit-vectors, that are neither divisible by 5, nor by 7.

SMTLib solution

With this rephrasing, coding becomes much easy. You can code it in SMTLib, the lingua franca of SMT-solvers:

(set-logic QF_BV)
(declare-fun b () (_ BitVec 5))
(assert (distinct (bvurem b #b00101) #b00000))
(assert (distinct (bvurem b #b00111) #b00000))
(check-sat)
(get-value (b))

This prints:

sat
((b #b11000))

i.e., in decimal 24; a value that satisfies your constraints.

Haskell solution

SMTLib is rather verbose and baroque. There are many other bindings to z3, a favorite of mine is SBV, if you are a Haskell person. In this case, it's literally a one liner:

ghci> sat $ \(x :: SWord 5) -> x `sMod` 5 ./= 0 .&& x `sMod` 7 ./= 0
Satisfiable. Model:
  s0 = 24 :: WordN 5

The good thing about these high-level interfaces is that you can easily get "all-solutions" as well. Simply change sat to allSat:

ghci> allSat $ \(x :: SWord 5) -> x `sMod` 5 ./= 0 .&& x `sMod` 7 ./= 0
Solution #1:
  s0 = 22 :: WordN 5
Solution #2:
  s0 = 6 :: WordN 5
... deleted lines for brevity ...
Solution #21:
  s0 = 24 :: WordN 5
Found 21 different solutions.

Apparently there are exactly 21 solutions to your problem.

Python solution

Python is everybody's favorite. While it has a lot of shortcomings, it's good for playing around:

from z3 import *

b = BitVec('b', 5)
s = Solver()
s.add(And(URem(b, 5) != 0, URem(b, 7) != 0))

if s.check() == sat:
    print(s.model())
else:
    print("No solution!")

Note the use of URem instead of the typical % operator: The latter does signed bit-vector arithmetic, which is not what we want here. This prints:

[b = 26]

You can iterate over this value to get all the solutions as well, see stack-overflow for many questions along these lines.

.NET solution

I don't have a .NET environment and I hate to post code that I haven't run myself. But you can use the skeleton Axel posted to port this solution there too. Just make sure you use the correct modulus operator, i.e., one over the unsigned bit-vectors.