0

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())
Łukasz
  • 102
  • 6

1 Answers1

1

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?)

alias
  • 28,120
  • 2
  • 23
  • 40
  • Is possible change this answer to using array? I need checking data using indexed element A = [ Int('a%s' % i) for i in range(4) ] or if You can show me how checking each index A[3] != A[0] etc. – Łukasz Oct 20 '22 at 13:42
  • Why first line is not sorting? [b = 0, d = 0, c = 0, a = 0] if I use a vector or array it is possible too? – Łukasz Oct 20 '22 at 13:43
  • What’s printed is a python dictionary, which doesn’t have any ordering on fields. You can post process it to print it in any way you like. Vector would be similar, just different coding. SMTLib arrays are indexed by their entire domain unlike software arrays, so I wouldn’t recommend using them for this problem. – alias Oct 20 '22 at 17:16
  • can You wrote example/answer with vector not dictionaty? – Łukasz Jan 31 '23 at 19:19