CODEWITHSUNDEEP
z3py
user1832524
user1832524

Reputation: 69

How to assert all variables equal in z3py?

To assert all elements of a list equal, is there no "Equal()" in z3py? There is for example Distinct(). Using numpy works:

from z3 import *
import numpy as np

s = Solver()

B = [BitVec(f"b{j}", 7) for j in range(11)]

C_eq = [B[i] == B[j] for i in range(3) for j in range(3) if i != j]

s.add(C_eq)

print(s.check())
print(s.model())

Upvotes: 0

Views: 386

Answers (1)

alias
alias

Reputation: 30428

Indeed z3py supports Distinct, but not Equals. The reason is that a straightforward encoding of Distinct requires quadratic number of constraints, and it can bog the solver down. Having a Distinct primitive allows the solver to avoid this bottleneck. Equals, however, only requires a linear number of constraints in the number of variables and typically doesn't need any special help to be efficient.

To simplify your programming, you can define it yourself, however. Something like this:

from z3 import *

def Equals(*xs):
    constr = True
    if xs:
        base = xs[0]
        for x in xs[1:]:
            constr = And(constr, base == x)
    return constr

And then use it like this:

x, y, z = Ints('x y z')
print(Equals())
print(Equals(x))
print(Equals(x, y))
print(Equals(x, y, z))

which prints:

True
True
And(True, x == y)
And(And(True, x == y), x == z)

Upvotes: 1

Related Questions