Order of definitions in models

[Gbury]

During the last SMT-COMP, there was an issue where a solver (cvc5 in this case) generated a model where the definition of a symbol/constant used a symbol/constant that was defined later in the model (and dolmen refused that model). It is not very clear whether the standard allows such models or not, so this issue is to ask for a clarification on whether this should be allowed, or whether models should be defined in a particular/defined order.

Personally, I'd argue for models to be at least defined in topological order (i.e. every constant is defined before being used), so let me copy part of my answer in the mentioned issue:

I'd argue that it's better for solvers to produce models in topological order, because 1) it makes it far easier to check, but also 2) I think it makes more sense: indeed, in the rest of the standard, typechecking of terms follows the regular scoping rules, and in particular terms cannot refer to constants declared later (that's why we have dedicated define-fun-rec commands, which are allowed in models) and 3) it is a good guard against accidental infinite recursive values (such as an infinite list) which I'm not sure we want to allow (and would probably make dolmen loop infinitely in the current state).

If one wants to go further, in order to make model validation as efficient as possible, the best things would be to have definitions in the model be in the same order as the declarations of the corresponding symbols appear in the original problem file. However, that may be too restrictive/annoying to implement for solvers.

In conclusion, I think requiring topological order of definitions is a reasonable constraint, helps prevent unwanted (and dangerous) situations such as infinite recursive values, and does not restrict expressiveness since there are dedicated commands to define recursive values.

[fontainep]

Hi Guillaume,

thanks for your comment! Clark, Cesare, and I discussed and worked on the issue. Here is a draft of a change that should fix the issue.

What do you think?

Best,

Pascal (also for Cesare and Clark)
model_proposal.pdf

[Gbury]

Hi Pascal,

That seems to fix the problem I raised indeed. That being said, your proposal also seem to forbid using theory-defined symbols in the terms for model values ?

For instance, +, or * will never be in the category of function symbols that have been "previously defined in the model or is one of the symbols being recursively defined" (at least in a problem using arithmetic). Is is intended that such function symbols are forbidden in model values ?

[Gbury]

Actually, after having thought about it some more: some models actually do require the use of theory-defined function symbols (which, as far as I understand it, would be forbidden by the proposed new spec, since they are not defined in the model). For instance:

• in arithmetic, there are no negative literals, therefore, negative values necessarily need at least eh - symbol
• similarly in real arithmetic, fractions need to use the / symbol to be expressed
• in the array theory, one needs to use the store and select function symbols to create any non-abstract value
• in the end even literals, such as 1 are technically defined by the arithmetic theory, and could be understood as being function symbols (with arity 0), that are not defined "previously in the model", nor "recursively defined".

So, I think that theory-defined function symbols must also be allowed, and the wording of the restriction should be adapted to make it clear that they are allowed.

[fontainep]

Hi Guillaume,

Thanks for your comment! You are right, we clarified that we meant that user symbols must be properly ordered. Theory symbols can indeed occur in definitions.
https://smt-lib.org/papers/smt-lib-reference-v2.7-draft.pdf

[Gbury]

That seems great ! Thanks for the effort