[SMT-LIB] Suggestion : rational constants

[Morgan Deters]

Hi Remi,

On Tue, Aug 30, 2011 at 9:12 AM, Rémi Delmas <Remi.Delmas at onera.fr> wrote:
> Hi Morgan, thank you for the hints. I wasn't aware that what you mentioned
> in your reply was allowed by the standard (is it really in the standard
> definition?)

They are in the "official" theory and logic definitions hosted at
smtlib.org.  They are not officially part of the standard document
itself, but they define logics and theories of interest, and the sort
and function declarations in them take effect (as well as any
restrictions, extensions, etc.) when the set-logic command is issued.

/ is nothing special (neither is +, -, *, ...) to the standard, it's
just a function declared and given an interpretation by the Reals
theory:

    http://goedel.cs.uiowa.edu/smtlib/theories/Reals.smt2

Your example (copied below) is ill-formed for LIA---in LIA, there is
no sort "Real" or division operator "/".  If I change LIA to LRA in
your input script, it passes the online Z3 demo (and perhaps the z3
binary you have as well).

Best,
Morgan

> Z3 does not seem to support these conventions as of today:
>
> $ z3 -in -smt2
> (set-logic LIA)
> success
> (declare-fun x () Real)
> success
> (assert (= x (/ 1 3)))
> (error "WARNING: Sort mismatch for argument 1 of (/ 1::Int 3::Int)
>
> Expected sort: Real
> Actual sort:   Int
> Function sort: (define / Real Real Real).
> ERROR: line 3 column 22: expression is not well sorted.")

Morgan
-- 
Morgan Deters
Postdoctoral Research Scientist
Courant Institute of Mathematical Sciences
251 Mercer St., New York, NY 10012
mdeters at cs.nyu.edu - http://cs.nyu.edu/~mdeters/