Recursive functions in models

[Halbaroth]

The SMT-LIB standard allows only three statements in models: declare-fun, declare-fun-rec and declare-funs-rec for respectively non-recursive functions, recursive functions and mutually recursive functions. Currently, Alt-Ergo prints all its declarations with declare-fun only.

We could print everything with declare-fun-rec but it would neater to recognize recursive values.

[bclement-ocp]

declare-fun-rec and declare-funs-rec do not exist in the SMT-LIB standard, do you mean define-fun-rec and define-funs-rec?

In any case, correct me if I'm wrong, but I don't think the solver is able to generate recursive functions atm, so this looks much more involved than printing issues (unless there is support in #776 maybe)?

[Halbaroth]

I meant declare-func-rec ;)

Sure, the solver cannot produce recursive functions yet. I wrote a function to produce dummy values in many cases. If I add the case of recursive functions, the solver should print it with the appropriate SMT-LIB statement.

[Halbaroth]

There is no support in #776 for recursive functions.

[bclement-ocp]

I meant declare-func-rec ;)

Can you point me to a page in the standard? I can't find declare-func-rec there either.

Sure, the solver cannot produce recursive functions yet. I wrote a function to produce dummy values in many cases. If I add the case of recursive functions, the solver should print it with the appropriate SMT-LIB statement.

I don't understand why we want to have support for printing values we cannot produce. Why can't we deal with this when (if) we add support for producing recursive functions?

[Halbaroth]

When I opened this issue, I thought we could have to produce dummy values for recursive functions but in fact, the only case where we could produce them easily is when there is no constraint at all on the value. But recursiveness is a constraint... So we can always produce non-recursive function for dummy values!

For the standard, looks for model_response.

[bclement-ocp]

When I opened this issue, I thought we could have to produce dummy values for recursive functions but in fact, the only case where we could produce them easily is when there is no constraint at all on the value. But recursiveness is a constraint... So we can always produce non-recursive function for dummy values!

Yeah, there is no need to build recursive functions for dummy values.

For the standard, looks for model_response.

model_response is defined in terms of define-fun / define-fun-rec / define-funs-rec there is no declare-func-rec? I am still confused.

[Halbaroth]

.. I meant define-... XD

[Halbaroth]

Of course, you cannot declare uninterpreted symbol in the model ;)