Is there a way to combine QF_BV and QF_IDL?

[ThomasHaas]

In concurrent program verification, we generate formulas involving QF_BV for the data flow and QF_IDL to specify ordering constraints.
However, SMTLIB2 does not specify a common logic fragment (except ALL) nor does it specify a way to combine individual theories.
Now, I have the strong suspicion that Z3 never uses the dedicated QF_IDL solver (with (set-logic ALL)) for our queries, judging from its output statistics:

 :arith-bound-propagations-lp 756994
 :arith-conflicts             3928
 :arith-fixed-eqs             36
 :arith-lower                 1261061
 :arith-make-feasible         101219
 :arith-max-columns           7358
 :arith-max-rows              6788
 :arith-upper                 1202740

Is there a way to specify QF_BV + QF_IDL in Z3? Maybe a command-line option or a custom extension of the SMTLIB2 spec (e.g. multiple (set-logic) commands?)

[NikolajBjorner]

You can set the smt.arith_solver to use an IDL backend.
You have to set smt.auth_config=false and since you are using BV, then smt.relevancy=0.

[ThomasHaas]

Great, I just tested it with smt.arith.solver=1 (bellman-ford) and smt.arith.solver=3 (floyd-warshall).
Bellman-ford is quite bad, but floyd-warshall was almost twice as fast as the default config on my test benchmark.
The other settings didn't seem to be relevant though, neither smt.auth_config=false nor smt.relevancy=0 changed anything. What is the interaction between smt.relevancy and BV?

EDIT: Even arith.solver=2 (Simplex) and arith.solver=5 (infinitary LRA) perform as well as Floyd-Warshall. It's the default LRA one that seems to be kinda bad in handling IDL constraints.

[NikolajBjorner]

@levnach - perf overhead with arith.solver=6.

[NikolajBjorner]

Can you share at least one benchmark where smt.arith.solver=6 is worse than smt.arith.solver=2?

[ThomasHaas]

Here is file generated by Dartagnan: cna.txt
Running z3 smt.arith.solver=X -st cna.txt with Z3 version 4.15.3 - 64 bit on my Mac M2 (Arm-based), I get:

arith.solver=2:     :total-time 26.21 // Simplex-based
arith.solver=3:     :total-time 18.31 // Floyd-Warshall
arith.solver=5:     :total-time 27.81 // infinitary LRA
arith.solver=6:     :total-time 36.79 // LRA (default)

Note that this is an incremental query over BV_QF + BV_IDL. But the two (very small) assertions at the very end can be merged into a single assertion with a single (check-sat) call. The performance discrepancy is still there in that case.

The query is large and likely hard to understand by manual inspection. But I can at least say that all IDL constraints are of shape x < y, x = 0, and 0 < x if that is of any help. Most constraints are enabled by guards g => x < y, so there is a large boolean structure around the IDL atoms which might affect the performance of the theory solvers.

I can also generate smaller variants of the test, but I think none of them will be very readable.
If needed, I can generate different benchmarks coming from the verification of other concurrent locks/data structures, but their overall shape will be identical to cna.txt.

[ThomasHaas]

Here is another slightly smaller example with even bigger difference: client.txt

// Z3 version 4.15.3 - 64 bit
arith.solver=2:     :total-time 4.29 // Simplex-based
arith.solver=3:     :total-time 1.84 // Floyd-Warshall
arith.solver=5:     :total-time 4.40 // infinitary LRA
arith.solver=6:     :total-time 15.98 // LRA (default)

As you can see, arith.solver=6 is at least 4x slower than the other solvers.

[ThomasHaas]

I'm not sure if this is helpful information, but in Dartagnan we can flip the role of the integer encoding, i.e., we can encode the data flow using integers and the ordering constraints using plain SAT.
In that case, arith.solver=6 is a lot faster than arith.solver=2, so my hypothesis is that arith.solver=6 is very good for data flow (complex arithmetic, many equalities) but very bad for ordering (simple/no arithmetic, inequalities) whereas arith.solver=2 deals a lot worse with the former but a lot better with the latter.
If that is true, then I expect arith.solver=2 to outperform arith.solver=6 on QF_IDL benchmarks in general.