GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/transcendental/transcendental_state.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 3 4 75.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file transcendental_state.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 Utilities for transcendental lemmas.
13
 **/
14
15
#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H
16
#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H
17
18
#include "expr/node.h"
19
#include "expr/proof_set.h"
20
#include "theory/arith/nl/nl_lemma_utils.h"
21
#include "theory/arith/nl/transcendental/proof_checker.h"
22
#include "theory/arith/nl/transcendental/taylor_generator.h"
23
24
namespace CVC4 {
25
class CDProof;
26
namespace theory {
27
namespace arith {
28
29
class InferenceManager;
30
31
namespace nl {
32
33
class NlModel;
34
35
namespace transcendental {
36
37
/**
38
 * This enum indicates whether some function is convex, concave or unknown at
39
 * some point.
40
 */
41
enum class Convexity
42
{
43
  CONVEX,
44
  CONCAVE,
45
  UNKNOWN
46
};
47
inline std::ostream& operator<<(std::ostream& os, Convexity c) {
48
  switch (c) {
49
    case Convexity::CONVEX: return os << "CONVEX";
50
    case Convexity::CONCAVE: return os << "CONCAVE";
51
    default: return os << "UNKNOWN";
52
  }
53
}
54
55
/**
56
 * Holds common state and utilities for transcendental solvers.
57
 *
58
 * This includes common lookups and caches as well as generic utilities for
59
 * secant plane lemmas and taylor approximations.
60
 */
61
4388
struct TranscendentalState
62
{
63
  TranscendentalState(InferenceManager& im,
64
                      NlModel& model,
65
                      ProofNodeManager* pnm,
66
                      context::UserContext* c);
67
68
  /**
69
   * Checks whether proofs are enabled.
70
   */
71
  bool isProofEnabled() const;
72
  /**
73
   * Creates and returns a new LazyCDProof that can be used to prove some lemma.
74
   */
75
  CDProof* getProof();
76
77
  /** init last call
78
   *
79
   * This is called at the beginning of last call effort check xts is the set of
80
   * extended function terms that are active in the current context.
81
   *
82
   * This call may add lemmas to lems based on registering term
83
   * information (for example to ensure congruence of terms).
84
   * It puts terms that need to be treated further as a master term on their own
85
   * (for example purification of sine terms) into needsMaster.
86
   */
87
  void init(const std::vector<Node>& xts, std::vector<Node>& needsMaster);
88
89
  /**
90
   * Checks for terms that are congruent but disequal to a.
91
   * If any are found, appropriate lemmas are sent.
92
   * @param a Some node
93
   * @param argTrie Lookup for equivalence classes
94
   */
95
  void ensureCongruence(TNode a, std::map<Kind, ArgTrie>& argTrie);
96
97
  /** Initialize members for pi-related values */
98
  void mkPi();
99
  /** Get current bounds for pi as a lemma */
100
  void getCurrentPiBounds();
101
102
  /**
103
   * Get the two closest secant points from the once stored already.
104
   * "closest" is determined according to the current model.
105
   * @param e The transcendental term (like (exp t))
106
   * @param center The point currently under consideration (probably the model
107
   * of t)
108
   * @param d The taylor degree.
109
   */
110
  std::pair<Node, Node> getClosestSecantPoints(TNode e,
111
                                               TNode center,
112
                                               unsigned d);
113
114
  /**
115
   * Construct a secant plane as function in arg between lower and upper
116
   * @param arg The argument of the transcendental term
117
   * @param lower Left secant point
118
   * @param upper Right secant point
119
   * @param lval Evaluation at lower
120
   * @param uval Evaluation at upper
121
   */
122
  Node mkSecantPlane(
123
      TNode arg, TNode lower, TNode upper, TNode lval, TNode uval);
124
125
  /**
126
   * Construct a secant lemma between lower and upper for tf.
127
   * @param lower Left secant point
128
   * @param upper Right secant point
129
   * @param concavity Concavity of the current regions
130
   * @param tf Current transcendental term
131
   * @param splane Secant plane as computed by mkSecantPlane()
132
   */
133
  NlLemma mkSecantLemma(TNode lower,
134
                        TNode upper,
135
                        TNode lapprox,
136
                        TNode uapprox,
137
                        int csign,
138
                        Convexity convexity,
139
                        TNode tf,
140
                        TNode splane,
141
                        unsigned actual_d);
142
143
  /**
144
   * Construct and send secant lemmas (if appropriate)
145
   * @param bounds Secant bounds
146
   * @param poly_approx Polynomial approximation
147
   * @param center Current point
148
   * @param cval Evaluation at c
149
   * @param tf Current transcendental term
150
   * @param d Current taylor degree
151
   * @param concavity Concavity in region of c
152
   */
153
  void doSecantLemmas(const std::pair<Node, Node>& bounds,
154
                      TNode poly_approx,
155
                      TNode center,
156
                      TNode cval,
157
                      TNode tf,
158
                      Convexity convexity,
159
                      unsigned d,
160
                      unsigned actual_d);
161
162
  Node d_true;
163
  Node d_false;
164
  Node d_zero;
165
  Node d_one;
166
  Node d_neg_one;
167
168
  /** The inference manager that we push conflicts and lemmas to. */
169
  InferenceManager& d_im;
170
  /** Reference to the non-linear model object */
171
  NlModel& d_model;
172
  /** Utility to compute taylor approximations */
173
  TaylorGenerator d_taylor;
174
  /**
175
   * Pointer to the current proof node manager. nullptr, if proofs are
176
   * disabled.
177
   */
178
  ProofNodeManager* d_pnm;
179
  /** The user context. */
180
  context::UserContext* d_ctx;
181
  /**
182
   * A CDProofSet that hands out CDProof objects for lemmas.
183
   */
184
  std::unique_ptr<CDProofSet<CDProof>> d_proof;
185
186
  /** The proof checker for transcendental proofs */
187
  std::unique_ptr<TranscendentalProofRuleChecker> d_proofChecker;
188
189
  /**
190
   * Some transcendental functions f(t) are "purified", e.g. we add
191
   * t = y ^ f(t) = f(y) where y is a fresh variable. Those that are not
192
   * purified we call "master terms".
193
   *
194
   * The maps below maintain a master/slave relationship over
195
   * transcendental functions (SINE, EXPONENTIAL, PI), where above
196
   * f(y) is the master of itself and of f(t).
197
   *
198
   * This is used for ensuring that the argument y of SINE we process is on
199
   * the interval [-pi .. pi], and that exponentials are not applied to
200
   * arguments that contain transcendental functions.
201
   */
202
  std::map<Node, Node> d_trMaster;
203
  std::map<Node, std::unordered_set<Node, NodeHashFunction>> d_trSlaves;
204
205
  /** concavity region for transcendental functions
206
   *
207
   * This stores an integer that identifies an interval in
208
   * which the current model value for an argument of an
209
   * application of a transcendental function resides.
210
   *
211
   * For exp( x ):
212
   *   region #1 is -infty < x < infty
213
   * For sin( x ):
214
   *   region #0 is pi < x < infty (this is an invalid region)
215
   *   region #1 is pi/2 < x <= pi
216
   *   region #2 is 0 < x <= pi/2
217
   *   region #3 is -pi/2 < x <= 0
218
   *   region #4 is -pi < x <= -pi/2
219
   *   region #5 is -infty < x <= -pi (this is an invalid region)
220
   * All regions not listed above, as well as regions 0 and 5
221
   * for SINE are "invalid". We only process applications
222
   * of transcendental functions whose arguments have model
223
   * values that reside in valid regions.
224
   */
225
  std::unordered_map<Node, int, NodeHashFunction> d_tf_region;
226
  /**
227
   * Maps representives of a congruence class to the members of that class.
228
   *
229
   * In detail, a congruence class is a set of terms of the form
230
   *   { f(t1), ..., f(tn) }
231
   * such that t1 = ... = tn in the current context. We choose an arbitrary
232
   * term among these to be the repesentative of this congruence class.
233
   *
234
   * Moreover, notice we compute congruence classes only over terms that
235
   * are transcendental function applications that are "master terms",
236
   * see d_trMaster/d_trSlave.
237
   */
238
  std::map<Node, std::vector<Node>> d_funcCongClass;
239
  /**
240
   * A list of all functions for each kind in { EXPONENTIAL, SINE, POW, PI }
241
   * that are representives of their congruence class.
242
   */
243
  std::map<Kind, std::vector<Node>> d_funcMap;
244
245
  /** secant points (sorted list) for transcendental functions
246
   *
247
   * This is used for tangent plane refinements for
248
   * transcendental functions. This is the set
249
   * "get-previous-secant-points" in "Satisfiability
250
   * Modulo Transcendental Functions via Incremental
251
   * Linearization" by Cimatti et al., CADE 2017, for
252
   * each transcendental function application. We store this set for each
253
   * Taylor degree.
254
   */
255
  std::unordered_map<Node,
256
                     std::map<unsigned, std::vector<Node>>,
257
                     NodeHashFunction>
258
      d_secant_points;
259
260
  /** PI
261
   *
262
   * Note that PI is a (symbolic, non-constant) nullary operator. This is
263
   * because its value cannot be computed exactly. We constraint PI to
264
   * concrete lower and upper bounds stored in d_pi_bound below.
265
   */
266
  Node d_pi;
267
  /** PI/2 */
268
  Node d_pi_2;
269
  /** -PI/2 */
270
  Node d_pi_neg_2;
271
  /** -PI */
272
  Node d_pi_neg;
273
  /** the concrete lower and upper bounds for PI */
274
  Node d_pi_bound[2];
275
};
276
277
}  // namespace transcendental
278
}  // namespace nl
279
}  // namespace arith
280
}  // namespace theory
281
}  // namespace CVC4
282
283
#endif /* CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H */