Add support for Ufs with 0 arguments for all solver / bugfixes

[daniel-raffler]

Hello,

this PR adds support for Ufs with no arguments to Bitwuzla and Boolector, where it was still missing. It also fixes various bugs on Princess, CVC4 and CVC5 where 0-ary Ufs and variables where treated as different symbols: Since all of these solvers are using a variable cache, it is our job to make sure that no duplicate symbols are created and (uf) and uf are treated the same

[kfriedberger]

Is this PR a solution to the old issue #171 ? If yes, please document the new rules for nullary UFs and variables.

Is there a difference in plain SMTLIB2 between nullary UFs and variables for parsing? Abd how do solvers handle each case?

[daniel-raffler]

Hello Karlheinz

Is this PR a solution to the old issue #171 ? If yes, please document the new rules for nullary UFs and variables.

Yes, I think it closes it and I'll add some documentation. Most solvers expect at least one argument when defining a UF and will throw an exception otherwise. In that case we simply return a variable as a workaround. It's often hard to say if the solver considers variables and 0-ary UFs the same as most solvers allows multiple variables with the same name. It's then up to the variable cache (= us) to decide if they are identical

Is there a difference in plain SMTLIB2 between nullary UFs and variables for parsing? Abd how do solvers handle each case?

In Smtlib nullary Ufs and variables are the same:

(declare-const f τ) has the same effect as the command (declare-fun f () τ)

(page 67, here)

In JavaSmt it's a bit more complicated as declareUF returns a FunctionDeclaration and not a Formula. However, we can guarantee that after applying the nullary UF the result is the same as when just declaring a variable

[baierd]

Good step towards uniform behavior! Thank you!

In Smtlib nullary Ufs and variables are the same
However, we can guarantee that after applying the nullary UF the result is the same as when just declaring a variable

The important part here is that all solvers need the same behavior. So we need tests that check the cases:

• Create a 0-ary UF with some name and a variable with the same name (both directions) with equal and not equal types. Behavior here needs to be consistent.
• Are 0-ary UFs treated the same as variables for (basically) all operations? Especially quantifiers and visitor/rebuilding needs to be checked.

[PhilippWendler]

What weighs higher?

1. If nullary UFs are supported: the inconsistency and potential surprise / risk of errors that when users create a nullary UF and then visit the formula, they do not see a UF but a variable.
2. If nullary UFs are forbidden: the inconsistency and potential hassle if users have code that does not care about argument count and simply want to use the same code/API for all arities of UFs (but note that even if nullary UFs are allowed to be created, these users would not be able to achieve their goal when visiting formulas), plus the backwards incompatibility for those solvers where JavaSMT already allowed nullary UFs.

To me the answer is not obvious, but I think this question is important and should be discussed deliberately before committing to one of the options.