1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
|
/******************************************************************************
* Top contributors (to current version):
* Andrew Reynolds, Gereon Kremer
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
* in the top-level source directory and their institutional affiliations.
* All rights reserved. See the file COPYING in the top-level source
* directory for licensing information.
* ****************************************************************************
*
* Solving for handling transcendental functions.
*/
#ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H
#define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H
#include <vector>
#include "expr/node.h"
#include "theory/arith/nl/transcendental/exponential_solver.h"
#include "theory/arith/nl/transcendental/sine_solver.h"
#include "theory/arith/nl/transcendental/transcendental_state.h"
namespace cvc5 {
namespace theory {
namespace arith {
class InferenceManager;
namespace nl {
class NlModel;
namespace transcendental {
/** Transcendental solver class
*
* This class implements model-based refinement schemes
* for transcendental functions, described in:
*
* - "Satisfiability Modulo Transcendental
* Functions via Incremental Linearization" by Cimatti
* et al., CADE 2017.
*
* It's main functionality are methods that implement lemma schemas below,
* which return a set of lemmas that should be sent on the output channel.
*/
class TranscendentalSolver
{
public:
TranscendentalSolver(InferenceManager& im,
NlModel& m,
ProofNodeManager* pnm,
context::UserContext* c);
~TranscendentalSolver();
/** init last call
*
* This is called at the beginning of last call effort check, where
* assertions are the set of assertions belonging to arithmetic,
* false_asserts is the subset of assertions that are false in the current
* model, and xts is the set of extended function terms that are active in
* the current context.
*
* This call may add lemmas to lems based on registering term
* information (for example, purification of sine terms).
*/
void initLastCall(const std::vector<Node>& xts);
/** increment taylor degree */
void incrementTaylorDegree();
/** get taylor degree */
unsigned getTaylorDegree() const;
/** preprocess assertions check model
*
* This modifies the given assertions in preparation for running a call
* to check model.
*
* This method returns false if a bound for a transcendental function
* was conflicting.
*/
bool preprocessAssertionsCheckModel(std::vector<Node>& assertions);
/** Process side effects in lemma se */
void processSideEffect(const NlLemma& se);
//-------------------------------------------- lemma schemas
// Relays to exp and sine solvers.
void checkTranscendentalInitialRefine();
// Relays to exp and sine solvers.
void checkTranscendentalMonotonic();
/** check transcendental tangent planes
*
* Constructs a set of valid theory lemmas, based on
* computing an "incremental linearization" of
* transcendental functions based on the model values
* of transcendental functions and their arguments.
* It is based on Figure 3 of "Satisfiability
* Modulo Transcendental Functions via Incremental
* Linearization" by Cimatti et al., CADE 2017.
* This schema is not terminating in general.
* It is not enabled by default, and can
* be enabled by --nl-ext-tf-tplanes.
*
* Example:
*
* Assume we have a term sin(y) where M( y ) = 1 where M is the current model.
* Note that:
* sin(1) ~= .841471
*
* The Taylor series and remainder of sin(y) of degree 7 is
* P_{7,sin(0)}( x ) = x + (-1/6)*x^3 + (1/20)*x^5
* R_{7,sin(0),b}( x ) = (-1/5040)*x^7
*
* This gives us lower and upper bounds :
* P_u( x ) = P_{7,sin(0)}( x ) + R_{7,sin(0),b}( x )
* ...where note P_u( 1 ) = 4243/5040 ~= .841865
* P_l( x ) = P_{7,sin(0)}( x ) - R_{7,sin(0),b}( x )
* ...where note P_l( 1 ) = 4241/5040 ~= .841468
*
* Assume that M( sin(y) ) > P_u( 1 ).
* Since the concavity of sine in the region 0 < x < PI/2 is -1,
* we add a tangent plane refinement.
* The tangent plane at the point 1 in P_u is
* given by the formula:
* T( x ) = P_u( 1 ) + ((d/dx)(P_u(x)))( 1 )*( x - 1 )
* We add the lemma:
* ( 0 < y < PI/2 ) => sin( y ) <= T( y )
* which is:
* ( 0 < y < PI/2 ) => sin( y ) <= (391/720)*(y - 2737/1506)
*
* Assume that M( sin(y) ) < P_u( 1 ).
* Since the concavity of sine in the region 0 < x < PI/2 is -1,
* we add a secant plane refinement for some constants ( l, u )
* such that 0 <= l < M( y ) < u <= PI/2. Assume we choose
* l = 0 and u = M( PI/2 ) = 150517/47912.
* The secant planes at point 1 for P_l
* are given by the formulas:
* S_l( x ) = (x-l)*(P_l( l )-P_l(c))/(l-1) + P_l( l )
* S_u( x ) = (x-u)*(P_l( u )-P_l(c))/(u-1) + P_l( u )
* We add the lemmas:
* ( 0 < y < 1 ) => sin( y ) >= S_l( y )
* ( 1 < y < PI/2 ) => sin( y ) >= S_u( y )
* which are:
* ( 0 < y < 1 ) => (sin y) >= 4251/5040*y
* ( 1 < y < PI/2 ) => (sin y) >= c1*(y+c2)
* where c1, c2 are rationals (for brevity, omitted here)
* such that c1 ~= .277 and c2 ~= 2.032.
*/
void checkTranscendentalTangentPlanes();
private:
/** check transcendental function refinement for tf
*
* This method is called by the above method for each "master"
* transcendental function application that occurs in an assertion in the
* current context. For example, an application like sin(t) is not a master
* if we have introduced the constraints:
* t=y+2*pi*n ^ -pi <= y <= pi ^ sin(t) = sin(y).
* See d_trMaster/d_trSlaves for more detail.
*
* This runs Figure 3 of Cimatti et al., CADE 2017 for transcendental
* function application tf for Taylor degree d. It may add a secant or
* tangent plane lemma to lems, which includes the side effect of the lemma
* (if one exists).
*
* It returns false if the bounds are not precise enough to add a
* secant or tangent plane lemma.
*/
bool checkTfTangentPlanesFun(Node tf, unsigned d);
//-------------------------------------------- end lemma schemas
/** get concavity
*
* Returns whether we are concave (+1) or convex (-1)
* in region of transcendental function with kind k,
* where region is defined above.
* Returns 0 if region is invalid.
*/
int regionToConcavity(Kind k, int region);
/** taylor degree
*
* Indicates that the degree of the polynomials in the Taylor approximation of
* all transcendental functions is 2*d_taylor_degree. This value is set
* initially to options::nlExtTfTaylorDegree() and may be incremented
* if the option options::nlExtTfIncPrecision() is enabled.
*/
unsigned d_taylor_degree;
/** Common state for transcendental solver */
transcendental::TranscendentalState d_tstate;
/** The solver responsible for the exponential function */
transcendental::ExponentialSolver d_expSlv;
/** The solver responsible for the sine function */
transcendental::SineSolver d_sineSlv;
}; /* class TranscendentalSolver */
} // namespace transcendental
} // namespace nl
} // namespace arith
} // namespace theory
} // namespace cvc5
#endif /* CVC5__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
|
