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