CODEWITHSUNDEEP
pythonz3smtz3py
Francis
Francis

Reputation: 199

How to add a constraint which requires an integer variable belongs to an array?

Suppose I have a z3py integer variable x = Int('x'), and an integer array a = [1, 2, 3]. Then I add a constraint through s.add(x in a).

I think this is satisfiable because x can be 1 or 2 or 3. But it's unsitisfiable actually. Can anyone tell me how can I add a constraint to make sure x in a?

Thanks!

Here is the python code I used. I thought the output answer would be s is satisfiable, because x can be equal to 1 or 2 or 3, then the constraint x in a is satisfied. But the answer is actually unsat. Maybe this is not the right method to specify this constraint. So my question is how to specify such a constraint to make sure a variable can only be instantiated with the value in a specific array.

from z3 import *
x = Int('x')

a = [1, 2, 3]

s = Solver()

s.add(x in a)

print(s.check())

Upvotes: 2

Views: 1675

Answers (3)

James McGuigan
James McGuigan

Reputation: 8086

One method is to build an z3.And or z3.Or constraint using a loop

# Finds all numbers in the domain, for which it's square is also in the domain

import z3
exclude = [1,2]
domain  = list(range(128))
number  = z3.Int('number')
squared = number * number
solver  = z3.Solver()
solver.add(z3.Or([  number  == value for value in domain  ]))
solver.add(z3.Or([  squared == value for value in domain  ]))
solver.add(z3.And([ number  != value for value in exclude ]))
solver.add(z3.And([ squared != value for value in exclude ]))
solver.push()  # create stack savepoint

output = []
while solver.check() == z3.sat:
  value = solver.model()[number].as_long()
  solver.add( number != value )
  output.append(value)

solver.pop()  # reset stack to last solver.push()

print(output)
# [10, 0, 4, 6, 5, 11, 9, 8, 3, 7]

print(sorted(output))
# [0, 3, 4, 5, 6, 7, 8, 9, 10, 11]

Upvotes: 0

Marco
Marco

Reputation: 336

"x in a" is a python expression, that evaluates to False before you assert the constraint, since the variable x does not belong to the array.

Upvotes: 0

alias
alias

Reputation: 30418

This should do:

from z3 import *

a = [1,2,3]

s = Solver()
x = Int('x')
s.add(Or([x == i for i in a]))

# Enumerate all possible solutions:
while True:
    r = s.check()
    if r == sat:
        m = s.model()
        print m
        s.add(x != m[x])
    else:
        print r
        break

When I run this, I get:

[x = 1]
[x = 2]
[x = 3]
unsat

Upvotes: 4

Related Questions