[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Looking for general strategy to solve inequality problem



Hi all,

I have the following statement, which 
[-1]  dx < -140
[-2]  dv < 50
  |-------
[1]   dx < -150
[2]   dv < 45
[3]   (1 + (dv - 50 + dv * ((140 + dx) / 10) - 50 * ((140 + dx) / 10)) / 5
+ (140 + dx) / 10)
       / 1
       >=
       122957620769739151/5000000000000000000 * dx -
475345081090927124023/100000000000000000000
+ 10091024637222290039/100000000000000000000 * dv

Leaving the original as-is and doing (field 3) results in:
{-1}  100000000000000000000 > 0
{-2}  dx < -140
{-3}  dv < 50
  |-------
{1}   dx < -150
{2}   dv < 45
{3}   500000000000000000000 +
       (20000000000000000000 * (dv * dx) + 2800000000000000000000 * dv) /
10
       - (140000000000000000000000 + 1000000000000000000000 * dx) / 10
       + 20000000000000000000 * dv
       + 10000000000000000000 * dx
       >=
       (10091024637222290039 * dv) - 475345081090927124023 +
2459152415394783020 * dx

I manually figured out that  [3] can also be simplified to:
   (dx + 150) * (dv - 45) / 50 >= 
       122957620769739151/5000000000000000000 * dx -
475345081090927124023/100000000000000000000
+ 10091024637222290039/100000000000000000000 * dv

Using a case-replace and field I end up with:
{-1}  100000000000000000000 > 0
{-2}  (1 + (140 + dx) / 10 +
        (-50 - 50 * ((140 + dx) / 10) + (140 + dx) / 10 * dv + dv) / 5)
       / 1
       = (dx + 150) * (dv - 45) / 50
{-3}  dx < -140
{-4}  dv < 50
  |-------
{1}   dx < -150
{2}   dv < 45
{3}   2000000000000000000 * ((dv - 45) * (dx + 150)) >=
       (10091024637222290039 * dv) - 475345081090927124023 +
        2459152415394783020 * dx

This still wasn’t very helpful, so I used Wolfram-Alpha to simplify the inequality and got:
(2000000000000000000 * dv - 92459152415394783020) * dx >= 13024654918909072875977 - 289908975362777709961 * dv

Using a case-replace and field I end up with:
{-1}  2000000000000000000 * ((dv - 45) * (dx + 150)) >=
       (10091024637222290039 * dv) - 475345081090927124023 +
        2459152415394783020 * dx
       =
       (2000000000000000000 * dv - 92459152415394783020) * dx >=
        13024654918909072875977 - 289908975362777709961 * dv
{-2}  100000000000000000000 > 0
{-3}  (1 + (140 + dx) / 10 +
        (-50 - 50 * ((140 + dx) / 10) + (140 + dx) / 10 * dv + dv) / 5)
       / 1
       = (dx + 150) * (dv - 45) / 50
{-4}  dx < -140
{-5}  dv < 50
  |-------
{1}   dx < -150
{2}   dv < 45
{3}   (2000000000000000000 * dv - 92459152415394783020) * dx >=
       13024654918909072875977 - 289908975362777709961 * dv

Now, I imagine I could probably solve this eventually (I’ve already graphed it to prove to myself that it’s true), but I was wondering if there’s a better strategy I could be using in general?

Best Regards,