NIL: Learning Nonlinear Interpolants
Author
Mingshuai Chen
Title
NIL: Learning Nonlinear Interpolants
Description
A learning-based tool in Mathematica that is dedicated to synthesizing nontrivial (reverse) Craig interpolants for the quantifier-free theory of nonlinear arithmetic.
Category
Academic Articles & Supplements
Keywords
Nonlinear Craig interpolant, counterexample-guided learning, program verification, support vector machines (SVMs)
URL
http://www.notebookarchive.org/2021-08-5lcsyb7/
DOI
https://notebookarchive.org/2021-08-5lcsyb7
Date Added
2021-08-12
Date Last Modified
2021-08-12
File Size
3.52 megabytes
Supplements
Rights
CC BY-NC-SA 4.0
Download
Open in Wolfram Cloud
NIL: learning nonlinear interpolant
NIL: learning nonlinear interpolant
The tool NIL is dedicated to synthesizing nontrivial (reverse) Craig interpolants for the quantifier-free theory of nonlinear arithmetic. It takes as input a pair (φ, ψ) of mutually contradictory formulas over the reals, and generates an interpolant I for (φ, ψ) s.t. φ ⊨ I and I ∧ ψ ⊨ False. NIL views interpolants as classifiers and adopts the sampling-guessing-refining philosophy, namely in each iteration it is fed with a classifier over a finite set of sample points from φ and ψ, and generates a bunch of counter-examples as new sample points to refine further classifiers, until a candidate classifier can be verified to be a real interpolant. LIBSVM is integrated as an engine to perform the classifications.
Current version: v1.1
Validated on platform: Mathematica 10, 64bit-Ubuntu-Desktop-16.04/Windows-10
Latest modification: on Aug. 31, 2021, by Mingshuai Chen, RWTH Aachen
Corresponding e-mail: chenms@cs.rwth-aachen.de
List of contributors: Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, and Naijun Zhan
Comments and bug-reports are highly appreciated.
© 2021 NIL, Lehrstuhl für Informatik 2, RWTH Aachen University. All rights reserved.
Current version: v1.1
Validated on platform: Mathematica 10, 64bit-Ubuntu-Desktop-16.04/Windows-10
Latest modification: on Aug. 31, 2021, by Mingshuai Chen, RWTH Aachen
Corresponding e-mail: chenms@cs.rwth-aachen.de
List of contributors: Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, and Naijun Zhan
Comments and bug-reports are highly appreciated.
© 2021 NIL, Lehrstuhl für Informatik 2, RWTH Aachen University. All rights reserved.
Source code
Source code
In[]:=
Benchmark A: working perfectly even w/o rounding.
Benchmark A: working perfectly even w/o rounding.
Dummy
Dummy
consPhi0=x<-1;consPsi0=x≥1;degree0=1;initialRange0={-3,3};
main[consPhi0,consPsi0,degree0,initialRange0]
Checking inputs ...
Legal inputs.
Checking unsatisfiability ...
Unsat.
Generating initial samplepoints ...
Learning a candidate interpolant at step 1 ...
Synthesized candidate interpolant: 0.00127295-0.497151(1-1.00414x)+0.497151(1+1.00158x)<0
Verifying the candidate ...
Valid interpolant (simplified): 0.00127659+1.x<0
Improved valid interpolant (rounded under precision 1.): x<0
Elapsed time: 0.108178
Done.
Necklace
Necklace
consPhi1=y-x^2-10;consPsi1=y+x^2+10;degree1=1;initialRange1={-3,3};
main[consPhi1,consPsi1,degree1,initialRange1]
Checking inputs ...
Legal inputs.
Checking unsatisfiability ...
Unsat.
Generating initial samplepoints ...
Learning a candidate interpolant at step 1 ...
Synthesized candidate interpolant: 6.93889×+0.499968(1+0.00565291x-1.00003y)-0.499968(1+0.00565291x+1.00003y)<0
-18
10
Verifying the candidate ...
Valid interpolant (simplified): y>0
Improved valid interpolant (rounded under precision 1.): -y<0
Elapsed time: 0.212085
Rendering graphics ...
 |
|
Done.
Face
Face
consPhi2=(x+4)^2+y^2-1≤0||(x-4)^2+y^2-1≤0;consPsi2=x^2+y^2-64≤0&&(x+4)^2+y^2-9≥0&&(x-4)^2+y^2-9≥0;degree2=4;initialRange2={-8,8};
main[consPhi2,consPsi2,degree2,initialRange2]
Checking inputs ...
Legal inputs.
Checking unsatisfiability ...
Unsat.
Generating initial samplepoints ...
Learning a candidate interpolant at step 1 ...
Synthesized candidate interpolant: 1.25304+0.000205205+0.0000465005-0.000144477+0.0028645-0.00218592-0.0044507+0.00024569+0.00303519+0.000384008<0
4
(1+1.45875x-1.73077y)
4
(1-6.7585x-1.24955y)
4
(1+3.94449x-0.888344y)
4
(1-1.02474x-0.672376y)
4
(1-3.22834x-0.352833y)
4
(1+3.1343x+0.405752y)
4
(1+7.02933x+0.578535y)
4
(1+1.16898x+1.13553y)
4
(1-1.24395x+1.33052y)
Verifying the candidate ...
Valid interpolant (simplified): 223.586+1.+(0.203313-0.627199y)+0.609577y+5.93026+2.33448+1.52974+(-49.5719-1.31492y+4.96677)+x(-4.00815-3.00414y+3.25148+2.50913)<0
4
x
3
x
2
y
3
y
4
y
2
x
2
y
2
y
3
y
Improved valid interpolant (rounded under precision 0.001): 1++-y++++--++x--++<0
4
x
223
y
366
3
x
356
2
y
37
3
y
95
4
y
146
2
x
2
9
y
170
2
y
45
1
55
y
74
2
y
68
3
y
89
Elapsed time: 0.329295
Rendering graphics ...
 |
