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_js.yml

@@ -52,7 +52,7 @@ jobs:
       # Install external dependencies
       # remove this step when opam 2.1 will be used
       - name: Install depext
-        run: opam depext alt-ergo-lib alt-ergo-parsers alt-ergo altgr-ergo
+        run: opam depext alt-ergo-lib alt-ergo-parsers alt-ergo altgr-ergo alt-ergo-osdp
 
       # Install dependencies
       - name: Install deps

.github/workflows/build_macos.yml

@@ -59,7 +59,7 @@ jobs:
       # Install external dependencies
       # remove this step when opam 2.1 will be used
       #- name: opam install depext
-      #  run: opam depext alt-ergo-lib alt-ergo-parsers alt-ergo altgr-ergo
+      #  run: opam depext alt-ergo-lib alt-ergo-parsers alt-ergo altgr-ergo alt-ergo-osdp
 
       # Install dependencies
       - name: Install deps

.github/workflows/build_make.yml

@@ -50,7 +50,7 @@ jobs:
       # Install external dependencies
       # remove this step when opam 2.1 will be used
       - name: opam install depext
-        run: opam depext alt-ergo-lib alt-ergo-parsers alt-ergo altgr-ergo
+        run: opam depext alt-ergo-lib alt-ergo-parsers alt-ergo altgr-ergo alt-ergo-osdp
 
       # Install dependencies
       - name: opam install deps

.github/workflows/build_ubuntu.yml

@@ -57,7 +57,7 @@ jobs:
       # Install external dependencies
       # remove this step when opam 2.1 will be used
       - name: Install depext
-        run: opam depext alt-ergo-lib alt-ergo-parsers alt-ergo altgr-ergo
+        run: opam depext alt-ergo-lib alt-ergo-parsers alt-ergo altgr-ergo alt-ergo-osdp
 
       # Install dependencies
       - name: Install deps

.github/workflows/build_windows.yml

@@ -52,7 +52,7 @@ jobs:
       # Install external dependencies
       # remove this step when opam 2.1 will be used
       - name: opam install depext
-        run: opam depext alt-ergo-lib alt-ergo-parsers alt-ergo altgr-ergo
+        run: opam depext alt-ergo-lib alt-ergo-parsers alt-ergo altgr-ergo alt-ergo-osdp
 
       # Install dependencies
       - name: Install deps

.github/workflows/documentation.yml

@@ -60,7 +60,7 @@ jobs:
       # Install external dependencies
       # remove this step when opam 2.1 will be used
       - name: opam install depext
-        run: opam depext alt-ergo-lib alt-ergo-parsers alt-ergo altgr-ergo
+        run: opam depext alt-ergo-lib alt-ergo-parsers alt-ergo altgr-ergo alt-ergo-osdp
 
       # Install dependencies if the cache is not retrieved
       # odoc is installed as deps with { with-doc } in opam files

Makefile

@@ -51,7 +51,7 @@ SPHINXBUILD = sphinx-build
 # - .ml files generated by menhir or ocamllex
 #   (since they reside in dune specific directory)
 GENERATED_USEFUL=$(UTIL_DIR)/config.ml $(BTEXT_DIR)/flags.dune
-GENERATED_LINKS=alt-ergo altgr-ergo alt-ergo.js alt-ergo-worker.js AB-Why3-plugin.cma AB-Why3-plugin.cmxs fm-simplex-plugin.cma fm-simplex-plugin.cmxs
+GENERATED_LINKS=alt-ergo altgr-ergo alt-ergo.js alt-ergo-worker.js AB-Why3-plugin.cma AB-Why3-plugin.cmxs fm-simplex-plugin.cma fm-simplex-plugin.cmxs osdp-plugin.cma osdp-plugin.cmxs
 GENERATED=$(GENERATED_USEFUL) $(GENERATED_LINKS)
 
 
@@ -108,6 +108,14 @@ fm-simplex:
 	ln -sf $(INSTALL_DIR)/default/share/alt-ergo/plugins/fm-simplex-plugin.cma fm-simplex-plugin.cma
 	ln -sf $(INSTALL_DIR)/default/share/alt-ergo/plugins/fm-simplex-plugin.cmxs fm-simplex-plugin.cmxs
 
+# OSDP plugin
+osdp:
+	$(DUNE) build $(DUNE_FLAGS) \
+		$(INSTALL_DIR)/default/share/alt-ergo/plugins/osdp-plugin.cma \
+		$(INSTALL_DIR)/default/share/alt-ergo/plugins/osdp-plugin.cmxs
+	ln -sf $(INSTALL_DIR)/default/share/alt-ergo/plugins/osdp-plugin.cma osdp-plugin.cma
+	ln -sf $(INSTALL_DIR)/default/share/alt-ergo/plugins/osdp-plugin.cmxs osdp-plugin.cmxs
+
 # Ab-Why3 plugin
 AB-Why3:
 	$(DUNE) build $(DUNE_FLAGS) \
