[SMTCOMP] The infinite-precision issue again

Albert Oliveras Llunell oliveras at lsi.upc.edu
Mon Jul 10 08:23:24 EDT 2006


Hi all,

first of all I would like to thank you for your detailed answer. These
are my reactions:

>So we would really need to stay with that decision at this point, since
>we had no complaints and the competition is coming up soon.
>  
>

Sure, I completely understand and accept that.

>Finally, even if the jury is still out on whether native arithmetic
>confers a crucial advantage on benchmarks of interest, supporting
>arbitrary precision numerals is more robust, and hence requiring such
>support seems like a reasonable default position in the absence of
>more evidence.
>
>  
>

Of course, if I had to choose between robustness and efficiency,
I would definetely choose robustness. However, the point I wanted to make
is that we should be careful about losing efficiency by incorporating
extensions that do not lead to a real gain in robustness. I thought that
big number support could be problematic in this direction, and this is
why I raised
this point. However, I am not religious about that. I fully understand
your explanations
and indeed they seem quite reasonable to me.

I hope to meet you all at Seattle and discuss about this and other issues.

Cheers

Albert


-- 
_______________________________________________________________________
Albert Oliveras Llunell                       www.lsi.upc.edu/~oliveras
Technical University of Catalonia (UPC)       oliveras at lsi.upc.edu
Dpt. Llenguatges i Sistemes Informatics(LSI)  Phone:   +34-93-4137861
Jordi Girona 1, E-08034 Barcelona, Spain      Fax:     +34-93-4137033
_______________________________________________________________________




More information about the SMT-COMP mailing list