|
Done.
Twisted
Twisted
consPhi3=-2*x*y^2+x^2+3*x*z-y^2-y*z+z^2-1≥0&&x^2*z^2+y^2*z^2-x^2-y^2+1/6*(x^4+2*x^2*y^2+y^4)-1/120*(x^6+y^6)-4≤0;consPsi3=4*(x-y)^4+(x+y)^2+w^2-80≤0&&100*(x+y)^2-w^2*(x-y)^4-3000≥0;degree3=4;initialRange3={-10,10};
main[consPhi3,consPsi3,degree3,initialRange3]
Checking inputs ...
Legal inputs.
Checking unsatisfiability ...
Unsat.
Generating initial samplepoints ...
Learning a candidate interpolant at step 1 ...
Synthesized candidate interpolant: -1.1155-0.000121252-0.000298621+0.0017033+0.00113251-0.0000340746-0.00196064-0.00122533+0.000639618+0.000164498<0
4
(1-6.68365x-5.84104y)
4
(1-2.3186x-4.83191y)
4
(1-2.27591x-3.31191y)
4
(1-3.27206x-2.31721y)
4
(1-4.5224x-1.94946y)
4
(1-0.956471x-0.15072y)
4
(1+2.96612x+0.822385y)
4
(1+4.01709x+2.40146y)
4
(1+2.24566x+3.80465y)
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{x-6.29179,y-5.02263,z-0.547621,w4.1},{x-6.18707,y-4.77132,z-0.399048,w0.2},{x-6.40467,y-5.70101,z-0.535211,w0.1},{x-1.30665,y-3.29288,z-0.277076,w-2.1},{x-6.19437,y-6.0291,z-0.507104,w0.6},{x-6.3101,y-5.66667,z-0.0366972,w-4.7},{x-1.9875,y-1.57211,z0.807579,w-2.7},{x-6.09789,y-6.11802,z0.192661,w-3.9},{x-5.92312,y-6.15712,z0.0588235,w0.7},{x-6.18215,y-4.86575,z0.227883,w-0.3},{x-5.88788,y-6.16028,z0.0730744,w-1.2},{x-1.84464,y-2.14414,z-0.010989,w-3.5},{x-5.94343,y-6.1547,z-0.243159,w2.2},{x-2.63095,y-1.3664,z-0.557599,w3.1},{x-1.22434,y-3.0625,z0.333333,w0},{x-1.71488,y-2.70476,z0.0384615,w4.1},{x-3.14345,y-1.46486,z0.0583327,w3.4},{x-1.33693,y-3.35373,z0.0689655,w1.7},{x-1.21936,y-2.51626,z-0.694687,w3.9},{x-6.12344,y-4.70148,z0.122442,w2.6},{x-6.15689,y-5.89579,z0.0830645,w-3.3},{x-6.14304,y-6.09919,z-0.514546,w1.6},{x-5.94469,y-6.15454,z0.245695,w-0.8},{x-6.21344,y-4.92927,z-0.320788,w1.3},{x-6.00267,y-6.14481,z-0.343912,w4.8},{x-5.95036,y-6.13509,z-0.166367,w1.1},{x-6.3101,y-5.07522,z0.11236,w2.8},{x-5.95143,y-6.13776,z0.185664,w-4.4},{x-6.12814,y-6.03947,z0.148148,w4.2}}
Learning a candidate interpolant at step 2 ...
Synthesized candidate interpolant: -5.13781-0.000656208-0.000149865-0.000160716-0.000233023+0.0190264-0.0213158+0.00179226-0.0000933163+0.000850859+0.000939383<0
4
(1-4.21549x-6.28511y)
4
(1-5.88788x-6.16028y)
4
(1-2.3186x-4.83191y)
4
(1-6.12344x-4.70148y)
4
(1-2.27591x-3.31191y)
4
(1-1.71488x-2.70476y)
4
(1-3.27206x-2.31721y)
4
(1+5.2139x+1.02834y)
4
(1+4.01709x+2.40146y)
4
(1+2.24566x+3.80465y)
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{x-3.26819,y-5.46494,z-0.203046,w0.1},{x-3.56955,y-1.92124,z-2.4,w-1.41968},{x-3.71759,y-5.78344,z0.0306122,w-3.7},{x-3.74008,y-5.89936,z-0.169231,w2.6},{x-3.70002,y-1.90667,z-4.4,w2.68175},{x-3.65077,y-5.85155,z-0.776803,w4.3},{x-3.64902,y-1.83427,z-3.3,w-0.323077},{x-3.31944,y-5.63383,z0.677997,w0.5},{x-3.39405,y-5.69055,z0.71403,w3.7},{x-1.95303,y-3.74444,z4.8,w2.5187},{x-3.64074,y-1.87559,z-4.,w-0.625},{x-3.73359,y-1.93651,z3.1,w-2.47611},{x-1.91806,y-3.74171,z-0.6,w1.9302},{x-1.79862,y-3.67877,z1.4,w-0.0359712},{x-3.60806,y-5.73737,z-0.549593,w1.9},{x-3.65579,y-5.87104,z-0.412698,w-3.2},{x-1.91806,y-3.74171,z-0.7,w-1.9302},{x-3.67887,y-1.90337,z1.4,w-3.01464},{x-3.67506,y-5.88323,z-0.209677,w3.1},{x-3.82984,y-1.9869,z-2.5,w0.151181},{x-3.73868,y-5.70621,z0.,w1.3},{x-3.53803,y-5.7933,z0.773608,w-0.1},{x-1.95774,y-3.6146,z-2.9,w-0.357143},{x-3.65833,y-5.80745,z0.328947,w-4.9},{x-3.69554,y-5.88842,z0.809066,w-1.9},{x-3.67882,y-1.80007,z4.2,w-0.383253},{x-3.67901,y-5.88571,z-0.820527,w-3.8},{x-3.59342,y-1.92541,z4.8,w2.43096},{x-3.65104,y-1.95011,z5.,w-3.89175}}
Learning a candidate interpolant at step 3 ...
Synthesized candidate interpolant: -10.6484-0.0228038-0.000343804+0.108022-0.0330395-0.0705039-0.0103795+0.025389+0.00104046+0.00261877<0
4
(1-2.3186x-4.83191y)
4
(1-6.12344x-4.70148y)
4
(1-1.79862x-3.67877y)
4
(1-1.33693x-3.35373y)
4
(1-1.71488x-2.70476y)
4
(1-4.5224x-1.94946y)
4
(1-3.67882x-1.80007y)
4
(1+4.01709x+2.40146y)
4
(1+2.24566x+3.80465y)
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{x3.45937,y2.03982,z0,w2.43663},{x1.9493,y3.77231,z3.8,w-1.7562},{x3.66563,y1.82248,z5.,w1.01684},{x3.67899,y1.81433,z1.9,w-1.20852},{x2.03011,y3.80282,z-0.4,w2.54476},{x3.67899,y1.80995,z2.9,w0.2},{x2.0316,y3.73011,z4.8,w3.67569},{x-5.60661,y-3.55198,z-0.0122783,w2.5},{x3.5482,y2.05746,z2.6,w5.36859},{x3.67891,y1.80008,z-3.3,w0.255474},{x3.66672,y1.89828,z-3.8,w-0.470588},{x2.0316,y3.57797,z-4.2,w-2.6},{x1.91745,y3.77476,z-1.1,w0},{x3.67897,y1.80985,z-3.2,w1.0207},{x1.93651,y3.6515,z1.8,w-0.857143},{x3.67889,y1.81622,z3.8,w1.27687},{x3.5134,y2.03896,z-2.5,w4.18755},{x1.87645,y3.60077,z-4.8,w0},{x3.67901,y1.81388,z0.7,w-1.19178},{x1.98826,y3.60819,z1.,w4.37862},{x1.96646,y3.61491,z2.6,w3.76923},{x3.67885,y1.81306,z1.9,w1.15259},{x3.6788,y1.82453,z2.7,w-1.55719},{x3.54232,y2.06519,z3.,w-5.43261},{x3.46666,y2.04363,z1.1,w-0.588235},{x3.60588,y1.87135,z-0.9,w0},{x1.90319,y3.62849,z1.3,w1.95},{x2.23692,y3.99744,z-4.2,w-0.645161},{x2.04347,y3.87465,z4.6,w0},{x1.86774,y3.67417,z-0.9,w-0.75}}
Learning a candidate interpolant at step 4 ...
Synthesized candidate interpolant: -11.0062-0.0257613+0.12249-0.000631156-0.0379806-0.0810112-0.011738+0.0290792+0.00204697+0.00350605<0
4
(1-2.3186x-4.83191y)
4
(1-1.79862x-3.67877y)
4
(1-5.60661x-3.55198y)
4
(1-1.33693x-3.35373y)
4
(1-1.71488x-2.70476y)
4
(1-4.5224x-1.94946y)
4
(1-3.67882x-1.80007y)
4
(1+3.67891x+1.80008y)
4
(1+1.86774x+3.67417y)
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{x-4.84696,y-2.40422,z-0.0123609,w-2.6},{x-5.05976,y-2.67867,z-0.139188,w0.3},{x-5.08538,y-2.7272,z0.0363036,w0.2},{x-4.86482,y-2.42774,z-0.0564346,w-1.1},{x-4.86482,y-2.42498,z-0.0825431,w-0.8},{x-4.84079,y-2.39713,z0.0535539,w-3.},{x-5.02245,y-2.62629,z-0.140908,w-3.2},{x-5.02957,y-2.63174,z0.161366,w2.4},{x-4.86087,y-2.42036,z0,w2.5},{x-4.85328,y-2.41217,z0.0641032,w-1.5},{x-4.84696,y-2.40702,z0.00564617,w4.4},{x-4.85328,y-2.41217,z0,w-4.4},{x-5.08538,y-2.70869,z0.167821,w-3.5},{x-5.23099,y-2.92943,z0.129998,w4.2},{x-5.23099,y-2.93172,z0.116139,w0.3},{x-5.08822,y-2.71412,z-0.161861,w-1.5},{x-5.20664,y-2.90011,z-0.0486656,w0.2},{x-5.23099,y-2.92943,z-0.0179949,w1.9},{x-5.1551,y-2.82775,z-0.00595238,w2.5},{x-5.03573,y-2.64005,z0.162507,w-3.},{x-5.08822,y-2.71272,z-0.167909,w-0.9},{x-5.23858,y-2.95183,z0.00318037,w1.1},{x-5.02245,y-2.6222,z-0.00949367,w-0.3},{x-5.29344,y-3.03582,z-1.89814×,w3.8},{x-4.95652,y-2.53998,z0.121548,w-1.9},{x-5.04585,y-2.66831,z0.0239617,w1.4},{x-5.1551,y-2.8105,z0.162183,w2.8},{x-4.85328,y-2.41153,z-0.0361613,w1.}}
-8
10
Learning a candidate interpolant at step 5 ...
Synthesized candidate interpolant: -10.8833-0.0260766+0.124504-0.0387075-0.0831946-0.00406131-0.00854882+0.0305137+0.00219452+0.00337696<0
4
(1-2.3186x-4.83191y)
4
(1-1.79862x-3.67877y)
4
(1-1.33693x-3.35373y)
4
(1-1.71488x-2.70476y)
4
(1-4.84079x-2.39713y)
4
(1-4.5224x-1.94946y)
4
(1-3.67882x-1.80007y)
4
(1+3.67891x+1.80008y)
4
(1+1.86774x+3.67417y)
Verifying the candidate ...
Valid interpolant (simplified): (-1.41063+0.9416y)+0.628457y+11.3225+(11.7913+2.08635y-0.710897)+x(-0.508114+15.8485y+2.52512+0.618257)<160.596+1.+1.70646+0.87528
3
x
2
y
2
x
2
y
2
y
3
y
4
x
3
y
4
y
Improved valid interpolant (rounded under precision 0.001): -1-+-+++--++-+x-+++<0
4
x
160
3
x
1
113
y
170
y
255
2
y
14
3
y
94
4
y
183
2
x
2
27
y
76
2
y
225
1
316
5y
51
2
y
63
3
y
259
Elapsed time: 140.624
Rendering graphics ...
 |
