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