Cannot get parameter of func decl of floating-point numeral expression

[pclayton]

For a func decl d of a floating-point numeral expression:

• Z3_get_decl_kind (ctx, d) returns Z3_OP_FPA_NUM.
• Z3_get_decl_num_parameters (ctx, d) returns 1.
• Z3_get_decl_parameter_kind (ctx, d, 0) returns Z3_PARAMETER_FUNC_DECL.
• Z3_get_decl_func_decl_parameter (ctx, d, 0) fails with the message invalid argument.

This can be seen in Python. The code

from z3 import *
fpSort = FPSort(8, 24)
x = fpSort.cast(1.0)
d = x.decl()
assert d.kind() == Z3_OP_FPA_NUM
d.params()

produces the following:

Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "C:\msys64\usr\share\python\Lib\site-packages\z3\z3.py", line 832, in params
    result[i] = FuncDeclRef(Z3_get_decl_func_decl_parameter(self.ctx_ref(), self.ast, i), ctx)
                            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "C:\msys64\usr\share\python\Lib\site-packages\z3\z3core.py", line 3020, in Z3_get_decl_func_decl_parameter
    _elems.Check(a0)
  File "C:\msys64\usr\share\python\Lib\site-packages\z3\z3core.py", line 1554, in Check
    raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: b'invalid argument'

[pclayton]

I should add that a floating-point numeral expression does not have the ast kind Z3_NUMERAL_AST. Continuing the example above:

>>> Z3_get_ast_kind(x.ctx_ref(), x.as_ast()) == Z3_NUMERAL_AST
False
>>> Z3_get_ast_kind(x.ctx_ref(), x.as_ast()) == Z3_APP_AST
True

This is Z3 4.13.0.

[pclayton]

I feel that something is not quite right somewhere. The reason I encountered the original issue was because a floating-point numeral expression constructed with Z3_mk_numeral (whose func decl has kind Z3_OP_FPA_NUM) never has the ast kind Z3_NUMERAL_AST. This is surprising when the floating-point numeral is a normal value because a floating-point expression constructed with Z3_mk_fpa_fp (whose func decl has kind Z3_OP_FPA_FP) does have the ast kind Z3_NUMERAL_AST if the arguments are bit vector values (i.e. literals). Z3_OP_FPA_NUM seems to be ruled out as a numeral in fpa_decl_plugin::is_unique_value due to non-uniqueness. Could someone explain what it is that is being made unique?

[wintersteiger]

IIRC (and I may not) an OP_FPA_NUM is not unique because it could be any float numeral (including NaN), which don't necessarily have a single representation. The bit-vector versions however are unique. This is the many-NaNs vs single-NaN issue (single NaN in the SMT spec, but still a to_fp for conversion from bit-vectors, and internally Z3 translates back to bitvectors...).

[NikolajBjorner]

OP_FPA_NUM uses an internal parameter which points to a global data-structure. It is opaque from user point of view. I have fixed the (python) bindings to at least not crash. They don't pretend the parameter is a function declaration any longer.