|
Done.
Ultimate
Ultimate
consPhi4=(x^2+y^2-3.8025≤0&&y≥0||(x-1)^2+y^2-0.9025≤0)&&(x-1)^2+y^2-0.09>0&&(x+1)^2+y^2-1.1025≥0||(x+1)^2+y^2-1/25≤0;consPsi4=(-3.8025++≤0&&-y≥0||-0.9025++≤0)&&-0.09++>0&&-1.1025++≥0||-1/25++≤0;degree4=7;initialRange4={-3,3};
2
x
2
y
2
(-1-x)
2
y
2
(-1-x)
2
y
2
(1-x)
2
y
2
(1-x)
2
y
main[consPhi4,consPsi4,degree4,initialRange4]
Checking inputs ...
Legal inputs.
Checking unsatisfiability ...
Unsat.
Generating initial samplepoints ...
Learning a candidate interpolant at step 1 ...
Synthesized candidate interpolant: 0.316745+0.199307-0.131172+0.0722783+9.29644+0.111143+0.0808693-10.4795-1.26547+2.87447-4.53059-2.59893+18.543-12.5259-0.122714+0.60758-0.237833+0.143773-0.0368275<0
7
(1+0.604563x-0.986663y)
7
(1+1.31867x-0.858457y)
7
(1+1.75008x-0.770764y)
7
(1-0.0162503x-0.344779y)
7
(1-0.857655x-0.340969y)
7
(1-1.1633x-0.337402y)
7
(1+0.111031x-0.332308y)
7
(1+1.23426x-0.238492y)
7
(1+1.00569x-0.137088y)
7
(1+0.109347x+0.0644046y)
7
(1-0.815682x+0.0646479y)
7
(1-0.0587404x+0.0998781y)
7
(1+0.108693x+0.110587y)
7
(1+1.18867x+0.239869y)
7
(1-1.14429x+0.264585y)
7
(1-0.498312x+0.934735y)
7
(1-0.984483x+0.94402y)
7
(1-1.5666x+0.980881y)
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{x0.832196,y0.10882},{x-0.136048,y0.651202},{x1.73512,y-0.749737},{x-1.60156,y0.952055},{x1.4974,y-0.809377},{x-1.54738,y0.969315},{x-0.264314,y0.773153},{x0.843233,y-0.124194},{x0.832339,y0.105251},{x0.816163,y0.0787643},{x1.77721,y-0.72426},{x1.10963,y0.279999},{x1.73323,y-0.751578},{x0.946194,y0.29808},{x-1.74352,y0.873285},{x1.84355,y-0.633121},{x-1.77661,y0.803842},{x-1.69808,y0.832759},{x0.366646,y-0.847045},{x0.832291,y0.10271},{x0.832471,y-0.109243},{x1.50882,y-0.791356},{x1.29798,y-0.89482},{x0.843995,y-0.0183903},{x0.965356,y0.306394},{x0.843995,y-0.0305254},{x1.51012,y-0.795956},{x0.195182,y-0.683573},{x1.28489,y-0.902548},{x-1.5396,y0.975495}}
Learning a candidate interpolant at step 2 ...
Synthesized candidate interpolant: 0.249625+0.0282828-0.0311583+0.700818+0.066274+10.6493+0.26461+0.0585193-12.7138-1.09456-0.307608+5.12547-0.227904-24.1224-3.60694+25.5571+0.959201-0.407203-0.902266-0.0302372+0.000392207+0.034095<0
7
(1+0.947723x-1.0537y)
7
(1+1.4974x-0.809377y)
7
(1+0.195182x-0.683573y)
7
(1+1.84355x-0.633121y)
7
(1-0.0162503x-0.344779y)
7
(1-0.857655x-0.340969y)
7
(1-1.1633x-0.337402y)
7
(1+0.111031x-0.332308y)
7
(1+1.17501x-0.29934y)
7
(1+1.23426x-0.238492y)
7
(1+0.832471x-0.109243y)
7
(1+0.649x+0.0207495y)
7
(1+0.109347x+0.0644046y)
7
(1-0.815682x+0.0646479y)
7
(1-0.0587404x+0.0998781y)
7
(1-1.14429x+0.264585y)
7
(1+0.946194x+0.29808y)
7
(1-0.136048x+0.651202y)
7
(1-1.77661x+0.803842y)
7
(1-1.34151x+0.878829y)
7
(1-0.984483x+0.94402y)
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{x-1.23862,y0.918155},{x-1.25861,y0.912812},{x1.08161,y-0.289282},{x-1.21774,y0.924711},{x-1.65977,y0.822061},{x-1.82204,y0.653267},{x1.09728,y-0.285084},{x-1.22142,y0.923836},{x-1.26202,y0.912441},{x-1.83665,y0.655146},{x-1.24249,y0.918531},{x-1.69621,y0.79531},{x-1.2386,y0.919548},{x1.84645,y-0.624009},{x-1.18082,y0.932633},{x-1.84612,y0.622105},{x1.84943,y-0.617226},{x1.84692,y-0.620666},{x-1.21801,y-0.210402},{x-1.73105,y0.808832},{x-1.23257,y-0.190642},{x1.11484,y-0.281721},{x-0.814891,y-0.257182},{x1.84289,y-0.626134},{x1.09622,y-0.284849},{x-1.81749,y0.658946},{x-1.24427,y0.917354},{x-1.2016,y0.927992},{x1.07866,y-0.289678},{x1.8491,y-0.617675}}
Learning a candidate interpolant at step 3 ...
Synthesized candidate interpolant: 0.251275+0.0315703+0.667552+0.0500918+8.24849-10.1086-1.63337-0.556775+1.06674+0.00886743+6.27748-29.0549-5.31727+30.3661-0.0289902+1.46449-0.535029-0.0462341-0.900238<0
7
(1+0.947723x-1.0537y)
7
(1+0.195182x-0.683573y)
7
(1+1.84943x-0.617226y)
7
(1-0.0162503x-0.344779y)
7
(1+0.111031x-0.332308y)
7
(1+1.09622x-0.284849y)
7
(1+1.11484x-0.281721y)
7
(1-0.814891x-0.257182y)
7
(1-1.23257x-0.190642y)
7
(1+0.832471x-0.109243y)
7
(1+0.109347x+0.0644046y)
7
(1-0.815682x+0.0646479y)
7
(1-0.0587404x+0.0998781y)
7
(1+1.18867x+0.239869y)
7
(1-1.14429x+0.264585y)
7
(1+0.946194x+0.29808y)
7
(1-1.84612x+0.622105y)
7
(1-0.136048x+0.651202y)
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{x-1.19746,y1.04116},{x1.3004,y-0.0752688},{x1.31365,y-1.01663},{x1.32145,y-0.999585},{x1.41775,y-0.963319},{x1.31477,y-0.0234261},{x1.21073,y-0.21804},{x1.2394,y-1.02234},{x1.28717,y0.0943035},{x1.25435,y-1.02897},{x1.50526,y-0.920441},{x1.0967,y-1.04785},{x1.23907,y-0.198025},{x1.26375,y-0.16906},{x1.15721,y-1.04714},{x1.3114,y-1.00276},{x1.30087,y-0.130809},{x1.08808,y-1.0463},{x1.45391,y-0.94682},{x1.26482,y0.144365},{x1.16762,y-1.04163},{x1.31778,y-1.00076},{x-1.28275,y1.05174},{x1.21813,y-1.03445},{x1.26998,y-1.0147},{x-0.873239,y1.04232},{x1.28337,y-0.110594},{x1.20842,y-1.02911},{x1.3114,y-1.02133},{x1.27683,y-1.01285}}
Learning a candidate interpolant at step 4 ...
Synthesized candidate interpolant: 0.243245+0.0158358+0.77764+0.0539098+8.68704-10.8998-1.98199+1.02742-0.286845+0.0106033+6.8356-0.787294-27.7741-5.21368+29.5327+1.43785-0.49588-0.0451168-0.892935-0.00103648<0
7
(1+1.08808x-1.0463y)
7
(1+0.195182x-0.683573y)
7
(1+1.84943x-0.617226y)
7
(1-0.0162503x-0.344779y)
7
(1+0.111031x-0.332308y)
7
(1+1.09622x-0.284849y)
7
(1-0.814891x-0.257182y)
7
(1+1.21073x-0.21804y)
7
(1-1.23257x-0.190642y)
7
(1+0.832471x-0.109243y)
7
(1+0.649x+0.0207495y)
7
(1+0.109347x+0.0644046y)
7
(1-0.815682x+0.0646479y)
7
(1-0.0587404x+0.0998781y)
7
(1-1.14429x+0.264585y)
7
(1+0.946194x+0.29808y)
7
(1-1.84612x+0.622105y)
7
(1-0.136048x+0.651202y)
7
(1-1.19746x+1.04116y)
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{x-0.0716748,y0.490624},{x-0.0374757,y0.422723},{x-0.0527184,y0.454681},{x-0.085,y0.515076},{x-0.056966,y0.461722},{x-0.0401699,y0.426946},{x-0.0305097,y0.406102},{x-0.0583252,y0.46532},{x-0.085,y0.515089},{x-0.0284951,y0.398938},{x-0.0420631,y0.42995},{x-0.0125114,y0.356884},{x-0.0527184,y0.455778},{x-0.0374757,y0.422574},{x-0.0367961,y0.418017},{x-0.056966,y0.464319},{x-0.0534466,y0.454463},{x-0.0170388,y0.369417},{x-0.0716748,y0.492054},{x-0.0534466,y0.457225},{x-0.0717961,y0.490854},{x-0.0527184,y0.452943},{x-0.0278641,y0.396802},{x-0.0576214,y0.464791},{x-0.033665,y0.411543},{x-0.0420631,y0.433108},{x-0.0716748,y0.490716},{x-0.0144903,y0.36267},{x-0.0420631,y0.433048},{x-0.0550728,y0.457835}}
Learning a candidate interpolant at step 5 ...
Synthesized candidate interpolant: 0.392557+1.34982+0.0515275+7.88808-12.9634-1.50618+1.18149-0.437811+5.75106-25.1144-5.6483+33.9908+1.54523-0.407134-5.88705-0.0472592+0.287378+0.00159908-0.0354633<0
7
(1+0.195182x-0.683573y)
7
(1+1.84943x-0.617226y)
7
(1-0.0162503x-0.344779y)
7
(1+0.111031x-0.332308y)
7
(1+1.09622x-0.284849y)
7
(1-0.814891x-0.257182y)
7
(1+1.21073x-0.21804y)
7
(1+0.832471x-0.109243y)
7
(1+0.109347x+0.0644046y)
7
(1-0.815682x+0.0646479y)
7
(1-0.0587404x+0.0998781y)
7
(1-1.14429x+0.264585y)
7
(1+0.946194x+0.29808y)
7
(1-0.0144903x+0.36267y)
7
(1-1.84612x+0.622105y)
7
(1-0.336689x+0.674633y)
7
(1-1.34151x+0.878829y)
7
(1-0.873239x+1.04232y)
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{x-1.84995,y0.616512},{x-1.84982,y0.616766},{x-1.84999,y0.616459},{x-1.84984,y0.616764},{x-1.43445,y0.840818},{x-1.84996,y0.616515},{x-1.84993,y0.616531},{x-1.84976,y0.616776},{x-1.84974,y0.61681},{x-1.84978,y0.616757},{x-1.84987,y0.616615},{x-1.84978,y0.616744},{x-1.84993,y0.616574},{x-1.44117,y0.84135},{x-1.41072,y0.856625},{x-1.84993,y0.616663},{x-1.84989,y0.616741},{x-1.84979,y0.61673},{x-1.51152,y0.796472},{x-1.84996,y0.616563},{x-1.8499,y0.616573},{x-1.47936,y0.820191},{x-1.56432,y0.764229},{x-1.84984,y0.616764},{x-1.84996,y0.616493},{x-1.84991,y0.616699},{x-1.84993,y0.616543},{x-1.85,y0.616442},{x-1.84973,y0.616812},{x-1.51063,y0.795187}}
Learning a candidate interpolant at step 6 ...
Synthesized candidate interpolant: 0.392666+1.35395+0.0514032+7.86972-12.9747-1.5015+1.19522-0.438209+5.73991-25.0503-5.67846+34.0147+1.55332-0.40545-5.96189-0.04789+0.317756+0.00311867-0.0407356<0
7
(1+0.195182x-0.683573y)
7
(1+1.84943x-0.617226y)
7
(1-0.0162503x-0.344779y)
7
(1+0.111031x-0.332308y)
7
(1+1.09622x-0.284849y)
7
(1-0.814891x-0.257182y)
7
(1+1.21073x-0.21804y)
7
(1+0.832471x-0.109243y)
7
(1+0.109347x+0.0644046y)
7
(1-0.815682x+0.0646479y)
7
(1-0.0587404x+0.0998781y)
7
(1-1.14429x+0.264585y)
7
(1+0.946194x+0.29808y)
7
(1-0.0144903x+0.36267y)
7
(1-1.85x+0.616442y)
7
(1-0.336689x+0.674633y)
7
(1-1.47936x+0.820191y)
7
(1-0.873239x+1.04232y)
Verifying the candidate ...
Valid interpolant (simplified): 0.327385+1.+(-0.289473-5.67609y)+4.89085+0.577725+(-14.1691-0.857304y+6.04098)+(0.901236+9.10259y-0.269838-5.93363)+(26.4312+1.5065y-21.4473+2.62665+2.5298)+(-0.84717-0.159728y+2.75826-9.4701-1.50527-1.11237)+x(-10.2067-0.616265y-27.9551-1.1172+4.95755-0.168956+0.39194)<0.469264y+4.4762+13.9573+4.12701+0.112326
7
x
6
x
4
y
6
y
5
x
2
y
4
x
2
y
3
y
3
x
2
y
3
y
4
y
2
x
2
y
3
y
4
y
5
y
2
y
3
y
4
y
5
y
6
y
2
y
3
y
5
y
7
y
Improved valid interpolant (rounded under precision 0.01): ++-----+-++--+++-++-+++-+---+x----++<0
1
85
7
x
27
6
x
1
96
y
5
y
59
2
y
6
3
y
2
4
y
6
5
y
7
6
y
48
5
x
1
2
y
32
2
2
y
9
4
x
1
31
y
3
2
3
y
9
3
x
15
16
y
18
10
2
y
13
3
y
10
4
y
11
2
x
1
32
2
y
10
3
y
3
4
y
18
5
y
25
3
8
y
45
2
y
3
y
25
2
4
y
11
6
y
71
Elapsed time: 48.8211
Rendering graphics ...
 |
