Having declared assertions on a solver, how can I get and exploit single assertions out of all of them? So, if s.assertions could be transformed to a list, we could access a single statement. This can not be done. I explain by the following assertions on 'BitVecs' and what I'd like to get out.
from z3 import *
s = Solver()
x,y,z,w = BitVecs("x y z w",7) #rows
a,b,c,d,e = BitVecs("a b c d e",7) #cols
constr = [x&a==a,x&b==b,x&c!=c,x&d!=d,x&e!=e,
y&a==a,y&b!=b,y&c!=c,y&d!=d,y&e==e,
z&a!=a,z&b==b,z&c==c,z&d==d,z&e!=e,
w&a!=a,w&b==b,w&c!=c,w&d==d,w&e==e ]
s.add(constr)
R = [x,y,z,w]
C = [a,b,c,d,e]
s.assertions()
I need a matrix (list of lists) that indicates wheter a R,C-pair has == or != type of 'constr'. So, the matrix for the declared constr is
[[1,1,0,0,0],
[1,0,0,0,1],
[0,1,1,1,0],
[0,1,0,1,1]]
.
This is rather an odd thing to want to do. You are constructing these assertions yourself, so it's much better to simply keep track of how you constructed them to find out what they contain.
If these are coming from some other source (possible, I suppose), then you'll have to "parse" them back into AST form and walk their structure to answer questions of the form "what are the variables", "what are the connectives" etc. Doing so will require an understanding of how z3py internally represents these objects. While this is possible, I very much doubt it's something you want to do unless you're working on a library that's supposed to handle everything. (i.e., since you know what you're constructing, simply keep track of it elsewhere.)
But, if you do want to analyze these expressions, the way to go is to study the AST structure. You'll have to become familiar with the contents of this file: https://github.com/Z3Prover/z3/blob/master/src/api/python/z3/z3.py, and especially the functions decl and children amongst others.