Incremental linearization is a conceptually simple, yet e ective, technique that we have recently proposed for solving satis ability problems over nonlinear real arithmetic constraints, including transcendental functions. A central step in the approach is the generation of linearization 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 e ectiveness of the technique that these constraints are valid (to not remove solutions) and as general as possible (to improve their pruning power). In this extended abstract, we provide more details about how linearization lemmas are generated for transcendental functions, including proofs of their soundness. Such details, which were missing in previous publications, are necessary for an independent reimplementation of the method.
Copyright c by the paper's authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). 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 2.1
We assume the standard rst-order quanti er-free logical setting and standard notions of theory, satis ability, 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
contrast to an algebraic function [
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 de ned as follows: TanLinef;a(x) =_ f (a) + f (a) (x
a) d dx where ddx f is the rst-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 de ned as follows: SecLinef;a;b(x) =_ (x
a) + f (a): f (a) a f (b) b
For a function f that is twice di erentiable 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 fhx; f (x)i j x 2 Rg. 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 2 [l; u], then for all a; x 2 [l; u] TanLinef;a(x) f (x), and for all a; b; x 2 [l; u] ((a 6= b ^ a x b) ! SecLinef;a;b(x) f (x)).
Pn;f;a(x) =_ (x
a)i n X f (i)(a) 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 di erentiable can be written as the sum of the Taylor series and the remainder term: 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 (x) = Pn;f;a(x) + Rn+1;f;a(x) Rn+1;f;a(x) =_ f (n+1)(b) (n + 1)! (x
a)n+1: bool incremental-linearization ('): 1. 'b = initial-abstraction(') 2. = ; 3. precision := initial-precision () 4. while true: 5. if budget-exhausted (): 6. abort 7. hres; bi = check-linear ('b ^ V ) 8. if not res: 9. return false 10. hsat; 0i := 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
The value of the point b is not known, but the upper bound on the size of the remainder Rnu+1;f;a(x) at a point x can be estimated by:
Rnu+1;f;a(x) =_
max ( f (n+1)(c)j) c2[min(a;x);max(a;x)] j j(x (n + 1)! a)n+1j : This allows to obtain two polynomials that are above and below the function at a given point x, by considering Pn;f;a(x) + Rnu+1;f;a(x) and Pn;f;a(x) Rnu+1;f;a(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 [
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 re nement of non-linear multiplications as described
in [
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.
[
If at least one point was re ned 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 1In this case, we add a constraint l
u , for two suitable values l and u , which are re ned when needed (see x5).
hbool; lemma-seti check-refine (', b, precision):
1. := check-refine-NRA (', b) # NRA re nement of [
Given a transcendental function application tf(x), the block-spurious-nta-term function generates a set of lemmas for re ning 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 re nement, a second value, di erent 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 re nement 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 in ection 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 re nement point b[x] by calling store-secant-point.
In the case of tangent re nement, 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 e ectively, 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 3.1
Since ddx exp(x) = exp(x), all the derivatives of exp are positive. The polynomial Pn;exp;0(x) is given by the Maclaurin series
Pn;exp;0(x) =
Xn xi
i!
i=0
and behaves di erently depending on the sign of x. Thus, get-polynomial-bounds (see Fig. 2) distinguishes
two cases for nding the polynomials Pl(x) and Pu(x):2
2The case x = 0 is treated specially, by adding the lemma exp(0) = 1 (see [
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 re nement 5. prev := get-previous-secant-points (tf(x)) 6. l := maxfp 2 prev j p < cg 7. u := minfp 2 prev j p > cg 8. P := (v Pl(c)) ? (Pl) : (Pu) 9. Sl(x) := P (l)l 10. Su(x) := P (uu) cP (c) (x u) + P (u) 11. l := (conc < 0) ? (ftf(x) Sl(x)) : (ftf(x) 12. u := (conc < 0) ? (ftf(x) Su(x)) : (ftf(x) 13. l := (x l) ^ (x c) 14. u := (x c) ^ (x u) 15. store-secant-point (tf(x), c) 16. return f( l ! l), ( u ! u)g 17. else: # (v Pl(c) and conc 0) or (v Pu(c) and conc
# tangent re nement 18. P := (v Pl(c)) ? (Pl) : (Pu) 19. T (x) := P (c) + ddx P (c) (x c) # tangent of P at c 20. hl; ui := get-tangent-bounds (tf(x), c, ddx P (c)) 21. := (conc < 0) ? (ftf(x) T (x)) : (ftf(x) T (x)) 22. return f((x l) ^ (x u)) ! g
Sl(x)) Su(x))
0) P (c) (x l) + P (l) # secant of P between l and c 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; Case x > 0: we have that Pn;exp;0(x) < exp(x) and Pn;exp;0(x) (1 therefore we set Pl(x) = Pn;exp;0(x) and Pu(x) = Pn;exp;0(x) (1 (xnn++11)! ) 1 > exp(x) when (1 xn+1 (n+1)! ) 1 for a suitable n xn+1 (n+1)! ) > 0, 3. 3
Since the concavity of exp is always positive, the tangent re nement will always give lower bounds for exp(x), and the secant re nement will give upper bounds (see Fig. 3). 3.2
Tangent Validity Interval Lemma 1 Let c 2 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 2 [c; 1].
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; 1]. 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; 1].
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 re nement of exp is [ 1; 1].
Proof. The tangent re nment 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; 1] and I denote the interval [ 1; c[. 3We slightly abuse the notation: Pu(x) is not a polynomial but a rational function.
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; 1] 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 1 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 1.
Case x < c and c < 0: Pl = Pn;exp;0(x) with n being an odd number. The rst-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 [ 1; 1]. 4
The correctness of our re nement 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 2 [ ; [ 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 [
Polynomial Approximation For each term sin(x) that needs to be re ned, we rst check whether b[x] 2 [ 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 re nement as shown in Fig. 3. More precisely, get-polynomial-bounds nds the lower and upper polynomials using Taylor's theorem, which ensures that:
Pn;sin;0(x)
Rnu+1;sin;0(x) sin(x)
Pn;sin;0(x) + Rnu+1;sin;0(x) where
Pn;sin;0(x) = Rnu+1;sin;0(x) = (2(n + 1))! n X ( 1)k (2k + 1)!
x2k+1 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[.
Lemma 5 Let c 2 ]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.
Case c > 2 : We know Pu(x) = Pkn=0 ( (12)kk+x12)k!+1 + (2x(2n(n++11)))! , and Pu00(x) = Pkn=02 ( 1)(k2+k+11x)2!k+1 + (2x(2n(n++11)))! . Moreover, Pu00(c) < 0. The derivative of Pu00 is given by Pu000(x) = Pkn=02 ( 1)(k2+k1)! x2k + (x2n2n++11)! , which can be rewritten as Pu000(x) = (Pn 2;cos;0(x) Rnu 1;cos;0(x)). By Taylor's Theorem, we know (Pn 2;cos;0(x) Rnu 1;cos;0(x)) < cos(x) and so Pu000(x) > cos(x). Since cos(x) > 0 in the interval ] 2 ; [, we can conclude that Pu00 is an increasing function. Given that Pu00(c) < 0 and we can conclude Pu00 will also be negative in the interval ]0; c[.
; 0[. If the concavity of Pl at point c is positive, then the concavity of Pl is also positive Lemma 6 Let c 2 ] in the interval [c; 0[.
Lemma 7 Let I+ =_ ]0; [. The validity bounds for the tangent re nement of sin in I+ is I+. Proof. The tangent re nement of sin in I+ is done by constructing a tangent line (TanLinePu;c(x)) at a point c 2 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 ; [.
Case x > c and c > 2 : The slope Pu0 (x) = Pkn=0 ( 1(2)kk)!x2k , which can be also rewritten as Pu0 (x) = Pn;cos;0(x)+ Rnu+1;cos;0(x). We know that sin0(x) = cos(x) and by Taylor's Theorem Pn;cos;0(x) + Rnu+1;cos;0(x) cos(x). And 4Hint: Apply Horner's rule for Pu00 interval evaluation. 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 re nement of sin in I is I .
Lemma 9 The validity interval for tangent re nement 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
The re nement of is done by expanding the series given by Machin's formula [
We would like to thank Dejan Jovanovic and Andrew Reynolds for fruitful discussions about the tangent re
nement, that motivated us to write this note.
5Note that the case of 0 is treated specially, by adding the lemma sin(0) = 0 (see [