|
Done.
IJCAR’16-1
IJCAR’16-1
consPhi12=-x1^2+4*x1+x2-4≥0&&-x1-x2+3-y^2>0;consPsi12=-3*x1^2-x2^2+1≥0&&x2-z^2≥0;degree12=1;initialRange12={-2,2};
main[consPhi12,consPsi12,degree12,initialRange12]
Checking inputs ...
Legal inputs.
Checking unsatisfiability ...
Unsat.
Generating initial samplepoints ...
Learning a candidate interpolant at step 1 ...
Synthesized candidate interpolant: 2.92005+3.79198(1+0.439977x1+0.632913x2)-2.32003(1+1.21631x1+0.740265x2)-1.47194(1+0.837402x1+1.39782x2)<0
Verifying the candidate ...
Valid interpolant (simplified): 1.x1+0.576236x2>1.22378
Improved valid interpolant (rounded under precision 0.1): 1--<0
3x1
4
x2
2
Elapsed time: 0.1635
Rendering graphics ...
 |
|
Done.
CAV’13-1: From L. Dai et al. [CAV’13: Generating non-linear interpolants by semidefinite programming].
CAV’13-1: From L. Dai et al. [CAV’13: Generating non-linear interpolants by semidefinite programming].
consPhi17=1-a^2-b^2>0&&a^2+b-1-x0&&b+x*b+1-y0;consPsi17=x^2-2*y^2-4>0;degree17=2;initialRange17={-5,5};
main[consPhi17,consPsi17,degree17,initialRange17]
Checking inputs ...
Legal inputs.
Checking unsatisfiability ...
Unsat.
Generating initial samplepoints ...
Learning a candidate interpolant at step 1 ...
Synthesized candidate interpolant: -0.994921+0.0290539+0.157464-0.186518<0
2
(1+2.01404x+0.123875y)
2
(1-2.26711x+0.647745y)
2
(1-1.5122x+1.26234y)
Verifying the candidate ...
Valid interpolant (simplified): -0.994921-0.0328426x+0.500669-0.259708y+0.264113xy-0.230705<0
2
x
2
y
Improved valid interpolant (rounded under precision 0.1): -1+-+-<0
2
x
2
y
3
xy
3
2
y
4
Elapsed time: 3.25069
Rendering graphics ...
 |
|
Done.
CAV’13-2: From L. Dai et al. [CAV’13].
CAV’13-2: From L. Dai et al. [CAV’13].
consPhi5=x^2+y^2+z^2-2≥0&&1.2x^2+y^2+xz==0;consPsi5=20-3x^2-4y^3-10z^2≥0&&x^2+y^2-z-1==0;degree5=4;initialRange5={-3,3};
main[consPhi5,consPsi5,degree5,initialRange5]
Checking inputs ...
Legal inputs.
Checking unsatisfiability ...
Unsat.
Generating initial samplepoints ...
Learning a candidate interpolant at step 1 ...
Synthesized candidate interpolant: 0.964937-0.0115105-0.00214521+0.0223284+0.0135042-0.0235766+0.000927089+0.000472651<0
4
(1-1.67058x)
4
(1+1.68358x)
4
(1-0.0429159x-0.606061y-0.630849z)
4
(1-0.912404x+0.0243902y-0.166923z)
4
(1-0.784033x+0.37146y+1.11683z)
4
(1+1.19871x+0.845625y+1.15198z)
4
(1+0.226337x-1.71819y+2.00339z)
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{x0.200387,y-0.886792,z-4.16487},{x0.620155,y0.891892,z-2.02688},{x-0.415268,y-0.552632,z1.23375},{x-1.18627,y-0.345455,z0.526586},{x-0.000174785,y-0.0158622,z1.43974},{x0.351984,y-0.542267,z-1.2578},{x1.44531,y0.771429,z-2.14612},{x0.356872,y-1.1922,z-4.41103},{x-0.22018,y-0.505238,z1.42356},{x-0.350062,y1.35313,z0.953491},{x0.3545,y1.00877,z-3.29598},{x0.337972,y-0.53841,z-1.26329},{x0.324135,y-0.534018,z-1.26876},{x-1.43738,y0.321105,z1.16916},{x-0.00151433,y0.0464806,z1.42848},{x0.346172,y0.540738,z-1.26007},{x0.726009,y-1.24242,z-2.99738},{x0.893338,y0.124206,z-1.08927},{x1.63113,y-0.365399,z-2.03921},{x-0.00100956,y0.0380178,z1.43288},{x0.339883,y1.12821,z-4.15282},{x-0.00346773,y0.0699304,z1.41438},{x-1.46936,y-0.0624165,z1.16292},{x0.787702,y-0.366596,z-1.11586},{x0.347669,y0.541141,z-1.25948},{x1.47155,y-0.99044,z-2.43249},{x0,y0,z1.41448},{x1.63137,y0.530924,z-2.13043},{x-0.24545,y-0.548028,z1.51815},{x-1.231,y-0.92061,z1.3629}}
Learning a candidate interpolant at step 2 ...
Synthesized candidate interpolant: 1.05283-0.00198816-0.0143455-0.0376399+0.0759819+0.0155189-0.0197394+0.00111982-0.0216329+0.00272533<0
4
(1+1.41448x)
4
(1+0.347669x+0.541141y-1.25948z)
4
(1+0.351984x-0.542267y-1.2578z)
4
(1-0.0429159x-0.606061y-0.630849z)
4
(1-1.18627x-0.345455y+0.526586z)
4
(1-0.784033x+0.37146y+1.11683z)
4
(1+1.19871x+0.845625y+1.15198z)
4
(1-0.22018x-0.505238y+1.42356z)
4
(1+0.226337x-1.71819y+2.00339z)
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{x-1.4251,y-0.398873,z1.19001},{x-0.115162,y1.38941,z0.943721},{x-0.121245,y1.38979,z0.946227},{x-0.956539,y1.08851,z1.09983},{x-1.41594,y-0.438006,z1.19672},{x-0.707024,y1.20871,z0.960859},{x-1.4117,y0.422391,z1.17132},{x-1.42877,y0.175182,z1.07207},{x-1.42877,y0.35876,z1.17009},{x-0.187631,y1.38733,z0.959883},{x-0.182412,y1.37084,z0.912469},{x-1.45612,y0.0948276,z1.12929},{x-0.133974,y1.38606,z0.939111},{x-1.1882,y0.859225,z1.15009},{x-0.871556,y1.06733,z0.898796},{x-1.03764,y0.962025,z1.00219},{x-0.956539,y1.05856,z1.03551},{x-1.21149,y-0.935806,z1.34343},{x-1.03764,y1.02079,z1.11871},{x-0.476135,y1.29491,z0.903487},{x-0.607295,y-1.57864,z1.86092},{x-1.45798,y0.200251,z1.1658},{x-0.720217,y-1.50825,z1.79354},{x-1.07567,y-1.16357,z1.51097},{x-1.41144,y-0.45603,z1.20012},{x-1.45186,y-0.253689,z1.17225},{x-0.108967,y1.39281,z0.951806},{x-0.14246,y1.39165,z0.95699},{x-0.493597,y-1.60467,z1.81859},{x-0.194916,y1.38652,z0.960422}}
Learning a candidate interpolant at step 3 ...
Synthesized candidate interpolant: 0.939928-0.011877-0.0426245+0.0976132+0.0167766+0.0373272-0.0932599-0.00504493+0.00108931<0
4
(1+0.347669x+0.541141y-1.25948z)
4
(1+0.351984x-0.542267y-1.2578z)
4
(1-0.0429159x-0.606061y-0.630849z)
4
(1-0.187631x+1.38733y+0.959883z)
4
(1-1.42877x+0.175182y+1.07207z)
4
(1-0.784033x+0.37146y+1.11683z)
4
(1-0.22018x-0.505238y+1.42356z)
4
(1+0.226337x-1.71819y+2.00339z)
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{x-1.25742,y0.689462,z1.05647},{x-0.859944,y1.09972,z0.948883},{x-1.00868,y0.983931,z0.985562},{x-0.697199,y1.24624,z1.03921},{x-1.15966,y0.822539,z1.02139},{x-0.808683,y1.14274,z0.95983},{x-1.33838,y0.615574,z1.17018},{x-1.16807,y0.884285,z1.14634},{x-1.33165,y0.629599,z1.16969},{x-1.00868,y1.04624,z1.11206},{x-0.847339,y1.16441,z1.07383},{x-0.643697,y1.24255,z0.958273},{x-1.25742,y0.761766,z1.1614},{x-0.572829,y1.29591,z1.00752},{x-0.658824,y1.26365,z1.03086},{x-0.859944,y1.15642,z1.07682},{x-0.697199,y1.20683,z0.942534},{x-1.21625,y0.819071,z1.15013},{x-0.643697,y1.27015,z1.02764},{x-1.13389,y0.882199,z1.06399},{x-1.33838,y0.604857,z1.1571},{x-0.730812,y1.1776,z0.920833},{x-0.814286,y1.18446,z1.06601},{x-0.935014,y1.03337,z0.942106},{x-1.13389,y0.924056,z1.13959},{x-0.969188,y1.06463,z1.07276},{x-0.969188,y1.07865,z1.10282},{x-0.740056,y1.18977,z0.963231},{x-0.838375,y1.16997,z1.0717},{x-0.808683,y1.18774,z1.0647}}
Learning a candidate interpolant at step 4 ...
Synthesized candidate interpolant: 0.794472-0.00869728-0.0496992+0.125332+0.00195602+0.0119537-0.131972+0.00113373+0.0386328+0.0108158+0.00054528<0
4
(1+0.347669x+0.541141y-1.25948z)
4
(1+0.351984x-0.542267y-1.2578z)
4
(1-0.0429159x-0.606061y-0.630849z)
4
(1-0.14246x+1.39165y+0.95699z)
4
(1-0.643697x+1.27015y+1.02764z)
4
(1-0.784033x+0.37146y+1.11683z)
4
(1+1.19871x+0.845625y+1.15198z)
4
(1-1.33165x+0.629599y+1.16969z)
4
(1-1.4251x-0.398873y+1.19001z)
4
(1+0.226337x-1.71819y+2.00339z)
Verifying the candidate ...
Valid interpolant (simplified): 6.63539+1.+0.496759+(-2.09483-0.760297y-2.36367z)+0.0608835+(0.284753+1.26084z)+(2.66558+1.98171z+1.16297)+y(-2.16486+0.596372z-1.30254-1.63679)+(0.452038+1.3399+3.17242z+0.99588+y(1.45747+1.10082z))+x(0.141155-0.647194+(-2.8253-1.34484z)+6.00189z-0.385724+2.42238+y(1.41104-1.82149z+1.60742))<2.61839z+6.05721+1.77051
4
x
4
y
3
x
3
z
3
y
2
y
2
z
2
z
3
z
2
x
2
y
2
z
3
y
2
y
2
z
3
z
2
z
2
z
4
z
Improved valid interpolant (rounded under precision 0.1): ++---+z--++y+++++++y---+x--+++y-+<0
4
3
3
4
4
x
8
3
x
1
3
z
3
z
3
3
y
6
2
2
z
3
4
z
4
2
x
2
y
6
1
5
z
7
z
3
2
z
8
2
y
1
3
z
4
2
z
7
1
3
2
z
6
3
z
5
2
y
1
3
z
6
2z
3
3
z
3
1
5
z
4
2
z
5
Elapsed time: 3857.89
Rendering graphics ...
 |
