[SMT-LIB] Suggestion : rational constants

[Rémi Delmas]

Hi again,

My suggestion was in fact a means to specify rational constants in LIA 
(in addition to decimals), which does not use any operators not in the 
theory, hence the specific notation 'N:D'. Sorry I wasn't specific 
enough in my first post.

/Rémi

On 30/08/2011 19:20, Morgan Deters wrote:
> 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


-- 
Rémi Delmas
Remi.Delmas at onera.fr
+33.5.62.25.26.54
http://www.onera.fr/dtim/systemes-critiques/
ONERA BP4025
2 avenue Edouard Belin
FR-31055 TOULOUSE CEDEX 4