Add OSDP plugin.

This is the plugin presented in the following paper:

Pierre Roux, Mohamed Iguernlala, Sylvain Conchon:
A Non-linear Arithmetic Procedure for Control-Command Software Verification.
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;
}

.github/workflows/build_make.yml

@@ -56,6 +56,9 @@ jobs:
       - name: opam install deps
         run: opam install ./*.opam --deps-only
 
+      - name: test
+        run: opam list
+
       # make use `dune build` which update .opam file if the dune-project is updated
       - name: Make
         run: opam exec -- make