|
Done.
accelerating: CAV’13-3, from L. Dai et al. [CAV’13].
accelerating: CAV’13-3, from L. Dai et al. [CAV’13].
consPhi17=vc<49.61&&fa0.5418vc^2&&fr1000-fa&&ac0.0005fr&&vc1vc+ac;consPsi17=vc1≥49.61;degree17=1;initialRange17={0,1000};
main[consPhi17,consPsi17,degree17,initialRange17]
Checking inputs ...
Legal inputs.
Checking unsatisfiability ...
Unsat.
Generating initial samplepoints ...
Learning a candidate interpolant at step 1 ...
Synthesized candidate interpolant: -1.01994-0.000794849(1+0.5vc1)+0.000794849(1+50.6618vc1)<0
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{vc126.9762,ac0.307328,fa385.343,fr614.657,vc26.6689},{vc139.0556,ac0.0886603,fa822.679,fr177.321,vc38.9669},{vc149.2222,ac-0.160635,fa1321.27,fr-321.27,vc49.3829},{vc127.4921,ac0.29969,fa400.621,fr599.379,vc27.1924},{vc134.1587,ac0.187367,fa625.266,fr374.734,vc33.9714},{vc142.4048,ac0.0131802,fa973.64,fr26.3604,vc42.3916},{vc136.8254,ac0.135325,fa729.35,fr270.65,vc36.6901},{vc136.4683,ac0.142532,fa714.937,fr285.063,vc36.3257},{vc127.0556,ac0.306163,fa387.674,fr612.326,vc26.7494},{vc133.381,ac0.201778,fa596.445,fr403.555,vc33.1792},{vc125.581,ac0.327233,fa345.534,fr654.466,vc25.2538},{vc137.2302,ac0.127068,fa745.863,fr254.137,vc37.1031},{vc143.7619,ac-0.0192585,fa1038.52,fr-38.517,vc43.7812},{vc140.2381,ac0.0627516,fa874.497,fr125.503,vc40.1753},{vc129.754,ac0.264416,fa471.168,fr528.832,vc29.4896},{vc147.1587,ac-0.105157,fa1210.31,fr-210.313,vc47.2639},{vc129.1825,ac0.273602,fa452.797,fr547.203,vc28.9089},{vc145.6349,ac-0.0657895,fa1131.58,fr-131.579,vc45.7007},{vc134.6508,ac0.178071,fa643.858,fr356.142,vc34.4727},{vc146.8095,ac-0.0960151,fa1192.03,fr-192.03,vc46.9055},{vc145.6746,ac-0.0667975,fa1133.59,fr-133.595,vc45.7414},{vc135.3413,ac0.164793,fa670.415,fr329.585,vc35.1765},{vc146.9206,ac-0.0989161,fa1197.83,fr-197.832,vc47.0196},{vc135.4444,ac0.162785,fa674.43,fr325.57,vc35.2817},{vc134.3968,ac0.182886,fa634.228,fr365.772,vc34.2139},{vc147.7222,ac-0.120059,fa1240.12,fr-240.117,vc47.8423},{vc141.746,ac0.0285394,fa942.921,fr57.0788,vc41.7175},{vc131.0794,ac0.242396,fa515.208,fr484.792,vc30.837},{vc142.9365,ac0.000597917,fa998.804,fr1.19583,vc42.9359},{vc144.5079,ac-0.0375469,fa1075.09,fr-75.0938,vc44.5455}}
Learning a candidate interpolant at step 2 ...
Synthesized candidate interpolant: -27.925-0.162986(1+47.1587vc1)+0.162986(1+50.6618vc1)<0
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{vc148.9414,ac-0.152937,fa1305.87,fr-305.875,vc49.0943},{vc149.2117,ac-0.160346,fa1320.69,fr-320.692,vc49.3721},{vc149.4393,ac-0.166615,fa1333.23,fr-333.23,vc49.6059},{vc148.9529,ac-0.153253,fa1306.51,fr-306.506,vc49.1062},{vc149.1021,ac-0.157338,fa1314.68,fr-314.675,vc49.2595},{vc149.2867,ac-0.162408,fa1324.82,fr-324.816,vc49.4491},{vc149.1618,ac-0.158975,fa1317.95,fr-317.95,vc49.3208},{vc149.1538,ac-0.158756,fa1317.51,fr-317.511,vc49.3126},{vc148.9432,ac-0.152986,fa1305.97,fr-305.972,vc49.0961},{vc149.0847,ac-0.15686,fa1313.72,fr-313.721,vc49.2416},{vc148.9102,ac-0.152085,fa1304.17,fr-304.171,vc49.0623},{vc149.1709,ac-0.159224,fa1318.45,fr-318.448,vc49.3301},{vc149.3171,ac-0.163244,fa1326.49,fr-326.489,vc49.4803},{vc149.2382,ac-0.161074,fa1322.15,fr-322.148,vc49.3993},{vc149.0036,ac-0.154637,fa1309.27,fr-309.275,vc49.1582},{vc149.3931,ac-0.16534,fa1330.68,fr-330.68,vc49.5584},{vc148.9908,ac-0.154287,fa1308.57,fr-308.575,vc49.1451},{vc149.359,ac-0.1644,fa1328.8,fr-328.799,vc49.5234},{vc149.1131,ac-0.15764,fa1315.28,fr-315.279,vc49.2708},{vc149.3853,ac-0.165125,fa1330.25,fr-330.249,vc49.5504},{vc149.3599,ac-0.164424,fa1328.85,fr-328.848,vc49.5243},{vc149.1286,ac-0.158063,fa1316.13,fr-316.127,vc49.2867},{vc149.3877,ac-0.165193,fa1330.39,fr-330.386,vc49.5529},{vc149.1309,ac-0.158127,fa1316.25,fr-316.254,vc49.289},{vc149.1075,ac-0.157484,fa1314.97,fr-314.967,vc49.2649},{vc149.4057,ac-0.165688,fa1331.38,fr-331.376,vc49.5714},{vc149.2719,ac-0.162002,fa1324.,fr-324.004,vc49.4339},{vc149.0332,ac-0.155449,fa1310.9,fr-310.898,vc49.1887},{vc149.2986,ac-0.162736,fa1325.47,fr-325.471,vc49.4613},{vc149.3337,ac-0.163704,fa1327.41,fr-327.409,vc49.4975}}
Learning a candidate interpolant at step 3 ...
Synthesized candidate interpolant: -81.8759-1.33812(1+49.4393vc1)+1.33812(1+50.6618vc1)<0
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{vc149.7686,ac2.,fa1.3,fr3.6,vc-1.},{vc149.6373,ac0.1,fa0.8,fr-1.9,vc-1.4},{vc149.9809,ac-0.4,fa3.3,fr-2.5,vc-3.6},{vc150.0047,ac0.9,fa4.4,fr4.,vc-5.},{vc149.8114,ac4.9,fa-5.,fr-4.,vc-0.1},{vc149.9212,ac-1.6,fa2.8,fr2.4,vc4.4},{vc150.0091,ac1.6,fa-4.1,fr3.4,vc-2.},{vc149.7924,ac1.5,fa-1.1,fr4.2,vc2.2},{vc149.931,ac3.6,fa-4.5,fr1.1,vc3.1},{vc149.9817,ac-4.,fa-0.4,fr-2.8,vc3.3},{vc149.7543,ac-4.3,fa-4.4,fr3.1,vc-3.4},{vc149.9463,ac-3.4,fa-2.4,fr-4.7,vc-4.2},{vc149.7117,ac3.7,fa0.2,fr-4.5,vc4.6},{vc149.6453,ac0.4,fa-0.1,fr-1.4,vc1.3},{vc149.8592,ac0.7,fa-1.9,fr-3.8,vc1.9},{vc149.6872,ac-4.7,fa4.7,fr1.7,vc-0.4},{vc149.773,ac0.4,fa-3.2,fr-5.,vc2.8},{vc149.7777,ac0.1,fa-2.,fr-3.3,vc0.2},{vc149.6766,ac3.2,fa-2.7,fr-3.3,vc4.2},{vc149.8811,ac3.4,fa-0.8,fr-4.,vc4.4},{vc150.0473,ac-0.1,fa0.4,fr2.3,vc1.4},{vc149.6358,ac3.3,fa1.2,fr-2.3,vc2.9},{vc149.818,ac4.5,fa-0.8,fr-4.4,vc-0.3},{vc150.0195,ac-1.1,fa3.2,fr4.3,vc-3.5},{vc149.8445,ac-0.1,fa-3.6,fr2.2,vc-0.2},{vc149.7905,ac-1.9,fa0.7,fr3.1,vc1.},{vc149.9601,ac4.3,fa4.,fr-4.2,vc3.1},{vc149.61,ac-4.4,fa-3.4,fr2.,vc1.9},{vc149.909,ac1.1,fa3.5,fr-4.9,vc1.9},{vc149.8255,ac2.6,fa4.3,fr4.7,vc-4.8}}
Learning a candidate interpolant at step 4 ...
Synthesized candidate interpolant: -582.126-68.8403(1+49.4393vc1)+68.8403(1+49.61vc1)<0
Verifying the candidate ...
Valid interpolant (simplified): 1.vc1<49.5249
Improved valid interpolant (rounded under precision 0.0001): -1+<0
2vc1
99
Elapsed time: 40.6298
Done.
Benchmark B: parallel/sharp/adjacent cases where numerical issues make trouble, however being well-addressed by the rounding (rational recovery) effect.
Benchmark B: parallel/sharp/adjacent cases where numerical issues make trouble, however being well-addressed by the rounding (rational recovery) effect.
Parallel_parabola
Parallel_parabola
consPhi6=y-x^2-1≥0;consPsi6=y-x^2<0;degree6=2;initialRange6={-5,5};
main[consPhi6,consPsi6,degree6,initialRange6]
Checking inputs ...
Legal inputs.
Checking unsatisfiability ...
Unsat.
Generating initial samplepoints ...
Learning a candidate interpolant at step 1 ...
Synthesized candidate interpolant: 0.907911+1.8922-2.33295+0.698649-0.443016+0.185107<0
2
(1+0.722374x+0.512151y)
2
(1+0.53848x+1.31544y)
2
(1-1.57577x+2.46792y)
2
(1-1.43783x+3.08982y)
2
(1+2.09897x+4.34937y)
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:x-,y,x-,y-,x-,y-,x-,y-,x,y-,x,y2620,x,y-,x,y-3676,x-,y-,x-,y-,x-,y-,x-,y-,x-,y,x-193,y,x-,y-,x-130,y-,x-,y2482,x,y,x,y,x-,y-,x,y,x-,y,x,y,x,y-,x-,y-,x-,y-,x46,y-,x,y,x-,y-,x,y
373
10
10687
10
1713
10
15797
5
1018
5
16659
5
393
10
2884
5
119
10
14359
10
385
2
541
5
16538
5
242
5
739
5
16553
5
897
10
19367
10
898
5
11029
5
17
5
6137
10
847
5
30899
10
13824
5
1326
5
18703
5
28629
10
849
5
1631
10
5993
2
957
10
5904
5
7
2
14716
5
249
10
3061
5
873
5
12297
5
391
5
9133
5
1029
5
34027
10
273
10
7347
10
331
10
4593
10
3317
2
739
5
18691
10
1633
10
11393
5
1443
10
34853
10
Learning a candidate interpolant at step 2 ...
Synthesized candidate interpolant: 0.983029+1.60978-2.11287+0.919548-0.674351+0.257888+4.23387×<0
2
(1+0.722374x+0.512151y)
2
(1+0.53848x+1.31544y)
2
(1-1.57577x+2.46792y)
2
(1-1.43783x+3.08982y)
2
(1+1.76827x+3.10385y)
-6
10
2
(1+24.9x+612.2y)
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{x15.0198,y27316.1},{x-39.0889,y1593.},{x2901.,y8.4158×},{x82.0727,y6736.93},{x-55.0889,y3061.},{x638.,y407096.},{x3007.,y9.04205×},{x2675.,y7.15566×},{x-1556.,y2.42114×},{x26.0792,y27251.1},{x37.4563,y27214.},{x812.,y659369.},{x-74.4357,y5541.68},{x37.1695,y26927.4},{x-1264.,y1.59776×},{x-208.,y43265.},{x66.5273,y4426.88},{x9.54455,y90.5588},{x-47.8,y2718.05},{x37.4104,y26917.2},{x-74.0222,y13573.5},{x-7.61177,y29239.},{x-7.61177,y29028.},{x3.15049,y27115.9},{x37.4104,y26998.},{x-62.4,y3894.76},{x-2928.,y8.57323×},{x-2928.,y8.57319×},{x14.,y27309.8},{x-36.1333,y24313.9}}
6
10
6
10
6
10
6
10
6
10
6
10
6
10
Learning a candidate interpolant at step 3 ...
Synthesized candidate interpolant (rounded under precision 0.1): +-y<0
1
2
2
x
Verifying the candidate ...
Valid interpolant (simplified): +<y
1
2
2
x
Elapsed time: 4.49543
Rendering graphics ...
 |
