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-22 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 4386 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& xts, std::vector& 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& 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 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& 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> d_proof; 185 186 /** The proof checker for transcendental proofs */ 187 std::unique_ptr 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 d_trMaster; 203 std::map> 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 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> 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> 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>, 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 */

 Generated by: GCOVR (Version 3.2)