NLFIntp
Home
Examples
Executable
Documentation
Contact
About
# Concave quadratic polynomial inequalities (CQI) + equalities over uninterpreted function symbols (EUF) phi: - y1^2 - x1^2 - 1 + x1 - 2 * y1 + 2 * x1 * y1 + x2 >= 0 y2 - alpha(y1) - 1 = 0 - x1^2 - x2^2 - y2^2 + 1 > 0 psi: - z1^2 - x2^2 - 1 + x2 - 2 * z1 + 2 * x2 * z1 + x1 >= 0 z2 - alpha(z1) + 1 = 0 - x1^2 - x2^2 - z2^2 + 1 > 0
input1
phi: -y1^2-x1^2-1+x1-2*y1+2*x1*y1+x2>=0 y2-alpha(y1)-1=0 -x1^2-x2^2-y2^2+1>0 psi: -z1^2-x2^2-1+x2-2*z1+2*x2*z1+x1>=0 z2-alpha(z1)+1=0 -x1^2-x2^2-z2^2+1>0 common symbols: [x1 x2 alpha] Interpolant: x1 - x2 < 0 \/ x1 - x2 = 0 /\ 20*alpha(x2 - 1) + 19499*x1 - 19499*x2 < 0 Time: 0.031000 seconds.
result1
# CQI phi: - y1 + x1 - 2 >= 0 2 * x2 - x1 - 1 > 0 - y1^2 - x1^2 + 2 * x1 * y1 - 2 * y1 + 2 * x1 >= 0 - y2^2 - y1^2 - x2^2 - 4 * y1 + 2 * x2 - 4 >= 0 psi: - z1 + 2 * x2 + 1 >= 0 2 * x1 - x2 - 1 > 0 - z1^2 - 4 * x2^2 + 4 * x2 * z1 + 3 * z1 - 6 * x2 - 2 >= 0 - z2^2 - x1^2 - x2^2 + 2 * x1 + z1 - 2 * x2 - 1 >= 0
input2
phi: -y1+x1-2>=0 2*x2-x1-1>0 -y1^2-x1^2+2*x1*y1-2*y1+2*x1>=0 -y2^2-y1^2-x2^2-4*y1+2*x2-4>=0 psi: -z1+2*x2+1>=0 2*x1-x2-1>0 -z1^2-4*x2^2+4*x2*z1+3*z1-6*x2-2>=0 -z2^2-x1^2-x2^2+2*x1+z1-2*x2-1>=0 common symbols: [x1 x2] Interpolant: x1 - x2 < 0 Time: 0.015000 seconds.
result2
# Linear arithmetic (LA) + EUF phi: f(x) >= 0 x - y >= 0 y - x >= 0 psi: - f(y) > 0
input3
phi: f(x)>=0 x-y>=0 y-x>=0 psi: -f(y)>0 common symbols: [y f] Interpolant: f(y) >= 0 Time: 0.000000 seconds.
result3
# CQI phi: - x1^2 + 4 * x1 + x2 - 4 >= 0 - x1 - x2 + 3 - y^2 > 0 psi: - 3 * x1^2 - x2^2 + 1 >= 0 x2 - z^2 >= 0
input4
phi: -x1^2+4*x1+x2-4>=0 -x1-x2+3-y^2>0 psi: -3*x1^2-x2^2+1>=0 x2-z^2>=0 common symbols: [x1 x2] Interpolant: 430804*x1^2 + 714286*x1 + 203125*x2^2 + 60594*x2 - 1158586 > 0 Time: 0.000000 seconds.
result4
# LA + nested EUF phi: g(a) - c - 5 = 0 f(g(a)) - c - 1 >= 0 psi: h(b) - d - 4 = 0 d - c - 1 = 0 - f(h(b)) + c + 1 > 0
input5
phi: g(a)-c-5=0 f(g(a))-c-1>=0 psi: h(b)-d-4=0 d-c-1=0 -f(h(b))+c+1>0 common symbols: [c f] Interpolant: f(c + 5) - c - 1 >= 0 Time: 0.031000 seconds.
result5
# CQI + EUF phi: a - x >= 0 y - a >= 0 - f(a)^2 + 2 * f(a) - z^2 >= 0 psi: b - y >= 0 x - b >= 0 - f(b)^2 - 2 * f(b) - z^2 - 2 * z - 1 >= 0
input6
phi: a-x>=0 y-a>=0 -f(a)^2+2*f(a)-z^2>=0 psi: b-y>=0 x-b>=0 -f(b)^2-2*f(b)-z^2-2*z-1>=0 common symbols: [x y z f] Interpolant: 400000*f(y) - 74627*x + 74627*y + 200000*z + 50000 > 0 Time: 0.015000 seconds.
result6
# General nonlinear arithmetic (NLA) beyond CQI phi: x^2 + y^2 + z^2 - 2 >= 0 1.2 * x^2 + y^2 + x*z = 0 psi: 20 - 3 * x^2 - 4 * y^3 - 10 * z^2 >= 0 x^2 + y^2 - z - 1 = 0
input7
# Fill this template file please. A = [x y z] f1 = x^2+y^2+z^2-2 f2 = 1.2*x^2+y^2+x*z h1 = 20-3*x^2-4*y^3-10*z^2 h2 = x^2+y^2-z-1 # Monomial templates (you can add more in the same form). M0 = monomial(A, [0]) M1 = monomial(A, [0 1]) M2 = monomial(A, [0 1 2]) M3 = monomial(A, [0 1 2 3]) M4 = monomial(A, [0 1 2 3 4]) # Set polynomial templates by replacing '?' with M0, M1 or M2 etc. s0 = sos(M4) s1 = sos(M2) s2 = poly(M2) t1 = sos(M2) t2 = poly(M4) interp(s0+f1*s1+f2*s2,h1*t1+h2*t2)
template7
Interpolant: -1024.9606 +611.3910*z -434.0546*z^2 -193.2607*z^3 +741.6569*z^4 -280.7146*y -69.6013*y*z -382.0356*y*z^2 +84.7298*y*z^3 +307.9591*y*z^4 -1196.1854*y^2 -411.3728*y^2*z -289.6189*y^2*z^2 -442.1176*y^2*z^3 +717.7450*y^2*z^4 +217.2563*y^3 +342.7021*y^3*z +575.0695*y^3*z^2 +121.4253*y^3*z^3 +181.2897*y^4 -942.6115*y^4*z +133.3381*y^4*z^2 -250.3602*x -1376.1646*x*z -982.1059*x*z^2 -31.2635*x*z^3 +280.9016*x*z^4 +28.0287*x*y -9.0497*x*y*z +308.7289*x*y*z^2 +260.8639*x*y*z^3 -0.8474*x*y*z^4 +173.0653*x*y^2 -175.8087*x*y^2*z +117.4491*x*y^2*z^2 -319.7504*x*y^2*z^3 +0.1250*x*y^3 -55.5300*x*y^3*z -93.3007*x*y^3*z^2 +32.1214*x*y^4 +294.5367*x*y^4*z -1457.6096*x^2 -512.2695*x^2*z +102.1421*x^2*z^2 -143.2230*x^2*z^3 +711.4509*x^2*z^4 +165.0656*x^2*y +428.4765*x^2*y*z +332.7175*x^2*y*z^2 -118.7956*x^2*y*z^3 -565.6429*x^2*y^2 -2086.6807*x^2*y^2*z +520.1720*x^2*y^2*z^2 -57.1560*x^2*y^3 -103.2550*x^2*y^3*z +467.1483*x^2*y^4 +279.5142*x^3 +243.7668*x^3*z +403.7487*x^3*z^2 -326.8257*x^3*z^3 +2.0870*x^3*y -180.0553*x^3*y*z -158.1158*x^3*y*z^2 +31.5303*x^3*y^2 +183.4025*x^3*y^2*z +115.8244*x^4 -704.6909*x^4*z +168.8983*x^4*z^2 -125.5648*x^4*y -130.1105*x^4*y*z +446.0649*x^4*y^2 > 0 Time: 0.281000 seconds.
result7