|
Done.
Parallel_halfplane
Parallel_halfplane
consPhi7=y-x-1≥0;consPsi7=y-x+1<0;degree7=1;initialRange7={-5,5};
main[consPhi7,consPsi7,degree7,initialRange7]
Checking inputs ...
Legal inputs.
Checking unsatisfiability ...
Unsat.
Generating initial samplepoints ...
Learning a candidate interpolant at step 1 ...
Synthesized candidate interpolant: -0.0029862+0.695357(1-0.144424x-1.15372y)-0.986762(1+0.115534x+1.11884y)+0.291405(1+4.14368x+3.13179y)<0
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{x-4121.,y-4118.51},{x4009.,y4007.86},{x3123.,y3121.37},{x-3188.,y-3186.08},{x1940.,y1939.},{x-2851.,y-2850.},{x3469.,y3467.17},{x-4000.,y-3999.},{x2598.,y2596.85},{x-3260.,y-3258.44},{x-1853.,y-1851.88},{x-1887.,y-1886.},{x-2851.,y-2849.52},{x-4482.,y-4481.},{x-3518.,y-3516.04},{x3156.,y3154.37},{x-1858.,y-1857.},{x-3600.,y-3597.83},{x-4482.,y-4480.62},{x-4482.,y-4479.3},{x-3188.,y-3187.},{x-3489.,y-3488.},{x-2002.,y-2000.82},{x-3136.,y-3134.11},{x-3661.,y-3660.},{x-2851.,y-2849.28},{x-1795.,y-1793.93},{x-3282.,y-3280.02},{x-2195.,y-2193.8},{x-3190.,y-3188.59}}
Learning a candidate interpolant at step 2 ...
Synthesized candidate interpolant: -0.00297762+0.986872(1-0.144424x-1.15372y)-0.987517(1+0.115534x+1.11884y)+0.000644515(1+1940x+1939.y)<0
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{x-264911.,y-264912.},{x267605.,y267606.},{x267019.,y267020.},{x265767.,y265768.},{x266696.,y266697.},{x266063.,y266064.},{x267120.,y267121.},{x-264894.,y-264895.},{x266883.,y266884.},{x265481.,y265482.},{x266628.,y266629.},{x266383.,y266384.},{x266177.,y266178.},{x-265514.,y-265515.},{x265069.,y265070.},{x267108.,y267109.},{x266567.,y266568.},{x-263429.,y-263430.},{x-265331.,y-265332.},{x-265295.,y-265296.},{x265715.,y265716.},{x265069.,y265070.},{x266350.,y266351.},{x266063.,y266064.},{x-263636.,y-263637.},{x266177.,y266178.},{x266681.,y266682.},{x265195.,y265196.},{x266183.,y266184.},{x265715.,y265716.}}
Learning a candidate interpolant at step 3 ...
Synthesized candidate interpolant (rounded under precision 0.1): x-y<0
Verifying the candidate ...
Valid interpolant (simplified): x<y
Elapsed time: 2.45773
Rendering graphics ...
 |
