Add smtzilla

[hra687261]

The purpose of the PR is to experiment with using machine learning models to try to select the best SMT solver for a given query.

A minimalist "smtzilla" solver was added which only does check_sat and get_model.

Among the things I am planning to do:

• We should think of how other functions of the API should be supported.

• Currently the selection is only done between Z3 and Bitwuzla, but it should be easy to extend this such that it selects the best solver among those installed (and ignores the models of those that are not).

• Currently the solver that is used for get_model is always the one that was last used for a check_sat , but as we have seen in Owi, for a given query, the best solver to do a check_sat with is not always the best solver to do get_model with, so two kinds of models are needed, one for when we just do a check_sat, one for when it is followed by a get_model.

  • for this we probably want a function that does check_sat_get_model to know in advance, if we will need a model from a given query or not and to be able to measure both the time of the check_sat and the get_model for that query.

(The code used to train models will be added shortly to symbocalypse OCamlPro/symbocalypse#32, but I am thinking that maybe it has its place in smtml actually)

[redianthus]

I am thinking that maybe it has its place in smtml actually

Yes, I think it definitively belongs to Smtml. Symbocalypse should only be used to generate datasets.

We should think of how other functions of the API should be supported.

I think we need get_sat_model in Owi.

Currently the selection is only done between Z3 and Bitwuzla, but it should be easy to extend this such that it selects the best solver among those installed (and ignores the models of those that are not).

It's probably fine as a first step! :)

for this we probably want a function that does check_sat_get_model to know in advance, if we will need a model from a given query or not and to be able to measure both the time of the check_sat and the get_model for that query.

Yes, and actually such function already exists (it is get_sat_model and that's what we already use in Owi so it's perfect! :-))

[filipeom]

Hi! Thanks for the PR it looks amazing! 😃

The purpose of the PR is to experiment with using machine learning models to try to select the best SMT solver for a given query.

A minimalist "smtzilla" solver was added which only does check_sat and get_model.

Among the things I am planning to do:

• We should think of how other functions of the API should be supported.

Like push and pop? I think we could probably just do something similar to the Batch solver and have a stack of expressions no? We just need to ensure the correct expressions are passed to check (although doing this would negate any incremental solving from the individual solvers?)

• Currently the selection is only done between Z3 and Bitwuzla, but it should be easy to extend this such that it selects the best solver among those installed (and ignores the models of those that are not).

• Currently the solver that is used for get_model is always the one that was last used for a check_sat , but as we have seen in Owi, for a given query, the best solver to do a check_sat with is not always the best solver to do get_model with, so two kinds of models are needed, one for when we just do a check_sat, one for when it is followed by a get_model.

  • for this we probably want a function that does check_sat_get_model to know in advance, if we will need a model from a given query or not and to be able to measure both the time of the check_sat and the get_model for that query.

I think I'm ok with merging a preliminary version without all these features and add them later. I think the current PR is already a lot of progress 😃

[hra687261]

Like push and pop? I think we could probably just do something similar to the Batch solver and have a stack of expressions no? We just need to ensure the correct expressions are passed to check (although doing this would negate any incremental solving from the individual solvers?)

I agree that something like that should work, I will look into it.
Alternatively, maybe simply calling push and pop for all existing solver instances should suffice? But in that case, if a new solver instance is created after the other ones, we should remember when we did the pushs and pops so that we can apply them again.
push and pop only apply on assertions added the add function right? When we check the list of assumptions is not affected since these ones are not added, right? (If I remember correctly, check/check_set behave like check-sat-assuming in the SMT-LIB standard)

I think I'm ok with merging a preliminary version without all these features and add them later. I think the current PR is already a lot of progress 😃

The PR is starting to get a bit too big as well, so I agree that we can merge a preliminary version and I'll add the other features later. Once I add push and pop, I'll put it as ready for review and we can try to merge it then.

[hra687261]

The Nix CI failure is the same as the one in Owi, maybe someone more familiar with Nix/CIs has an idea of why its happening?

[redianthus]

It seems like a containerd bug which is specifically triggered by the nix image:
containerd/containerd#12683 :S

EDIT: see also actions/runner-images#13682

[filipeom]

Thanks! The code looks great! 😃

[hra687261]

Thanks!