From 5eeb383b124c80c865a441c46b252ca8511836d1 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 20 Jun 2018 17:11:05 +0200 Subject: [PATCH] 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 | 2 +- .github/workflows/build_macos.yml | 2 +- .github/workflows/build_make.yml | 2 +- .github/workflows/build_ubuntu.yml | 2 +- .github/workflows/build_windows.yml | 2 +- .github/workflows/documentation.yml | 2 +- Makefile | 14 +- alt-ergo-osdp.opam | 43 +++ alt-ergo-osdp.opam.template | 12 + configure.ml | 5 +- dune-project | 37 ++- src/bin/common/parse_command.ml | 32 +- src/lib/dune | 2 +- src/lib/reasoners/ac.ml | 19 ++ src/lib/reasoners/ac.mli | 2 + src/lib/reasoners/intervalCalculus.ml | 13 + src/lib/reasoners/intervalCalculus.mli | 2 + src/lib/reasoners/polynomialInequalities.ml | 94 ++++++ src/lib/reasoners/polynomialInequalities.mli | 43 +++ src/lib/reasoners/shostak.ml | 2 +- src/lib/util/numbersInterface.mli | 2 + src/lib/util/numsNumbers.ml | 2 + src/lib/util/options.ml | 9 + src/lib/util/options.mli | 22 +- src/lib/util/timers.ml | 10 +- src/lib/util/timers.mli | 2 + src/lib/util/zarithNumbers.ml | 2 + src/plugins/osdp/dune | 22 ++ src/plugins/osdp/index_sdp.mld | 2 + src/plugins/osdp/osdpIneqs.ml | 327 +++++++++++++++++++ src/plugins/osdp/osdpIneqs.mli | 20 ++ 31 files changed, 731 insertions(+), 21 deletions(-) create mode 100644 alt-ergo-osdp.opam create mode 100644 alt-ergo-osdp.opam.template create mode 100644 src/lib/reasoners/polynomialInequalities.ml create mode 100644 src/lib/reasoners/polynomialInequalities.mli create mode 100644 src/plugins/osdp/dune create mode 100644 src/plugins/osdp/index_sdp.mld create mode 100644 src/plugins/osdp/osdpIneqs.ml create mode 100644 src/plugins/osdp/osdpIneqs.mli diff --git a/.github/workflows/build_js.yml b/.github/workflows/build_js.yml index 1b55ccafe9..e6156d8a32 100644 --- a/.github/workflows/build_js.yml +++ b/.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 diff --git a/.github/workflows/build_macos.yml b/.github/workflows/build_macos.yml index 12c42f550f..daa4062cf1 100644 --- a/.github/workflows/build_macos.yml +++ b/.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 diff --git a/.github/workflows/build_make.yml b/.github/workflows/build_make.yml index 7cd03ae559..1532c4dc6c 100644 --- a/.github/workflows/build_make.yml +++ b/.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 diff --git a/.github/workflows/build_ubuntu.yml b/.github/workflows/build_ubuntu.yml index 1c0ebe616e..9aab077821 100644 --- a/.github/workflows/build_ubuntu.yml +++ b/.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 diff --git a/.github/workflows/build_windows.yml b/.github/workflows/build_windows.yml index dee7867b5b..5d9d3ef32e 100644 --- a/.github/workflows/build_windows.yml +++ b/.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 diff --git a/.github/workflows/documentation.yml b/.github/workflows/documentation.yml index d488a6c614..9a3b17667d 100644 --- a/.github/workflows/documentation.yml +++ b/.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 diff --git a/Makefile b/Makefile index ad425a607d..5b60849584 100644 --- a/Makefile +++ b/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 # ===================== diff --git a/alt-ergo-osdp.opam b/alt-ergo-osdp.opam new file mode 100644 index 0000000000..276a8d4d17 --- /dev/null +++ b/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.1.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" diff --git a/alt-ergo-osdp.opam.template b/alt-ergo-osdp.opam.template new file mode 100644 index 0000000000..ca9c679c2c --- /dev/null +++ b/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] +] diff --git a/configure.ml b/configure.ml index 0eaf465545..087009d04f 100644 --- a/configure.ml +++ b/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" diff --git a/dune-project b/dune-project index 917facb936..05be4a05af 100644 --- a/dune-project +++ b/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.1.0)) + ) +) diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index 46a2ad21af..40355f0901 100644 --- a/src/bin/common/parse_command.ml +++ b/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) diff --git a/src/lib/dune b/src/lib/dune index 91399d1e29..36ba37c049 100644 --- a/src/lib/dune +++ b/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 diff --git a/src/lib/reasoners/ac.ml b/src/lib/reasoners/ac.ml index a064d16fa0..e4f97953d8 100644 --- a/src/lib/reasoners/ac.ml +++ b/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 diff --git a/src/lib/reasoners/ac.mli b/src/lib/reasoners/ac.mli index 9ce128925a..3192fde414 100644 --- a/src/lib/reasoners/ac.mli +++ b/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 diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml index 2ed4c7560c..2b9aa1f184 100644 --- a/src/lib/reasoners/intervalCalculus.ml +++ b/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; diff --git a/src/lib/reasoners/intervalCalculus.mli b/src/lib/reasoners/intervalCalculus.mli index c0c513d5ef..9fde10b4f0 100644 --- a/src/lib/reasoners/intervalCalculus.mli +++ b/src/lib/reasoners/intervalCalculus.mli @@ -27,3 +27,5 @@ (******************************************************************************) include Sig_rel.RELATION + +val refresh_plugins: unit -> unit diff --git a/src/lib/reasoners/polynomialInequalities.ml b/src/lib/reasoners/polynomialInequalities.ml new file mode 100644 index 0000000000..dae0d1795d --- /dev/null +++ b/src/lib/reasoners/polynomialInequalities.ml @@ -0,0 +1,94 @@ +(******************************************************************************) +(* *) +(* The Alt-Ergo theorem prover *) +(* Copyright (C) 2006-2013 *) +(* *) +(* Sylvain Conchon *) +(* Evelyne Contejean *) +(* *) +(* Francois Bobot *) +(* Mohamed Iguernelala *) +(* Stephane Lescuyer *) +(* Alain Mebsout *) +(* *) +(* CNRS - INRIA - Universite Paris Sud *) +(* *) +(* This file is distributed under the terms of the Apache Software *) +(* License version 2.0 *) +(* *) +(* ------------------------------------------------------------------------ *) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2013-2017 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of the Apache Software *) +(* License version 2.0 *) +(* *) +(******************************************************************************) + +open Format + +module P = Shostak.Polynome + +module type S = sig + (* Raises Intervals.NotConsistent expl if it manages to prove that + the semi-algebraic set defined by polynomial inequalities in + [env] is empty. *) + val test_polynomes : (P.t * Intervals.t) list -> unit +end + +let test_polynomes_ref = ref (fun _ -> ()) +let set_test_polynomes myfun = test_polynomes_ref := myfun + +module Container : S = struct + let test_polynomes poly = !test_polynomes_ref poly +end + +let refresh () = + match Options.get_polynomial_plugin () with + | "" -> + if Options.get_debug_sdp () then + eprintf "[Dynlink] Using the default do-nothing module for polynomial \ + inequalities@." + | path -> + if Options.get_debug_sdp () then + eprintf "[Dynlink] Loading the 'polynomial inequalities' reasoner in \ + %s ...@." path; + try + MyDynlink.loadfile path; + if Options.get_debug_sdp () then eprintf "Success !@.@." + with + | MyDynlink.Error m1 -> + if Options.get_debug_sdp() then begin + eprintf + "[Dynlink] Loading the 'polynomial inequalities' reasoner in \ + \"%s\" failed!@." + path; + Format.eprintf ">> Failure message: %s@.@." + (MyDynlink.error_message m1); + end; + let prefixed_path = sprintf "%s/%s" Config.osdp_pluginsdir path in + if Options.get_debug_sdp () then + eprintf + "[Dynlink] Loading the 'polynomial inequalities' reasoner in \ + %s with prefix %s@." + path Config.osdp_pluginsdir; + try + MyDynlink.loadfile prefixed_path; + if Options.get_debug_sdp () then eprintf "Success !@.@." + with + | MyDynlink.Error m2 -> + if not (Options.get_debug_sdp()) then begin + eprintf + "[Dynlink] Loading the 'polynomial inequalities' reasoner in \ + \"%s\" failed!@." + path; + Format.eprintf ">> Failure message: %s@.@." + (MyDynlink.error_message m1); + end; + eprintf + "[Dynlink] Trying to load the plugin from \"%s\" failed too!@." + prefixed_path; + Format.eprintf ">> Failure message: %s@.@." + (MyDynlink.error_message m2); + exit 1 diff --git a/src/lib/reasoners/polynomialInequalities.mli b/src/lib/reasoners/polynomialInequalities.mli new file mode 100644 index 0000000000..30e23e20e6 --- /dev/null +++ b/src/lib/reasoners/polynomialInequalities.mli @@ -0,0 +1,43 @@ +(******************************************************************************) +(* *) +(* The Alt-Ergo theorem prover *) +(* Copyright (C) 2006-2013 *) +(* *) +(* Sylvain Conchon *) +(* Evelyne Contejean *) +(* *) +(* Francois Bobot *) +(* Mohamed Iguernelala *) +(* Stephane Lescuyer *) +(* Alain Mebsout *) +(* *) +(* CNRS - INRIA - Universite Paris Sud *) +(* *) +(* This file is distributed under the terms of the Apache Software *) +(* License version 2.0 *) +(* *) +(* ------------------------------------------------------------------------ *) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2013-2018 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of the Apache Software *) +(* License version 2.0 *) +(* *) +(******************************************************************************) + +module type S = sig + (* Raises Intervals.NotConsistent expl if it manages to prove that + the semi-algebraic set defined by the given polynomial inequalities + is empty. *) + val test_polynomes : (Shostak.Polynome.t * Intervals.t) list -> unit +end + +module Container : S + +(* reload dyn lib *) +val refresh : unit -> unit + +(* used by dyn lib to change the actual function in Container *) +val set_test_polynomes : + ((Shostak.Polynome.t * Intervals.t) list -> unit) -> unit diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index c51033843f..bfb789638d 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -163,7 +163,7 @@ struct | X5 _ -> X5.term_extract r | X6 _ -> X6.term_extract r | X7 _ -> X7.term_extract r - | Ac _ -> None, false (* SYLVAIN : TODO *) + | Ac r -> AC.term_extract r | Term t -> Some t, true let top () = term_embed Expr.vrai diff --git a/src/lib/util/numbersInterface.mli b/src/lib/util/numbersInterface.mli index ec219e9640..375e23601a 100644 --- a/src/lib/util/numbersInterface.mli +++ b/src/lib/util/numbersInterface.mli @@ -146,4 +146,6 @@ module type QSig = sig val div_2exp: t -> int -> t (** divides the first argument by 2^(the second argument) *) + val to_zarith : t -> Q.t + val of_zarith : Q.t -> t end diff --git a/src/lib/util/numsNumbers.ml b/src/lib/util/numsNumbers.ml index 2207bde0ec..fc3e00c701 100644 --- a/src/lib/util/numsNumbers.ml +++ b/src/lib/util/numsNumbers.ml @@ -241,5 +241,7 @@ module Q : NumbersInterface.QSig with module Z = Z = struct let div_2exp t n = div t (power (Int 2) n) + let to_zarith t = Q.of_string (Num.string_of_num t) + let of_zarith t = Num.num_of_string (Q.to_string t) (* TODO: test and fix *) end diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index 4504acec37..4dd6fab427 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -104,6 +104,7 @@ let debug_combine = ref false let debug_constr = ref false let debug_explanations = ref false let debug_fm = ref false +let debug_sdp = ref false let debug_fpa = ref 0 let debug_gc = ref false let debug_interpretation = ref false @@ -132,6 +133,7 @@ let set_debug_combine b = debug_combine := b let set_debug_constr b = debug_constr := b let set_debug_explanations b = debug_explanations := b let set_debug_fm b = debug_fm := b +let set_debug_sdp b = debug_sdp := b let set_debug_fpa i = debug_fpa := i let set_debug_gc b = debug_gc := b let set_debug_interpretation b = debug_interpretation := b @@ -160,6 +162,7 @@ let get_debug_combine () = !debug_combine let get_debug_constr () = !debug_constr let get_debug_explanations () = !debug_explanations let get_debug_fm () = !debug_fm +let get_debug_sdp () = !debug_sdp let get_debug_fpa () = !debug_fpa let get_debug_gc () = !debug_gc let get_debug_interpretation () = !debug_interpretation @@ -446,9 +449,11 @@ let get_term_like_pp () = !term_like_pp let disable_adts = ref false let inequalities_plugin = ref "" +let polynomial_plugin = ref "" let no_ac = ref false let no_contracongru = ref false let no_fm = ref false +let no_sdp = ref false let no_nla = ref false let no_tcp = ref false let no_theory = ref false @@ -458,9 +463,11 @@ let use_fpa = ref false let set_disable_adts b = disable_adts := b let set_inequalities_plugin b = inequalities_plugin := b +let set_polynomial_plugin b = polynomial_plugin := b let set_no_ac b = no_ac := b let set_no_contracongru b = no_contracongru := b let set_no_fm b = no_fm := b +let set_no_sdp b = no_sdp := b let set_no_nla b = no_nla := b let set_no_tcp b = no_tcp := b let set_no_theory b = no_theory := b @@ -470,9 +477,11 @@ let set_use_fpa b = use_fpa := b let get_disable_adts () = !disable_adts let get_inequalities_plugin () = !inequalities_plugin +let get_polynomial_plugin () = !polynomial_plugin let get_no_ac () = !no_ac let get_no_contracongru () = !no_contracongru let get_no_fm () = !no_fm +let get_no_sdp () = !no_sdp let get_no_nla () = !no_nla let get_no_tcp () = !no_tcp let get_no_theory () = !no_theory diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index 308dbaae60..e9085ee4ba 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -97,6 +97,9 @@ val set_debug_explanations : bool -> unit (** Set [debug_fm] accessible with {!val:get_debug_fm} *) val set_debug_fm : bool -> unit +(** Set [debug_sdp] accessible with {!val:get_debug_sdp} *) +val set_debug_sdp : bool -> unit + (** Set [debug_fpa] accessible with {!val:get_debug_fpa} *) val set_debug_fpa : int -> unit @@ -407,9 +410,15 @@ val set_disable_adts : bool -> unit (** Set [inequalities_plugin] accessible with {!val:get_inequalities_plugin} *) val set_inequalities_plugin : string -> unit +(** Set [polynomial_plugin] accessible with {!val:get_polynomial_plugin} *) +val set_polynomial_plugin : string -> unit + (** Set [no_fm] accessible with {!val:get_no_fm} *) val set_no_fm : bool -> unit +(** Set [no_sdp] accessible with {!val:get_no_sdp} *) +val set_no_sdp : bool -> unit + (** Set [no_tcp] accessible with {!val:get_no_tcp} *) val set_no_tcp : bool -> unit @@ -454,6 +463,9 @@ val get_debug_uf : unit -> bool (** Get the debugging flag of inequalities. *) val get_debug_fm : unit -> bool +(** Get the debugging flag of polynomial. *) +val get_debug_sdp : unit -> bool + (** Get the debugging value of floating-point. *) val get_debug_fpa : unit -> int (** Default to [0]. *) @@ -894,7 +906,11 @@ val get_disable_adts : unit -> bool (** Value specifying which module is used to handle inequalities of linear arithmetic. *) val get_inequalities_plugin : unit -> string -(** Default to [false] *) +(** Default to [""] *) + +(** Value specifying which module is used to handle polynomoial. *) +val get_polynomial_plugin : unit -> string +(** Default to [""] *) (** [true] if the AC (Associative and Commutative) theory is disabled for function symbols. *) @@ -909,6 +925,10 @@ val get_no_contracongru : unit -> bool val get_no_fm : unit -> bool (** Default to [false] *) +(** [true] if SDP algorithm is disabled. *) +val get_no_sdp : unit -> bool +(** Default to [false] *) + (** [true] if non-linear arithmetic reasoning (i.e. non-linear multplication, division and modulo on integers and rationals) is disabled. Non-linear multiplication remains AC. *) diff --git a/src/lib/util/timers.ml b/src/lib/util/timers.ml index cb4c1d4cd4..d2cbd39f13 100644 --- a/src/lib/util/timers.ml +++ b/src/lib/util/timers.ml @@ -67,6 +67,8 @@ type ty_function = | F_add_terms | F_are_equal | F_assume + | F_sdp + | F_osdp | F_class_of | F_leaves | F_make @@ -86,6 +88,8 @@ let ftag f = match f with | F_add -> 0 | F_add_lemma -> 1 | F_assume -> 2 + | F_sdp -> 20 + | F_osdp -> 21 | F_class_of -> 3 | F_leaves -> 4 | F_make -> 5 @@ -104,7 +108,7 @@ let ftag f = match f with | F_apply_subst -> 18 | F_instantiate -> 19 -let nb_ftag = 20 +let nb_ftag = 22 let string_of_ty_module k = match k with | M_None -> "None" @@ -126,6 +130,8 @@ let string_of_ty_function f = match f with | F_add -> "add" | F_add_lemma -> "add_lemma" | F_assume -> "assume" + | F_sdp -> "sdp" + | F_osdp -> "osdp" | F_class_of -> "class_of" | F_leaves -> "leaves" | F_make -> "make" @@ -263,6 +269,8 @@ let all_functions = F_add_terms; F_are_equal; F_assume; + F_sdp; + F_osdp; F_class_of; F_leaves; F_make; diff --git a/src/lib/util/timers.mli b/src/lib/util/timers.mli index 8f4ab7f940..28a6f2c7d8 100644 --- a/src/lib/util/timers.mli +++ b/src/lib/util/timers.mli @@ -49,6 +49,8 @@ type ty_function = | F_add_terms | F_are_equal | F_assume + | F_sdp + | F_osdp | F_class_of | F_leaves | F_make diff --git a/src/lib/util/zarithNumbers.ml b/src/lib/util/zarithNumbers.ml index f95e152e73..3c88b19808 100644 --- a/src/lib/util/zarithNumbers.ml +++ b/src/lib/util/zarithNumbers.ml @@ -169,4 +169,6 @@ module Q : NumbersInterface.QSig with module Z = Z = struct let div_2exp = Q.div_2exp + let to_zarith t = t + let of_zarith t = t end diff --git a/src/plugins/osdp/dune b/src/plugins/osdp/dune new file mode 100644 index 0000000000..9cb7f3b520 --- /dev/null +++ b/src/plugins/osdp/dune @@ -0,0 +1,22 @@ +(executable + (name OsdpIneqs) + (public_name alt-ergo-osdp) + (package alt-ergo-osdp) + (modes native plugin) ; produce a cmxs + ; no modules declaration since we have a single module + (libraries alt-ergo-lib osdp) + (embed_in_plugin_libraries osdp) ; link statically osdp +) + +(documentation + (package alt-ergo-osdp) + (mld_files :standard) +) + +(install + (package alt-ergo-osdp) + (section share) + (files + (OsdpIneqs.cmxs as plugins/osdp-plugin.cmxs) + ) +) diff --git a/src/plugins/osdp/index_sdp.mld b/src/plugins/osdp/index_sdp.mld new file mode 100644 index 0000000000..143b838c51 --- /dev/null +++ b/src/plugins/osdp/index_sdp.mld @@ -0,0 +1,2 @@ +{1 SDP/SOS plugin} + diff --git a/src/plugins/osdp/osdpIneqs.ml b/src/plugins/osdp/osdpIneqs.ml new file mode 100644 index 0000000000..5d685c09d3 --- /dev/null +++ b/src/plugins/osdp/osdpIneqs.ml @@ -0,0 +1,327 @@ +(* + * OSDP (OCaml SDP) plugin for Alt-Ergo + * Copyright (C) 2018, ONERA + * + * This program is free software; you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published by + * the Free Software Foundation; either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with this program; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA + *) +open AltErgoLib + +module PolyIneqs : PolynomialInequalities.S = struct + module P = Shostak.Polynome + module X = Shostak.Combine + + module Q = Numbers.Q + + module I = Intervals + + module MX0 = Map.Make(struct type t = X.r let compare = X.hash_cmp end) + + module Sos = Osdp.Sos.Q + module SosP = Sos.Poly + + module SSosP = Set.Make (SosP) + module SSSosP = Set.Make (SSosP) + + module MSSosP = Map.Make + (struct type t = SSosP.t let compare = SSosP.compare end) + + let cache_polynomes = ref MSSosP.empty + + let cache_entry_of pge = + let pge = List.map fst pge in + let set_of polys = List.fold_right SSosP.add polys SSosP.empty in + set_of pge + let find_res_in_cache ce = MSSosP.find ce !cache_polynomes + let add_res_to_cache ce res = + cache_polynomes := MSSosP.add ce res !cache_polynomes + + let p_to_osdp p = + let combine_opt_env f ft2 opt1 t2 = match opt1 with + | None -> None + | Some (t1, env, next) -> + match ft2 t2 env next with + | None -> None + | Some (t2, env, next) -> Some (f t1 t2, env, next) in + let rec trans_monom t env next = match Expr.term_view t with + | Expr.Term { Expr.f = Symbols.Op Symbols.Mult ; xs = l ; _ } -> + List.fold_left + (combine_opt_env SosP.mult trans_monom) + (Some (SosP.one, env, next)) l + | _ -> + let v, env, next = + try Expr.Map.find t env, env, next + with Not_found -> next, Expr.Map.add t next env, next + 1 in + Some (SosP.var v, env, next) in + let trans_monom m env next = + match X.term_extract m with + | None, _ -> None + | Some t, _ -> trans_monom t env next in + let opt = + let pm, pc = P.to_list p in + List.fold_left + (fun opt (c, m) -> + combine_opt_env + (fun t1 t2 -> SosP.(add t1 (mult_scalar (Q.to_zarith c) t2))) + trans_monom opt m) + (Some (SosP.const (Q.to_zarith pc), Expr.Map.empty, 0)) pm in + match opt with + | None -> None + | Some (p, env, _) -> Some (p, env) + + let tr_polys polys = + try + List.map + (fun (p, i) -> + match p_to_osdp p with + | None -> raise Exit + | Some (p, env) -> (p, i), env) + polys + with Exit -> [] + + (* For a list [polys] of pairs [pi, env] with [env] a mapping from + terms, [partition polys] returns a list of lists [l] such that + [pi, env] in differents lists [l] have [env] with empty + intersection. *) + let partition polys = + let uf = + List.fold_left + (fun uf (_, env) -> + match Expr.Map.bindings env with + | [] -> uf + | (t, _) :: env -> + let uf, _ = Uf.add uf t in + let r, _ = Uf.find uf t in + List.fold_left + (fun uf (t', _) -> + let uf, _ = Uf.add uf t' in + let r', _ = Uf.find uf t' in + fst (Uf.union uf r r' Explanation.empty)) + uf env) + (Uf.empty ()) polys in + List.fold_left + (fun m (pi, env) -> + try + let t, _ = Expr.Map.choose env in + let r, _ = Uf.find uf t in + let l = try MX0.find r m with Not_found -> [] in + MX0.add r ((pi, env) :: l) m + with Not_found -> m) + MX0.empty polys + |> MX0.bindings |> List.map snd + + (* For a list [polys] of pairs [(p, i), env] with [p] a polynomial + and [env] a mapping from terms to variable indices in [p], + [merge polys] returns a list of polynomials using the same + variable indices for the same symbols. *) + let merge polys = + (* For [env] and [env'] mappings from terms to integer indices, + [merge_env env env'] returns a pair [env'', trans]. [env''] + contains the same mapping as [env] plus mapping for extra + variables in [env'] to new indices (not appearing in + [env]). [trans] is an array of integer indices such that + [trans.(i) = j] for each variable mapped to [i] in [env'] and + to [j] in [env'']. *) + let merge_env env env' = + let next, trans = + let sz e = 1 + Expr.Map.fold (fun _ -> max) e (-1) in + sz env, Array.make (sz env') 0 in + let env'', _ = + Expr.Map.fold + (fun v i (env, next) -> + let j, env, next = + try Expr.Map.find v env, env, next + with Not_found -> next, Expr.Map.add v next env, next + 1 in + trans.(i) <- j; + env, next) + env' (env, next) in + env'', trans in + let apply_trans p trans = + let trans = Array.to_list trans |> List.map SosP.var in + SosP.compose p trans in + let polys, _ = + List.fold_left + (fun (polys, env) ((p, i), env') -> + let env, trans = merge_env env env' in + (apply_trans p trans, i) :: polys, env) + ([], Expr.Map.empty) polys in + List.rev polys + + (* For a list of polynomials and intervals [p_i, i_i], returns a + list [lpge0] of pairs [lpge0_i, e_i] such that \forall i, p_i + \in i_i implies \forall j, lpge0_j >= 0. [e_i] are explanations + for lpge0_i >= 0 *) + let pi_to_pge0 pil = + let pil = List.filter (fun (_, i) -> I.is_point i = None) pil in + let d = List.fold_left (fun d (p, _) -> max d (SosP.degree p)) 0 pil in + let lpe = + List.map + (fun (p, i) -> + let l = + try let v, ex, _ = I.borne_inf i in Some (Q.to_zarith v, ex) + with I.No_finite_bound -> None in + let u = + try let v, ex, _ = I.borne_sup i in Some (Q.to_zarith v, ex) + with I.No_finite_bound -> None in + (* normalize polynomials so that all coeffs are less than 1 *) + let c = + SosP.to_list p + |> List.map (fun (_, n) -> Q.of_zarith n |> Q.abs) + |> List.fold_left Q.max Q.zero |> Q.to_zarith in + match l, u with + | None, None -> [] + | None, Some (u, e) -> SosP.([(!u - p) / c, e]) + | Some (l, e), None -> SosP.([(p - !l) / c, e]) + | Some (l, el), Some (u, eu) -> + let pl, pu = SosP.((p - !l) / c, (!u - p) / c) in + if SosP.degree p > d / 2 then [(pl, el); (pu, eu)] + else [SosP.(pl * pu), Explanation.union el eu]) + pil in + List.flatten lpe + + (* For a list of polynomials [pge0_i], returns true iff it manages + to prove that the semi-algebraic set { x \in \R^n | \forall i + pge0_i >= 0 } is empty. *) + let psatz pge0 = + let pge0, expls = List.split pge0 in + let has_null_const p = + let zeros = + SosP.(Array.to_list (Array.make (nb_vars p) Coeff.zero)) in + SosP.(Coeff.compare (eval p zeros) Coeff.zero = 0) in + (* if none of pge0 has a constant, 0 satisfies the constraints *) + if List.for_all has_null_const pge0 then None else + try + let get_wits keep = + let sum, sigmas = + let n = List.map SosP.nb_vars pge0 |> List.fold_left max 0 in + let degs = List.map SosP.degree pge0 in + let max_deg = List.fold_left max 0 degs in + let rec prod i j = if i > j then 1 else i * prod (i + 1) j in + let among k n = + if k > n / 2 then prod (k + 1) n / prod 1 (n - k) + else prod (n - k + 1) n / prod 1 k in + (* Format.printf *) + (* "n = %d, max_deg = %d, (n parmi n + (d+1)/2) = %d@." *) + (* n max_deg (among n (n + (max_deg + 1) / 2)); *) + if among n (n + (max_deg + 1) / 2) > 64 then raise Exit; + let max_deg_list = + pge0 |> List.map SosP.degree_list + |> List.map Osdp.Monomial.of_list + |> Osdp.Monomial.(List.fold_left lcm one) in + let rup n = (n + 1) / 2 * 2 in + let rup_monomial m = + Osdp.Monomial.(m |> to_list |> List.map rup |> of_list) in + List.fold_left + (fun (sum, sigmas) (p, d) -> + let s = + let l = + let d = max_deg - d in + let d = if keep then d else rup d in + Sos.make ~n ~d "s" |> Sos.to_list in + let l = + if keep then l else + let lim = + let pl = + Osdp.Monomial.of_list (SosP.degree_list p) in + rup_monomial (Osdp.Monomial.div max_deg_list pl) in + List.filter + (fun (m, _) -> Osdp.Monomial.divide m lim) + l in + Sos.of_list l in + (* Format.printf *) + (* "p = %a ~~> s = %a@." Sos.Poly.pp p Sos.pp s; *) + Sos.(sum - s * !!p), s :: sigmas) + (Sos.(!!Poly.zero), []) (List.combine pge0 degs) in + (* Format.printf "sum: %a@." Sos.pp sum; *) + (* Format.printf "degrees: @[%a@]@." (Osdp.Utils.pp_list ~sep:",@ " + (fun fmt p -> Format.fprrintf \ + fmt "%d" (Sos.degree p))) sigmas; *) + let ret, _, _, witnesses = + let options = + { Sos.default + with Sos.verbose = 0(*3*) ; + Sos.sdp = + { Osdp.Sdp.default + with Osdp.Sdp.verbose = 0(*1*) } } in + Sos.solve ~options ~solver:Osdp.Sdp.Csdp + Sos.Purefeas (sum :: sigmas) in + match ret, witnesses with + | Osdp.SdpRet.Success, (m, _) :: _ + when + (* check that we proved sum > 0 (and not just sum >= 0) *) + Array.length m > 0 && Osdp.Monomial.(compare m.(0) one) = 0 -> + Some Explanation.(List.fold_left union empty expls) + | _ -> None in + match get_wits false with + | Some e -> Some e + | None -> get_wits true + with Exit -> None + + let psatz pge0 = + if Options.get_timers() then + try + Timers.exec_timer_start Timers.M_Arith Timers.F_osdp; + let res = psatz pge0 in + Timers.exec_timer_pause Timers.M_Arith Timers.F_osdp; + res + with e -> + Timers.exec_timer_pause Timers.M_Arith Timers.F_osdp; + raise e + else psatz pge0 + + let test_polynomes polys = + let polys = tr_polys polys in + let polys = partition polys in + if Options.get_debug_sdp () then + Printer.print_dbg "[sdp] %d partition(s)@." (List.length polys); + polys + |> List.iter + (fun polys -> + (* we don't do anything when everything is linear *) + if List.exists (fun ((p, _), _) -> SosP.degree p > 1) polys then + let polys = merge polys in + let pge0 = pi_to_pge0 polys in + let ce = cache_entry_of pge0 in + let res = + try + let tmp = find_res_in_cache ce in + if Options.get_debug_sdp () then + Printer.print_dbg "[sdp] reuse result in cache@."; + tmp + with Not_found -> + if Options.get_debug_sdp () then begin + Printer.print_dbg "[sdp] new problem@."; + Printer.print_dbg + "[sdp] @[%a@]@." + (Osdp.Utils.pp_list + ~sep: ",@ " + (fun fmt (p, _) -> + Format.fprintf fmt "%a >= 0" SosP.pp p)) + pge0; + end; + let tmp = psatz pge0 in + add_res_to_cache ce tmp; + tmp + in + match res with + | None -> () + | Some expls -> + if Options.get_debug_sdp () then + Printer.print_dbg "[sdp] Inconsistent@."; + raise (I.NotConsistent expls) + ) +end + +let () = + PolynomialInequalities.set_test_polynomes PolyIneqs.test_polynomes diff --git a/src/plugins/osdp/osdpIneqs.mli b/src/plugins/osdp/osdpIneqs.mli new file mode 100644 index 0000000000..114e452165 --- /dev/null +++ b/src/plugins/osdp/osdpIneqs.mli @@ -0,0 +1,20 @@ +(* + * OSDP (OCaml SDP) plugin for Alt-Ergo + * Copyright (C) 2018, ONERA + * + * This program is free software; you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published by + * the Free Software Foundation; either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with this program; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA + *) + +(* empty interface file *)