Error solving for boolean operations about cvc5 HOT 4 CLOSED

It is likely returning unknown because the algorithm that is handling the quantifiers is incomplete in the general case. In this specific case it is complete but perhaps we don't test for that. Probably because quantification over Booleans is not that common in our usecases. From the working example it looks like this is a quantifiers / UF interaction.

Have you minimised these? Does uf4 need to have four arguments?

from cvc5.

It is likely returning unknown because the algorithm that is handling the quantifiers is incomplete in the general case. In this specific case it is complete but perhaps we don't test for that. Probably because quantification over Booleans is not that common in our usecases. From the working example it looks like this is a quantifiers / UF interaction.

Have you minimised these? Does uf4 need to have four arguments?

yes it is. At the beginning, uf4 was solved with two parameters, and it could be processed correctly. I tried adding two parameters, but there was a problem with the logic.

from cvc5.

Hello, cvc5 can solve the attached benchmark with the command line --finite-model-find. Unfortunately, this option is not enabled by default, as it enables techniques that degrade performance on unsat queries.

For more information, I have a flowchart that summarizes which options to use with cvc5 when handling quantified formulas: https://homepage.cs.uiowa.edu/~ajreynol/flowchart-quantifiers.png

We are planning to make this flowchart more accessible to users who run into these kinds of issues.

from cvc5.

--finite-model-find

I learned, thanks for the guidance :)

from cvc5.