5

I want to use a Int vector as an array index.

python.

array = [12,45,66,34]
s= Solver()
x = Int('x')
s.add(array[x] == 66)

so the x should be 2..

how can i do it?

pandaos
  • 51
  • 1
  • 3

2 Answers2

8

Here's one way to do it:

from z3 import *

s = Solver ()

array = [12, 45, 66, 34]

A = Array ('A', IntSort(), IntSort())
i = 0
for elem in array:
  A = Store(A, i, elem)
  i = i + 1

x = Int ('x')
s.add(x >= 0)
s.add(x < len(array))
s.add(Select(A, x) == 66)

if s.check() == sat:
  print s.model()
else:
  print "Not found!"

This prints:

$ python a.py
[x = 2]
alias
  • 28,120
  • 2
  • 23
  • 40
  • Why did you add the `x >= 0` and `x < len(array)` constraints. I thought `Select` only chooses from that range anyway? – stklik Mar 26 '18 at 06:28
  • 1
    @stklik That is not true. `Select` will operate over the entire domain, i.e., all integer values. Z3 arrays have no notion of lower/upper bounds. You can easily see that by removing those constraints and observing what Z3 does. – alias Mar 26 '18 at 13:57
1

It is not possible to access integer array element with Z3 ArithRef variables. I suppose, the specified problem is looking for an element in an integer array (index) through Z3 solver.

Another possible way of doing it might be:

array = [12, 45, 66, 34]
x = Int('x')

s= Solver()

for i in range(len(array)):
    s.add(Implies(array[i] == 66, x == i)) 

if s.check() == sat:
    print(s.model())
Nur Imtiazul Haque
  • 383
  • 1
  • 2
  • 10