[SMT-LIB] Benchmark Conformance: log in AUFLIRA/nasa/

Tjark Weber tjark.weber at gmx.de
Wed Oct 13 08:24:52 EDT 2010


Certain benchmarks in AUFLIRA/nasa/ declare a function

  (declare-fun log (Real) Real)

and apply this function to a numeral: e.g., (log 330) at line 64, column
95 in benchmark AUFLIRA/nasa/fol_simplify/gauss_init_0057.fof.smt2.

As far as I can tell, this is not valid.  Logic AUFLIRA is based on
theory Reals_Ints, which declares NUMERALs to be of sort Int (while
DECIMALs are of sort Real).  The :extensions in AUFLIRA permit implicit
conversion from Int to Real only for binary operators; they do not apply
to the unary function log.  Hence, (log 330) is ill-typed.

I believe that in total, this issue affects at least 549 benchmarks in
AUFLIRA/nasa.

A possible solution would be to write arguments to log as decimals:
e.g., (log 330.0).  Alternatively, one could augment the definition of
AUFLIRA to permit implicit conversion also for unary functions, or even
for functions of arbitrary arity.

Regards,
Tjark



More information about the SMT-LIB mailing list