timing in pySMT

[Matthias Heinzmann]

Hi there!

I'm currently working on a graduate student's project for which I use the pySMT API. 

As part of my project, I create in every loop a new solver (Z3) and a bunch of assertions corresponding to the parameters of the respective loop.

I then measure in every loop the time it takes the solver to find the solution and I investigate on how these time measures behave in different loops.

Now my first problem is to reliably measure this time.
I currently do it in the following way:

        t_start = clock()
        solution_found = solver.solve()
        t_end = clock()
        delta_t = t_end - t_start

where clock() is taken from the python library 'time' and delta_t is my final measure.
Is this the right way to do it or is there some internal time measurement inside pysmt?

And then I have a second more severe problem:
The time measures in the individual loops are not same depending on the ordering of the loop!

For example, when I loop over the parameters [2,4,6,10,15,20,30] the time measure in the loop of parameter '30' deviates significantly from when I loop over the parameters [30,20,15,10,6,4,2] and look at the same time measure (for parameter '30').

Apparently, information from previous loops is somehow saved although I create a new solver instance in each loop...

You have any idea where this might come from?

Looking forward to your help! Thanks!

Matthias

[Marco Gario]

Hi,

 

Now my first problem is to reliably measure this time.
I currently do it in the following way:

        t_start = clock()
        solution_found = solver.solve()
        t_end = clock()
        delta_t = t_end - t_start

where clock() is taken from the python library 'time' and delta_t is my final measure.
Is this the right way to do it or is there some internal time measurement inside pysmt?

There is no internal pySMT function for this. I think this will be a good way of measuring time. Just remember to do it more than once per parameter value, so that you can than average out the results.
Depending on how precise you want the measure to be, you might consider dumping the formula in SMT-LIB format (using pysmt smtlib printer) and then call z3 externally from command line, using a tool like runlim to measure the execution time. This might help with reproducibility and with your issue below.

 

The time measures in the individual loops are not same depending on the ordering of the loop!

Apparently, information from previous loops is somehow saved although I create a new solver instance in each loop...

This might be reasonable, but if you could provide the code that you are running, it would be better.

The keypoint is that pySMT has an internal cache of all expressions you create. This comes into play when you create an expression, independently of the solver that you are using. pySMT expressions are then converted into solver specific expressions before solving. This last step has some caching, but if you create a new solver (i.e., solver = Solver() ) then it should not come into play. However, you will see this effect if you just assert something: e.g.,

  solver.add_assertion(huge_expression())   # <- Takes time to convert the pySMT expression into the solver specific (e.g., z3) expression
  solver.add_assertion(huge_expression())   # <- Reuses the cached conversion

The pySMT cache is within the FormulaManager. To reset it, you need to reset the current environment (see http://pysmt.readthedocs.io/en/latest/api_ref.html#pysmt.shortcuts.reset_env ).

Again, maybe dumping your expression into SMT-LIB format would be the easiest way to avoid side-effects from your measures.

Hope this helps.
Marco



 
 

[Andrea Micheli]

Just a follow up on Marco's answer.

Keep in mind that creating a new solver in pysmt is not like running a fresh instance of Z3 on the shell: since we are accessing Z3 via its API, multiple instances of solvers are created in the same process, so there could be shared state between the solvers. For example, I doubt the internal pseudo-random number generator of Z3 is local to the solver and thus is a good candidate for explaining the behavior you are experiencing. In general, pysmt has no control on these issues because these depend on the solver API internal implementation.

As Marco suggested, running a solver via its SMTLIB API could be a better option if you are really interested in performance measurement (remember to force a random seed on the command line for solvers that support this).

As final note, SMT solvers are in general quite sensitive to the input formula, so even minor changes like slightly modifying the formula structure in a logically equivalent way could visibly impact performance. So, you probably could take an average over multiple runs for your results to be less sensitive on this behavior.

HTH

Andrea

 

--
You received this message because you are subscribed to the Google Groups "pySMT" group.
To unsubscribe from this group and stop receiving emails from it, send an email to pysmt+unsubscribe@googlegroups.com.
To post to this group, send email to py...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/pysmt/d7a539cb-3a96-48c1-804b-d7fdc9a7e845%40googlegroups.com.

For more options, visit https://groups.google.com/d/optout.