Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/nl/transcendental/transcendental_state.h	Lines:	1	1	100.0 %
Date:	2021-08-01	Branches:	3	4	75.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Gereon Kremer, Andrew Reynolds
 *
 * 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.
 * ****************************************************************************
 *
 * Utilities for transcendental lemmas.
 */

#ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H
#define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H

#include "expr/node.h"
#include "proof/proof_set.h"
#include "theory/arith/nl/nl_lemma_utils.h"
#include "theory/arith/nl/transcendental/proof_checker.h"
#include "theory/arith/nl/transcendental/taylor_generator.h"

namespace cvc5 {
class CDProof;
namespace theory {
namespace arith {

class InferenceManager;

namespace nl {

class NlModel;

namespace transcendental {

/**
 * This enum indicates whether some function is convex, concave or unknown at
 * some point.
 */
enum class Convexity
{
  CONVEX,
  CONCAVE,
  UNKNOWN
};
inline std::ostream& operator<<(std::ostream& os, Convexity c) {
  switch (c) {
    case Convexity::CONVEX: return os << "CONVEX";
    case Convexity::CONCAVE: return os << "CONCAVE";
    default: return os << "UNKNOWN";
  }
}

/**
 * Holds common state and utilities for transcendental solvers.
 *
 * This includes common lookups and caches as well as generic utilities for
 * secant plane lemmas and taylor approximations.
 */
struct TranscendentalState
{
  TranscendentalState(InferenceManager& im,
                      NlModel& model,
                      ProofNodeManager* pnm,
                      context::UserContext* c);

  /**
   * Checks whether proofs are enabled.
   */
  bool isProofEnabled() const;
  /**
   * Creates and returns a new LazyCDProof that can be used to prove some lemma.
   */
  CDProof* getProof();

  /** init last call
   *
   * This is called at the beginning of last call effort check 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 to ensure congruence of terms).
   * It puts terms that need to be treated further as a master term on their own
   * (for example purification of sine terms) into needsMaster.
   */
  void init(const std::vector<Node>& xts, std::vector<Node>& needsMaster);

  /**
   * Checks for terms that are congruent but disequal to a.
   * If any are found, appropriate lemmas are sent.
   * @param a Some node
   * @param argTrie Lookup for equivalence classes
   */
  void ensureCongruence(TNode a, std::map<Kind, ArgTrie>& argTrie);

  /** Initialize members for pi-related values */
  void mkPi();
  /** Get current bounds for pi as a lemma */
  void getCurrentPiBounds();

  /**
   * Get the two closest secant points from the once stored already.
   * "closest" is determined according to the current model.
   * @param e The transcendental term (like (exp t))
   * @param center The point currently under consideration (probably the model
   * of t)
   * @param d The taylor degree.
   */
  std::pair<Node, Node> getClosestSecantPoints(TNode e,
                                               TNode center,
                                               unsigned d);

  /**
   * Construct a secant plane as function in arg between lower and upper
   * @param arg The argument of the transcendental term
   * @param lower Left secant point
   * @param upper Right secant point
   * @param lval Evaluation at lower
   * @param uval Evaluation at upper
   */
  Node mkSecantPlane(
      TNode arg, TNode lower, TNode upper, TNode lval, TNode uval);

  /**
   * Construct a secant lemma between lower and upper for tf.
   * @param lower Left secant point
   * @param upper Right secant point
   * @param concavity Concavity of the current regions
   * @param tf Current transcendental term
   * @param splane Secant plane as computed by mkSecantPlane()
   */
  NlLemma mkSecantLemma(TNode lower,
                        TNode upper,
                        TNode lapprox,
                        TNode uapprox,
                        int csign,
                        Convexity convexity,
                        TNode tf,
                        TNode splane,
                        unsigned actual_d);

  /**
   * Construct and send secant lemmas (if appropriate)
   * @param bounds Secant bounds
   * @param poly_approx Polynomial approximation
   * @param center Current point
   * @param cval Evaluation at c
   * @param tf Current transcendental term
   * @param d Current taylor degree
   * @param concavity Concavity in region of c
   */
  void doSecantLemmas(const std::pair<Node, Node>& bounds,
                      TNode poly_approx,
                      TNode center,
                      TNode cval,
                      TNode tf,
                      Convexity convexity,
                      unsigned d,
                      unsigned actual_d);

