cvc5 reports unknown in "apparently simple" quantifier tests about cvc5 HOT 7 CLOSED

@ajreynol Thank you, that clarifies things a lot for me!

Right now a HolSmt user should only care about unsat, as that's the only significant result in most real-world cases. However, HolSmt tests do test for sat results and in the long-term, I expect sat results to be significant to users as well, corresponding to false theorems more often, once the translation from HOL -> SMT-LIB becomes more complete and doesn't generate as many uninterpreted symbols. That is, unless I'm missing something, of course (quite possible).

It sounds like mbqi should be a good compromise, although it flies in the face of my instinct to imitate what F* has done. However, it really sounds like the best long-term solution would be to do a sort of "portfolio approach", where multiple cvc5 processes would try to solve the same problem in parallel, each using one CPU core and running with slightly different options. This is similar to what zipperposition and eprover have done, and I'm sure many others as well (like Isabelle I think?). I mean, most of the time my CPU cores are idle, might as well use them for something useful when I'm trying to prove something.

I envision this could be implemented as a script that wraps cvc5. In fact, it could be something almost identical to the script that @hansjoergschurr linked to, but running cvc5 multiple times in parallel (in the background) rather than in sequence. This script would kill all remaining background processes once the first sat or unsat result is obtained, to avoid wasting CPU time. With some more effort, you could even adapt the script to run cvc5 in a more powerful remote machine, if necessary.

But I think for now I will leave cvc5 running without any such parameters, suggesting the user to override the path to the cvc5 binary with the path to a specific implementation of such a script (since they already have to manually configure the path anyway).

Thanks!

EDIT: for those who are in the same situation, this blog article might also be a relevant read.

from cvc5.

There are a variety of options to make cvc5 put "more effort" into quantifier instantiation, including:
--mbqi
--finite-model-find
--enum-inst
Most of these options solve the given problems.

As more explanation, by default, cvc5 will only will apply E-matching and conflict-based instantiation for quantified formulas, since many users would prefer an answer of "unknown" instead of timing out. The intuition is if these light-weight techniques don't solve quickly, we answer "unknown".

Z3 also has a similar option smt.mbqi which in contrast is enabled by default, as I recall.

from cvc5.

I vaguely remember that F* heavily uses triggers to guide the instantiation process. They might turn off instantiation procuedures to aid that.
A possible source of inspiration for options to try are the competiton scripts: https://github.com/cvc5/cvc5/blob/main/contrib/competitions/smt-comp/run-script-smtcomp2023
Note however that some options used there are expermental. Furthermore, some option combinations in those scripts are intentionally limted, but complementary to other option combinations.

from cvc5.

@someplaceguy Most applications that use SMT solvers and are developed for any length of time wind up developing some kind of portfolio. Sometimes it is one solver and several sets of options, sometimes it is multiple solvers, sometimes it is both. Some libraries like https://github.com/stanford-centaur/smt-switch/ aim to make this easier ( https://github.com/stanford-centaur/smt-switch/blob/master/include/portfolio_solver.h ).

from cvc5.

@ajreynol Thanks for your quick response and suggestions!

I'd like to find a reasonable default set of options that would work well for typical software verification purposes (I know, that's not saying much... oh well 😆 ).

In my case, I think I'd much rather prefer that cvc5 times out more often (as opposed to quickly replying unknown), if that also leads to more unsat/sat results (each one potentially saving several minutes worth of manual proof effort), rather than giving up prematurely just to save a few seconds worth of CPU time.

Regarding your suggestions:

• --mbqi: I'd much rather leave this off, if possible. Whenever I'm in doubt, I always look into how F* uses Z3, since the level of performance they have achieved would be perfect for my needs. Apparently, they are explicitly disabling mbqi: (set-option :smt.mbqi false), so according to my ignorance in the matter, I'm inclined to do the same unless there's a very good reason not to.
• --finite-model-find: This indeed works for these examples and doesn't seem to cause any regressions in our (small) test suite! So I guess I will add this as a default option for now.
• --enum-inst: This works for the first example but not for the second, so I'm tempted to leave it off.

I also noticed cvc5 has an overwhelming (well, overwhelming to me) amount of options in its "quantifiers" module, but I wouldn't know how to choose a good set of options from there, since I don't really know many details about how SMT solvers are implemented... I guess it's just a matter of waiting to see if I run into any roadblocks as I go along, and then check if anything from there might help, I guess.

In any case, many thanks and feel free to close the issue!

from cvc5.

I vaguely remember that F* heavily uses triggers to guide the instantiation process. They might turn off instantiation procuedures to aid that.

Indeed, they do that and they also limit how much some of those triggers are triggered by using the concept of "fuel", e.g. to limit how much Z3 tries to unroll/unfold the definition of a recursive function (since you almost never need to unfold a function more than a handful of times to prove something about it). Their inductive datatypes are also encoded using fuel to prevent infinite unfoldings.

Note, however, that in this specific case, Z3 is able to solve both these examples with mbqi disabled and without triggers or any concept of fuel and without any non-default command-line options. However, I don't know what Z3 is doing by default to find these solutions or what would be its equivalent in cvc5, e.g. I don't know whether Z3 does the equivalent of --finite-model-find by default.

A possible source of inspiration for options to try are the competiton scripts: https://github.com/cvc5/cvc5/blob/main/contrib/competitions/smt-comp/run-script-smtcomp2023 Note however that some options used there are expermental. Furthermore, some option combinations in those scripts are intentionally limted, but complementary to other option combinations.

This is great, thank you! This will definitely greatly reduce my search space if I hit some roadblock in the future. Many thanks!

from cvc5.

Some more notes here:

Conceptually --finite-model-find is a "heavier hammer" version of --mbqi. In detail it enables techniques from https://homepage.divms.uiowa.edu/~ajreynol/cade24.pdf which are good in some cases for "sat" but are expected to degrade the performance for "unsat".

In general mbqi should not degrade "unsat" performance too much, should be good for "sat" (although not as good as finite model finding for quantified formulas over small domains).

--enum-inst enables https://homepage.divms.uiowa.edu/~ajreynol/tacas18.pdf which is IMHO the best option for improved "unsat". However, it has no ability to answer "sat".

Summarizing:
If you only care about "unsat", I recommend --enum-inst.
If you care about "sat" and the domains of quantified formulas are uninterpreted/small, I recommend --finite-model-find.
If you care about "sat" and the domains of quantified formulas are infinite, I recommend --mbqi.

from cvc5.