CODEWITHSUNDEEP
pythonz3z3pytheorem-proving
Pushpa
Pushpa

Reputation: 458

Creating formula taking too much time in Z3py

Using Z3py to generate formula but formula generation taking too much time. Is it normal ? In the below code i'm just taking M-1 arguments and creating a formula with equality. I found similar time in regards to Implies. 

from z3 import *
import time
import sys

M = 32 
N = 8

p  = [ [Bool ("p_{}_{}".format(i,k)) for k in range(M)] for i in range(N)]
a  = [ [Bool ("a_{}_{}".format(i,k)) for k in range(M)] for i in range(N)]

sorts = [BoolSort() for m in range(M)]
f = [Function ("f_{}".format(m), *sorts) for m in range(M)]

starttime = time.time()

B = True
for i in range(N):
   for j in range(M):
     s = []
     for k in range(M):
        if j == k:
          continue
        s.append(p[i][k])
     B = And (a[i][j] == f[j](*s), B)
print "B", str(time.time() - starttime)

For example above code took :

59.5714960098 sec

changing code and pushing the formula to the list made it far better. But still 8 secs..! 

 ....   
 A_list = []
 s = []
 for i in range(N):
   for j in range(M):
     del [:]
     .....
     l = And (a[i][j] == f_n[j](*s))
     A_list.append(l)
A0 = And( A_list )

print "A0", str(time.time() - starttime)

8.89373087883 sec

I'm first time user of Z3py Api. Can someone explain it why it is taking too much time and is this the norm?

Upvotes: 0

Views: 96

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

There is an immediate workaround, which is to run python with debugging disabled. This is a flag you can use from the command line. I have also fixed Z3 now to avoid the time overhead. It would print expressions and format strings that are never used in assertion statements (since _z3_assert is not a macro, it uses the typical call by value evaluation semantics and therefore incurs cost to also evaluate arguments that are thrown away). The first example now takes under a second even with the debug build of Z3.

Upvotes: 1

Related Questions