Name:

implementpoly implements a polynomial using double, double-double and triple-double arithmetic and generates a Gappa proof

Library names:

sollya_obj_t sollya_lib_implementpoly(sollya_obj_t, sollya_obj_t,                                       sollya_obj_t, sollya_obj_t,                                       sollya_obj_t, sollya_obj_t, ...) sollya_obj_t sollya_lib_v_implementpoly(sollya_obj_t, sollya_obj_t,                                         sollya_obj_t, sollya_obj_t,                                         sollya_obj_t, sollya_obj_t, va_list)

Usage:

implementpoly(polynomial, range, error bound, format, functionname, filename) : (function, range, constant, D|double|DD|doubledouble|TD|tripledouble, string, string) -> function implementpoly(polynomial, range, error bound, format, functionname, filename, honor coefficient precisions) : (function, range, constant, D|double|DD|doubledouble|TD|tripledouble, string, string, honorcoeffprec) -> function implementpoly(polynomial, range, error bound, format, functionname, filename, proof filename) : (function, range, constant, D|double|DD|doubledouble|TD|tripledouble, string, string, string) -> function implementpoly(polynomial, range, error bound, format, functionname, filename, honor coefficient precisions, proof filename) : (function, range, constant, D|double|DD|doubledouble|TD|tripledouble, string, string, honorcoeffprec, string) -> function

Description:

Example 1:

   > implementpoly(1 - 1/6 * x^2 + 1/120 * x^4, [-1b-10;1b-10], 1b-30, D, "p","implementation.c");
   1 + x^2 * (-0.166666666666666657414808128123695496469736099243164 + x^2 * 8.3333333333333332176851016015461937058717012405396e-3)
   > bashevaluate("tail -n -29 implementation.c");
   #define p_coeff_0h 1.00000000000000000000000000000000000000000000000000000000000000000000000000000000e+00
   #define p_coeff_2h -1.66666666666666657414808128123695496469736099243164062500000000000000000000000000e-01
   #define p_coeff_4h 8.33333333333333321768510160154619370587170124053955078125000000000000000000000000e-03
   
   
   void p(double *p_resh, double x) {
   double p_x_0_pow2h;
   
   
   p_x_0_pow2h = x * x;
   
   
   double p_t_1_0h;
   double p_t_2_0h;
   double p_t_3_0h;
   double p_t_4_0h;
   double p_t_5_0h;
    
   
   
   p_t_1_0h = p_coeff_4h;
   p_t_2_0h = p_t_1_0h * p_x_0_pow2h;
   p_t_3_0h = p_coeff_2h + p_t_2_0h;
   p_t_4_0h = p_t_3_0h * p_x_0_pow2h;
   p_t_5_0h = p_coeff_0h + p_t_4_0h;
   *p_resh = p_t_5_0h;
   
   
   }

Example 2:

   > implementpoly(1 - 1/6 * x^2 + 1/120 * x^4, [-1b-10;1b-10], 1b-30, D, "p","implementation.c","implementation.gappa");
   1 + x^2 * (-0.166666666666666657414808128123695496469736099243164 + x^2 * 8.3333333333333332176851016015461937058717012405396e-3)

Example 3:

   > verbosity = 1!;
   > q = implementpoly(1 - dirtysimplify(TD(1/6)) * x^2,[-1b-10;1b-10],1b-60,DD,"p","implementation.c");
   Warning: at least one of the coefficients of the given polynomial has been rounded in a way
   that the target precision can be achieved at lower cost. Nevertheless, the implemented polynomial
   is different from the given one.
   > printexpansion(q);
   0x3ff0000000000000 + x^2 * 0xbfc5555555555555
   > r = implementpoly(1 - dirtysimplify(TD(1/6)) * x^2,[-1b-10;1b-10],1b-60,DD,"p","implementation.c",honorcoeffprec);
   Warning: the infered precision of the 2th coefficient of the polynomial is greater than
   the necessary precision computed for this step. This may make the automatic determination
   of precisions useless.
   > printexpansion(r);
   0x3ff0000000000000 + x^2 * (0xbfc5555555555555 + 0xbc65555555555555 + 0xb905555555555555)

Example 4:

   > p = 0x3ff0000000000000 + x * (0x3ff0000000000000 + x * (0x3fe0000000000000 + x * (0x3fc5555555555559 + x * (0x3fa55555555555bd + x * (0x3f811111111106e2 + x * (0x3f56c16c16bf5eb7 + x * (0x3f2a01a01a292dcd + x * (0x3efa01a0218a016a + x * (0x3ec71de360331aad + x * (0x3e927e42e3823bf3 + x * (0x3e5ae6b2710c2c9a + x * (0x3e2203730c0a7c1d + x * 0x3de5da557e0781df))))))))))));
   > q = implementpoly(p,[-1/2;1/2],1b-60,D,"p","implementation.c",honorcoeffprec,"implementation.gappa");
   > if (q != p) then print("During implementation, rounding has happened.") else print("Polynomial implemented as given.");
   Polynomial implemented as given.
See also: honorcoeffprec, roundcoefficients, double, doubledouble, tripledouble, bashevaluate, printexpansion, error, remez, fpminimax, taylor, implementconstant
Go back to the list of commands