[Why3-club] encoding of real.From_Int in cvc4 driver

Claire Dross dross at adacore.com
Thu Jan 31 14:56:00 CET 2019

Hi Why3 team,

while working on the port of SPARK to the current master of why3, I 
noticed that we have a difference between our current driver for smtlib 
and the driver from why3 master. In gnatwhy3, we have some mappings, in 
particular from real.From_Int to to_real. I don't see such a mapping for 
CVC4 in the master of Why3. Is there a reason for that?

Here are the additional mappings in smt_libv2.gen in gnatwhy3:

theory real.Abs
   syntax function abs "(ite (>= %1 0.0) %1 (- %1))"

   remove allprops

theory real.MinMax
   syntax function min "(ite (< %1 %2) %1 %2)"
   syntax function max "(ite (< %1 %2) %2 %1)"

   remove allprops

theory real.FromInt
   syntax function from_int "(to_real %1)"

   remove allprops

theory real.Truncate
   syntax function truncate "(ite (>= %1 0.0)
                                  (to_int %1)
                                  (- (to_int (- %1))))"
   syntax function floor "(to_int %1)"
   syntax function ceil "(- 1 (to_int (- 1.0 %1)))"

   remove allprops

Thanks for your help,

Claire Dross, PhD
Software Engineer
<dross at adacore.com>

More information about the Why3-club mailing list