I'm trying to encode 'EXACTLY N' in the UOD (here List) in Z3. The way I used to achieve in CBMC (C Bounded model checker) is that I define List to be _Bool and use an unsigned int and just state B1 == N.
// L is the length of the List b1.
unsigned int B1 = 0
for i in range(L):
B1 = b[i] + B1
....
__CPROVER_assume (B1 == N);
It is not straight forward in Z3 as the variables are the expressions, not the type values themselves. So my initial attempt was to encode 'At least N' And 'At most N' and do conjunction of them to get 'ExACTLY N'. Improving over the initial idea and using my logic class I replaced 'At most N' by (Not) 'At least N+1'. But for N >= 5 with L =~ 600. The code running out of memory on my 4 Gb RAM machine.
# b1 is the List
X_list = []
for i in range(L-3):
for j in range(i+1,L-2):
l = And ( b1[j], b1[i])
for k in range(j+1,L-1):
l1 = And ( l, b1[k])
for l in range(k+1,L):
X_list.append( And (b1[l], l1))
B1 = Or(X_list)
File "file1.py", line 49, in <module>
X_list.append( And (b1[l], l1))
File "/usr/lib/python2.7/dist-packages/z3/z3.py", line 1611, in And
return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx)
File "/usr/lib/python2.7/dist-packages/z3/z3core.py", line 1653, in
Z3_mk_and
raise Z3Exception(lib().Z3_get_error_msg(a0, err))
z3.z3types.Z3Exception: out of memory
Is there any better way to encode this in Z3. Maybe seasoned Z3 users have some great way to encode it. Thanks.