|
Done.
Sharper-1:
From T. Okudono et al. [APLAS’17: Sharper and simpler nonlinear interpolants for program verification].
Their result: 34y^2 − 68 y − 102 > 0, ours: 2y-y-2>0.
Sharper-1:
From T. Okudono et al. [APLAS’17: Sharper and simpler nonlinear interpolants for program verification].
Their result: 34y^2 − 68 y − 102 > 0, ours:-y-2>0.
From T. Okudono et al. [APLAS’17: Sharper and simpler nonlinear interpolants for program verification].
Their result: 34y^2 − 68 y − 102 > 0, ours:
2
y
consPhi8=y+1<0;consPsi8=x^2+y^2-1≤0;degree8=2;initialRange8={-5,5};
main[consPhi8,consPsi8,degree8,initialRange8]
Checking inputs ...
Legal inputs.
Checking unsatisfiability ...
Unsat.
Generating initial samplepoints ...
Learning a candidate interpolant at step 1 ...
Synthesized candidate interpolant: 5.52694-7.52526+7.52526<0
2
(1-1.00866y)
2
(1-0.782785y)
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{y-0.949169,x-0.314766},{y-0.907593,x0.419851},{y-0.96092,x0.0546448},{y-0.96092,x-0.276826},{y-0.949402,x0.314062},{y-0.973936,x-0.226825},{y-0.952998,x0.173653},{y-0.90453,x-0.426409},{y-0.967844,x-0.251551},{y-0.981958,x-0.0410448},{y-0.967844,x0.251551},{y-0.907593,x-0.419851},{y-0.96092,x0.276826},{y-0.993975,x-0.109608},{y-0.953297,x0.047619},{y-0.90453,x0.426409},{y-0.99737,x0.0703013},{y-0.908525,x-0.0247934},{y-0.953297,x-0.302034},{y-0.981958,x-0.189099},{y-0.955394,x-0.0175439},{y-1.,x0},{y-0.955394,x0.295333},{y-0.995073,x0.099141},{y-0.952998,x-0.302978},{y-0.991611,x0.0588235},{y-0.966646,x-0.256118},{y-0.908525,x-0.41783},{y-0.964615,x-0.263662},{y-0.91192,x0.282258}}
Learning a candidate interpolant at step 2 ...
Synthesized candidate interpolant: 83.3081-1000-1000+1000+1000<0
2
(1-1.00937y)
2
(1-1.00866y)
2
(1-y)
2
(1-0.99737y)
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{y-1.0021,x4.2},{y-1.00264,x2.7},{y-1.0035,x4.1},{y-1.00218,x4.},{y-1.00051,x2.9},{y-1.00226,x1.1},{y-1.00427,x-0.2},{y-1.00237,x1.},{y-1.00228,x3.5},{y-1.0026,x1.2},{y-1.00285,x0},{y-1.00217,x-2.8},{y-1.00231,x1.7},{y-1.00316,x2.3},{y-1.00333,x3.6},{y-1.00036,x-0.3},{y-1.00392,x4.5},{y-1.00416,x2.9},{y-1.00276,x-3.7},{y-1.00211,x-4.7},{y-1.00027,x-1.1},{y-1.00402,x0.8},{y-1.0029,x4.9},{y-1.00028,x-2.},{y-1.00169,x1.},{y-1.00049,x-0.6},{y-1.00032,x1.8},{y-1.00019,x-0.3},{y-1.0023,x-2.2},{y-1.00076,x3.7}}
Learning a candidate interpolant at step 3 ...
Synthesized candidate interpolant (rounded under precision 0.1): 1+-<0
y
2
2
y
2
Verifying the candidate ...
Valid interpolant (simplified): 2+y<
2
y
Elapsed time: 2.19135
Done.
Sharper-2: From T. Okudono et al. [ APLAS’17].
Their result: 8 y + 4 x^2 > 0, ours: y>0.
Sharper-2: From T. Okudono et al. [ APLAS’17].
Their result: 8 y + 4 x^2 > 0, ours:.
Their result: 8 y + 4 x^2 > 0, ours:
y>0
consPhi9=y-x>0&&x+y>0;consPsi9=y+x^2≤0;degree9=2;initialRange9={-5,5};
main[consPhi9,consPsi9,degree9,initialRange9]
Checking inputs ...
Legal inputs.
Checking unsatisfiability ...
Unsat.
Generating initial samplepoints ...
Learning a candidate interpolant at step 1 ...
Synthesized candidate interpolant: 0.698165+6.35104-5.62997-0.721069<0
2
(1+0.0686465x-0.064659y)
2
(1+0.116488x+0.32185y)
2
(1-0.14208x+0.339649y)
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{x-1618.,y-2.61799×},{x-0.0765118,y0.105089},{x-0.0355584,y-84.},{x1959.,y-3.83775×},{x2435.,y-5.9293×},{x3.09721,y-2416.},{x0.0309847,y-51.},{x0.114048,y-64.},{x2.12846,y-67.},{x3.09721,y-2943.},{x3.09721,y-538.},{x-536.,y-287296.},{x-0.0879396,y0.14392},{x-0.0678797,y-62.},{x3.09721,y-2010.},{x-0.125362,y-90.},{x1.14822,y-95.},{x0.127834,y0.131547},{x-0.0326647,y0.140819},{x-0.0385992,y0.138071},{x-0.02982,y0.140658},{x-0.133013,y0.142478},{x762.,y-580644.},{x-2.02208,y-106.},{x-0.0460542,y0.141575},{x-0.543375,y-22.},{x2419.,y-5.85156×},{x-2.17114,y-21.},{x-0.133013,y0.146412},{x2.31719,y-10.}}
6
10
6
10
6
10
6
10
Learning a candidate interpolant at step 2 ...
Synthesized candidate interpolant (rounded under precision 1.): -y<0
Verifying the candidate ...
Valid interpolant (simplified): y>0
Elapsed time: 2.38085
Rendering graphics ...
 |
|
Done.
Sharper-3: From T. Okudono et al. [ APLAS’17].
Sharper-3: From T. Okudono et al. [ APLAS’17].
In[]:=
consPhi20=x^2+(y-1)^2<1;consPsi20=x^2+(y-2)^2≥4;degree20=2;initialRange20={-3,3};
In[]:=
main[consPhi20,consPsi20,degree20,initialRange20]
Checking inputs ...
Legal inputs.
Checking unsatisfiability ...
Unsat.
Generating initial samplepoints ...
Learning a candidate interpolant at step 1 ...
Synthesized candidate interpolant: 0.974225+967.36+82.89-1055.28+1.82619+2.56437+0.643779<0
2
(1-0.201241x-0.000747645y)
2
(1-0.339761x+0.0113412y)
2
(1-0.219038x+0.035215y)
2
(1-1.53175x+0.647677y)
2
(1-2.01155x+1.95088y)
2
(1+1.85836x+2.77648y)
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{x-1.85427,y1.23157},{x-1.78371,y1.07195},{x-1.72558,y0.966283},{x-1.59775,y0.797006},{x-0.968975,y3.76378},{x0.20026,y4.01346},{x0.578035,y3.91465},{x1.56069,y3.25774},{x-0.876655,y3.80026},{x-1.64667,y0.857657},{x-0.541052,y3.93794},{x-0.932652,y3.79598},{x-0.876655,y3.79763},{x0.347204,y0.0655942},{x-1.25047,y3.56952},{x0.190414,y0.0365879},{x-0.339009,y3.9798},{x0.194873,y4.05587},{x0.00575887,y0.0172008},{x0.740366,y3.85792},{x0.364481,y0.0713664},{x-0.178158,y3.99205},{x-1.57644,y0.769219},{x-0.254229,y3.98378},{x-1.59724,y0.796327},{x-1.53792,y0.716529},{x-0.612183,y0.0959958},{x0.00575887,y0.000850629},{x-1.88205,y1.32333},{x-1.47181,y0.632387}}
Learning a candidate interpolant at step 2 ...
Synthesized candidate interpolant: -0.940373+1000+1000-1791.51-126.688-80.4038-2.78949+1.3897<0
2
(1+0.209925x-0.00715669y)
2
(1-0.201241x-0.000747645y)
2
(1+0.00575887x+0.000850629y)
2
(1+0.364481x+0.0713664y)
2
(1-0.623891x+0.224801y)
2
(1+0.763088x+0.367216y)
2
(1-0.541052x+3.93794y)
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{x0.190823,y0.00912414},{x-0.0473715,y-0.00674974},{x-0.173894,y0.00757409},{x-0.0882091,y0.00194616},{x-0.108999,y-0.00531428},{x0.184289,y0.00850868},{x-0.00950401,y-0.00156829},{x-0.0233145,y0.000135896},{x0.027324,y-0.00132372},{x-0.0647461,y-0.00824242},{x0.156222,y-0.000495197},{x-0.0579151,y-0.00262041},{x0.138699,y0.00481516},{x-0.0882091,y-0.00865847},{x0.0582121,y-0.00231548},{x0.187853,y0.00378463},{x-0.169439,y0.00657652},{x0.0960796,y-0.00241319},{x0.157262,y0.00619239},{x0.174636,y0.00763904},{x-0.108999,y0.00297241},{x0.229433,y0.0132034},{x0.13172,y0.00434223},{x0.13172,y-0.00301694},{x0.0503416,y0.000633668},{x-0.0473715,y0.000561095},{x-0.0647461,y0.00104829},{x0.242501,y0.0140606},{x0.175379,y0.00770426},{x-0.0847936,y0.0017983}}
Learning a candidate interpolant at step 3 ...
Synthesized candidate interpolant (rounded under precision 0.1): -y+<0
2
x
2
2
y
3
Verifying the candidate ...
Valid interpolant (simplified): 3+2(-3+y)y<0
2
x
Elapsed time: 2.91455
Rendering graphics ...
 |
