Add new plugin for polynomial inequalities (using OSDP)

.github/workflows/build_docker.yml

@@ -36,6 +36,8 @@ jobs:
 
       # Create a switch with the system compiler (no compilation needed).
       # And then, install external (no need for depext with opam 2.1) and libs deps.
+      # Don't install alt-ergo-osdp since depext not available
+      - run: mv alt-ergo-osdp.opam alt-ergo-osdp.noinstall
       - run: opam switch create . ocaml-system --deps-only
 
       # Install the project packages

.github/workflows/build_js.yml

@@ -56,7 +56,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

@@ -48,8 +48,9 @@ jobs:
 
       # Pin the packages, this is needed for opam depext
       # remove this step when opam 2.1 will be used
+      # Don't install alt-ergo-osdp since depext not available on MacOS
       - name: Pin no action
-        run: opam pin add . --no-action
+        run: mv alt-ergo-osdp.opam alt-ergo-osdp.noinstall && opam pin add . --no-action
 
       # Install external dependencies
       # remove this step when opam 2.1 will be used
@@ -63,11 +64,12 @@ jobs:
 
       # Build and install with opam
       - name: Install
-        run: opam reinstall .
+        run: opam install  ./*.opam
 
       # Run non regression tests
+      # don't run the OSDP tests since we don't have it
       - name: Run non regression tests
-        run: opam exec -- rsc/extra/non_regression.sh
+        run: rm -rf non-regression/valid/osdp && opam exec -- rsc/extra/non_regression.sh
 
       # Get and Set version of the installed alt-ergo binary
       # Get and Set the path where alt-ergo binary is located

.github/workflows/build_make.yml

@@ -54,12 +54,15 @@ 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
         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

.github/workflows/build_ubuntu.yml

@@ -61,7 +61,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

@@ -64,7 +64,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.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"

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

@@ -161,7 +161,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)
@@ -114,3 +113,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.0-or-later")
+
+ (depends
+  (ocaml (>= 4.05.0))
+  (dune (>= 2.9))
+  dune-configurator
+  alt-ergo
+  (alt-ergo-lib (= :version))
+  alt-ergo
+  (osdp (>= 1.1.0))
+ )
+)

examples/valid/poly_v10_d1_s121_2.ae

@@ -0,0 +1,3 @@
+goal g:
+  forall x0, x1, x2, x3, x4, x5, x6, x7, x8, x9:real.
+    4.66599589671989*x0 * x0 + 5.44030782356989*x0*x1 + 4.86253647018718*x0*x2 + 5.78216238523859*x0*x3 + 5.51925877424655*x0*x4 + 6.60534392790455*x0*x5 + 3.75227069449988*x0*x6 + 5.70370161441604*x0*x7 + 7.69339787773855*x0*x8 + 7.12222231250226*x0*x9 + 6.68558506060876*x0 + 2.53648277537877*x1 * x1 + 3.28352733582592*x1*x2 + 3.85450290502748*x1*x3 + 4.48951551408735*x1*x4 + 4.26791605229313*x1*x5 + 2.27143280170943*x1*x6 + 3.82235211808492*x1*x7 + 4.78813235074348*x1*x8 + 4.88042925417463*x1*x9 + 3.77504572888355*x1 + 1.78354087266182*x2 * x2 + 3.77689378813167*x2*x3 + 4.00806258405655*x2*x4 + 3.45749896727473*x2*x5 + 1.82706457527954*x2*x6 + 2.91350805428827*x2*x7 + 3.89007652776802*x2*x8 + 3.82791983574596*x2*x9 + 3.23017374573781*x2 + 2.91287718862589*x3 * x3 + 4.80655583675996*x3*x4 + 3.8093661953241*x3*x5 + 2.25263131648088*x3*x6 + 2.97220460172864*x3*x7 + 5.91166978288215*x3*x8 + 4.77758315442805*x3*x9 + 3.5823149304611*x3 + 2.9228150679484*x4 * x4 + 4.01245022289054*x4*x5 + 1.71896073812602*x4*x6 + 3.5049159095768*x4*x7 + 4.5770407110903*x4*x8 + 5.16893279801215*x4*x9 + 4.37530648538669*x4 + 2.6946703738345*x5 * x5 + 2.51388816704055*x5*x6 + 4.41650120194594*x5*x7 + 5.19475489721844*x5*x8 + 5.28737231945276*x5*x9 + 4.56881600192816*x5 + 1.02837791930916*x6 * x6 + 2.11160213607309*x6*x7 + 3.75585643668981*x6*x8 + 2.57090661226126*x6*x9 + 2.19061543714949*x6 + 2.23078471405026*x7 * x7 + 4.47701159683909*x7*x8 + 4.96412957059534*x7*x9 + 4.36849060887653*x7 + 4.20242678972929*x8 * x8 + 5.98225131904998*x8*x9 + 4.72611589454344*x8 + 3.21204838235355*x9 * x9 + 5.3694230537461*x9 + 2.99979973557218 >= 0.

examples/valid/poly_v11_d1_s144.ae

@@ -0,0 +1,3 @@
+goal g:
+  forall x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10:real.
+    4.24377189200859*x0 * x0 + 7.07822432021484*x0*x1 + 6.70810502354405*x0*x10 + 3.77443060690717*x0*x2 + 5.77234362509289*x0*x3 + 4.57279406684069*x0*x4 + 5.69503470484061*x0*x5 + 7.2678051050147*x0*x6 + 4.06456494962836*x0*x7 + 5.48182611132358*x0*x8 + 6.71190211313931*x0*x9 + 4.33615675677875*x0 + 3.30669935703648*x1 * x1 + 6.08221667574597*x1*x10 + 3.45689024031082*x1*x2 + 4.92169693013621*x1*x3 + 4.55430930304004*x1*x4 + 5.17262286476038*x1*x5 + 5.85860721937296*x1*x6 + 2.91558197318275*x1*x7 + 4.59479244996331*x1*x8 + 6.32747345083722*x1*x9 + 4.15800457136264*x1 + 3.52542526185143*x10 * x10 + 2.94280830346092*x10*x2 + 5.82229167438256*x10*x3 + 4.12853351423838*x10*x4 + 4.64318949749067*x10*x5 + 5.73823007907904*x10*x6 + 3.98182931181197*x10*x7 + 4.36357902816048*x10*x8 + 6.27898599261738*x10*x9 + 4.02580887420205*x10 + 1.06114660967939*x2 * x2 + 2.6085723200662*x2*x3 + 2.21217888989074*x2*x4 + 2.7829021128658*x2*x5 + 3.41119240573835*x2*x6 + 1.65753910890614*x2*x7 + 2.24209831677702*x2*x8 + 3.01355266749208*x2*x9 + 2.32575155454443*x2 + 3.21539325909752*x3 * x3 + 3.29521472090781*x3*x4 + 4.09902918013888*x3*x5 + 5.62825838551548*x3*x6 + 4.05229911146811*x3*x7 + 3.92988492639456*x3*x8 + 5.73387308792003*x3*x9 + 3.76552759277205*x3 + 2.59965757616045*x4 * x4 + 3.97900860948233*x4*x5 + 4.3644366652006*x4*x6 + 1.76480643887881*x4*x7 + 3.55682080927437*x4*x8 + 5.86258301279279*x4*x9 + 3.04224412645116*x4 + 2.55786806835177*x5 * x5 + 5.66380495156692*x5*x6 + 2.958922834759*x5*x7 + 4.13254853625108*x5*x8 + 5.63389851495912*x5*x9 + 4.11864999950547*x5 + 4.06958879372296*x6 * x6 + 4.6855965507652*x6*x7 + 5.31410867488205*x6*x8 + 6.4202575833643*x6*x9 + 5.10836629417853*x6 + 1.94495829270157*x7 * x7 + 2.75443759264689*x7*x8 + 3.24593399270224*x7*x9 + 2.44803598812575*x7 + 2.12087702490646*x8 * x8 + 5.21758656350205*x8*x9 + 3.51552050395994*x8 + 3.98992001067828*x9 * x9 + 4.94409460725083*x9 + 2.48249314671914 >= 0.

examples/valid/poly_v12_d1_s169.ae

@@ -0,0 +1,3 @@
+goal g:
+  forall x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11:real.
+    3.78789117344196*x0 * x0 + 5.50636575663713*x0*x1 + 5.76800227547484*x0*x10 + 8.50079042638222*x0*x11 + 4.95226881585845*x0*x2 + 6.348310388855*x0*x3 + 5.77998496019916*x0*x4 + 4.79117972700113*x0*x5 + 4.77626614851139*x0*x6 + 7.02555238033268*x0*x7 + 6.69902620876129*x0*x8 + 4.15188073973749*x0*x9 + 2.43369799442552*x0 + 3.3792119361662*x1 * x1 + 6.03577146781658*x1*x10 + 7.74019587723462*x1*x11 + 3.98407508263698*x1*x2 + 5.76848804114997*x1*x3 + 4.40235546837408*x1*x4 + 5.26466332946827*x1*x5 + 4.47083591263493*x1*x6 + 5.26140181509637*x1*x7 + 5.80399591062533*x1*x8 + 4.24450987295115*x1*x9 + 2.72446373587487*x1 + 4.33475710102188*x10 * x10 + 8.29891975683631*x10*x11 + 5.88030267983263*x10*x2 + 7.28787477489123*x10*x3 + 4.42287493480225*x10*x4 + 6.67367792630676*x10*x5 + 4.47867692615852*x10*x6 + 6.42228068625723*x10*x7 + 6.86415015466853*x10*x8 + 4.29265589333101*x10*x9 + 2.67156767185587*x10 + 6.37836550832093*x11 * x11 + 7.65669814471314*x11*x2 + 9.00362278171107*x11*x3 + 7.4088826516463*x11*x4 + 8.34865018673983*x11*x5 + 6.70731087851813*x11*x6 + 8.86849006302579*x11*x7 + 8.87716144810621*x11*x8 + 6.61012035897661*x11*x9 + 4.78429890238261*x11 + 3.66613286853186*x2 * x2 + 6.03843732377242*x2*x3 + 4.70949045713566*x2*x4 + 5.62489452190249*x2*x5 + 5.2228296086109*x2*x6 + 5.75895673086989*x2*x7 + 5.76756402568235*x2*x8 + 4.12721377487065*x2*x9 + 2.91443032413838*x2 + 4.57430803715456*x3 * x3 + 5.4391637457494*x3*x4 + 6.34905130182843*x3*x5 + 4.97504116913045*x3*x6 + 6.72432580145434*x3*x7 + 7.05480521047214*x3*x8 + 4.41137286826602*x3*x9 + 3.08583578243987*x3 + 2.62089318584753*x4 * x4 + 4.22567196463169*x4*x5 + 3.68020890856631*x4*x6 + 5.40288097911125*x4*x7 + 5.23454259297348*x4*x8 + 3.98630276459232*x4*x9 + 2.72881975190473*x4 + 3.51152695371882*x5 * x5 + 4.56073731445259*x5*x6 + 5.4108674011187*x5*x7 + 5.5526372646395*x5*x8 + 4.94290213654144*x5*x9 + 3.42794452015534*x5 + 2.93414905791984*x6 * x6 + 4.98420247417378*x6*x7 + 5.2994445019168*x6*x8 + 3.15626101538272*x6*x9 + 2.32606790730931*x6 + 4.21432764387877*x7 * x7 + 7.73679579846689*x7*x8 + 4.18800173265495*x7*x9 + 2.60776374695464*x7 + 4.23946816258*x8 * x8 + 4.50281407686828*x8*x9 + 3.0206408451216*x8 + 2.26117946929622*x9 * x9 + 2.94757853346605*x9 + 1.26526532456826 >= 0.

examples/valid/poly_v13_d1_s196.ae

@@ -0,0 +1,3 @@
+goal g:
+  forall x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12:real.
+    2.83102888299718*x0 * x0 + 6.42572751371778*x0*x1 + 8.25129911435135*x0*x10 + 5.69559635923303*x0*x11 + 5.92481178553981*x0*x12 + 6.40801707188141*x0*x2 + 4.45554945694266*x0*x3 + 4.22400532761251*x0*x4 + 4.8274232196426*x0*x5 + 3.48028805745454*x0*x6 + 5.78748914362644*x0*x7 + 5.21064397488342*x0*x8 + 5.0793315545896*x0*x9 + 5.1862877193636*x0 + 5.41352138522961*x1 * x1 + 11.3548655923759*x1*x10 + 7.83838360683478*x1*x11 + 8.22294739107078*x1*x12 + 9.45331015083392*x1*x2 + 8.23532738555902*x1*x3 + 7.44396710394009*x1*x4 + 7.03463115038658*x1*x5 + 5.72702589443565*x1*x6 + 8.97553124713695*x1*x7 + 7.30547593063181*x1*x8 + 7.11289034545645*x1*x9 + 7.13147868676461*x1 + 7.39053287368915*x10 * x10 + 9.8585370992914*x10*x11 + 9.30487038802938*x10*x12 + 10.7435557582942*x10*x2 + 9.36717836185677*x10*x3 + 8.39506492631014*x10*x4 + 9.44251568584143*x10*x5 + 7.56959591716191*x10*x6 + 10.5979696294947*x10*x7 + 9.77365395020882*x10*x8 + 9.75860570439304*x10*x9 + 8.87466106589898*x10 + 4.0113960765002*x11 * x11 + 6.60778478207752*x11*x12 + 7.55727192983668*x11*x2 + 5.60263086589518*x11*x3 + 5.81408722893603*x11*x4 + 6.05413766453025*x11*x5 + 5.7651429012274*x11*x6 + 7.33213022036221*x11*x7 + 6.2820263310694*x11*x8 + 6.49351841578276*x11*x9 + 6.40341481795197*x11 + 4.77950866429708*x12 * x12 + 7.17468768766861*x12*x2 + 6.01397420396598*x12*x3 + 4.69150807901878*x12*x4 + 6.24332181268*x12*x5 + 4.71947753366447*x12*x6 + 7.94121292178011*x12*x7 + 7.83388596172375*x12*x8 + 6.80460442955207*x12*x9 + 6.71302785117923*x12 + 4.84230860940341*x2 * x2 + 6.96211651017846*x2*x3 + 6.92247290682851*x2*x4 + 7.11932314305198*x2*x5 + 5.47875816829853*x2*x6 + 7.35666395735198*x2*x7 + 6.53863009741832*x2*x8 + 6.76101366463307*x2*x9 + 7.43623396686927*x2 + 4.07662006409758*x3 * x3 + 6.19479771336636*x3*x4 + 6.22057491918846*x3*x5 + 4.99808762145413*x3*x6 + 7.38466307073201*x3*x7 + 6.33250779142934*x3*x8 + 6.41941541320814*x3*x9 + 5.03782318336003*x3 + 3.54575861333983*x4 * x4 + 5.75643766633469*x4*x5 + 4.85141067205359*x4*x6 + 6.78109619222705*x4*x7 + 5.48500226186499*x4*x8 + 5.8725725602546*x4*x9 + 5.01918918494266*x4 + 3.77949334818819*x5 * x5 + 5.47271314695513*x5*x6 + 6.30109416667329*x5*x7 + 7.08206999789588*x5*x8 + 6.84213475530338*x5*x9 + 6.6487557402538*x5 + 3.44789342086681*x6 * x6 + 6.42214457970531*x6*x7 + 5.56545097458968*x6*x8 + 5.48430793839471*x6*x9 + 5.59505198744665*x6 + 5.08067621964833*x7 * x7 + 7.9675258570982*x7*x8 + 7.20535509063727*x7*x9 + 6.65592796406722*x7 + 4.36663874534883*x8 * x8 + 7.74186369044291*x8*x9 + 6.55457010998327*x8 + 3.91290587481992*x9 * x9 + 5.63806506952456*x9 + 3.85442937686288 >= 0.