GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/transcendental/sine_solver.h Lines: 24 28 85.7 %
Date: 2021-03-22 Branches: 12 16 75.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sine_solver.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 Solving for handling exponential function.
13
 **/
14
15
#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H
16
#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H
17
18
#include <map>
19
20
#include "expr/node.h"
21
#include "theory/arith/nl/transcendental/transcendental_state.h"
22
23
namespace CVC4 {
24
namespace theory {
25
namespace arith {
26
namespace nl {
27
namespace transcendental {
28
29
/** Transcendental solver class
30
 *
31
 * This class implements model-based refinement schemes
32
 * for transcendental functions, described in:
33
 *
34
 * - "Satisfiability Modulo Transcendental
35
 * Functions via Incremental Linearization" by Cimatti
36
 * et al., CADE 2017.
37
 *
38
 * It's main functionality are methods that implement lemma schemas below,
39
 * which return a set of lemmas that should be sent on the output channel.
40
 */
41
class SineSolver
42
{
43
 public:
44
  SineSolver(TranscendentalState* tstate);
45
  ~SineSolver();
46
47
  /**
48
   * Introduces new_a as purified version of a which is also shifted to the main
49
   * phase (from -pi to pi). y is the new skolem used for purification.
50
   */
51
  void doPhaseShift(TNode a, TNode new_a, TNode y);
52
53
  /**
54
   * check initial refine
55
   *
56
   * Constructs a set of valid theory lemmas, based on
57
   * simple facts about the sine function.
58
   * This mostly follows the initial axioms described in
59
   * Section 4 of "Satisfiability
60
   * Modulo Transcendental Functions via Incremental
61
   * Linearization" by Cimatti et al., CADE 2017.
62
   *
63
   * Examples:
64
   *
65
   * sin( x ) = -sin( -x )
66
   * ( PI > x > 0 ) => 0 < sin( x ) < 1
67
   */
68
  void checkInitialRefine();
69
70
  /**
71
   * check monotonicity
72
   *
73
   * Constructs a set of valid theory lemmas, based on a
74
   * lemma scheme that ensures that applications
75
   * of the sine function respect monotonicity.
76
   *
77
   * Examples:
78
   *
79
   * PI/2 > x > y > 0 => sin( x ) > sin( y )
80
   * PI > x > y > PI/2 => sin( x ) < sin( y )
81
   */
82
  void checkMonotonic();
83
84
  /** Sent tangent lemma around c for e */
85
  void doTangentLemma(
86
      TNode e, TNode c, TNode poly_approx, int region, std::uint64_t d);
87
88
  /** Sent secant lemmas around c for e */
89
  void doSecantLemmas(TNode e,
90
                      TNode poly_approx,
91
                      TNode c,
92
                      TNode poly_approx_c,
93
                      unsigned d,
94
                      unsigned actual_d,
95
                      int region);
96
97
 private:
98
  std::pair<Node, Node> getSecantBounds(TNode e,
99
                                        TNode c,
100
                                        unsigned d,
101
                                        int region);
102
103
  /** region to lower bound
104
   *
105
   * Returns the term corresponding to the lower
106
   * bound of the region of transcendental function
107
   * with kind k. Returns Node::null if the region
108
   * is invalid, or there is no lower bound for the
109
   * region.
110
   */
111
92
  Node regionToLowerBound(int region)
112
  {
113
92
    switch (region)
114
    {
115
8
      case 1: return d_data->d_pi_2;
116
43
      case 2: return d_data->d_zero;
117
28
      case 3: return d_data->d_pi_neg_2;
118
13
      case 4: return d_data->d_pi_neg;
119
      default: return Node();
120
    }
121
  }
122
123
  /** region to upper bound
124
   *
125
   * Returns the term corresponding to the upper
126
   * bound of the region of transcendental function
127
   * with kind k. Returns Node::null if the region
128
   * is invalid, or there is no upper bound for the
129
   * region.
130
   */
131
92
  Node regionToUpperBound(int region)
132
  {
133
92
    switch (region)
134
    {
135
13
      case 1: return d_data->d_pi;
136
28
      case 2: return d_data->d_pi_2;
137
43
      case 3: return d_data->d_zero;
138
8
      case 4: return d_data->d_pi_neg_2;
139
      default: return Node();
140
    }
141
  }
142
143
683
  int regionToMonotonicityDir(int region)
144
  {
145
683
    switch (region)
146
    {
147
285
      case 1:
148
285
      case 4: return -1;
149
398
      case 2:
150
398
      case 3: return 1;
151
      default: return 0;
152
    }
153
  }
154
104
  Convexity regionToConvexity(int region)
155
  {
156
104
    switch (region)
157
    {
158
52
      case 1:
159
52
      case 2: return Convexity::CONCAVE;
160
52
      case 3:
161
52
      case 4: return Convexity::CONVEX;
162
      default: return Convexity::UNKNOWN;
163
    }
164
  }
165
166
  /** Holds common state for transcendental solvers */
167
  TranscendentalState* d_data;
168
169
  /** The transcendental functions we have done initial refinements on */
170
  std::map<Node, bool> d_tf_initial_refine;
171
172
}; /* class SineSolver */
173
174
}  // namespace transcendental
175
}  // namespace nl
176
}  // namespace arith
177
}  // namespace theory
178
}  // namespace CVC4
179
180
#endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */