Model formats that are currently ambiguous

[barrettcw]

Email from Francois Bobot (Feb 15, 2023):

Hello!

we want to try out some new, experimental divisions in the
Model-Validation Track of future SMT Competitions; if possible even one
or two already this year. Candidates for new divisions are
QF_NonLinearIntArith (QF_NIA, QF_NIRA), QF_NonLinearRealArith (QF_NRA),
QF_Datatypes (QF_DT, QF_UFDT), and QF_Array (QF_AX). This means we need
to define acceptable formats for models in these divisions. Please send
us your preferred model formats for the associated logics and existing
model formats if you already have a solver that returns a model for one
of the associated logics. Of particular interest to us are answers to
the following questions:

How do you (want us to) represent the value of an array constant?
How do you (want us to) represent irrational algebraic numbers as
values
of constants?
How do you (want us to) represent the undefined part of the projection
function in datatypes?
At the same time clarification for how to represent the model for
division by zero is welcomed.

[fontainep]

Possible solutions:
using choose to describe the values, but this might be too powerful, allowing arbitrary formulas to describe values.
For algebraic numbers, we could introduce higher order functions, e.g.
sqrt2 = polynomial_solution_int(0,2, lambda(x, x² - 2))
sqrt2 = polynomial_solution_ord(2, lambda(x, x² - 2))

[barrettcw]

Again, from Francois (Sep 20 2023):

Hi Cesare,

Le mercredi 20 septembre 2023 à 16:28 +0000, Tinelli, Cesare a écrit :
Clark, Pascal and I are finally looking at how to extend the definition of the SMT-LIB model format to address a number of requests.

I seem to remember that at some point, you had a concrete proposal for arrays, algebraic numbers and possibly more. Would you mind sharing that proposal with us again? We have lost track of it.

The proposition for algebraic number and arrays is described at https://smt-comp.github.io/2023/model.html .

The proposal described for partial functions has been a lot less welcomed (it feels like keeping digging in the wrong direction). The proposal from Martin Brain to totalize partial functions using a default argument has been viewed by many as the most reasonable and useful.

Concretely the proposal is to add a final argument to every partial functions that is returned when the normal argument are not part of the domain of the mathematical function:

(div x y def) returns def if y is 0 and otherwise the division of x by y

The list of partial functions in the current SMTLIB:

• ADT destructors
• fp.min, fp.max fp.to_ubv, fp.to_sbv
• int: div and mod
• real: division
• string?

An advantage is that theories like QF_NRA would not contain anymore "hidden" uninterpreted functions. Indeed the previous behavior is obtained by explicitly declaring an uninterpreted function:

(declare-fun mydiv0 ((Real x)) Real)

(define-fun mydiv ((Real x)(Real y)) (div x y (mydiv0 x))

Uninterpreted functions does not need to always be defined, for example when translating match to test/destructor it is known that the valuation does not depend on the default value, so a constant can be used:

(ite (is_cons l) (... (hd l 0)...) (...))

For a transition period both version with and without the final argument would be accepted. Model could be requested in both cases but the model would be complete only if the version with default argument is used. Indeed if the version without default argument is used, the value chosen in the corner cases will not be available to the user.

Thank you all for grooming with care the SMTLIB,

Best,

--
François

[fontainep]

From the discussion on October 4th, on arrays: an easy first step would be to add to the existing features to describe models of array an array constant operator. Models for arrays could then be described by abstract values, stores, and this new array constant. As a second step, as SMT-LIB gets HOL stabilized, we could introduce (axiomatize) a function to array operator.

[fontainep]

For the non-linear arithmetic theory, we would basically go with the solution from the SMT-COMP proposal. It would require to introduce a n-ary function coef...

[tinelli]

About arrays, this would be along the lines of the SMT COMP proposal.

[tinelli]

The coeff function would have to be a multi-arity functions. We need to introduce this into the language, perhaps using a :multiargs attribute,

[tinelli]

The arity of coeffs could be

((! Real :multiargs) (-> Real Real))

where it can have one or more arguments of sort Real and return a univariate polynomial as a function from Real to Real.
In effect coefficient would be a family of functions.

(coeffs p_0 p_1 ... p_n)