Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/nl/transcendental/transcendental_solver.cpp	Lines:	177	206	85.9 %
Date:	2021-11-05	Branches:	348	827	42.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Gereon Kremer, Tim King
 *
 * 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.
 * ****************************************************************************
 *
 * Implementation of solver for handling transcendental functions.
 */

#include "theory/arith/nl/transcendental/transcendental_solver.h"

#include <cmath>
#include <set>

#include "expr/node_algorithm.h"
#include "expr/node_builder.h"
#include "expr/skolem_manager.h"
#include "options/arith_options.h"
#include "theory/arith/arith_msum.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/inference_manager.h"
#include "theory/arith/nl/nl_model.h"
#include "theory/arith/nl/transcendental/taylor_generator.h"
#include "theory/rewriter.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace arith {
namespace nl {
namespace transcendental {

TranscendentalSolver::TranscendentalSolver(InferenceManager& im,
                                           NlModel& m,
                                           Env& env)
    : d_tstate(im, m, env), d_expSlv(&d_tstate), d_sineSlv(&d_tstate)
{
  d_taylor_degree = d_tstate.d_env.getOptions().arith.nlExtTfTaylorDegree;
}

TranscendentalSolver::~TranscendentalSolver() {}

void TranscendentalSolver::initLastCall(const std::vector<Node>& xts)
{
  std::vector<Node> needsMaster;
  d_tstate.init(xts, needsMaster);

  if (d_tstate.d_im.hasUsed()) {
    return;
  }

  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  for (const Node& a : needsMaster)
  {
    // should not have processed this already
    Assert(d_tstate.d_trMaster.find(a) == d_tstate.d_trMaster.end());
    Kind k = a.getKind();
    Assert(k == Kind::SINE || k == Kind::EXPONENTIAL);
    Node y = sm->mkDummySkolem(
        "y", nm->realType(), "phase shifted trigonometric arg");
    Node new_a = nm->mkNode(k, y);
    d_tstate.d_trSlaves[new_a].insert(new_a);
    d_tstate.d_trSlaves[new_a].insert(a);
    d_tstate.d_trMaster[a] = new_a;
    d_tstate.d_trMaster[new_a] = new_a;
    switch (k)
    {
      case Kind::SINE: d_sineSlv.doPhaseShift(a, new_a, y); break;
      case Kind::EXPONENTIAL: d_expSlv.doPurification(a, new_a, y); break;
      default: AlwaysAssert(false) << "Unexpected Kind " << k;
    }
  }
}

bool TranscendentalSolver::preprocessAssertionsCheckModel(
    std::vector<Node>& assertions)
{
  Subs subs;
  for (const auto& sub : d_tstate.d_trMaster)
  {
    subs.add(sub.first, sub.second);
  }

  // initialize representation of assertions
  std::vector<Node> passertions;
  for (const Node& a : assertions)

  {
    Node pa = a;
    if (!subs.empty())
    {
      pa = arithSubstitute(pa, subs);
      pa = Rewriter::rewrite(pa);
    }
    if (!pa.isConst() || !pa.getConst<bool>())
    {
      Trace("nl-ext-cm-assert") << "- assert : " << pa << std::endl;
      passertions.push_back(pa);
    }
  }
  // get model bounds for all transcendental functions
  Trace("nl-ext-cm") << "----- Get bounds for transcendental functions..."
                     << std::endl;
  for (std::pair<const Kind, std::vector<Node> >& tfs : d_tstate.d_funcMap)
  {
    for (const Node& tf : tfs.second)
    {
      Trace("nl-ext-cm") << "- Term: " << tf << std::endl;
      bool success = true;
      // tf is Figure 3 : tf( x )
      std::pair<Node, Node> bounds;
      if (tfs.first == Kind::PI)
      {
        bounds = {d_tstate.d_pi_bound[0], d_tstate.d_pi_bound[1]};
      }
      else
      {
        bounds = d_tstate.d_taylor.getTfModelBounds(
            tf, d_taylor_degree, d_tstate.d_model);
        if (bounds.first != bounds.second)
        {
          d_tstate.d_model.setUsedApproximate();
        }
      }
      if (!bounds.first.isNull() && !bounds.second.isNull())
      {
        // for each function in the congruence classe
        for (const Node& ctf : d_tstate.d_funcCongClass[tf])
        {
          // each term in congruence classes should be master terms
          Assert(d_tstate.d_trSlaves.find(ctf) != d_tstate.d_trSlaves.end());
          // we set the bounds for each slave of tf
          for (const Node& stf : d_tstate.d_trSlaves[ctf])
          {
            Trace("nl-ext-cm")
                << "...bound for " << stf << " : [" << bounds.first << ", "
                << bounds.second << "]" << std::endl;
            success =
                d_tstate.d_model.addBound(stf, bounds.first, bounds.second);
          }
        }
      }
      else
      {
        Trace("nl-ext-cm") << "...no bound for " << tf << std::endl;
      }
      if (!success)
      {
        // a bound was conflicting
        Trace("nl-ext-cm") << "...failed to set bound for " << tf << std::endl;
        Trace("nl-ext-cm") << "-----" << std::endl;
        return false;
      }
    }
  }
  // replace the assertions
  assertions = std::move(passertions);
  return true;
}

void TranscendentalSolver::incrementTaylorDegree() { d_taylor_degree++; }
unsigned TranscendentalSolver::getTaylorDegree() const
{
  return d_taylor_degree;
}

void TranscendentalSolver::processSideEffect(const NlLemma& se)
{
  for (const std::tuple<Node, unsigned, Node>& sp : se.d_secantPoint)
  {
    Node tf = std::get<0>(sp);
    unsigned d = std::get<1>(sp);
    Node c = std::get<2>(sp);
    d_tstate.d_secant_points[tf][d].push_back(c);
  }
}

void TranscendentalSolver::checkTranscendentalInitialRefine()
{
  d_expSlv.checkInitialRefine();
  d_sineSlv.checkInitialRefine();
}

void TranscendentalSolver::checkTranscendentalMonotonic()
{
  d_expSlv.checkMonotonic();
  d_sineSlv.checkMonotonic();
}

void TranscendentalSolver::checkTranscendentalTangentPlanes()
{
  if (Trace.isOn("nl-ext"))
  {
    if (!d_tstate.d_funcMap.empty())
    {
      Trace("nl-ext")
          << "Get tangent plane lemmas for transcendental functions..."
          << std::endl;
    }
  }
  // this implements Figure 3 of "Satisfiaility Modulo Transcendental Functions
  // via Incremental Linearization" by Cimatti et al
  for (const std::pair<const Kind, std::vector<Node> >& tfs :
       d_tstate.d_funcMap)
  {
    Kind k = tfs.first;
    if (k == PI)
    {
      // We do not use Taylor approximation for PI currently.
      // This is because the convergence is extremely slow, and hence an
      // initial approximation is superior.
      continue;
    }

    // we substitute into the Taylor sum P_{n,f(0)}( x )

    for (const Node& tf : tfs.second)
    {
      // tf is Figure 3 : tf( x )
      Trace("nl-ext-tftp") << "Compute tangent planes " << tf << std::endl;
      // go until max degree is reached, or we don't meet bound criteria
      for (unsigned d = 1; d <= d_taylor_degree; d++)
      {
        Trace("nl-ext-tftp") << "- run at degree " << d << "..." << std::endl;
        unsigned prev =
            d_tstate.d_im.numPendingLemmas() + d_tstate.d_im.numWaitingLemmas();
        if (checkTfTangentPlanesFun(tf, d))
        {
          Trace("nl-ext-tftp") << "...fail, #lemmas = "
                               << (d_tstate.d_im.numPendingLemmas()
                                   + d_tstate.d_im.numWaitingLemmas() - prev)
                               << std::endl;
          break;
        }
        else
        {
          Trace("nl-ext-tftp") << "...success" << std::endl;
        }
      }
    }
  }
}

bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d)
{
  NodeManager* nm = NodeManager::currentNM();
  Kind k = tf.getKind();
  // this should only be run on master applications
  Assert(d_tstate.d_trSlaves.find(tf) != d_tstate.d_trSlaves.end());

  // Figure 3 : c
  Node c = d_tstate.d_model.computeAbstractModelValue(tf[0]);
  int csign = c.getConst<Rational>().sgn();
  if (csign == 0)
  {
    // no secant/tangent plane is necessary
    return true;
  }
  Assert(csign == 1 || csign == -1);

  // Figure 3: P_l, P_u
  // mapped to for signs of c
  std::map<int, Node> poly_approx_bounds[2];
  TaylorGenerator::ApproximationBounds pbounds;
  std::uint64_t actual_d =
      d_tstate.d_taylor.getPolynomialApproximationBoundForArg(k, c, d, pbounds);
  poly_approx_bounds[0][1] = pbounds.d_lower;
  poly_approx_bounds[0][-1] = pbounds.d_lower;
  poly_approx_bounds[1][1] = pbounds.d_upperPos;
  poly_approx_bounds[1][-1] = pbounds.d_upperNeg;

  // Figure 3 : v
  Node v = d_tstate.d_model.computeAbstractModelValue(tf);

  // check value of tf
  Trace("nl-ext-tftp-debug") << "Process tangent plane refinement for " << tf
                             << ", degree " << d << "..." << std::endl;
  Trace("nl-ext-tftp-debug") << "  value in model : " << v << std::endl;
  Trace("nl-ext-tftp-debug") << "  arg value in model : " << c << std::endl;

  // compute the concavity
  int region = -1;
  std::unordered_map<Node, int>::iterator itr = d_tstate.d_tf_region.find(tf);
  if (itr != d_tstate.d_tf_region.end())
  {
    region = itr->second;
    Trace("nl-ext-tftp-debug") << "  region is : " << region << std::endl;
  }
  // Figure 3 : conc
  int concavity = regionToConcavity(k, itr->second);
  Trace("nl-ext-tftp-debug") << "  concavity is : " << concavity << std::endl;
  if (concavity == 0)
  {
    // no secant/tangent plane is necessary
    return true;
  }

  // Figure 3: P
  Node poly_approx;

  // compute whether this is a tangent refinement or a secant refinement
  bool is_tangent = false;
  bool is_secant = false;
  std::pair<Node, Node> mvb =
      d_tstate.d_taylor.getTfModelBounds(tf, d, d_tstate.d_model);
  // this is the approximated value of tf(c), which is a value such that:
  //    M_A(tf(c)) >= poly_appox_c >= tf(c) or
  //    M_A(tf(c)) <= poly_appox_c <= tf(c)
  // In other words, it is a better approximation of the true value of tf(c)
  // in the case that we add a refinement lemma. We use this value in the
  // refinement schemas below.
  Node poly_approx_c;
  for (unsigned r = 0; r < 2; r++)
  {
    Node pab = poly_approx_bounds[r][csign];
    Node v_pab = r == 0 ? mvb.first : mvb.second;
    if (!v_pab.isNull())
    {
      Trace("nl-trans") << "...model value of " << pab << " is " << v_pab
                        << std::endl;

      Assert(v_pab.isConst());
      Node comp = nm->mkNode(r == 0 ? LT : GT, v, v_pab);
      Trace("nl-trans") << "...compare : " << comp << std::endl;
      Node compr = Rewriter::rewrite(comp);
      Trace("nl-trans") << "...got : " << compr << std::endl;
      if (compr == d_tstate.d_true)
      {
        poly_approx_c = Rewriter::rewrite(v_pab);
        // beyond the bounds
        if (r == 0)
        {
          poly_approx = poly_approx_bounds[r][csign];
          is_tangent = concavity == 1;
          is_secant = concavity == -1;
        }
        else
        {
          poly_approx = poly_approx_bounds[r][csign];
          is_tangent = concavity == -1;
          is_secant = concavity == 1;
        }
        if (Trace.isOn("nl-ext-tftp"))
        {
          Trace("nl-ext-tftp") << "*** Outside boundary point (";
          Trace("nl-ext-tftp") << (r == 0 ? "low" : "high") << ") ";
          printRationalApprox("nl-ext-tftp", v_pab);
          Trace("nl-ext-tftp") << ", will refine..." << std::endl;
          Trace("nl-ext-tftp")
              << "    poly_approx = " << poly_approx << std::endl;
          Trace("nl-ext-tftp")
              << "    is_tangent = " << is_tangent << std::endl;
          Trace("nl-ext-tftp") << "    is_secant = " << is_secant << std::endl;
        }
        break;
      }
      else
      {
        Trace("nl-ext-tftp")
            << "  ...within " << (r == 0 ? "low" : "high") << " bound : ";
        printRationalApprox("nl-ext-tftp", v_pab);
        Trace("nl-ext-tftp") << std::endl;
      }
    }
  }

  // Figure 3: P( c )
  if (is_tangent || is_secant)
  {
    Trace("nl-trans") << "...poly approximation at c is " << poly_approx_c
                      << std::endl;
  }
  else
  {
    // we may want to continue getting better bounds
    return false;
  }

  if (is_tangent)
  {
    if (k == Kind::EXPONENTIAL)
    {
      d_expSlv.doTangentLemma(tf, c, poly_approx_c, d);
    }
    else if (k == Kind::SINE)
    {
      d_sineSlv.doTangentLemma(tf, c, poly_approx_c, region, d);
    }
  }
  else if (is_secant)
  {
    if (k == EXPONENTIAL)
    {
      d_expSlv.doSecantLemmas(tf, poly_approx, c, poly_approx_c, d, actual_d);
    }
    else if (k == Kind::SINE)
    {
      d_sineSlv.doSecantLemmas(
          tf, poly_approx, c, poly_approx_c, d, actual_d, region);
    }
  }
  return true;
}

int TranscendentalSolver::regionToConcavity(Kind k, int region)
{
  if (k == EXPONENTIAL)
  {
    if (region == 1)
    {
      return 1;
    }
  }
  else if (k == SINE)
  {
    if (region == 1 || region == 2)
    {
      return -1;
    }
    else if (region == 3 || region == 4)
    {
      return 1;
    }
  }
  return 0;
}

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


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Gereon Kremer, Tim King
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		* Implementation of solver for handling transcendental functions.
14		*/
15
16		#include "theory/arith/nl/transcendental/transcendental_solver.h"
17
18		#include <cmath>
19		#include <set>
20
21		#include "expr/node_algorithm.h"
22		#include "expr/node_builder.h"
23		#include "expr/skolem_manager.h"
24		#include "options/arith_options.h"
25		#include "theory/arith/arith_msum.h"
26		#include "theory/arith/arith_utilities.h"
27		#include "theory/arith/inference_manager.h"
28		#include "theory/arith/nl/nl_model.h"
29		#include "theory/arith/nl/transcendental/taylor_generator.h"
30		#include "theory/rewriter.h"
31
32		using namespace cvc5::kind;
33
34		namespace cvc5 {
35		namespace theory {
36		namespace arith {
37		namespace nl {
38		namespace transcendental {
39
40	9700	TranscendentalSolver::TranscendentalSolver(InferenceManager& im,
41		NlModel& m,
42	9700	Env& env)
43	9700	: d_tstate(im, m, env), d_expSlv(&d_tstate), d_sineSlv(&d_tstate)
44		{
45	9700	d_taylor_degree = d_tstate.d_env.getOptions().arith.nlExtTfTaylorDegree;
46	9700	}
47
48	9697	TranscendentalSolver::~TranscendentalSolver() {}
49
50	3532	void TranscendentalSolver::initLastCall(const std::vector<Node>& xts)
51		{
52	6452	std::vector<Node> needsMaster;
53	3532	d_tstate.init(xts, needsMaster);
54
55	3532	if (d_tstate.d_im.hasUsed()) {
56	612	return;
57		}
58
59	2920	NodeManager* nm = NodeManager::currentNM();
60	2920	SkolemManager* sm = nm->getSkolemManager();
61	3061	for (const Node& a : needsMaster)
62		{
63		// should not have processed this already
64	141	Assert(d_tstate.d_trMaster.find(a) == d_tstate.d_trMaster.end());
65	141	Kind k = a.getKind();
66	141	Assert(k == Kind::SINE \|\| k == Kind::EXPONENTIAL);
67		Node y = sm->mkDummySkolem(
68	282	"y", nm->realType(), "phase shifted trigonometric arg");
69	282	Node new_a = nm->mkNode(k, y);
70	141	d_tstate.d_trSlaves[new_a].insert(new_a);
71	141	d_tstate.d_trSlaves[new_a].insert(a);
72	141	d_tstate.d_trMaster[a] = new_a;
73	141	d_tstate.d_trMaster[new_a] = new_a;
74	141	switch (k)
75		{
76	141	case Kind::SINE: d_sineSlv.doPhaseShift(a, new_a, y); break;
77		case Kind::EXPONENTIAL: d_expSlv.doPurification(a, new_a, y); break;
78		default: AlwaysAssert(false) << "Unexpected Kind " << k;
79		}
80		}
81		}
82
83	247	bool TranscendentalSolver::preprocessAssertionsCheckModel(
84		std::vector<Node>& assertions)
85		{
86	494	Subs subs;
87	631	for (const auto& sub : d_tstate.d_trMaster)
88		{
89	384	subs.add(sub.first, sub.second);
90		}
91
92		// initialize representation of assertions
93	494	std::vector<Node> passertions;
94	4468	for (const Node& a : assertions)
95
96		{
97	8442	Node pa = a;
98	4221	if (!subs.empty())
99		{
100	1789	pa = arithSubstitute(pa, subs);
101	1789	pa = Rewriter::rewrite(pa);
102		}
103	4221	if (!pa.isConst() \|\| !pa.getConst<bool>())
104		{
105	4181	Trace("nl-ext-cm-assert") << "- assert : " << pa << std::endl;
106	4181	passertions.push_back(pa);
107		}
108		}
109		// get model bounds for all transcendental functions
110	494	Trace("nl-ext-cm") << "----- Get bounds for transcendental functions..."
111	247	<< std::endl;
112	447	for (std::pair<const Kind, std::vector<Node> >& tfs : d_tstate.d_funcMap)
113		{
114	527	for (const Node& tf : tfs.second)
115		{
116	327	Trace("nl-ext-cm") << "- Term: " << tf << std::endl;
117	327	bool success = true;
118		// tf is Figure 3 : tf( x )
119	654	std::pair<Node, Node> bounds;
120	327	if (tfs.first == Kind::PI)
121		{
122	58	bounds = {d_tstate.d_pi_bound[0], d_tstate.d_pi_bound[1]};
123		}
124		else
125		{
126	269	bounds = d_tstate.d_taylor.getTfModelBounds(
127		tf, d_taylor_degree, d_tstate.d_model);
128	269	if (bounds.first != bounds.second)
129		{
130	269	d_tstate.d_model.setUsedApproximate();
131		}
132		}
133	327	if (!bounds.first.isNull() && !bounds.second.isNull())
134		{
135		// for each function in the congruence classe
136	654	for (const Node& ctf : d_tstate.d_funcCongClass[tf])
137		{
138		// each term in congruence classes should be master terms
139	327	Assert(d_tstate.d_trSlaves.find(ctf) != d_tstate.d_trSlaves.end());
140		// we set the bounds for each slave of tf
141	711	for (const Node& stf : d_tstate.d_trSlaves[ctf])
142		{
143	768	Trace("nl-ext-cm")
144	384	<< "...bound for " << stf << " : [" << bounds.first << ", "
145	384	<< bounds.second << "]" << std::endl;
146	384	success =
147	768	d_tstate.d_model.addBound(stf, bounds.first, bounds.second);
148		}
149		}
150		}
151		else
152		{
153		Trace("nl-ext-cm") << "...no bound for " << tf << std::endl;
154		}
155	327	if (!success)
156		{
157		// a bound was conflicting
158		Trace("nl-ext-cm") << "...failed to set bound for " << tf << std::endl;
159		Trace("nl-ext-cm") << "-----" << std::endl;
160		return false;
161		}
162		}
163		}
164		// replace the assertions
165	247	assertions = std::move(passertions);
166	247	return true;
167		}
168
169	16	void TranscendentalSolver::incrementTaylorDegree() { d_taylor_degree++; }
170	286	unsigned TranscendentalSolver::getTaylorDegree() const
171		{
172	286	return d_taylor_degree;
173		}
174
175		void TranscendentalSolver::processSideEffect(const NlLemma& se)
176		{
177		for (const std::tuple<Node, unsigned, Node>& sp : se.d_secantPoint)
178		{
179		Node tf = std::get<0>(sp);
180		unsigned d = std::get<1>(sp);
181		Node c = std::get<2>(sp);
182		d_tstate.d_secant_points[tf][d].push_back(c);
183		}
184		}
185
186	3361	void TranscendentalSolver::checkTranscendentalInitialRefine()
187		{
188	3361	d_expSlv.checkInitialRefine();
189	3361	d_sineSlv.checkInitialRefine();
190	3361	}
191
192	1441	void TranscendentalSolver::checkTranscendentalMonotonic()
193		{
194	1441	d_expSlv.checkMonotonic();
195	1441	d_sineSlv.checkMonotonic();
196	1441	}
197
198	395	void TranscendentalSolver::checkTranscendentalTangentPlanes()
199		{
200	395	if (Trace.isOn("nl-ext"))
201		{
202		if (!d_tstate.d_funcMap.empty())
203		{
204		Trace("nl-ext")
205		<< "Get tangent plane lemmas for transcendental functions..."
206		<< std::endl;
207		}
208		}
209		// this implements Figure 3 of "Satisfiaility Modulo Transcendental Functions
210		// via Incremental Linearization" by Cimatti et al
211	218	for (const std::pair<const Kind, std::vector<Node> >& tfs :
212	395	d_tstate.d_funcMap)
213		{
214	218	Kind k = tfs.first;
215	218	if (k == PI)
216		{
217		// We do not use Taylor approximation for PI currently.
218		// This is because the convergence is extremely slow, and hence an
219		// initial approximation is superior.
220	67	continue;
221		}
222
223		// we substitute into the Taylor sum P_{n,f(0)}( x )
224
225	438	for (const Node& tf : tfs.second)
226		{
227		// tf is Figure 3 : tf( x )
228	287	Trace("nl-ext-tftp") << "Compute tangent planes " << tf << std::endl;
229		// go until max degree is reached, or we don't meet bound criteria
230	1239	for (unsigned d = 1; d <= d_taylor_degree; d++)
231		{
232	1171	Trace("nl-ext-tftp") << "- run at degree " << d << "..." << std::endl;
233		unsigned prev =
234	1171	d_tstate.d_im.numPendingLemmas() + d_tstate.d_im.numWaitingLemmas();
235	1171	if (checkTfTangentPlanesFun(tf, d))
236		{
237	438	Trace("nl-ext-tftp") << "...fail, #lemmas = "
238	219	<< (d_tstate.d_im.numPendingLemmas()
239	438	+ d_tstate.d_im.numWaitingLemmas() - prev)
240	219	<< std::endl;
241	219	break;
242		}
243		else
244		{
245	952	Trace("nl-ext-tftp") << "...success" << std::endl;
246		}
247		}
248		}
249		}
250	395	}
251
252	1171	bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d)
253		{
254	1171	NodeManager* nm = NodeManager::currentNM();
255	1171	Kind k = tf.getKind();
256		// this should only be run on master applications
257	1171	Assert(d_tstate.d_trSlaves.find(tf) != d_tstate.d_trSlaves.end());
258
259		// Figure 3 : c
260	2342	Node c = d_tstate.d_model.computeAbstractModelValue(tf[0]);
261	1171	int csign = c.getConst<Rational>().sgn();
262	1171	if (csign == 0)
263		{
264		// no secant/tangent plane is necessary
265		return true;
266		}
267	1171	Assert(csign == 1 \|\| csign == -1);
268
269		// Figure 3: P_l, P_u
270		// mapped to for signs of c
271	2342	std::map<int, Node> poly_approx_bounds[2];
272	2342	TaylorGenerator::ApproximationBounds pbounds;
273		std::uint64_t actual_d =
274	1171	d_tstate.d_taylor.getPolynomialApproximationBoundForArg(k, c, d, pbounds);
275	1171	poly_approx_bounds[0][1] = pbounds.d_lower;
276	1171	poly_approx_bounds[0][-1] = pbounds.d_lower;
277	1171	poly_approx_bounds[1][1] = pbounds.d_upperPos;
278	1171	poly_approx_bounds[1][-1] = pbounds.d_upperNeg;
279
280		// Figure 3 : v
281	2342	Node v = d_tstate.d_model.computeAbstractModelValue(tf);
282
283		// check value of tf
284	2342	Trace("nl-ext-tftp-debug") << "Process tangent plane refinement for " << tf
285	1171	<< ", degree " << d << "..." << std::endl;
286	1171	Trace("nl-ext-tftp-debug") << " value in model : " << v << std::endl;
287	1171	Trace("nl-ext-tftp-debug") << " arg value in model : " << c << std::endl;
288
289		// compute the concavity
290	1171	int region = -1;
291	1171	std::unordered_map<Node, int>::iterator itr = d_tstate.d_tf_region.find(tf);
292	1171	if (itr != d_tstate.d_tf_region.end())
293		{
294	1171	region = itr->second;
295	1171	Trace("nl-ext-tftp-debug") << " region is : " << region << std::endl;
296		}
297		// Figure 3 : conc
298	1171	int concavity = regionToConcavity(k, itr->second);
299	1171	Trace("nl-ext-tftp-debug") << " concavity is : " << concavity << std::endl;
300	1171	if (concavity == 0)
301		{
302		// no secant/tangent plane is necessary
303		return true;
304		}
305
306		// Figure 3: P
307	2342	Node poly_approx;
308
309		// compute whether this is a tangent refinement or a secant refinement
310	1171	bool is_tangent = false;
311	1171	bool is_secant = false;
312		std::pair<Node, Node> mvb =
313	2342	d_tstate.d_taylor.getTfModelBounds(tf, d, d_tstate.d_model);
314		// this is the approximated value of tf(c), which is a value such that:
315		// M_A(tf(c)) >= poly_appox_c >= tf(c) or
316		// M_A(tf(c)) <= poly_appox_c <= tf(c)
317		// In other words, it is a better approximation of the true value of tf(c)
318		// in the case that we add a refinement lemma. We use this value in the
319		// refinement schemas below.
320	2342	Node poly_approx_c;
321	3178	for (unsigned r = 0; r < 2; r++)
322		{
323	4233	Node pab = poly_approx_bounds[r][csign];
324	4233	Node v_pab = r == 0 ? mvb.first : mvb.second;
325	2226	if (!v_pab.isNull())
326		{
327	4452	Trace("nl-trans") << "...model value of " << pab << " is " << v_pab
328	2226	<< std::endl;
329
330	2226	Assert(v_pab.isConst());
331	4233	Node comp = nm->mkNode(r == 0 ? LT : GT, v, v_pab);
332	2226	Trace("nl-trans") << "...compare : " << comp << std::endl;
333	4233	Node compr = Rewriter::rewrite(comp);
334	2226	Trace("nl-trans") << "...got : " << compr << std::endl;
335	2226	if (compr == d_tstate.d_true)
336		{
337	219	poly_approx_c = Rewriter::rewrite(v_pab);
338		// beyond the bounds
339	219	if (r == 0)
340		{
341	116	poly_approx = poly_approx_bounds[r][csign];
342	116	is_tangent = concavity == 1;
343	116	is_secant = concavity == -1;
344		}
345		else
346		{
347	103	poly_approx = poly_approx_bounds[r][csign];
348	103	is_tangent = concavity == -1;
349	103	is_secant = concavity == 1;
350		}
351	219	if (Trace.isOn("nl-ext-tftp"))
352		{
353		Trace("nl-ext-tftp") << "*** Outside boundary point (";
354		Trace("nl-ext-tftp") << (r == 0 ? "low" : "high") << ") ";
355		printRationalApprox("nl-ext-tftp", v_pab);
356		Trace("nl-ext-tftp") << ", will refine..." << std::endl;
357		Trace("nl-ext-tftp")
358		<< " poly_approx = " << poly_approx << std::endl;
359		Trace("nl-ext-tftp")
360		<< " is_tangent = " << is_tangent << std::endl;
361		Trace("nl-ext-tftp") << " is_secant = " << is_secant << std::endl;
362		}
363	219	break;
364		}
365		else
366		{
367	4014	Trace("nl-ext-tftp")
368	2007	<< " ...within " << (r == 0 ? "low" : "high") << " bound : ";
369	2007	printRationalApprox("nl-ext-tftp", v_pab);
370	2007	Trace("nl-ext-tftp") << std::endl;
371		}
372		}
373		}
374
375		// Figure 3: P( c )
376	1171	if (is_tangent \|\| is_secant)
377		{
378	438	Trace("nl-trans") << "...poly approximation at c is " << poly_approx_c
379	438	<< std::endl;
380		}
381		else
382		{
383		// we may want to continue getting better bounds
384	952	return false;
385		}
386
387	219	if (is_tangent)
388		{
389	96	if (k == Kind::EXPONENTIAL)
390		{
391	56	d_expSlv.doTangentLemma(tf, c, poly_approx_c, d);
392		}
393	40	else if (k == Kind::SINE)
394		{
395	40	d_sineSlv.doTangentLemma(tf, c, poly_approx_c, region, d);
396		}
397		}
398	123	else if (is_secant)
399		{
400	123	if (k == EXPONENTIAL)
401		{
402	43	d_expSlv.doSecantLemmas(tf, poly_approx, c, poly_approx_c, d, actual_d);
403		}
404	80	else if (k == Kind::SINE)
405		{
406	80	d_sineSlv.doSecantLemmas(
407		tf, poly_approx, c, poly_approx_c, d, actual_d, region);
408		}
409		}
410	219	return true;
411		}
412
413	1171	int TranscendentalSolver::regionToConcavity(Kind k, int region)
414		{
415	1171	if (k == EXPONENTIAL)
416		{
417	749	if (region == 1)
418		{
419	749	return 1;
420		}
421		}
422	422	else if (k == SINE)
423		{
424	422	if (region == 1 \|\| region == 2)
425		{
426	211	return -1;
427		}
428	211	else if (region == 3 \|\| region == 4)
429		{
430	211	return 1;
431		}
432		}
433		return 0;
434		}
435
436		} // namespace transcendental
437		} // namespace nl
438		} // namespace arith
439		} // namespace theory
440	31125	} // namespace cvc5