[SMT-LIB] Mixing Integers and Reals in SMT2 formulas

[Tinelli, Cesare]

Jochen and all,

On 19 Jul 2014, at 09:48, Jochen Hoenicke <hoenicke at informatik.uni-freiburg.de> wrote:

> 
> One can now argue whether the equality symbol is declared as (= Real
> Real Bool), since it is really a polymorphic operator.

This is a subtle point, but strictly speaking we abuse the terminology when we say that equality is polymorphic in SMT-LIB 2. In SMT-LIB 2's underlying logic no function symbols are polymorphic because the logic does not have have parametric types.

We use a poor man's version of polymorphism where we allow theory function symbols to be overloaded with an infinite set of types/ranks described schematically.

For example, the type of = is not really  alpha x alpha -> Bool  but  s x s -> Bool *for each sort s*.

In particular then, = does have type Real x Real -> Bool .


Cesare


PS: For those who are puzzled by the difference above, in a truly polymorphic logic, type parameters range over all (uncountably many) subsets of a sufficiently large universe. In SMT-LIB 2, sort parameters range over (countably many) sort terms. For all practical purposes, in our case, this difference is immaterial, but it exists.


> Of course, if
> the solver supports this extension, then it should also produce the
> right result, i.e., (= 0 0.5) is unsatisfiable.