=Paper=
{{Paper
|id=Vol-2460/paper8
|storemode=property
|title=Lemmas for Satisfiability Modulo Transcendental Functions via Incremental Linearization
|pdfUrl=https://ceur-ws.org/Vol-2460/paper8.pdf
|volume=Vol-2460
|authors=Ahmed Irfan,Alessandro Cimatti,Alberto Griggio,Marco Roveri,Roberto Sebastiani
|dblpUrl=https://dblp.org/rec/conf/scsquare/IrfanCGRS19
}}
==Lemmas for Satisfiability Modulo Transcendental Functions via Incremental Linearization==
https://ceur-ws.org/Vol-2460/paper8.pdf
Lemmas for Satisfiability Modulo Transcendental
Functions via Incremental Linearization
(extended abstract)
Ahmed Irfan1 Alessandro Cimatti2 Alberto Griggio2 Marco Roveri2
Roberto Sebastiani3
1 2 3
Stanford University, USA Fondazione Bruno Kessler, Italy University of Trento, Italy
Abstract
Incremental linearization is a conceptually simple, yet effective, tech-
nique that we have recently proposed for solving satisfiability prob-
lems over nonlinear real arithmetic constraints, including transcenden-
tal functions. A central step in the approach is the generation of lin-
earization lemmas, constraints that are added during search to the
SMT problem and that form a piecewise-linear approximation of the
nonlinear functions in the input problem. It is crucial for both the
soundness and the effectiveness of the technique that these constraints
are valid (to not remove solutions) and as general as possible (to im-
prove their pruning power). In this extended abstract, we provide more
details about how linearization lemmas are generated for transcenden-
tal functions, including proofs of their soundness. Such details, which
were missing in previous publications, are necessary for an independent
reimplementation of the method.
1 Introduction
The field of Satisfiability Modulo Theories (SMT) has seen tremendous progress in the last decade. Nowadays,
powerful and effective SMT solvers are available for a number of quantifier-free theories and their combinations,
such as equality and uninterpreted functions, bit-vectors, arrays, and linear arithmetic. A fundamental challenge
is to go beyond the linear case, by introducing nonlinear polynomials and transcendental functions.
Recently, we have proposed a conceptually simple, yet effective approach for dealing with the quantifier-free
theory of nonlinear arithmetic over the reals, called Incremental Linearization [2, 3, 4, 5]. Its underlying idea is
that of trading the use of expensive, exact solvers for nonlinear arithmetic for an abstraction-refinement loop on
top of much less expensive solvers for linear arithmetic and uninterpreted functions. The approach is based on
an abstraction-refinement loop, in which the input problem is overapproximated using an SMT formula in which
nonlinear multiplications and transcendental functions are treated as uninterpreted. The initial approximation
is then iteratively refined, by incrementally adding linearization lemmas, i.e. constraints that form a piecewise-
linear approximation of the nonlinear functions in the input problem. How such lemmas are actually generated
is a central aspect of the incremental linearization method. Although most of the details have been provided
in previous publications (most notably [5]), some aspects of the lemma generation procedure for transcendental
functions were only described at a high level of abstraction, leaving a gap between the algorithmic description
and the actual implementation that might make an independent reimplementation of the method difficult. In
Copyright c by the paper’s authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
In: J. Abbott, A. Griggio (eds.): Proceedings of the 4th SC-square Workshop, Bern, Switzerland, 10th July 2019, published at
http://ceur-ws.org
this extended abstract, we close this gap, by providing the missing details about how linearization lemmas are
generated for transcendental functions, including proofs of their soundness.
2 Background
2.1 Basic definitions
We assume the standard first-order quantifier-free logical setting and standard notions of theory, satisfiability,
and logical consequence. We denote formulas with ϕ, ψ, terms with t, variables with x, y, a, b, functions with
f, tf, ftf , each possibly with subscripts. If µ is a model and x is a variable, we write µ[x] to denote the value
of x in µ, and we extend this notation to terms and formulas in the usual way.
A transcendental function (tf) is an analytic function that does not satisfy a polynomial equation (in con-
trast to an algebraic function [8, 6]). Within this paper we consider univariate exponential, logarithmic, and
trigonometric functions. We denote with NTA the theory of non-linear real arithmetic (NRA) extended with
these transcendental functions.
A tangent line to a univariate function f (x) at a point of interest x = a is a straight line that “just touches”
the function at the point, and represents the instantaneous rate of change of the function f at that one point.
The tangent line TanLinef,a (x) to the function f at point a is the straight line defined as follows:
d
TanLinef,a (x) =
˙ f (a) + f (a) ∗ (x − a)
dx
d
where dx f is the first-order derivative of f wrt. x.
A secant line to a univariate function f (x) is a straight line that connects two points on the function plot.
The secant line SecLinef,a,b (x) to a function f between points a and b is defined as follows:
f (a) − f (b)
SecLinef,a,b (x) =
˙ ∗ (x − a) + f (a).
a−b
For a function f that is twice differentiable at point c, the concavity of f at c is the sign of its second
derivative evaluated at c. We denote open and closed intervals between two real numbers l and u as ]l, u[ and
[l, u] respectively. Given a univariate function f over the reals, the graph of f is the set of pairs {hx, f (x)i | x ∈ R}.
We might sometimes refer to an element hx, f (x)i of the graph as a point.
Proposition 1 Let f be a univariate function. If f 00 (x) > 0 for all x ∈ [l, u], then for all a, x ∈ [l, u]
TanLinef,a (x) ≤ f (x), and for all a, b, x ∈ [l, u] ((a 6= b ∧ a ≤ x ≤ b) → SecLinef,a,b (x) ≥ f (x)).
If f 00 (x) < 0, then the dual property holds.
Taylor Series and Taylor’s Theorem.
Given a function f (x) that has n + 1 continuous derivatives at x = a, the Taylor series of degree n centered
around a is the polynomial:
n
X f (i) (a)
Pn,f,a (x) =
˙ ∗ (x − a)i
i=0
i!
where f (i) (a) is the evaluation of i-th derivative of f (x) at point x = a. The Taylor series centered around 0 is
also called Maclaurin series.
According to Taylor’s theorem, any continuous function f (x) that is n + 1 differentiable can be written as the
sum of the Taylor series and the remainder term:
f (x) = Pn,f,a (x) + Rn+1,f,a (x)
where Rn+1,f,a (x) is basically the Lagrange form of the remainder, and for some point b between x and a it is
given by:
f (n+1) (b)
Rn+1,f,a (x) =
˙ ∗ (x − a)n+1 .
(n + 1)!
bool incremental-linearization (ϕ):
1. ϕb = initial-abstraction(ϕ)
2. Γ = ∅
3. precision := initial-precision ()
4. while true:
5. if budget-exhausted ():
6. abort V
7. hres, µ
bi = check-linear (ϕ b ∧ Γ)
8. if not res:
9. return false
10. hsat, Γ0 i := check-refine (ϕ, µ
b, precision)
11. if sat:
12. return true
13. else:
14. precision := maybe-increase-precision ()
15. Γ00 := refine-extra (ϕ, µb)
16. Γ := Γ ∪ Γ0 ∪ Γ00
Figure 1: Solving SMT(NTA) via incremental linearization.
u
The value of the point b is not known, but the upper bound on the size of the remainder Rn+1,f,a (x) at a point
x can be estimated by:
|(x − a)n+1 |
u
Rn+1,f,a (x) =
˙ max (|f (n+1) (c)|) ∗ .
c∈[min(a,x),max(a,x)] (n + 1)!
This allows to obtain two polynomials that are above and below the function at a given point x, by considering
u
Pn,f,a (x) + Rn+1,f,a (x) and Pn,f,a (x) − Rn+1,f,a
u
(x) respectively.
2.2 Incremental linearization
The main incremental linearization algorithm is shown in Fig. 1. In the following, we summarize its main steps.
For the full details, we refer the reader to [5]. The solving procedure follows a classic abstraction-refinement
loop. Initially, all non-linear multiplications and transcendental functions are treated as uninterpreted functions,
resulting in a formula ϕ b over the theory of linear arithmetic and uninterpreted functions. Note that also π is
treatead as an uninterpreted constant.1 Then, at each iteration the current safe approximation ϕ b of the input
formula ϕ is refined by adding new constraints Γ that rule out one (or possibly more) spurious solutions, until one
of the following
V conditions occurs: (i) the resource budget (e.g. time, memory, number of iterations) is exhausted;
b ∧ Γ becomes unsatisfiable in the theory ofVlinear arithmetic and uninterpreted functions (UFLRA);
or (ii) ϕ
or (iii) the satisfiability result (in UFLRA) for ϕ b ∧ Γ can be lifted to a satisfiability result for the original
formula ϕ. An initial current precision is set (calling the function initial-precision), and this value is possibly
increased at each iteration (calling maybe-increase-precision) according to the result of check-refine and
some heuristic.
The core of the procedure is the check-refine function, shown in Fig. 2. First, if the formula contains also
some non-linear polynomials, check-refine performs the refinement of non-linear multiplications as described
in [5]. Then, the function iterates over all the transcendental function applications tf(x) in ϕ (lines 3–7), and
checks whether the model µ b computed for ϕ b is consistent with their semantics.
Intuitively, in principle, this amounts to check that tf(b µ[x]) is equal to µ
b[ftf (x)]. In practice, however, the
check cannot be exact, since transcendental functions at rational points typically have irrational values (see e.g.
[7]), which cannot be represented exactly in an SMT solver for linear arithmetic. Therefore, for each tf(x) in
ϕ, we instead compute two polynomials, Pl (x) and Pu (x), with the property that tf(b µ[x]) belongs to the open
interval ]Pl (b
µ[x]), Pu (b
µ[x])[. The polynomials are computed using Taylor series, according to the given current
precision, by the function get-polynomial-bounds. If the model value µ b[ftf (x)] for tf(x) is outside the above
interval, then the function block-spurious-nta-term is used to generate some linear lemmas that will remove
the spurious point hb µ[x], µ
b[ftf (x)]i from the graph of the current abstraction of tf(x) (line 7).
If at least one point was refined in the loop of lines 3–7, the current set of lemmas Γ is returned (line 10). If
instead none of the points was determined to be spurious, the function check-model is called (line 9). This
1 In this case, we add a constraint l
π ≤ π ≤ uπ , for two suitable values lπ and uπ , which are refined when needed (see §5).
hbool, lemma-seti check-refine (ϕ, µ b, precision):
1. Γ := check-refine-NRA (ϕ, µ b) # NRA refinement of [2]
2. := 10−precision
3. for all tf(x) ∈ ϕ:
4. c := µb[x]
5. hPl (x), Pu (x)i := get-polynomial-bounds (tf(x), c, )
6. b[ftf (x)] ≤ Pl (c) or µ
if µ b[ftf (x)] ≥ Pu (c):
7. Γ := Γ∪ block-spurious-nta-term (tf(x), µ b, Pl (x), Pu (x))
8. if Γ = ∅:
9. if check-model (ϕ, µ b):
10. return htrue, ∅i
11. else:
12. return check-refine (ϕ, µ b, precision+1)
13. else:
14. return hfalse, Γi
Figure 2: The main refinement procedure.
function tries to determine whether the abstract model µ b does indeed imply the existence of a model for the
original formula ϕ. If the check fails, we repeat the check-refine call with an increased precision (line 12).
Refining a spurious point with secant and tangent lines.
Given a transcendental function application tf(x), the block-spurious-nta-term function generates a set
of lemmas for refining the interpretation of ftf (x) by constructing a piecewise-linear approximation of tf(x)
around the point µ b[x], using one of the polynomials Pl (x) and Pu (x) computed in check-refine. The kind
of lemmas generated, and which of the two polynomials is used, depend on (i) the position of the spurious
value µb[ftf (x)] relative to the correct value tf(b µ[x]), and (ii) the concavity of tf around the point µ b[x]. If the
concavity is negative (resp. positive) and the point is below (resp. above) the function, the linear approximation
is given by a pair of secants to the lower (resp. upper) bound polynomial Pl (resp. Pu ) around µ b[x] (lines 4–16
of Fig. 3). Otherwise, i.e. the concavity is positive (resp. negative) or equal to zero, and the point lies below
(resp. above) the function, then the linear approximation is given by a tangent to the lower (resp. upper) bound
polynomial Pl (resp. Pu ) at µ b[x] (lines 17–22 of Fig. 3). The two situations are illustrated in Fig. 4.
In the case of secant refinement, a second value, different from µ b[x], is required to draw a secant line. The
function get-previous-secant-points returns the set of all the points at which a secant refinement was
performed in the past for tf(x). From this set, we take the two points closest to µ b[x], such that l < µb[x] < u and
that l, u do not cross any inflection point, and use those points to generate two secant lines and their validity
intervals. Before returning the set of the two corresponding lemmas, we also store the new secant refinement
point µb[x] by calling store-secant-point.
In the case of tangent refinement, the function get-tangent-bounds (line 20) returns a validity interval for
the lemma, i.e. an interval [l, u] such that the tangent line is guaranteed not to cross the transcendental function
tf. In order to generate strong lemmas that can prune the search space effectively, it is important that this
validity interval is as large as possible. At the same time, it is critical for correctness that the interval is not too
large, i.e. that no intersection exists between the transcendental function and its tangent at c in [l, u]. We shall
describe in detail how such validity intervals are computed for the transcendental functions that are currently
supported by our implementation (namely exp and sin) in the next two Sections.
3 Lemmas for exp
3.1 Polynomial Approximation
d
Since dx exp(x) = exp(x), all the derivatives of exp are positive. The polynomial Pn,exp,0 (x) is given by the
Maclaurin series
n
X xi
Pn,exp,0 (x) =
i=0
i!
and behaves differently depending on the sign of x. Thus, get-polynomial-bounds (see Fig. 2) distinguishes
two cases for finding the polynomials Pl (x) and Pu (x):2
2 The case x = 0 is treated specially, by adding the lemma exp(0) = 1 (see [5]).
lemma-set block-spurious-nta-term (tf(x), µ b, Pl (x), Pu (x)):
1. c := µb[x]
2. v := µb[ftf (x)]
3. conc := get-concavity (tf(x), c)
4. if (v ≤ Pl (c) and conc < 0) or (v ≥ Pu (c) and conc > 0):
# secant refinement
5. prev := get-previous-secant-points (tf(x))
6. l := max{p ∈ prev | p < c}
7. u := min{p ∈ prev | p > c}
8. P := (v ≤ Pl (c)) ? (Pl ) : (Pu )
P (l) − P (c)
9. Sl (x) := · (x − l) + P (l) # secant of P between l and c
l−c
P (u) − P (c)
10. Su (x) := · (x − u) + P (u)
u−c
11. ψl := (conc < 0) ? (ftf (x) ≥ Sl (x)) : (ftf (x) ≤ Sl (x))
12. ψu := (conc < 0) ? (ftf (x) ≥ Su (x)) : (ftf (x) ≤ Su (x))
13. φl := (x ≥ l) ∧ (x ≤ c)
14. φu := (x ≥ c) ∧ (x ≤ u)
15. store-secant-point (tf(x), c)
16. return {(φl → ψl ), (φu → ψu )}
17. else: # (v ≤ Pl (c) and conc ≥ 0) or (v ≥ Pu (c) and conc ≤ 0)
# tangent refinement
18. P := (v ≤ Pl (c)) ? (Pl ) : (Pu )
d
19. T (x) := P (c) + dx P (c) · (x − c) # tangent of P at c
d
20. hl, ui := get-tangent-bounds (tf(x), c, dx P (c))
21. ψ := (conc < 0) ? (ftf (x) ≤ T (x)) : (ftf (x) ≥ T (x))
22. return {((x ≥ l) ∧ (x ≤ u)) → ψ}
Figure 3: Piecewise-linear refinement for the transcendental function tf(x) at point c.
Case x < 0: we have that Pn,exp,0 (x) < exp(x) if n is odd and n ≥ 3, and Pn,exp,0 (x) > exp(x) if n is even and
n ≥ 3; we therefore set Pl (x) = Pn,exp,0 (x) and Pu (x) = Pn+1,exp,0 (x) for a suitable n so that the required
precision is met;
n+1 n+1
x
Case x > 0: we have that Pn,exp,0 (x) < exp(x) and Pn,exp,0 (x) ∗ (1 − (n+1)! )−1 > exp(x) when (1 − (n+1)!
x
) > 0,
n+1
x
therefore we set Pl (x) = Pn,exp,0 (x) and Pu (x) = Pn,exp,0 (x) ∗ (1 − (n+1)! )−1 for a suitable n ≥ 3. 3
Since the concavity of exp is always positive, the tangent refinement will always give lower bounds for exp(x),
and the secant refinement will give upper bounds (see Fig. 3).
3.2 Tangent Validity Interval
Lemma 1 Let c ∈ Q and c 6= 0. If the concavity of Pl at point c is positive, then the concavity of Pl is also
positive for x ∈ [c, ∞].
Proof. We know Pl (x) = Pn,exp,0 (x) and its second-order derivative is Pl00 (x) = Pn−2,exp,0 (x). Let us suppose
that the concavity of Pl at a point c is positive, i.e. Pl00 (c) > 0. We now show that the concavity of Pl remains
postive in the interval [c, ∞]. We split the proof into two cases: c > 0 and c < 0.
Case c > 0: The statement holds because Pl00 is an increasing function – Pl000 is positive in the interval [c, ∞].
Case c < 0: The statement also holds because Pl00 is an increasing function – Pl000 (x) = Pn−3,exp,0 (x) is an
even-degree polynomial and by Taylor’s Theorem we know that it is greater than exp, which is always positive.
Lemma 2 The validity interval for the tangent refinement of exp is [−∞, ∞].
Proof. The tangent refinment of exp is done by constructing a tangent line at a point c (TanLinePl ,c (x)) to Pl .
Due to the way we construct Pl , the concavity of Pl is ensured to match with the concavity of exp (meaning the
concavity is positive) at c. Let I+ denote the interval [c, ∞] and I− denote the interval [−∞, c[.
3 We slightly abuse the notation: P
u (x) is not a polynomial but a rational function.
1.2
p1 tf(x)
1 Pl(x)
Pu(x)
0.8 T(x)
Sl(x), Su(x)
0.6 p2
0.4
0.2
lx ux
0
-0.2
0 0.5 1 1.5 2 2.5 3 3.5 4
Figure 4: Piecewise-linear refinement illustration.
Case x ≥ c: by Lemma 1 we can conclude that the concavity of Pl (x) will remain positive in I+ .
TanLinePl ,c (x) will be below Pl in I+ , and therefore it will be also below exp in I+ .
Case x < c and c > 0: We know that the concavity of Pl is positive in the interval [0, ∞] and TanLinePl ,c (x)
will be below exp. Moreover, the slope Pl0 (c) is always greater than 1, which is greater than the slope exp(d)
for every d < 0. And moving towards −∞ the slope of exp is decreasing, while the slope of TanLinePl ,c (x) is
constant and its values are going to decrease quicker than exp. Moreover, TanLinePl ,c (x) will cross the origin
whereas exp stays positive and converges to zero at −∞.
Case x < c and c < 0: Pl = Pn,exp,0 (x) with n being an odd number. The first-order derivative of Pl is
Pl0 =
˙ Pn−1,exp,0 (x), which is above exp. This means that the slope of TanLinePl ,c (x) is greater than the exp
slope. So, TanLinePl ,c (x) will be below exp (same argument as above).
Thanks to Lemma 2, therefore, the implementation of get-tangent-bounds for exp can always return the
interval [−∞, ∞].
4 Lemmas for sin
The correctness of our refinement procedure relies crucially on being able to compute the concavity of the
transcendental function tf at a given point c. This is needed in order to know whether a computed tangent or
secant line constitutes a valid upper or lower bound for tf around c (see 3). In the case of the sin function,
computing the concavity at an arbitrary point c is problematic, since this essentially amounts to computing the
value c0 ∈ [−π, π[ s.t. c = 2πn + c0 for some integer n, because in [−π, π[ the concavity of sin(c0 ) is the opposite
of the sign of c0 . This is not easy to compute because π is a transcendental number.
In order to solve this problem, we exploit another property of sin, namely its periodicity (with period 2π).
More precisely, we split the reasoning about sin depending on two kinds of periods: base period, in the interval
[−π, π], and extended period (everywhere else in R). For more details about the extended period, we refer to
Section 4.2.2 in [5]. Here, we focus only on the base period, where all the refinement lemmas are instantiated.
We can easily compute the concavity of sin in the base period by just looking at the sign of µ b[x], provided that
−lπ ≤ µb[x] ≤ lπ , where lπ is the current lower bound for π.
4.1 Polynomial Approximation
For each term sin(x) that needs to be refined, we first check whether µb[x] ∈ [−lπ , lπ ], where lπ is the current lower
bound for π. If this is the case, then we derive the concavity of sin at µ
b[x] by just looking at the sign of µ b[x]. We
can therefore perform tangent or secant refinement as shown in Fig. 3. More precisely, get-polynomial-bounds
finds the lower and upper polynomials using Taylor’s theorem, which ensures that:
u u
Pn,sin,0 (x) − Rn+1,sin,0 (x) ≤ sin(x) ≤ Pn,sin,0 (x) + Rn+1,sin,0 (x)
where
n
X (−1)k ∗ x2k+1
Pn,sin,0 (x) =
(2k + 1)!
k=0
2(n+1)
u x
Rn+1,sin,0 (x) =
(2(n + 1))!
We set Pl (x) = Pn,sin,0 (x) − Rn+1,sin,0
u u
(x) and Pu (x) = Pn,sin,0 (x) + Rn+1,sin,0 (x).
The remaining case to discuss is when the value of x in µ b is not within the interval [−lπ , lπ ] (which means
that |b
µ[x]| ∈ (lπ , uπ ]). In this case, we cannot reliably compute the concavity of sin at µb[x]. Therefore, we refine
the approximation for π instead, as described in §5.
4.2 Tangent Validity Interval
Lemma 3 The concavity of Pu matches with the concavity of sin in the interval ]0, π2 ].
Proof. The concavity of sin is negative in the interval ]0, π[. At a point of interest c > 0, we ensure that
Pu00 (c) < 0. This requires that we expand the Taylor series with n > 0, so that the resulting polynomial has
degree strictly greater than 2. Using interval arithmetic, we can easily show that Pu00 is always negative in the
interval ]0, π2 ] 4 .
Lemma 4 The concavity of Pl matches with the concavity of sin in the interval [− π2 , 0[.
Proof. Similar to the proof of Lemma 3.
Lemma 5 Let c ∈ ]0, π[. If the concavity of Pu at point c is negative, then the concavity of Pu is also negative
in the interval ]0, c].
Proof. Case c ≤ π2 : the statement holds due to Lemma 3.
k
Pn ∗x2k+1 x2(n+1)
Pn−2 k+1
∗x2k+1 x2(n+1)
Case c > π2 : We know Pu (x) = k=0 (−1) (2k+1)! + (2(n+1))! , and Pu00 (x) = k=0 (−1)(2k+1)! + (2(n+1))! .
00 00 000
Pn−2 (−1)k+1 ∗x2k x2n+1
Moreover, Pu (c) < 0. The derivative of Pu is given by Pu (x) = k=0 (2k)! + (2n+1)! , which can be rewrit-
ten as Pu000 (x) = −(Pn−2,cos,0 (x)−Rn−1,cos,0
u
(x)). By Taylor’s Theorem, we know (Pn−2,cos,0 (x)−Rn−1,cos,0u
(x)) <
cos(x) and so Pu000 (x) > − cos(x). Since − cos(x) > 0 in the interval ] π2 , π[, we can conclude that Pu00 is an in-
creasing function. Given that Pu00 (c) < 0 and we can conclude Pu00 will also be negative in the interval ]0, c[.
Lemma 6 Let c ∈ ] − π, 0[. If the concavity of Pl at point c is positive, then the concavity of Pl is also positive
in the interval [c, 0[.
Proof. Similar to the proof of Lemma 5.
Lemma 7 Let I+ =
˙ ]0, π[. The validity bounds for the tangent refinement of sin in I+ is I+ .
Proof. The tangent refinement of sin in I+ is done by constructing a tangent line (TanLinePu ,c (x)) at a point
c ∈ I+ to Pu . Due to the way we construct Pu , the concavity of Pu is ensured to match with the concavity of
sin (meaning the concavity is negative) at c.
Case x ≤ c: By Lemma 5, we can conclude that the concavity of Pu (x) remains negative. TanLinePu ,c (x) is
above Pu , and therefore it is also above sin.
Case x > c and c ≤ π2 : Due to Lemma 3, the concavity of Pu matches with the concavity of sin. So,
TanLinePu ,c (x) is above in the interval ]0, π2 [. Moreover, the slope of TanLinePu ,c (x) is positive and the line
does not cross sin in the interval because the slope of sin is negative in ] π2 , π[.
k
Pn ∗x2k
Case x > c and c > π2 : The slope Pu0 (x) = k=0 (−1)(2k)! , which can be also rewritten as Pu0 (x) = Pn,cos,0 (x)+
0
u
Rn+1,cos,0 u
(x). We know that sin (x) = cos(x) and by Taylor’s Theorem Pn,cos,0 (x) + Rn+1,cos,0 (x) ≥ cos(x). And
4 Hint: Apply Horner’s rule for P 00 interval evaluation.
u
therefore Pu0 (x) ≥ sin0 (x). The slope of sin keeps decreasing when moving from π2 to π, whereas the slope of
TanLinePu ,c (x) is greater than the slope of sin and is also constant. Therefore, sin will decrease and crosses the
origin faster than the tangent line.
˙ ] − π, 0[. The validity interval for tangent refinement of sin in I− is I− .
Lemma 8 Let I− =
Proof. Similar to the proof of Lemma 7.
Lemma 9 The validity interval for tangent refinement is ]0, π[ when x > 0 and ] − π, 0[ when x < 0.
Proof. The statement holds due to Lemma 7 and Lemma 8.
Thanks to Lemma 9, therefore, the implementation of get-tangent-bounds for sin (see Fig. 3) returns the
interval ] − π, 0[ if the input tangent point c is negative, and ]0, π[ if it is positive.5
5 Lemmas for π
The refinement of π is done by expanding the series given by Machin’s formula [1]. We keep a current precision
n (a positive integer) for π, which is used to update the bounds lπ and uπ using the inequalities (1) and (2)
respectively:
2n+1
X (−1)k
4 1
π >4∗ ∗ 2k+1
− (1)
2k + 1 5 2392k+1
k=0
2(n+1)
(−1)k
X 4 1
π <4∗ ∗ − . (2)
2k + 1 52k+1 2392k+1
k=0
Acknowledgement
We would like to thank Dejan Jovanovic and Andrew Reynolds for fruitful discussions about the tangent refine-
ment, that motivated us to write this note.
References
[1] Berggren, J., Borwein, J., Borwein, P.: Pi: A Source Book. Springer New York (2013)
[2] Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Invariant checking of NRA transition systems
via incremental reduction to LRA with EUF. In: TACAS. LNCS, vol. 10205, pp. 58–75 (2017)
[3] Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Satisfiability modulo transcendental functions
via incremental linearization. In: de Moura, L. (ed.) CADE 26. LNCS, vol. 10395, pp. 95–113. Springer (2017)
[4] Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Experimenting on solving nonlinear integer
arithmetic with incremental linearization. In: SAT. Lecture Notes in Computer Science, vol. 10929, pp.
383–398. Springer (2018)
[5] Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Incremental Linearization for Satisfiability
and Verification Modulo Nonlinear Arithmetic and Transcendental Functions. ACM Trans. Comput. Log.
19(3), 19:1–19:52 (2018). https://doi.org/10.1145/3230639
[6] Hazewinkel, M.: Encyclopaedia of Mathematics: Stochastic Approximation – Zygmund Class of Functions.
Encyclopaedia of Mathematics, Springer Netherlands (1993)
[7] Niven, I.: Numbers: Rational and Irrational. Mathematical Association of America (1961)
[8] Townsend, E.: Functions of a Complex Variable. Read Books (2007)
5 Note that the case of 0 is treated specially, by adding the lemma sin(0) = 0 (see [5]).