Underspecified and partial functions in SMT-LIB

[barrettcw]

From Martin Brain (Jul 13, 2018):

Hi all,
This is not intended as kindling but after last year I said I
would write up the consensus on partial functions that we achieved(?)
during a special discussion session. I have been somewhat slow about
doing this. Anyway:

The Problem

There are a number of functions in SMT-LIB which are not (intuitively)
clearly defined at points. These are:

*. div, mod (Integer)
*. / (Real)
*. fp.max, fp.min
*. fp.to_sbv, fp.to_ubv, fp.to_real

The current approach is to say these are partially specified at the
contentious points. I.E. they act as uninterpreted functions. This is
theoretically sound, by there have been objections to this:

A. Some people feel this is unclear or unintuitive for users.
B. It forces people to implement a UF solver, even when it is not
otherwise needed.
C. It makes the implementation and handling of these more complicated.

The Proposal

1. Each of the functions is replaced in the /theory/ with a total
   version which takes an additional argument. For example:

div_total : Int x Int x Int -> Int
div_total(x,y,z) = { ... as before ... y != 0 }
{ z y = 0 }

2. In the /logics/ QF_UFNIA, QF_UFNRA and QF_UFFP and all logics that
   include them, we add in the existing functions with their current
   definition. For example:

div : Int x Int -> Int
div(x,y) = div_total(x,y, div_zero_case(x,y))

where div_zero_case is a fresh uninterpreted function symbol of type
Int x Int -> Int

Pros and Cons

• All theories are now total.

• Semantically backwards compatible.

• If users disagree with the semantics for these, they can provide
  whatever value they want.

• Inline with many existing implementations.

• If the logic does not include UF, you do not have to implement a UF
  solver.

• Some benchmarks from QF_NRA, QF_LRA and QF_FP will have to be
  reclassified.

• Requires changes to both theories and logics.

• Requires digging up this contentious topic.

Is it enough of an improvement over the current state of things to be
worth doing?

Cheers,

• Martin