I'm currently using CVC4 to solve formulas of the following form:
exists f1, ..., fn . P(f1, ..., fn) /\ forall (b1...bk) . Q(f1,...fn,b1,...bk)
Here, the f1...fn are functions from some number of Bool to Bool, and the
b1...bk are boolean values.
My problem falls squarely into the UF fragment of SMT: it has quantifiers, but no sorts other than Functions and Booleans.
When I try my problem with the default settings on CVC4, it immediately returns Unknown, despite the fact that all my quantification is over finite domains.
The problem is, CVC4 has an extremely large number of options for dealing with quantifiers: there's a bunch of cegqi, a bunch of fmf, there's mbqi, etc. I get the impression that most of these were added from specific research projects, and I'd rather not have to read through 20 different papers just to get my solution going.
My question: Is there a recommended set of options for solving this kind of problems?
I know it's possible with CVC4, since they competed and performed quite well at the UF Track of the SMT competition, but I can't find the specifics arguments used for that competition.
You can try "--finite-model-find" which more info can be found here: Exactly what quantifiers is SMT complete for?
If that doesn't work you might want to try looking through the configuration used in the smt-comp: https://www.starexec.org/starexec/secure/details/configuration.jsp?id=220723 I found the option there first and then had the stack-overflow question pointed out to me.