search

VeriFIT / z3-noodler

The Z3-Noodler String Solver
Other
6 stars 5 forks source link

Collecting statistics #169

Closed vhavlena closed 2 weeks ago

vhavlena commented 3 weeks ago

This PR utilizes Z3's mechanism for collecting statistics in the Noodler string theory (invoked by -st). So-far a counter for each decision procedure is provided + number of solved cases by purely preprocessing.

vhavlena commented 3 weeks ago

@jurajsic Any more ideas what to include to the statistics?

jurajsic commented 2 weeks ago

I would add something for decision procedures that can fail solving, for example underapproximation. Something like "how many times it did not solve" or something. I think it is the only one that can fail, right?

jurajsic commented 2 weeks ago

Also, on line 245/253, we check if we have UNSAT from init length constraints. I think we can make this another statistic (or a part of "number of times preprocessing solved").

vhavlena commented 2 weeks ago

Also, on line 245/253, we check if we have UNSAT from init length constraints. I think we can make this another statistic (or a part of "number of times preprocessing solved").

Done (included to the preprocessing counter)

vhavlena commented 2 weeks ago

I would add something for decision procedures that can fail solving, for example underapproximation. Something like "how many times it did not solve" or something. I think it is the only one that can fail, right?

Done. I distinguished the number of starts and number of finishes for each decision procedure (even though it is not necessary for all of them). It might be interesting to track how precise the suitability checking functions are.