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