Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add new plugin for polynomial inequalities (using OSDP) #499

Open
wants to merge 3 commits into
base: next
Choose a base branch
from
Open

Add new plugin for polynomial inequalities (using OSDP) #499

wants to merge 3 commits into from

Commits on Sep 28, 2022

  1. Add OSDP plugin. 

    This is the plugin presented in the following paper:

A Non-linear Arithmetic Procedure for Control-Command Software Verification,
Pierre Roux, Mohamed Iguernlala, Sylvain Conchon, TACAS 2018

In particular, it enables to solve goals like:

logic v__0 : real
logic v_x0 : real
logic v_x1 : real
logic v_x2 : real
goal g:
  6.04 * v_x0 * v_x0 + (- (9.65)) * v_x0 * v_x1 + (- (2.26)) * v_x0 * v_x2
  + 11.36 * v_x1 * v_x1 + 2.67 * v_x1 * v_x2 + 3.76 * v_x2 * v_x2 <= 1.0
  and v__0 <= 1.0 and (- (1.0)) <= v__0
  -> 6.04
     * (0.9379 * v_x0 + (- (0.0381)) * v_x1 + (- (0.0414)) * v_x2
        + 0.0237 * v__0)
     * (0.9379 * v_x0 + (- (0.0381)) * v_x1 + (- (0.0414)) * v_x2
        + 0.0237 * v__0)
     + (- (9.65))
       * (0.9379 * v_x0 + (- (0.0381)) * v_x1 + (- (0.0414)) * v_x2
          + 0.0237 * v__0)
       * ((- (0.0404)) * v_x0 + 0.968 * v_x1 + (- (0.0179)) * v_x2
          + 0.0143 * v__0)
     + (- (2.26))
       * (0.9379 * v_x0 + (- (0.0381)) * v_x1 + (- (0.0414)) * v_x2
          + 0.0237 * v__0)
       * (0.0142 * v_x0 + (- (0.0197)) * v_x1 + 0.9823 * v_x2 + 0.0077 * v__0)
     + 11.36
       * ((- (0.0404)) * v_x0 + 0.968 * v_x1 + (- (0.0179)) * v_x2
          + 0.0143 * v__0)
       * ((- (0.0404)) * v_x0 + 0.968 * v_x1 + (- (0.0179)) * v_x2
          + 0.0143 * v__0)
     + 2.67
       * ((- (0.0404)) * v_x0 + 0.968 * v_x1 + (- (0.0179)) * v_x2
          + 0.0143 * v__0)
       * (0.0142 * v_x0 + (- (0.0197)) * v_x1 + 0.9823 * v_x2 + 0.0077 * v__0)
     + 3.76
       * (0.0142 * v_x0 + (- (0.0197)) * v_x1 + 0.9823 * v_x2 + 0.0077 * v__0)
       * (0.0142 * v_x0 + (- (0.0197)) * v_x1 + 0.9823 * v_x2 + 0.0077 * v__0)
     <= 1.0

that are out of reach of most SMT solvers.
This goals come from verification of the following linear controller:

typedef struct { double x0, x1, x2; } state;

/*@ predicate inv(state *s) = 6.04 * s->x0 * s->x0 - 9.65 * s->x0 * s->x1
  @   - 2.26 * s->x0 * s->x2 + 11.36 * s->x1 * s->x1
  @   + 2.67 * s->x1 * s->x2 + 3.76 * s->x2 * s->x2 <= 1; */

/*@ requires \valid(s) && inv(s) && -1 <= in0 <= 1;
  @ ensures inv(s); */
void step(state *s, double in0) {
  double pre_x0 = s->x0, pre_x1 = s->x1, pre_x2 = s->x2;

  s->x0 = 0.9379 * pre_x0 - 0.0381 * pre_x1 - 0.0414 * pre_x2 + 0.0237 * in0;
  s->x1 = -0.0404 * pre_x0 + 0.968 * pre_x1 - 0.0179 * pre_x2 + 0.0143 * in0;
  s->x2 = 0.0142 * pre_x0 - 0.0197 * pre_x1 + 0.9823 * pre_x2 + 0.0077 * in0;
}
    @proux01
    proux01 committed Sep 28, 2022
    Configuration menu
    Copy the full SHA
    bfe2ed0 View commit details
    Browse the repository at this point in the history

  2. Examples of goals with polynomial constraints

    @ploc @proux01
    ploc authored and proux01 committed Sep 28, 2022
    Configuration menu
    Copy the full SHA
    055499f View commit details
    Browse the repository at this point in the history

  3. Add regression tests for the OSDP plugin

    @proux01
    proux01 committed Sep 28, 2022
    Configuration menu
    Copy the full SHA
    912bb49 View commit details
    Browse the repository at this point in the history