[SMT-LIB] Suggestion : rational constants

[Rémi Delmas]

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?)

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.")

On 30/08/2011 00:44, Morgan Deters wrote:
> Hi Remi,
>
>> as of today the standard allows decimals constants, how about allowing
>> rational constants specified as N:D, with N and D two arbitrary precision
>> integers ?
>
> I guess it's not covered by the "standard" document itself, but there
> already are forms:
>
>    (/ m n)
>    (/ (- m) n)
>
> provided by the Reals theory (for m, n appropriate numerals), and
>
>    (/ (to_real m) (to_real n))
>    (/ (- (to_real m)) (to_real n))
>
> in the Reals_Ints theory.  In some (all?) logics that use Reals_Ints,
> there is additionally syntactic sugar defined:
>
>    (/ t1 t2) is syntactic sugar for (/ (to_real t1) (to_real t2))
>
> In "linear" logics, the use of "/" is banned _except_ for such use as
> rational literals.
>
> This should cover (substantially) everything that your N:D proposal
> would, I think...
>
> Best,
> 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