GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/transcendental/taylor_generator.h Lines: 2 2 100.0 %
Date: 2021-03-22 Branches: 3 10 30.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file taylor_generator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Gereon Kremer, Andrew Reynolds
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Generate taylor approximations transcendental lemmas.
13
 **/
14
15
#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TAYLOR_GENERATOR_H
16
#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TAYLOR_GENERATOR_H
17
18
#include "expr/node.h"
19
20
namespace CVC4 {
21
namespace theory {
22
namespace arith {
23
namespace nl {
24
25
class NlModel;
26
27
namespace transcendental {
28
29
4453
class TaylorGenerator
30
{
31
 public:
32
  /** Stores the approximation bounds for transcendental functions */
33
9962
  struct ApproximationBounds
34
  {
35
    /** Lower bound */
36
    Node d_lower;
37
    /** Upper bound for negative values */
38
    Node d_upperNeg;
39
    /** Upper bound for positive values */
40
    Node d_upperPos;
41
  };
42
43
  TaylorGenerator();
44
45
  /**
46
   * Return the variable used as x in getTaylor().
47
   */
48
  TNode getTaylorVariable();
49
50
  /**
51
   * Get Taylor series of degree n for function fa centered around zero.
52
   *
53
   * Return value is ( P_{n,f(0)}( x ), R_{n+1,f(0)}( x ) ) where
54
   * the first part of the pair is the Taylor series expansion :
55
   *    P_{n,f(0)}( x ) = sum_{i=0}^n (f^i(0)/i!)*x^i
56
   * and the second part of the pair is the Taylor series remainder :
57
   *    R_{n+1,f(0)}( x ) = x^{n+1}/(n+1)!
58
   *
59
   * The above values are cached for each (f,n).
60
   */
61
  std::pair<Node, Node> getTaylor(Kind k, std::uint64_t n);
62
63
  /**
64
   * polynomial approximation bounds
65
   *
66
   * This adds P_l+[x], P_l-[x], P_u+[x], P_u-[x] to pbounds, where x is
67
   * d_taylor_real_fv. These are polynomial approximations of the Taylor series
68
   * of <k>( 0 ) for degree 2*d where k is SINE or EXPONENTIAL.
69
   * These correspond to P_l and P_u from Figure 3 of Cimatti et al., CADE 2017,
70
   * for positive/negative (+/-) values of the argument of <k>( 0 ).
71
   *
72
   * Notice that for certain bounds (e.g. upper bounds for exponential), the
73
   * Taylor approximation for a fixed degree is only sound up to a given
74
   * upper bound on the argument. To obtain sound lower/upper bounds for a
75
   * given <k>( c ), use the function below.
76
   */
77
  void getPolynomialApproximationBounds(Kind k,
78
                                        std::uint64_t d,
79
                                        ApproximationBounds& pbounds);
80
81
  /**
82
   * polynomial approximation bounds
83
   *
84
   * This computes polynomial approximations P_l+[x], P_l-[x], P_u+[x], P_u-[x]
85
   * that are sound (lower, upper) bounds for <k>( c ). Notice that these
86
   * polynomials may depend on c. In particular, for P_u+[x] for <k>( c ) where
87
   * c>0, we return the P_u+[x] from the function above for the minimum degree
88
   * d' >= d such that (1-c^{2*d'+1}/(2*d'+1)!) is positive.
89
   * @return the actual degree of the polynomial approximations (which may be
90
   * larger than d).
91
   */
92
  std::uint64_t getPolynomialApproximationBoundForArg(
93
      Kind k, Node c, std::uint64_t d, ApproximationBounds& pbounds);
94
95
  /** get transcendental function model bounds
96
   *
97
   * This returns the current lower and upper bounds of transcendental
98
   * function application tf based on Taylor of degree 2*d, which is dependent
99
   * on the model value of its argument.
100
   */
101
  std::pair<Node, Node> getTfModelBounds(Node tf,
102
                                         std::uint64_t d,
103
                                         NlModel& model);
104
105
 private:
106
  NodeManager* d_nm;
107
  const Node d_taylor_real_fv;
108
109
  /**
110
   * For every kind (EXP or SINE) and every degree we store the taylor series up
111
   * to this degree and the next term in the series.
112
   */
113
  std::map<Kind, std::map<std::uint64_t, std::pair<Node, Node>>> d_taylor_terms;
114
  std::map<Kind, std::map<std::uint64_t, ApproximationBounds>> d_poly_bounds;
115
};
116
117
}  // namespace transcendental
118
}  // namespace nl
119
}  // namespace arith
120
}  // namespace theory
121
}  // namespace CVC4
122
123
#endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */