[SMT-LIB] Suggestion : rational constants

[Morgan Deters]

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
-- 
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/