@@ -121,6 +129,8 @@ plugins:
 	$(DUNE) build $(DUNE_FLAGS) \
 		$(INSTALL_DIR)/default/share/alt-ergo/plugins/fm-simplex-plugin.cma \
 		$(INSTALL_DIR)/default/share/alt-ergo/plugins/fm-simplex-plugin.cmxs \
+		$(INSTALL_DIR)/default/share/alt-ergo/plugins/osdp-plugin.cma \
+		$(INSTALL_DIR)/default/share/alt-ergo/plugins/osdp-plugin.cmxs \
 		$(INSTALL_DIR)/default/share/alt-ergo/plugins/AB-Why3-plugin.cma \
 		$(INSTALL_DIR)/default/share/alt-ergo/plugins/AB-Why3-plugin.cmxs
 
@@ -135,7 +145,7 @@ all: gen
 
 # declare these targets as phony to avoid name clashes with existing directories,
 # particularly the "plugins" target
-.PHONY: lib bin gui fm-simplex AB-Why3 plugins all
+.PHONY: lib bin gui fm-simplex osdp AB-Why3 plugins all
 
 
 # =====================

alt-ergo-osdp.opam

@@ -0,0 +1,43 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "dev"
+synopsis: "The Alt-Ergo SMT prover: OSDP PLugin"
+description: """
+This is the OSDP plugin for the Alt-Ergo SMT solver.
+
+Alt-Ergo is an automatic theorem prover of mathematical formulas. It was developed at LRI, and is now maintained at OCamlPro.
+
+See more details on http://alt-ergo.ocamlpro.com/
+
+The OSDP plugin relies on the OSDP library to attempt to solve goals
+with polynomial inequalities using SDP (SemiDefinite Programming)
+numerical solvers as backend. Despite the numerical solvers providing
+only approximate solutions, the OSDP library performs an a-posteriori
+rigorous check to ensure soundness. The ValidSDP library provides a
+Coq verified version of this soundness check.
+
+To use, run alt-ergo with option
+alt-ergo --polynomial-plugin osdp-plugin.cmxs"""
+maintainer: ["Alt-Ergo developers"]
+authors: ["Alt-Ergo developers"]
+license: "LGPL-3"
+homepage: "https://alt-ergo.ocamlpro.com/"
+doc: "https://ocamlpro.github.io/alt-ergo"
+bug-reports: "https://github.com/OCamlPro/alt-ergo/issues"
+depends: [
+  "ocaml" {>= "4.05.0"}
+  "dune" {>= "2.9" & >= "2.9"}
+  "dune-configurator"
+  "alt-ergo"
+  "alt-ergo-lib" {= version}
+  "alt-ergo"
+  "osdp" {>= "1.0.0"}
+  "odoc" {with-doc}
+]
+
+build: [
+  ["ocaml" "unix.cma" "configure.ml" name "--prefix" prefix "--libdir" lib "--mandir" man]
+  ["dune" "subst"] {dev}
+  ["dune" "build" "-p" name "-j" jobs]
+]
+dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"

alt-ergo-osdp.opam.template

@@ -0,0 +1,12 @@
+# This part comes from the template. Please edit alt-ergo-osdp.opam.template
+# and not alt-ergo-osdp.opam which is generated by dune
+
+license: [
+  "LGPL-3"
+]
+
+build: [
+  ["ocaml" "unix.cma" "configure.ml" name "--prefix" prefix "--libdir" lib "--mandir" man]
+  ["dune" "subst"] {pinned}
+  ["dune" "build" "-p" name "-j" jobs]
+]

configure.ml

@@ -157,7 +157,10 @@ let datadir =
   |> Filename.dirname
   |> follow Filename.parent_dir_name
   |> follow "share"
-  |> follow "alt-ergo"
+
+let osdp_pluginsdir = datadir |> follow "alt-ergo-osdp" |> follow "plugins"
+
+let datadir = datadir |> follow "alt-ergo"
 
 let pluginsdir = datadir |> follow "plugins"
 

dune-project

@@ -1,5 +1,4 @@
-(lang dune 2.0)
-(allow_approximate_merlin)
+(lang dune 2.9)
 
 ; Since we want to generate opam files we need to provide informations ;
 (generate_opam_files true)
@@ -113,3 +112,37 @@ See more details on http://alt-ergo.ocamlpro.com/"
   (odoc :with-doc)
  )
 )
