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
|
/********************* */
/*! \file sine_solver.h
** \verbatim
** Top contributors (to current version):
** Gereon Kremer, Andrew Reynolds
** This file is part of the CVC4 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.\endverbatim
**
** \brief Solving for handling exponential function.
**/
#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H
#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H
#include <map>
#include "expr/node.h"
#include "theory/arith/nl/transcendental/transcendental_state.h"
namespace CVC5 {
namespace theory {
namespace arith {
namespace nl {
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 SineSolver
{
public:
SineSolver(TranscendentalState* tstate);
~SineSolver();
/**
* Introduces new_a as purified version of a which is also shifted to the main
* phase (from -pi to pi). y is the new skolem used for purification.
*/
void doPhaseShift(TNode a, TNode new_a, TNode y);
/**
* check initial refine
*
* Constructs a set of valid theory lemmas, based on
* simple facts about the sine function.
* This mostly follows the initial axioms described in
* Section 4 of "Satisfiability
* Modulo Transcendental Functions via Incremental
* Linearization" by Cimatti et al., CADE 2017.
*
* Examples:
*
* sin( x ) = -sin( -x )
* ( PI > x > 0 ) => 0 < sin( x ) < 1
*/
void checkInitialRefine();
/**
* check monotonicity
*
* Constructs a set of valid theory lemmas, based on a
* lemma scheme that ensures that applications
* of the sine function respect monotonicity.
*
* Examples:
*
* PI/2 > x > y > 0 => sin( x ) > sin( y )
* PI > x > y > PI/2 => sin( x ) < sin( y )
*/
void checkMonotonic();
/** Sent tangent lemma around c for e */
void doTangentLemma(
TNode e, TNode c, TNode poly_approx, int region, std::uint64_t d);
/** Sent secant lemmas around c for e */
void doSecantLemmas(TNode e,
TNode poly_approx,
TNode c,
TNode poly_approx_c,
unsigned d,
unsigned actual_d,
int region);
private:
std::pair<Node, Node> getSecantBounds(TNode e,
TNode c,
unsigned d,
int region);
/** region to lower bound
*
* Returns the term corresponding to the lower
* bound of the region of transcendental function
* with kind k. Returns Node::null if the region
* is invalid, or there is no lower bound for the
* region.
*/
Node regionToLowerBound(int region)
{
switch (region)
{
case 1: return d_data->d_pi_2;
case 2: return d_data->d_zero;
case 3: return d_data->d_pi_neg_2;
case 4: return d_data->d_pi_neg;
default: return Node();
}
}
/** region to upper bound
*
* Returns the term corresponding to the upper
* bound of the region of transcendental function
* with kind k. Returns Node::null if the region
* is invalid, or there is no upper bound for the
* region.
*/
Node regionToUpperBound(int region)
{
switch (region)
{
case 1: return d_data->d_pi;
case 2: return d_data->d_pi_2;
case 3: return d_data->d_zero;
case 4: return d_data->d_pi_neg_2;
default: return Node();
}
}
int regionToMonotonicityDir(int region)
{
switch (region)
{
case 1:
case 4: return -1;
case 2:
case 3: return 1;
default: return 0;
}
}
Convexity regionToConvexity(int region)
{
switch (region)
{
case 1:
case 2: return Convexity::CONCAVE;
case 3:
case 4: return Convexity::CONVEX;
default: return Convexity::UNKNOWN;
}
}
/** Holds common state for transcendental solvers */
TranscendentalState* d_data;
/** The transcendental functions we have done initial refinements on */
std::map<Node, bool> d_tf_initial_refine;
}; /* class SineSolver */
} // namespace transcendental
} // namespace nl
} // namespace arith
} // namespace theory
} // namespace CVC5
#endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
|
