Guarantees about makeVariable

[JohnnyJayJay]

Hi there,

is it guaranteed that two variables created via FormulaManager#makeVariable are the same when the provided name is the same? E.g. if I call it twice with the same FormulaType and name, will the two results be identical in the eyes of the solver?
I see that this is the case for SMTInterpol (the implementation for it appears to have a variable cache), but is this a property of the API or implementation detail?

I'm asking myself the same about UFManager#declareFunction as well.

Thanks in advance.

[kfriedberger]

The API guarantees:

• creating a variable twice with same name and same sort returns the same symbol.
• creating an uninterpreted function twice with same name and same sort (argument sorts and return sort) returns the same symbol.

It depends on the solver whether the following cases are supported:

• creating variables with same name and different sorts.
• creating uninterpreted functions with same namen and different sorts (in arguments and/or return sort).
• creating a variable and an UF with the same name and different sorts.

Those cases are (still?) supported by some solvers, due to historic reason, and the solvers include Z3, Princess, and Bitwuzla. We aim for exception in those cases, but have not yet completed this work (see #172).

[JohnnyJayJay]

Thank you for the swift response! That answers my question.