+
+; Fifth package, the alt-ergo OSDP plugin
+
+(package
+ (name alt-ergo-osdp)
+ (synopsis "The Alt-Ergo SMT prover: OSDP PLugin")
+ (description "\
+This is the OSDP plugin for the Alt-Ergo SMT solver.
+
+Alt-Ergo is an automatic theorem prover of mathematical formulas. It was developed at LRI, and is now maintained at OCamlPro.
+
+See more details on http://alt-ergo.ocamlpro.com/
+
+The OSDP plugin relies on the OSDP library to attempt to solve goals
+with polynomial inequalities using SDP (SemiDefinite Programming)
+numerical solvers as backend. Despite the numerical solvers providing
+only approximate solutions, the OSDP library performs an a-posteriori
+rigorous check to ensure soundness. The ValidSDP library provides a
+Coq verified version of this soundness check.
+
+To use, run alt-ergo with option
+alt-ergo --polynomial-plugin osdp-plugin.cmxs"
+ ) (license "LGPL-3")
+
+ (depends
+  (ocaml (>= 4.05.0))
+  (dune (>= 2.9))
+  dune-configurator
+  alt-ergo
+  (alt-ergo-lib (= :version))
+  alt-ergo
+  (osdp (>= 1.0.0))
+ )
+)

src/bin/common/parse_command.ml

@@ -157,11 +157,12 @@ let mk_dbg_opt_spl1 debug debug_ac debug_adt debug_arith debug_arrays
   set_debug_constr debug_constr;
   `Ok()
 
-let mk_dbg_opt_spl2 debug_explanations debug_fm debug_fpa debug_gc
+let mk_dbg_opt_spl2 debug_explanations debug_fm debug_sdp debug_fpa debug_gc
     debug_interpretation debug_ite debug_matching debug_sat
   =
   set_debug_explanations debug_explanations;
   set_debug_fm debug_fm;
+  set_debug_sdp debug_sdp;
   set_debug_fpa debug_fpa;
   set_debug_gc debug_gc;
   set_debug_interpretation debug_interpretation;
@@ -385,16 +386,19 @@ let mk_term_opt disable_ites inline_lets rewriting term_like_pp
   set_inline_lets inline_lets;
   `Ok()
 
-let mk_theory_opt disable_adts inequalities_plugin no_ac no_contracongru
-    no_fm no_nla no_tcp no_theory restricted tighten_vars use_fpa
+let mk_theory_opt disable_adts inequalities_plugin polynomial_plugin
+    no_ac no_contracongru no_fm no_sdp no_nla
+    no_tcp no_theory restricted tighten_vars use_fpa
   =
   set_no_ac no_ac;
   set_no_fm no_fm;
+  set_no_sdp no_sdp;
   set_no_nla no_nla;
   set_no_tcp no_tcp;
   set_no_theory no_theory;
   set_use_fpa use_fpa;
   set_inequalities_plugin inequalities_plugin;
+  set_polynomial_plugin polynomial_plugin;
   set_restricted restricted;
   set_disable_adts disable_adts;
   set_tighten_vars tighten_vars;
@@ -549,6 +553,10 @@ let parse_dbg_opt_spl2 =
     let doc = "Set the debugging flag of inequalities." in
     Arg.(value & flag & info ["dfm"] ~docs ~doc) in
 
+  let debug_sdp =
+    let doc = "Set the debugging flag of polynomial." in
+    Arg.(value & flag & info ["dsdp"] ~docs ~doc) in
+
   let debug_fpa =
     let doc = "Set the debugging flag of floating-point." in
     Arg.(value & opt int (get_debug_fpa ()) & info ["dfpa"] ~docs ~doc) in
@@ -580,6 +588,7 @@ let parse_dbg_opt_spl2 =
 
              debug_explanations $
              debug_fm $
+             debug_sdp $
              debug_fpa $
              debug_gc $
              debug_interpretation $
@@ -1170,6 +1179,12 @@ let parse_theory_opt =
     Arg.(value & opt string (get_inequalities_plugin ()) &
          info ["inequalities-plugin"] ~docs ~doc) in
 
+  let polynomial_plugin =
+    let doc =
+      "Use the given module to handle polynomial." in
+    Arg.(value & opt string (get_polynomial_plugin ()) &
+         info ["polynomial-plugin"] ~docs ~doc) in
+
   let no_ac =
     let doc = "Disable the AC theory of Associative and \
                Commutative function symbols." in
@@ -1183,6 +1198,10 @@ let parse_theory_opt =
     let doc = "Disable Fourier-Motzkin algorithm." in
     Arg.(value & flag & info ["no-fm"] ~docs ~doc) in
 
