CODEWITHSUNDEEP
performancez3z3py
Kausik Subramanian
Kausik Subramanian

Reputation: 25

Why does creating And/Or objects in Z3py take more time than expected?

I am using Z3py where I have to create thousands of And() and Or() objects to feed to the Z3 Solver. It seems that the majority of the time taken is to just create these objects (adding them to the solver and solving them is much faster). As an extreme case, I tried this : 

assertion = True
for i in range(10000):
    assertion = Or(assertion, True)

This takes about 0.8 seconds to execute (for And() as well), which seems to be pretty high for just generating Or assertion objects.

Does Z3 perform any preprocessing when creating And/Or objects or is such a behaviour unexpected? I am running Z3 using Z3py on a Macbook Pro(2.4 GHz Intel i5, 8 Gb RAM).

Upvotes: 1

Views: 191

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

The functions 

   def And(..):
       ...
   def Or(..):
       ...

In the file z3.py perform a number of checks on the arguments to compute types. They also include some debug assertions. You can disable debug assertions in python by setting a built-in parameter or calling python with an -O flag.

Eventually, these functions call the Z3_mk_and and Z3_mk_or functions. You can also call these directly from python and bypass the additional checks and coercions. For example you can define something along the following lines that implements a function that bypasses several sanity checks, so if your code has bugs, the error messages would not be as informative.

  def myAnd(es):       
      if es = []:
         return BoolVal(True, get_ctx())    
      num = len(es)
      ctx = es[0].ctx()
      _es = (Ast * num)()
      for I in range(num):
          _es[I] = es[I].as_ast()
      return BoolRef(Z3_mk_and(ctx.ref(), num, _es), ctx)

Upvotes: 1

Related Questions