  Node d_true;
  Node d_false;
  Node d_zero;
  Node d_one;
  Node d_neg_one;

  /** The inference manager that we push conflicts and lemmas to. */
  InferenceManager& d_im;
  /** Reference to the non-linear model object */
  NlModel& d_model;
  /** Utility to compute taylor approximations */
  TaylorGenerator d_taylor;
  /**
   * Pointer to the current proof node manager. nullptr, if proofs are
   * disabled.
   */
  ProofNodeManager* d_pnm;
  /** The user context. */
  context::UserContext* d_ctx;
  /**
   * A CDProofSet that hands out CDProof objects for lemmas.
   */
  std::unique_ptr<CDProofSet<CDProof>> d_proof;

  /** The proof checker for transcendental proofs */
  std::unique_ptr<TranscendentalProofRuleChecker> d_proofChecker;

  /**
   * Some transcendental functions f(t) are "purified", e.g. we add
   * t = y ^ f(t) = f(y) where y is a fresh variable. Those that are not
   * purified we call "master terms".
   *
   * The maps below maintain a master/slave relationship over
   * transcendental functions (SINE, EXPONENTIAL, PI), where above
   * f(y) is the master of itself and of f(t).
   *
   * This is used for ensuring that the argument y of SINE we process is on
   * the interval [-pi .. pi], and that exponentials are not applied to
   * arguments that contain transcendental functions.
   */
  std::map<Node, Node> d_trMaster;
  std::map<Node, std::unordered_set<Node>> d_trSlaves;

  /** concavity region for transcendental functions
   *
   * This stores an integer that identifies an interval in
   * which the current model value for an argument of an
   * application of a transcendental function resides.
   *
   * For exp( x ):
   *   region #1 is -infty < x < infty
   * For sin( x ):
   *   region #0 is pi < x < infty (this is an invalid region)
   *   region #1 is pi/2 < x <= pi
   *   region #2 is 0 < x <= pi/2
   *   region #3 is -pi/2 < x <= 0
   *   region #4 is -pi < x <= -pi/2
   *   region #5 is -infty < x <= -pi (this is an invalid region)
   * All regions not listed above, as well as regions 0 and 5
   * for SINE are "invalid". We only process applications
   * of transcendental functions whose arguments have model
   * values that reside in valid regions.
   */
  std::unordered_map<Node, int> d_tf_region;
  /**
   * Maps representives of a congruence class to the members of that class.
   *
   * In detail, a congruence class is a set of terms of the form
   *   { f(t1), ..., f(tn) }
   * such that t1 = ... = tn in the current context. We choose an arbitrary
   * term among these to be the repesentative of this congruence class.
   *
   * Moreover, notice we compute congruence classes only over terms that
   * are transcendental function applications that are "master terms",
   * see d_trMaster/d_trSlave.
   */
  std::map<Node, std::vector<Node>> d_funcCongClass;
  /**
   * A list of all functions for each kind in { EXPONENTIAL, SINE, POW, PI }
   * that are representives of their congruence class.
   */
  std::map<Kind, std::vector<Node>> d_funcMap;

  /** secant points (sorted list) for transcendental functions
   *
   * This is used for tangent plane refinements for
   * transcendental functions. This is the set
   * "get-previous-secant-points" in "Satisfiability
   * Modulo Transcendental Functions via Incremental
   * Linearization" by Cimatti et al., CADE 2017, for
   * each transcendental function application. We store this set for each
   * Taylor degree.
   */
  std::unordered_map<Node, std::map<unsigned, std::vector<Node>>>
      d_secant_points;

  /** PI
   *
   * Note that PI is a (symbolic, non-constant) nullary operator. This is
   * because its value cannot be computed exactly. We constraint PI to
   * concrete lower and upper bounds stored in d_pi_bound below.
   */
  Node d_pi;
  /** PI/2 */
  Node d_pi_2;
  /** -PI/2 */
  Node d_pi_neg_2;
  /** -PI */
  Node d_pi_neg;
  /** the concrete lower and upper bounds for PI */
  Node d_pi_bound[2];
};

}  // namespace transcendental
}  // namespace nl
}  // namespace arith
}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H */


Generated by: GCOVR (Version 3.2)

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