tangentspace : linearize nonlinear functions

ver.2019-04-13, Copyright (C) 2019 Norbert Müller

Tangentspace is a tool to compute linearizations to nonlinear functions, suitable for the inclusion into CDCL style SMT solvers like ksmt .

• Download of statically linked linux executables: version 2019-04-13, version 2019-04-11, version 2019-03-24.

• The sources as well as a submitted paper describing the mathematical background will be added after the paper has been accepted.

Usage:

• Define a multivariate function f via a term in prefix notation, for example f(x0,x1) = x0^2 - sin(x1)

  function - * x0 x0 sin x1 end
  

  Currently supported operators and functions: "+", "-", "*", "/", sin, cos, tan, exp, abs and sgn

  Rational constants can have one of the forms 1, -2, 3/4, -5/6. The use of floating point numbers like 7.89 is not supported.

• Specify an argument vector for applying the function defined above, for example x0 = -7/10 = 0.7 and x1 = 2/10 = 0.2

  args -7/10 2/10 end
  

• Specify a value z different from the functional value (a 'conflict'), for example z = 0.3, so z > f(x0,x1)

  conflict 3/10                    
  

• Optionally lists of coordinates for "recycling" linear inequations can be given

  prefer to use bounds from {1.0, -0.6} for variable x0:

  bounds 0 10/10 -6/10 end
  

  prefer to use bounds from {-1, 0, 1, 2} for variable x1:

  bounds 1 -1/1 0/1 1/1 2/1 end
  

• A further option allows to limit the precision in the linearization process and fail deliberately:

  effort 20 
  

  Limit the search for the initial hypercube to a radius of at least 2^-20. The default is to do an unbounded search for arbitraily small cubes.

• Enhance the output by commands suitable to visualize the linearization with gnuplot (restricted to functions with arity <=2). :

  plot 
  

Output is a (lower or upper) linearization (a list of hyperplanes separating conflict and function).

Example 1, Linearization of f(x) = x^3 with conflict f(-0.5) != 1.0

echo 'function * * x0 x0 x0 end args -50/100 end conflict 0/100 plot' | ./tangentspace

decided: upper conflict

x0 >= -72046032675/419430400
x0 <= 30306083976075/27487790694400
z <= 769/2048 + 7/8 * x0

gnuplot -p << PLOTCMD
set grid; set style fill transparent solid 0.2;set xrange [-2:2]; set yrange [-2:2];\
plot ((x*x)*x) with filledc x1,\
[-0.5:-0.5]0 with lp ls 7 title 'conflict',\
(-171.771 < x && x < 1.10253)?0.375488 + 0.875 * x: 1000 with filledc x1 title 'linearization'
PLOTCMD

Example 2, Linearization of f(x) = 4 * sin |x| - 2 with conflict f(-0.4) != 0.5

echo 'function - * 4 sin abs x0 2 end args -40/100 end conflict 5000/10000 plot' | ./tangentspace

decided: upper conflict

x0 >= -27034438435/419430400
x0 <= 90814698736365/7036874417766400
z <= -311471/163840 + -60049/16384 * x0

gnuplot -p << PLOTCMD
set grid; set style fill transparent solid 0.2;set xrange [-2:2]; set yrange [-2:2];\
plot ((4.000000*sin (abs (x)))-2.000000) with filledc x1,\
[-0.4:-0.4]0.5 with lp ls 7 title 'conflict',\
(-64.4551 < x && x < 0.0129055)?-1.90107 + -3.6651 * x: 1000 with filledc x1 title 'linearization'
PLOTCMD

Example 3: Linearization of f(x,y) = sin (x * y) with conflict f(0.5, 0.2) != 1.0

echo 'function sin * x0 x1 end args 50/100 20/100 end conflict 100/100 plot' | ./tangentspace

decided: upper conflict

x0 >= -140085176588125/1759218604441600
x0 <= 3425/3200
x1 >= -15985/51200
x1 <= 41344645822785/54975581388800
z <= 395/2048 + 25/128 * x0 + 125/256 * x1

gnuplot -p << PLOTCMD
set hidden3d;set iso 30;set xrange [-2:2]; set yrange [-2:2]; set zrange [-2:2];
splot sin ((x*y)) with l,\
(-0.0796292 < x && x < 1.07031) &&(-0.312207 < y && y < 0.752055)?0.192871 + 0.195312 * x  + 0.488281 * y : -1000 with l title 'linearization'
PLOTCMD

gnuplot -p << PLOTCMD
set hidden3d;set iso 30;set xrange [-2:2]; set yrange [-2:2]; set zrange [-2:2];
splot  [-0.6546:1.64528]  [-0.844338:1.28419] sin ((x*y)) with l,\
(-0.0796292 < x && x < 1.07031) &&(-0.312207 < y && y < 0.752055)?0.192871 + 0.195312 * x  + 0.488281 * y : -1000  with l title 'linearization'
PLOTCMD

Example 4: Linearization of f(x,y) = sgn(x)*sin(|x*y|) with conflict f(0.0, 0.0) != 1.0

echo 'function * sgn x0 sin abs * x0 x1  end args 0/1 0/1 end conflict 1/1 plot' | ./tangentspace

decided: upper conflict

x0 >= -315214400559/137438953472
x0 <= 141555854681841/281474976710656
x1 >= -1/2
x1 <= 1/2
z <= 515/2048 + 0 * x0 + 0 * x1

gnuplot -p << PLOTCMD
set hidden3d;set iso 30;set xrange [-2:2]; set yrange [-2:2]; set zrange [-2:2];
splot (sgn (x)*sin (abs ((x*y)))) with l,\
(-2.29349 < x && x < 0.502907) &&(-0.5 < y && y < 0.5)?0.251465 + 0 * x  + 0 * y : -1000 with l title 'linearization'
PLOTCMD

gnuplot -p << PLOTCMD
set hidden3d;set iso 30;set xrange [-2:2]; set yrange [-2:2]; set zrange [-2:2];
splot  [-3.69168:1.9011]  [-1:1] (sgn (x)*sin (abs ((x*y)))) with l,\
(-2.29349 < x && x < 0.502907) &&(-0.5 < y && y < 0.5)?0.251465 + 0 * x  + 0 * y : -1000  with l title 'linearization'
PLOTCMD