CODEWITHSUNDEEP
pythonz3z3py
Venkatesh-Prasad Ranganath
Venkatesh-Prasad Ranganath

Reputation: 1886

Why is z3.And() slow?

I am using Z3 Python bindings to create an And expression via z3.And(exprs) where exprs is a python list of 48000 equality constraints over boolean variables. This operation takes 2 seconds on a MBP with 2.6GHz processor.

What could I be doing wrong? Is this an issue with z3 Python bindings? Any ideas on how to optimize such constructions?

Incidentally, in my experiments, the constructions of such expressions is taking more time than solving the resulting formulae :)

Upvotes: 4

Views: 419

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8369

Using Z3 over Python is generally pretty slow. It includes parameter checks and marshaling (_coerce_expr among others). For scalability you will be better of using one of the other bindings or bypass the Python runtime where possible.

Upvotes: 2

Related Questions