Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/nl/transcendental/sine_solver.h	Lines:	24	28	85.7 %
Date:	2021-11-07	Branches:	12	16	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.
 * ****************************************************************************
 *
 * Solving for handling exponential function.
 */

#ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H
#define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H

#include <map>

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