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

[Jochen Hoenicke]

Hello,

2014-07-19 8:22 GMT+02:00 Martin Brain <martin.brain at cs.ox.ac.uk>:
> On Fri, 2014-07-18 at 11:16 -0700, Levent Erkok wrote:
>> I think the point is that such queries should be rejected by compliant
>> solvers. Or, contrapositively, any solver not rejecting such a query is
>> non-compliant with the standard. This follows from the core theory
>> definition in
>> http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r10.12.21.pdf,
>> page 30; which requires equality to receive the same "sort" for its
>> arguments.
>
> The problem with requiring all compliant solvers to reject non-compliant
> input is that it prevents developers adding their own extensions.  As I
> understand it, SMT-LIB is written to support authors in further
> developing and extending the language.

I just wanted to point out, that the syntax may be officially correct.
There is an extension in AUFLIRA and AUFNIRA.

>From http://smtlib.cs.uiowa.edu/logics/AUFLIRA.smt2

 "For every operator op with declaration (op Real Real s) for some sort s,
  and every term t1, t2 of sort Int and t of sort Real, the expression
  - (op t1 t) is syntactic sugar for (op (to_real t1) t)
  - (op t t1) is syntactic sugar for (op t (to_real t1))
  - (/ t1 t2) is syntactic sugar for (/ (to_real t1) (to_real t2))
 "

One can now argue whether the equality symbol is declared as (= Real
Real Bool), since it is really a polymorphic operator. Of course, if
the solver supports this extension, then it should also produce the
right result, i.e., (= 0 0.5) is unsatisfiable.

Our solver smtinterpol (which only supports the inofficial logic
QF_AUFLIRA) has some code that is only used to support this extension.

Regards,
  Jochen