z3smtsatisfiability

Specifying modular arithmetic conditions in Z3

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

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

Solution

  • 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]>