How create array of integer and show all array with this same element A = [0..4,0..4,0..4]
i need print to screen each: [0,0,0,0] and [1,1,1,1] and .... [4,4,4,4]
from z3 import *
#A = [ Int('a%s' % i) for i in range(4) ]
A = IntVector('a', 4)
print( 'A = ', A )
i = Int('i'); j = Int('j')
r = Solver()
r.add( i >= 0 ); r.add( i < 3 )
r.add( j >= 0 ); r.add( j < 3 )
#r.add( Select(A,i) == Select(A,j) )
print(r.check())
print(r.model())
It isn't quite clear to me what you're trying to achieve. Do you want to generate all length-4 lists with same elements between 0 and 4? There could be many ways to encode that in z3; here's one approach:
from z3 import *
A = Ints('a b c d')
s = Solver()
for a in A[1:]:
s.add(A[0] == a)
s.add(A[0] >= 0)
s.add(A[0] <= 4)
for m in list(all_smt(s, A)):
print(m)
Note that the above uses the function all_smt whose definition you can find at https://stackoverflow.com/a/70656700/936310
When run, the above prints:
[b = 0, d = 0, c = 0, a = 0]
[b = 1, a = 1, c = 1, d = 1]
[b = 2, a = 2, c = 2, d = 2]
[b = 3, a = 3, c = 3, d = 3]
[b = 4, a = 4, c = 4, d = 4]
Of course, you can post-process the models in any particular way you want. In fact, if what you're trying to generate is simply the same elements always, you don't even need 4 variables, but I assume there's a reason why you wanted it that way. (Perhaps they come from some other part of your program?)