[Feature request] Setting Solver Logic via JavaSMT

[ThomasHaas]

Is it possible to add a way to set the solver logic from within JavaSMT similar to Smtlib's (set-logic <LOGIC>) command?

This is particularly interesting in the context of incremental solving, because no matter how smart the SMT solver is, with the default ALL logic, he has to assume that subsequent queries introduce new logics.
This can easily be demonstrated with Z3 and verbose=5 on smtlib2 QF_BV queries (outside JavaSMT):

• on non-incremental queries, Z3 bit-blasts and uses its SAT solver even with (set-logic ALL)
• on incremental queries, Z3 runs its general-purpose SMT core with (set-logic ALL), even if the whole file only uses bit vectors. When changing the logic to (set-logic QF_BV), Z3 bit-blasts again.

In the context for program verification, we often do incremental queries (via JavaSMT) that only make use of QF_BV. We have observed that if we dump the generated queries to smtlib2 and simply change the logic from ALL to QF_BV, the solver performance can increase by 50-100%. Granted, there are also cases where changing the logic makes the solver slower, but it is hard to evaluate the exact impact if we have to dump and modify the encoding and then invoke the solver externally.

[baierd]

Hi Thomas,

we discussed this feature a while back, but were not sure how helpful it really is. OpenSMT2 is currently the only solver that can choose the logic, as it needs it and does not support all.

I'll try to take a look at how difficult a general solution for this would be and add it once i can.

[ThomasHaas]

Z3 also has smt.logic as option to set the logic. But I agree that setting the logic has only limited application, even if possible. For example, in the context of concurrent program verification, it is quite natural to capture data flow via QF_BV and ordering constraints via QF_IDL, but the only smtlib theory that combines both is ALL.
To exploit dedicated logic settings, the user either has to bit-blast to reduce the formula to QF_IDL or replace the ordering constraints by a SAT or BV-based encoding (e.g. vertex elimination).

So what would be even more useful in practice is the ability to pass more options to the SMT solver as was requested a while ago.
Regarding QF_BV+QF_IDL, I asked Nikolaj if Z3 can be configured for this setting and it can be (see here). By default, Z3 will use the general-purpose simplex algorithm to solve IDL formulas instead of Floyd-Warshall and currently there is no way via JavaSMT to tell Z3 to use Floyd-Warshall (Floyd-Warshall is almost twice as fast on some benchmarks!).
I suspect that this might affect every single solver backend, e.g., Yices2 also has a Floyd-Warshall solver that is likely inaccessible via JavaSMT (though their documentation claims that the Floyd-Warshall solver is only usable if the logic is also set to QF_IDL ).

EDIT: It turns out that Z3's simplex-based solver (for LIA?) is actually as fast as Floyd-Warshall, but the default solver in Z3 uses LRA-based techniques which don't seem to handle our IDL constraints all too well.

[baierd]

@ThomasHaas i am currently trying to implement logic selection and other option setting for Z3. Do you by chance have access to an example SMT2 program that is only solvable when setting a logic and possibly even two, one with only setting a logic and one that needs a logic and another setting? (I struggle to find good tests that are not solved by Z3 alone)

[ThomasHaas]

I think the settings do not have such dramatic impact that an unsolvable problem becomes solvable (maybe if qunatifier were involved?). But I mentioned a benchmark here where setting arith.solver=3 was twice as fast. You should definitely be able to measure the difference.

IIRC, I also had a case where setting QF_BV as logic was really advantagous, but I need to reconstruct it. Maybe I can do it tomorrow. If you only want to check if the setting works, you can try dumping the statistics of any incremental (needs push/pop) QF_BV formula.
With logic ALL Z3 uses its SMT core but with QF_BV it does pure SAT solving and IIRC you can observe that in the SMT statistics which JavaSMT can generate.

[ThomasHaas]

Here is an example where setting QF_BV solves the problem in around 1 sec and using ALL takes 9 seconds on my machine: manyRegReads.txt
The smtlib2 program is currently set to QF_BV.

[baierd]

Thank you very much!

[ThomasHaas]

I posted another example here Z3Prover/z3#8940 (comment) where changing smt.arith.solver can be up to 8x faster.

[baierd]

@ThomasHaas Thanks again! Seems like the default setting improved a bit. It takes ~9s on my machine. But using Simplex is still much faster. Seems like the options setting is working as expected.

Would you say that you use arith.solver often? Are there some options that you would consider important enough to warrant a dedicated option in JavaSMT?

[ThomasHaas]

Would you say that you use arith.solver often? Are there some options that you would consider important enough to warrant a dedicated option in JavaSMT?

Since the default variant of our encoding generates QF_BV + QF_IDL formulas, I would like to always use the smt.arith.solver=3 option, it's just that right now we cannot use it via JavaSMT :).
Regarding other options: I haven't done much testing there, but most options don't look promising really and only have small effect like, e.g., restart frequency.
The most promising option was multi-threading via the parallel option, but it turns out to only increase verification time.
Stochastic local search and the likes is also quite bad for program verification.
Basically, besides changing the theory and/or the theory solvers, I haven't found any fruitful options yet.

What I still need to try is bv.size_reduce, an option that Nikolaj added upon request, but I could never test it yet really.
Also, with the ability to set QF_BV as logic and hence using only the SAT solver, we might want to experiment with SAT solver-specific options.

[baierd]

OK thanks for the feedback!

We generally want to avoid handing all solver options to users, simply because of the massive amount of options over all solvers. So we usually add a configuration option furtherOptions that takes all non-explicitly declared options and hands them to the solver. This generally works with all options.

It seems like setting the smt.arith.solver option fits well into this furtherOptions category for now.

There are 2 special options that i want to have more control over, logic selection (because i want to move to a JavaSMT internal but common way to select the logic in as many solvers as possible soon) and Z3s engine (because i want to explicitly enable HORN solving and also explicitly build a HORN prover at some point, and spacer is very interesting in that regard). So they have explicit options now that may not be set via furtherOptions (setting them there throws).

You can take a look here if you want to see an example and maybe give some feedback.