In Python (Collab), I have the following variable c:

array([x_1 > 1000, y_1 < x_1   1], dtype=object)

Where x_1 > 1000 and y_1 < x_1 1 are z3 (py) variables / predicates. I would like to access its 'first element': the array / list [x_1 > 1000, y_1 < x_1 1], entirely, but I am not capable.

These are the attempts I have made:

• c[0] yields x_1 > 1000 (and, of course, c[1] yields y_1 < x_1 1).
• a, b = c yields, again, a to be x_1 > 1000 and b to be y_1 < x_1 1.
• c.0 yields an error (and, obviously, so does c.1).

The reason why I want to access that element of the array is I want to perform the following z3 computation in an automatic way:

And([x_1 > 1000, y_1 < x_1 1]). So it would be nice to make something like And(c[0]).

This is probably a beginner mistake, but I cannot see it. Any help?

EDIT:

Note that, the problem of asking And(c[0]), is that I am doing And(x_1 > 1000), while I would like to perform: And(x_1 > 1000, y_1 < x_1 1) (i.e., apparently And(c[0],c[1]).

CodePudding user response：

It's always best to post full code segments, i.e., those that can be loaded and executed by readers without filling up the missing parts. Otherwise it's really hard to replicate/understand what you're trying to do and what error you're getting.

I don't use collab (not sure what it is), but if c is a list, you can use the * notation to turn its contents to arguments. Something like this:

from z3 import *

x_1, y_1 = Ints('x_1 y_1')
c = [x_1 > 1000, y_1 < x_1   1]

s = Solver()
s.add(And(*c))
print(s.sexpr())

This prints:

(declare-fun x_1 () Int)
(declare-fun y_1 () Int)
(assert (and (> x_1 1000) (< y_1 (  x_1 1))))

This'll work correctly regardless of how many elements you have in the list c. Note that this has nothing to do with z3, but it is a Python idiom.

I'm not sure about your array construct; but if it can be turned into a list, the above trick should work. Is this what you're looking for?