PV2 ⊧ Daisysynthesises a Scala or C program where performance of floating-point operations are optimised

Application domain/field

• Program approximation
• Performance optimization
• Synthesis

Type of tool

Performance optimizer

Expected input

• Floating-point program with elementary function calls (e.g. sin, `exp
• Domains of all inputs
• Target overall absolute error

Format:

Input file (one single file) should follow the structure:

  import daisy.lang._
  import Real._

  object TestObject {

    def function1(x: Real): Real \= {
      require(0 <= x && x <= 1)

      val z \= x + x
      z \* x

    } ensuring(res \=> res +/- 1e-5)

    def function2 ...
  }

The repository has some more details

Expected output

Optimized program in Scala or C with the guaranteed error below the specified target error

Internals

Framework for verifying and optimizing numerical programs. Given a program it provides an efficient implementation for floating-point programs with elementary function calls. Uses Z3, dReal, MPFR, Metalibm