search

cvc5 / cvc5-projects

1 stars 0 forks source link

Completeness of set theory with set comprehension #457

Open fhoushmand opened 3 years ago

fhoushmand commented 3 years ago

Hi, the input.zip consists of three simple assertions with no quantifiers (theory of sets and uf). CVC4 produces unknown even with the following options. I have checked cvc5/cvc5#6274 and tried both finite-model-find and full-saturate-quant options with no luck. Are there other options to try? Because it seems to me that this example should not hit the limit of CVC4.

Command line arguments: cvc4 --sets-ext --finite-model-find input.smt2 CVC4 version/commit: CVC4 1.8 Operating system: CentOS Linux 7

ajreynol commented 3 years ago

Thanks for the benchmark. Set comprehension should generally be thought of as a quantified formula, so cvc5 is expected to be incomplete in general when comprehension is present. I'm marking this "performance" and will look into this in more detail.

fhoushmand commented 3 years ago

Thanks!