Error solving for boolean operations

[Heaven2024]

Hi!
cvc5 1.1.3-dev.291.900587976 [git 9005879 on branch main]
ubuntu:22.04

cvc5  --produce-models test.smt2
unknown
(
(define-fun uf4 ((BOUND_VARIABLE_438 Bool) (BOUND_VARIABLE_439 Bool) (BOUND_VARIABLE_440 Bool) (BOUND_VARIABLE_441 Bool)) Bool false)
(define-fun v8 () Bool false)
(define-fun v9 () Bool false)
)

cat test.smt2
(set-logic UF)
(declare-fun uf4 (Bool Bool Bool Bool) Bool)
(declare-fun v8 () Bool)
(declare-fun v9 () Bool)
(assert (uf4 true false true false))
(assert (forall ((q23 Bool)) (or (xor v9 q23 q23 v8 q23) (exists ((q9 Bool)) (and q9 (uf4 q9 q23 q9 v8))))))
(assert (not (uf4 v9 true false v8)))
(check-sat)
(get-model)

Obviously this problem is sat（z3,yices can solve correctly),and In fact, this model is correct but it is wrongly return unkown? For a similar example, it can solve it correctly：

(set-logic UF)
(declare-fun uf4 (Bool Bool Bool Bool) Bool)
(declare-fun v8 () Bool)
(declare-fun v9 () Bool)
(assert (uf4 (or true false) (and true false) (xor true false) (not false)))
(assert (forall ((q23 Bool)) (or (xor v9 (not q23) q23 v8 q23) (exists ((q9 Bool)) (and q9 q9)))))
(check-sat)

You can check this out when you have time. thanks :)

[martin-cs]

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?

[Heaven2024]

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.

[ajreynol]

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.

[Heaven2024]

--finite-model-find

I learned, thanks for the guidance :)