|
Done.
Sharper-4: From T. Okudono et al. [ APLAS’17].
Sharper-4: From T. Okudono et al. [ APLAS’17].
In[]:=
consPhi20=x^2+(y-1)^2<1;consPsi20=x^2+(y+1)^2≤1;degree20=1;initialRange20={-3,3};
In[]:=
main[consPhi20,consPsi20,degree20,initialRange20]
Checking inputs ...
Legal inputs.
Checking unsatisfiability ...
Unsat.
Generating initial samplepoints ...
Learning a candidate interpolant at step 1 ...
Synthesized candidate interpolant: -0.579427+386.712(1-0.226317x-0.0727238y)+511.802(1+0.101396x-0.0220103y)-898.514(1-0.0468636x+0.00278714y)<0
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{x0.0152007,y-0.000115537},{x-0.221517,y-0.0377793},{x-0.347255,y-0.0622293},{x-0.262102,y-0.0349597},{x-0.282763,y-0.055814},{x0.0087072,y-0.0000379084},{x-0.183884,y-0.019985},{x-0.197609,y-0.0197191},{x-0.147285,y-0.0134929},{x-0.238784,y-0.0454349},{x-0.0191854,y-0.0111861},{x-0.231995,y-0.0333407},{x-0.0365998,y-0.000669996},{x-0.262102,y-0.0540593},{x-0.116588,y-0.0121528},{x0.0122491,y-0.00833725},{x-0.342828,y-0.0617614},{x-0.0789551,y-0.0111212},{x-0.0181523,y-0.000164767},{x-0.000885478,y-3.92036×},{x-0.282763,y-0.0408101},{x0.0535714,y-0.00143598},{x-0.043536,y-0.000948142},{x-0.043536,y-0.013209},{x-0.12441,y-0.00776906},{x-0.221517,y-0.0248435},{x-0.238784,y-0.0289273},{x0.0665584,y-0.00334335},{x-0.00014758,y-1.08899×},{x-0.258707,y-0.0340442}}
-7
10
-8
10
Learning a candidate interpolant at step 2 ...
Synthesized candidate interpolant (rounded under precision 1.): -y<0
Verifying the candidate ...
Valid interpolant (simplified): y>0
Elapsed time: 0.961523
Rendering graphics ...
 |
|
Done.
Adjacent-1
Adjacent-1
consPhi15=x+y>0||x+y<0;consPsi15=x+y0;degree15=2;initialRange15={-5,5};
main[consPhi15,consPsi15,degree15,initialRange15]
Checking inputs ...
Legal inputs.
Checking unsatisfiability ...
Unsat.
Generating initial samplepoints ...
Learning a candidate interpolant at step 1 ...
Synthesized candidate interpolant (rounded under precision 0.1): --xy-<0
2
x
2
2
y
2
Verifying the candidate ...
Valid interpolant (simplified): >0
2
(x+y)
Elapsed time: 0.183805
Rendering graphics ...
 |
|
Done.
Adjacent-2
Adjacent-2
consPhi10=y-x^2>0;consPsi10=y-x^2≤0;degree10=2;initialRange10={-5,5};
main[consPhi10,consPsi10,degree10,initialRange10]
Checking inputs ...
Legal inputs.
Checking unsatisfiability ...
Unsat.
Generating initial samplepoints ...
Learning a candidate interpolant at step 1 ...
Synthesized candidate interpolant (rounded under precision 0.1): -y<0
2
x
Verifying the candidate ...
Valid interpolant (simplified): <y
2
x
Elapsed time: 0.251797
Rendering graphics ...
 |
|
Done.
IJCAR’16-2
IJCAR’16-2
consPhi11=-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;consPsi11=-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;degree11=1;initialRange11={-3,3};
main[consPhi11,consPsi11,degree11,initialRange11]
Checking inputs ...
Legal inputs.
Checking unsatisfiability ...
Unsat.
Generating initial samplepoints ...
Learning a candidate interpolant at step 1 ...
Synthesized candidate interpolant: -0.266009+3.90077(1+0.923065x1+0.4x2)+3.39763(1+1.45522x1+0.89038x2)-7.2984(1+0.816059x1+1.01325x2)<0
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{x11.07396,x20.935223,y11.2,y24.9,z12.87045,z20.346249},{x11.08776,x20.923818,y10,y21.9,z12.84764,z2-0.372639},{x11.0747,x20.940704,y13.4,y2-0.3,z12.88141,z20.104575},{x11.09909,x20.958873,y10.4,y24.2,z12.91775,z20.265978},{x10.868646,x20.722309,y10.1,y2-2.,z12.44462,z2-0.226667},{x11.10739,x20.936992,y1-4.,y20.1,z12.87398,z20.164474},{x10.890209,x20.769648,y10.5,y2-2.,z12.5393,z20.246914},{x11.08776,x20.923818,y10.4,y2-3.8,z12.84764,z2-0.25},{x10.956929,x20.900878,y1-0.8,y21.7,z12.80176,z20.401709},{x10.937025,x20.770833,y12.5,y23.8,z12.54167,z20.633917},{x11.05868,x20.970964,y10.1,y23.3,z12.94193,z20.231918},{x10.956929,x20.900878,y11.4,y2-1.7,z12.80176,z20.43193},{x10.936383,x20.817805,y1-0.6,y2-1.,z12.63561,z20.247191},{x11.05868,x20.970964,y14.9,y24.6,z12.94193,z2-0.087156},{x11.02416,x20.994039,y1-4.7,y2-0.4,z12.98808,z2-0.0968421},{x10.961958,x20.793464,y14.,y21.5,z12.58693,z20.309524},{x11.12262,x20.992454,y14.4,y24.7,z12.98491,z20},{x10.93847,x20.795983,y14.2,y2-3.,z12.59197,z20.464286},{x11.0798,x20.976145,y1-2.7,y24.6,z12.95229,z20.201923},{x11.06726,x20.939655,y1-4.2,y2-3.6,z12.87931,z2-0.335446},{x11.01391,x20.984152,y1-5.,y2-1.1,z12.9683,z2-0.0769231},{x10.933868,x20.828629,y1-2.,y2-0.6,z12.65726,z20.555878},{x11.01322,x20.880573,y12.3,y24.6,z12.76115,z20.473726},{x10.966667,x20.880435,y10.1,y23.1,z12.76087,z20.472994},{x11.02616,x20.999658,y11.1,y2-2.5,z12.99932,z20},{x10.997271,x20.959596,y12.9,y20.4,z12.91919,z20.281368},{x10.980738,x20.894419,y14.5,y24.8,z12.78884,z2-0.446814},{x11.10739,x20.936992,y1-2.4,y2-4.1,z12.87398,z2-0.332436},{x11.15605,x20.975072,y1-4.3,y23.7,z12.95014,z20.157745},{x11.16607,x20.986115,y14.7,y2-2.,z12.97223,z20}}
Learning a candidate interpolant at step 2 ...
Synthesized candidate interpolant: -3.3169+11.4186(1+0.890209x1+0.769648x2)+47.5228(1+0.997271x1+0.959596x2)-58.9414(1+0.816059x1+1.01325x2)<0
Verifying the candidate ...
Invalid.
Generating counter-examples...
counterExamples:{{x10.995988,x21.08948,y1-1.00401,y20,z1-3.,z20.9},{x10.993236,x21.11611,y1-1.00676,y20,z11.2,z24.3},{x10.990761,x21.02164,y1-1.00924,y20.0793651,z13.4,z24.3},{x10.988154,x21.11653,y1-1.01185,y2-0.0998589,z1-0.1,z2-3.1},{x10.997291,x21.07356,y1-1.00271,y20,z1-3.5,z20.9},{x10.990761,x21.09566,y1-1.00924,y2-0.0961404,z12.1,z2-3.3},{x10.990841,x21.13504,y1-1.00916,y20,z11.,z20.9},{x10.898925,x20.96252,y1-1.10107,y20.436495,z1-1.1,z2-3.7},{x10.945429,x20.980408,y1-1.05457,y20.0769231,z1-2.1,z23.7},{x10.999009,x21.04452,y1-1.00099,y20,z13.6,z2-0.7},{x10.968863,x21.01111,y1-1.03114,y2-0.247346,z13.9,z20.9},{x10.997635,x21.04152,y1-1.00236,y20.054766,z1-4.5,z24.9},{x10.990761,x21.03047,y1-1.00924,y2-0.132156,z10.3,z23.9},{x10.989584,x21.13354,y1-1.01042,y20.0537643,z1-1.6,z2-3.8},{x10.990761,x21.0529,y1-1.00924,y2-0.017284,z1-1.3,z24.8},{x10.99605,x21.02066,y1-1.00395,y20.0478632,z11.9,z2-2.},{x10.935123,x20.990391,y1-1.06488,y20.174825,z11.2,z2-1.4},{x10.935123,x20.990391,y1-1.06488,y20.354193,z1-5.,z23.},{x10.896872,x20.96062,y1-1.10313,y2-0.440534,z1-2.7,z2-3.4},{x10.945319,x20.97392,y1-1.05468,y20.325104,z1-4.8,z20.6},{x10.922874,x21.01518,y1-1.07713,y2-0.384803,z1-0.9,z20.3},{x10.988154,x21.11653,y1-1.01185,y20.0750988,z1-2.9,z2-2.5},{x10.900722,x20.956555,y1-1.09928,y2-0.00854701,z12.3,z