Parsing Performance Regression (internal API)

[baierd]

Hello,

we've noticed that there is a massive performance regression concerning a parsed UF + Array formula.
We use the (internal) Java API.
Using the "normal" Java API or Z3 directly on the SMT2 file yields a result immediately.
I've written a example in Java that illustrates the problem.
Maybe you can tell us what we are doing wrong.
(Note: we at JavaSMT use this code for years without issues, hence our confusion)
You can find the example program and the query here.

To execute the program:
Drop both files into the folder that contains the build Z3 binaries with the Java interface and then execute:
javac -cp com.microsoft.z3.jar:. Z3SlowdownExamples.java
LD_LIBRARY_PATH=. java -cp com.microsoft.z3.jar:. Z3SlowdownExamples

I've added prints and some comments that explain the pathing in the program.
If you need more information or a C program, please let me know.

Thank you very much with your help!

[NikolajBjorner]

I can try to build your Java code and test, but a few things that could aid in throwing it over the fence:

• Z3.openLog can be used to trace precisely the calls to z3 from custom APIs. The text file is a replacement for the SMT2 file. It is not readable but gives an easier way to exchange repros that don't have external dependencies.
• running with verbose = 10 can tell something about different pre-processing. It could be that the solver objects differ between approaches.
• git bisect can be used to narrow down root causes.

[NikolajBjorner]

I will have to ask you to provide a z3.log. Add Native.openLog("z3.log"); before you do anything else.
My Java build environment isn't streamlined and I end up spending too much time figuring out Java build issues.
If you can use binaries from the current master it is easier for me to reliably rerun (can also be based on a tagged release).

[baierd]

Thank you for your help!
The log for the program that parses the smt2 file and then tries to solve it can be found here.
I used the current main branch for this.

[NikolajBjorner]

The z3.log repro is useful.
I identified a place where pre-processing causes an increase in term size instead of a decrease.
The place is relatively new so likely the cause of a general regression.
I am therefore blocking such rewrites during pre-processing.

After the change, the pre-processing does not expand term size and solving on z3.log now works much faster.
There is still a difference between the formula dumped (we need to add a "push" statement to get something comparable, but still it has different behavior due to how terms are built) and the binary version.

You can try the current master.

[baierd]

This fixes the regression!
Thank you very much for your help!