Increase visitors performance

[cheshire]

While visitors provide very convenient methods for formula transformation, their performance is sometimes suboptimal.

Using a following fuzzer (https://gist.github.com/cheshire/c43575a86be1b58e3c40f95f1ba8ec07) , I've tried creating a random integer formula of size 1000, then transforming it with do-nothing operator, traversing it while doing nothing, and then solving. One would think that traversal would be almost free, transforming more expensive and solving considerably more expensive, but the data is very different:

Solver = MATHSAT5
Creating the formula took = 38.64 ms
Transformation took = 74.14 ms
Traversal took = 24.14 ms
Solving took = 6.874 ms
Solver = SMTINTERPOL
Creating the formula took = 33.94 ms
Transformation took = 50.36 ms
Traversal took = 13.69 ms
Solving took = 49.12 ms
Solver = Z3
Creating the formula took = 24.89 ms
Transformation took = 38.60 ms
Traversal took = 10.79 ms
Solving took = 3.074 ms
Solver = PRINCESS
Creating the formula took = 33.44 ms
Transformation took = 13.78 ms
Traversal took = 2.462 ms
Solving took = 188.0 ms

[PhilippWendler]

How did you measure this? Doing micro benchmarks in Java is very difficult and hard to get right. If you did not use a framework for this, your data are probably invalid. Consider using Caliper or something similar.

[cheshire]

What's "invalid"? This is indeed one particular run.

However, I was running things multiple times, and on average, the order of magnitude for the numbers stays the same (e.g. 23ms may become 10ms or 30ms but will not turn into 100ms).

Also we are talking about MILLIseconds, it's not MICRO anymore.

[PhilippWendler]

There is tons of documentation on this, the data are invalid and not worth thinking about unless you reproduce them with correct measurements. Millisecond benchmarks are certainly very micro benchmarks.

Please read for example https://stackoverflow.com/questions/504103/how-do-i-write-a-correct-micro-benchmark-in-java

[cheshire]

@PhilippWendler technically speaking, the word "micro" implies 10^-6 scale. In any case, I can raise the size of the formula such that solving takes seconds, and it is still often faster than recursive transformation. In that case solving time on different solvers gets too different though.

[cheshire]

@PhilippWendler the data is actually correct, and seconds is enough for JIT to kick in. Moreover, this is also corroborated by the profiling data, and moreover, by the fact that LPI started running much faster after some refactorings for visitors.

[PhilippWendler]

I see two further possible optimizations for calling the visitFunction method of visitors:

• Make the args list lazy.
• Cache FunctionDeclaration instances.

In neither case I am sure whether this is actually better. Lazy lists may be slower when they are iterated multiple times in the visitor. For FunctionDeclaration, we need to make sure not to use non-unique cache keys (is the function name guaranteed to be unique?). Is there a way where function declarations can be removed and we need to invalidate cache entries (for SMTInteperpol at least there is until #69 is solved)?

[PhilippWendler]

Doesn't "wontfix" mean this should be closed?