Problem in bitwise operation

[jacopodabramo]

I developed a function called 'at_most_one_bw' which execute the bitwise operation to check whether a list of Bool() variables has at most one variable True.

def at_most_one_bw(bool_vars, name):
    constraints = []
    n = len(bool_vars)
    m = math.ceil(math.log2(n))
    r = [Bool(f"r{name}{i}") for i in range(m)]
    binaries = [toBinary(i, m) for i in range(n)]
    print(binaries)
    for i in range(n):
        for j in range(m):
            phi = Not(r[j])
            if binaries[i][j] == "1":
                phi = r[j]
            constraints.append(Or(Not(bool_vars[i]), phi))
    return And(constraints)

def toBinary(num, length = None):
      num_bin = bin(num).split("b")[-1]
      if length:
          return "0"*(length - len(num_bin)) + num_bin
      return num_bin

But when using twise the same function in the same model, it triggers. For example, in the following code the first model is unsat, the second is sat, and the third should be unsat due to the fact the first is unsat and the second sat.

a = Solver()
b = Solver()
c = Solver()


l1 = [True, False, False, True]
l2 = [True, False, False, False]


a.add(at_most_one_bw(l1,'AAA'))
b.add(at_most_one_bw(l2,'BBB'))
c.add(at_most_one_bw(l1,'CCC') == at_most_one_bw(l2,'DDD'))

print(a.check())
print(b.check())
print(c.check())

The output is

unsat
sat
sat

I can't understand what's the problem. I tried not to use a function to execute the 'at most one bitwise operation' and different experiments such as defining the r-variables outside the function but it doesn't work.

[NikolajBjorner]

The constraint "at_most_one_bw(l2,'DDD')" simplifies to

And(Not(rDDD0), Not(rDDD1))

The constraint

simplify(at_most_one_bw(l1,'CCC'))

Simplifies to False.

The equivalence between False and And(Not(rDDD0), Not(rDDD1))
is satisfiable by setting rDDDD0 to True

Z3 provides a number of facilities that help you debug formulas sent to z3

• You can simplify formulas and print the result of simplification
• You can print the solver state and inspect it
• You can get models from satisfiable formulas

Example:

print(simplify(at_most_one_bw(l2,'DDD')))
print(simplify(at_most_one_bw(l1,'CCC')))
print(c.sexpr())

print(a.check())
print(b.check())

set_param(verbose=10)
print(c.check())
print(c.model())