+  let no_sdp =
+    let doc = "Disable Sum of Square algorithm." in
+    Arg.(value & flag & info ["no-sdp"] ~docs ~doc) in
+
   let no_nla =
     let doc = "Disable non-linear arithmetic reasoning (i.e. non-linear \
                multplication, division and modulo on integers and rationals). \
@@ -1212,8 +1231,9 @@ let parse_theory_opt =
     Arg.(value & flag & info ["use-fpa"] ~docs ~doc) in
 
   Term.(ret (const mk_theory_opt $
-             disable_adts $ inequalities_plugin $ no_ac $ no_contracongru $
-             no_fm $ no_nla $ no_tcp $ no_theory $ restricted $
+             disable_adts $ inequalities_plugin $ polynomial_plugin $
+             no_ac $ no_contracongru $
+             no_fm $ no_sdp $ no_nla $ no_tcp $ no_theory $ restricted $
              tighten_vars $ use_fpa
             )
        )
@@ -1316,5 +1336,5 @@ let parse_cmdline_arguments () =
   let r = Cmdliner.Term.(eval main) in
   match r with
   | `Ok false -> raise (Exit_parse_command 0)
-  | `Ok true -> ()
+  | `Ok true -> IntervalCalculus.refresh_plugins ()
   | e -> exit @@ Term.(exit_status_of_result e)

src/lib/dune

@@ -32,7 +32,7 @@
     Cnf Input Frontend Parsed_interface Typechecker
     ; reasoners
     Ac Arith Arrays Arrays_rel Bitv Ccx Shostak Relation Enum Enum_rel
-    Fun_sat Inequalities Bitv_rel Th_util Adt Adt_rel
+    Fun_sat Inequalities PolynomialInequalities Bitv_rel Th_util Adt Adt_rel
     Instances IntervalCalculus Intervals Ite_rel Ite Matching Matching_types
     Polynome Records Records_rel Satml_frontend_hybrid Satml_frontend Satml
     Sat_solver Sat_solver_sig Sig Sig_rel Theory Uf Use

src/lib/reasoners/ac.ml

@@ -67,6 +67,8 @@ module type S = sig
   (* replaces the first argument by the second one in the given AC value *)
   val subst : r -> r -> t -> r
 
+  val term_extract : t -> Expr.t option * bool (* original term ? *)
+
   (* add flatten the 2nd arg w.r.t HS.t, add it to the given list
      and compact the result *)
   val add : Sy.t -> r * int -> (r * int) list -> (r * int) list
@@ -279,6 +281,23 @@ module Make (X : Sig.X) = struct
     t
 
 
+  let term_extract {h=h;l=l;t=t; distribute=_} =
+    let expand =
+      List.fold_left
+        (fun l (x,n) -> let l= ref l in for _=1 to n do l:=x::!l done; !l) [] in
+    let l =
+      List.fold_left
+        (fun l e -> match l with
+           | None -> None
+           | Some l ->
+             match X.term_extract e with
+             | None, _ -> None
+             | Some e, _ -> Some (e :: l))
+        (Some []) (expand l) in
+    match l with
+    | None -> None, false
+    | Some l -> Some (Expr.mk_term h l t), false
+
   let add h arg arg_l =
     Timers.exec_timer_start Timers.M_AC Timers.F_add;
     let r = compact (flatten h arg arg_l) in

src/lib/reasoners/ac.mli

@@ -61,6 +61,8 @@ module type S = sig
   (* replaces the first argument by the second one in the given AC value *)
   val subst : r -> r -> t -> r
 
+  val term_extract : t -> Expr.t option * bool (* original term ? *)
+
   (* add flatten the 2nd arg w.r.t HS.t, add it to the given list
      and compact the result *)
   val add : Symbols.t -> r * int -> (r * int) list -> (r * int) list

src/lib/reasoners/intervalCalculus.ml

@@ -42,6 +42,9 @@ module I = Intervals
 module OracleContainer =
   (val (Inequalities.get_current ()) : Inequalities.Container_SIG)
 
+(* Refresh plugins after proper parse of parameters. *)
+let refresh_plugins () =
+  PolynomialInequalities.refresh ()
 
 module X = Shostak.Combine
 
@@ -54,6 +57,7 @@ module MX0 = Shostak.MXH
 module MPL = Expr.Map
 
 module Oracle = OracleContainer.Make(P)
+module PolynomialIneqs = PolynomialInequalities.Container
 
 module SE = Expr.Set
 module ME = Expr.Map
@@ -1673,6 +1677,15 @@ let assume ~query env uf la =
       in
       let env = Sim_Wrap.solve env 1 in
       let env = loop_update_intervals are_eq env 0 in
+      let () =
+        if new_ineqs then
+          let polys =
+            List.filter
+              (fun (p, i) ->
+                 Uf.is_normalized uf (alien_of p) && not (I.is_undefined i))
+              (MP.bindings env.polynomes) in
+          PolynomialIneqs.test_polynomes polys in
+
       let env, eqs = equalities_from_intervals env eqs in
 
       Debug.env env;

src/lib/reasoners/intervalCalculus.mli

@@ -27,3 +27,5 @@
 (******************************************************************************)
 
 include Sig_rel.RELATION
+
+val refresh_plugins: unit -> unit