Add regression tests for the OSDP plugin

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

@@ -48,13 +48,14 @@ 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
       #- name: opam install depext
-      #  run: opam depext alt-ergo-lib alt-ergo-parsers alt-ergo altgr-ergo alt-ergo-osdp
+      #  run: opam depext alt-ergo-lib alt-ergo-parsers alt-ergo altgr-ergo
 
       # Install dependencies
       - name: Install deps
@@ -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

non-regression/run_valid.sh

@@ -13,7 +13,8 @@ do
     for f in $files
     do
         cpt=`expr $cpt + 1`
-        res=`$alt_ergo_bin -o native --timelimit $timelimit $options --sat-solver CDCL-Tableaux $f`
+        opt=`(echo $f | grep -q 'valid/osdp/') && echo "--polynomial-plugin=osdp-plugin.cmxs"`
+        res=`$alt_ergo_bin -o native --timelimit $timelimit $options $opt --sat-solver CDCL-Tableaux $f`
         if [ "`echo $res | grep -c "Valid"`" -eq "0" ]
         then
             echo "[run_valid > default cdcl solver with tableaux] issue with file $f"
@@ -29,7 +30,8 @@ cpt=0
 for f in $files
 do
     cpt=`expr $cpt + 1`
-    res=`$alt_ergo_bin -o native --timelimit $timelimit --sat-solver Tableaux $f`
+    opt=`(echo $f | grep -q 'valid/osdp/') && echo "--polynomial-plugin=osdp-plugin.cmxs"`
+    res=`$alt_ergo_bin -o native --timelimit $timelimit $opt --sat-solver Tableaux $f`
     if [ "`echo $res | grep -c "Valid"`" -eq "0" ]
     then
         echo "[run_valid > tableaux solver] issue with file $f"
@@ -44,7 +46,8 @@ cpt=0
 for f in $files
 do
     cpt=`expr $cpt + 1`
-    res=`$alt_ergo_bin -o native --timelimit $timelimit --sat-solver Tableaux-CDCL $f`
+    opt=`(echo $f | grep -q 'valid/osdp/') && echo "--polynomial-plugin=osdp-plugin.cmxs"`
+    res=`$alt_ergo_bin -o native --timelimit $timelimit $opt --sat-solver Tableaux-CDCL $f`
     if [ "`echo $res | grep -c "Valid"`" -eq "0" ]
     then
         echo "[run_valid > tableaux solver with cdcl] issue with file $f"
@@ -61,7 +64,8 @@ do
     for f in $files
     do
         cpt=`expr $cpt + 1`
-        res=`$alt_ergo_bin -o native --timelimit $timelimit $options --sat-solver CDCL $f`
+        opt=`(echo $f | grep -q 'valid/osdp/') && echo "--polynomial-plugin=osdp-plugin.cmxs"`
+        res=`$alt_ergo_bin -o native --timelimit $timelimit $options $opt --sat-solver CDCL $f`
         if [ "`echo $res | grep -c "Valid"`" -eq "0" ]
         then
             echo "[run_valid > cdcl solver] issue with file $f"
@@ -77,7 +81,8 @@ done
 # for f in $files
 # do
 #     cpt=`expr $cpt + 1`
-#     res=`$alt_ergo_bin -o native -timelimit $timelimit -inequalities-plugin fm-simplex-plugin.cmxs $f`
+#     opt=`(echo $f | grep -q 'valid/osdp/') && echo "--polynomial-plugin=osdp-plugin.cmxs"`
+#     res=`$alt_ergo_bin -o native -timelimit $timelimit $opt -inequalities-plugin fm-simplex-plugin.cmxs $f`
 #     if [ "`echo $res | grep -c ":Valid"`" -eq "0" ]
 #     then
 #         echo "[run_valid > fm-simplex-plugin test] issue with file $f"
@@ -93,7 +98,8 @@ done
 # for f in $files
 # do
 #     cpt=`expr $cpt + 1`
-#     res=`$alt_ergo_bin -o native -timelimit $timelimit -sat-plugin satML-plugin.cmxs -inequalities-plugin fm-simplex-plugin.cmxs $f`
+#     opt=`(echo $f | grep -q 'valid/osdp/') && echo "--polynomial-plugin=osdp-plugin.cmxs"`
+#     res=`$alt_ergo_bin -o native -timelimit $timelimit $opt -sat-plugin satML-plugin.cmxs -inequalities-plugin fm-simplex-plugin.cmxs $f`
 #     if [ "`echo $res | grep -c ":Valid"`" -eq "0" ]
 #     then
 #         echo "[run_valid > satML-plugin+fm-simplex-plugin test] issue with file $f"

non-regression/valid/osdp/3_variable_reaction_diffusion_lb.ae

@@ -0,0 +1,12 @@
+logic x1 : real
+logic x2 : real
+logic x3 : real
+axiom ax0: (- (5.0)) <= x1
+axiom ax1: x1 <= 5.0
+axiom ax2: (- (5.0)) <= x2
+axiom ax3: x2 <= 5.0
+axiom ax4: (- (5.0)) <= x3
+axiom ax5: x3 <= 5.0
+goal g:
+  (- (36.7127))
+  < (- (x1)) + 2.0 * x2 + (- (x3)) + (- (0.835634534 * x2 * (1.0 + x2)))

non-regression/valid/osdp/3_variable_reaction_diffusion_ub.ae

@@ -0,0 +1,12 @@
+logic x1 : real
+logic x2 : real
+logic x3 : real
+axiom ax0: (- (5.0)) <= x1
+axiom ax1: x1 <= 5.0
+axiom ax2: (- (5.0)) <= x2
+axiom ax3: x2 <= 5.0
+axiom ax4: (- (5.0)) <= x3
+axiom ax5: x3 <= 5.0
+goal g:
+  (- (x1)) + 2.0 * x2 + (- (x3)) + (- (0.835634534 * x2 * (1.0 + x2)))
+  < 10.4388

non-regression/valid/osdp/7_variable_magnetism_lb.ae

@@ -0,0 +1,25 @@
+logic x1 : real
+logic x2 : real
+logic x3 : real
+logic x4 : real
+logic x5 : real
+logic x6 : real
+logic x7 : real
+axiom ax0: (- (1.0)) <= x1
+axiom ax1: x1 <= 1.0
+axiom ax2: (- (1.0)) <= x2
+axiom ax3: x2 <= 1.0
+axiom ax4: (- (1.0)) <= x3
+axiom ax5: x3 <= 1.0
+axiom ax6: (- (1.0)) <= x4
+axiom ax7: x4 <= 1.0
+axiom ax8: (- (1.0)) <= x5
+axiom ax9: x5 <= 1.0
+axiom ax10: (- (1.0)) <= x6
+axiom ax11: x6 <= 1.0
+axiom ax12: (- (1.0)) <= x7
+axiom ax13: x7 <= 1.0
+goal g:
+  (- (0.2501))
+  < x1 * x1 + 2.0 * x2 * x2 + 2.0 * x3 * x3 + 2.0 * x4 * x4 + 2.0 * x5 * x5
+    + 2.0 * x6 * x6 + 2.0 * x7 * x7 + (- (x1))

non-regression/valid/osdp/7_variable_magnetism_ub.ae

@@ -0,0 +1,24 @@
+logic x1 : real
+logic x2 : real
+logic x3 : real
+logic x4 : real
+logic x5 : real
+logic x6 : real
+logic x7 : real
+axiom ax0: (- (1.0)) <= x1
+axiom ax1: x1 <= 1.0
+axiom ax2: (- (1.0)) <= x2
+axiom ax3: x2 <= 1.0
+axiom ax4: (- (1.0)) <= x3
+axiom ax5: x3 <= 1.0
+axiom ax6: (- (1.0)) <= x4
+axiom ax7: x4 <= 1.0
+axiom ax8: (- (1.0)) <= x5
+axiom ax9: x5 <= 1.0
+axiom ax10: (- (1.0)) <= x6
+axiom ax11: x6 <= 1.0
+axiom ax12: (- (1.0)) <= x7
+axiom ax13: x7 <= 1.0
+goal g:
+  x1 * x1 + 2.0 * x2 * x2 + 2.0 * x3 * x3 + 2.0 * x4 * x4 + 2.0 * x5 * x5
+  + 2.0 * x6 * x6 + 2.0 * x7 * x7 + (- (x1)) < 14.0001

non-regression/valid/osdp/adaptative_lotka_voltera_system_lb.ae

@@ -0,0 +1,15 @@
+logic x1 : real
+logic x2 : real
+logic x3 : real
+logic x4 : real
+axiom ax0: (- (2.0)) <= x1
+axiom ax1: x1 <= 2.0
+axiom ax2: (- (2.0)) <= x2
+axiom ax3: x2 <= 2.0
+axiom ax4: (- (2.0)) <= x3
+axiom ax5: x3 <= 2.0
+axiom ax6: (- (2.0)) <= x4
+axiom ax7: x4 <= 2.0
+goal g:
+  (- (20.8001))
+  < x1 * x2 * x2 + x1 * x3 * x3 + x1 * x4 * x4 + (- (1.1 * x1)) + 1.0

non-regression/valid/osdp/adaptative_lotka_voltera_system_ub.ae

@@ -0,0 +1,14 @@
+logic x1 : real
+logic x2 : real
+logic x3 : real
+logic x4 : real
+axiom ax0: (- (2.0)) <= x1
+axiom ax1: x1 <= 2.0
+axiom ax2: (- (2.0)) <= x2
+axiom ax3: x2 <= 2.0
+axiom ax4: (- (2.0)) <= x3
+axiom ax5: x3 <= 2.0
+axiom ax6: (- (2.0)) <= x4
+axiom ax7: x4 <= 2.0
+goal g:
+  x1 * x2 * x2 + x1 * x3 * x3 + x1 * x4 * x4 + (- (1.1 * x1)) + 1.0 < 22.8001

non-regression/valid/osdp/butcher_lb.ae

@@ -0,0 +1,22 @@
+logic x1 : real
+logic x2 : real
+logic x3 : real
+logic x4 : real
+logic x5 : real
+logic x6 : real
+axiom ax0: (- (1.0)) <= x1
+axiom ax1: x1 <= 0.0
+axiom ax2: (- (0.1)) <= x2
+axiom ax3: x2 <= 0.9
+axiom ax4: (- (0.1)) <= x3
+axiom ax5: x3 <= 0.5
+axiom ax6: (- (1.0)) <= x4
+axiom ax7: x4 <= (- (0.1))
+axiom ax8: (- (0.1)) <= x5
+axiom ax9: x5 <= (- (0.05))
+axiom ax10: (- (0.1)) <= x6
+axiom ax11: x6 <= (- (0.03))
+goal g:
+  (- (1.4394))
+  < x6 * x2 * x2 + x5 * x3 * x3 + (- (x1 * x4 * x4)) + x4 * x4 * x4 + 
+    x4 * x4 + (- (1.0 / 3.0 * x1)) + 4.0 / 3.0 * x4

non-regression/valid/osdp/butcher_ub.ae

@@ -0,0 +1,21 @@
+logic x1 : real
+logic x2 : real
+logic x3 : real
+logic x4 : real
+logic x5 : real
+logic x6 : real
+axiom ax0: (- (1.0)) <= x1
+axiom ax1: x1 <= 0.0
+axiom ax2: (- (0.1)) <= x2
+axiom ax3: x2 <= 0.9
+axiom ax4: (- (0.1)) <= x3
+axiom ax5: x3 <= 0.5
+axiom ax6: (- (1.0)) <= x4
+axiom ax7: x4 <= (- (0.1))
+axiom ax8: (- (0.1)) <= x5
+axiom ax9: x5 <= (- (0.05))
+axiom ax10: (- (0.1)) <= x6
+axiom ax11: x6 <= (- (0.03))
+goal g:
+  x6 * x2 * x2 + x5 * x3 * x3 + (- (x1 * x4 * x4)) + x4 * x4 * x4 + x4 * x4
+  + (- (1.0 / 3.0 * x1)) + 4.0 / 3.0 * x4 < 0.2191

non-regression/valid/osdp/caprasses_system_lb.ae

@@ -0,0 +1,17 @@
+logic x1 : real
+logic x2 : real
+logic x3 : real
+logic x4 : real
+axiom ax0: (- (0.5)) <= x1
+axiom ax1: x1 <= 0.5
+axiom ax2: (- (0.5)) <= x2
+axiom ax3: x2 <= 0.5
+axiom ax4: (- (0.5)) <= x3
+axiom ax5: x3 <= 0.5
+axiom ax6: (- (0.5)) <= x4
+axiom ax7: x4 <= 0.5
+goal g:
+  (- (3.1801))
+  < (- (x1 * x3 * x3 * x3)) + 4.0 * x2 * x3 * x3 * x4
+    + 4.0 * x1 * x3 * x4 * x4 + 2.0 * x2 * x4 * x4 * x4 + 4.0 * x1 * x3
+    + 4.0 * x3 * x3 + (- (10.0 * x2 * x4)) + (- (10.0 * x4 * x4)) + 2.0

non-regression/valid/osdp/caprasses_system_ub.ae

@@ -0,0 +1,16 @@
+logic x1 : real
+logic x2 : real
+logic x3 : real
+logic x4 : real
+axiom ax0: (- (0.5)) <= x1
+axiom ax1: x1 <= 0.5
+axiom ax2: (- (0.5)) <= x2
+axiom ax3: x2 <= 0.5
+axiom ax4: (- (0.5)) <= x3
+axiom ax5: x3 <= 0.5
+axiom ax6: (- (0.5)) <= x4
+axiom ax7: x4 <= 0.5
+goal g:
+  (- (x1 * x3 * x3 * x3)) + 4.0 * x2 * x3 * x3 * x4 + 4.0 * x1 * x3 * x4 * x4
+  + 2.0 * x2 * x4 * x4 * x4 + 4.0 * x1 * x3 + 4.0 * x3 * x3
+  + (- (10.0 * x2 * x4)) + (- (10.0 * x4 * x4)) + 2.0 < 4.4853

non-regression/valid/osdp/ex01_0.ae

@@ -0,0 +1,9 @@
+goal g :
+  forall x0, x1, x2 : real.
+    (x1 * x1 <= 2244380813988371./8796093022208.
+     and 5434649265398495./288230376151711744. * x1 * x1 + -2235225908102023./72057594037927936. * x1 * x2 + 2309742551941169./144115188075855872. * x2 * x2 <= 1126256253765299./1125899906842624. and 
+     x0 <= 1. and 0. <= 1. and -x0 <= 1.)
+    -> 1086929853079699./22517998136852480. * x0 * x0 + 7363044163787393./180143985094819840. * 
+       x0 * x1 + 13744362009667255./1152921504606846976. * x1 * x1 + -7608508971557893./180143985094819840. * 
+       x0 * x2 + -51541309146511751./2882303761517117440. * x1 * x2 + 53259562800905251./5764607523034234880. * 
+       x2 * x2 <= 1126256253765299./1125899906842624.

non-regression/valid/osdp/ex01_1.ae

@@ -0,0 +1,6 @@
+goal g :
+  forall x0, x1, x2 : real.
+    (x1 * x1 <= 2244380813988371./8796093022208.
+     and 5434649265398495./288230376151711744. * x1 * x1 + -2235225908102023./72057594037927936. * x1 * x2 + 2309742551941169./144115188075855872. * x2 * x2 <= 1126256253765299./1125899906842624. and 
+     x0 <= 1. and 0. <= 1. and -x0 <= 1.)
+    -> 64./25. * x0 * x0 + 24./5. * x0 * x1 + 9./4. * x1 * x1 + -56./25. * x0 * x2 + -21./10. * x1 * x2 + 49./100. * x2 * x2 <= 2244380813988371./8796093022208.

non-regression/valid/osdp/ex01_s.ae

@@ -0,0 +1,8 @@
+goal g :
+  forall x0, x1, x2 : real.
+    (5434649265398495./288230376151711744. * x1 * x1 + -2235225908102023./72057594037927936. * x1 * x2 + 2309742551941169./144115188075855872. * x2 * x2 <= 4505025181421617./4503599627370496. and 
+     x0 <= 1. and 0. <= 1. and -x0 <= 1.)
+    -> 1086929853079699./22517998136852480. * x0 * x0 + 7363044163787393./180143985094819840. * 
+       x0 * x1 + 13744362009667255./1152921504606846976. * x1 * x1 + -7608508971557893./180143985094819840. * 
+       x0 * x2 + -51541309146511751./2882303761517117440. * x1 * x2 + 53259562800905251./5764607523034234880. * 
+       x2 * x2 <= 4505025181421617./4503599627370496.

non-regression/valid/osdp/ex02_0.ae

@@ -0,0 +1,18 @@
+goal g :
+  forall x0, x1, x2, x3, x4 : real.
+    (x1 * x1 <= 6104882730649731./2251799813685248.
+     and 7337111046759473./2251799813685248. * x1 * x1 + -2907612138424301./562949953421312. * 
+         x1 * x2 + 1409542041811277./562949953421312. * x2 * x2 + -3668555522676813./1125899906842624. * 
+         x1 * x3 + 726903034475363./281474976710656. * x2 * x3 + 4681875744883939./4503599627370496. * 
+         x3 * x3 + 5081513174290049./2251799813685248. * x1 * x4 + -5056645740656145./2251799813685248. * 
+         x2 * x4 + -5081513173034077./4503599627370496. * x3 * x4 + 6119136129884633./9007199254740992. * 
+         x4 * x4 <= 1126156385803479./1125899906842624.
+     and x0 <= 1. and 0. <= 1. and -x0 <= 1.)
+    -> 2026640445820099./9007199254740992. * x0 * x0 + 2126145./4503599627370496. * 
+       x0 * x1 + 18803980767632465./9007199254740992. * x1 * x1 + -9840929./22517998136852480. * 
+       x0 * x2 + -14533238421213701./4503599627370496. * x1 * x2 + 359518441291214177./225179981368524800. * 
+       x2 * x2 + -3561069./22517998136852480. * x0 * x3 + -2350497594913961./1125899906842624. * 
+       x1 * x3 + 90832740095531231./56294995342131200. * x2 * x3 + 39197730584506643./56294995342131200. * 
+       x3 * x3 + 1405847./5629499534213120. * x0 * x4 + 2076176917316243./1125899906842624. * 
+       x1 * x4 + -51359777327316311./28147497671065600. * x2 * x4 + -12976105727933033./14073748835532800. * 
+       x3 * x4 + 7337111046759473./14073748835532800. * x4 * x4 <= 1126156385803479./1125899906842624.

non-regression/valid/osdp/ex02_1.ae

@@ -0,0 +1,14 @@
+goal g :
+  forall x0, x1, x2, x3, x4 : real.
+    (x1 * x1 <= 6104882730649731./2251799813685248.
+     and 7337111046759473./2251799813685248. * x1 * x1 + -2907612138424301./562949953421312. * 
+         x1 * x2 + 1409542041811277./562949953421312. * x2 * x2 + -3668555522676813./1125899906842624. * 
+         x1 * x3 + 726903034475363./281474976710656. * x2 * x3 + 4681875744883939./4503599627370496. * 
+         x3 * x3 + 5081513174290049./2251799813685248. * x1 * x4 + -5056645740656145./2251799813685248. * 
+         x2 * x4 + -5081513173034077./4503599627370496. * x3 * x4 + 6119136129884633./9007199254740992. * 
+         x4 * x4 <= 1126156385803479./1125899906842624.
+     and x0 <= 1. and 0. <= 1. and -x0 <= 1.)
+    -> 1./4. * x0 * x0 + 3./2. * x0 * x1 + 9./4. * x1 * x1 + -7./10. * x0 * x2 + -21./10. * 
+       x1 * x2 + 49./100. * x2 * x2 + -7./10. * x0 * x3 + -21./10. * x1 * x3 + 49./50. * 
+       x2 * x3 + 49./100. * x3 * x3 + 2./5. * x0 * x4 + 6./5. * x1 * x4 + -14./25. * 
+       x2 * x4 + -14./25. * x3 * x4 + 4./25. * x4 * x4 <= 6104882730649731./2251799813685248.

non-regression/valid/osdp/ex02_s.ae

@@ -0,0 +1,17 @@
+goal g :
+  forall x0, x1, x2, x3, x4 : real.
+    (7337111046759473./2251799813685248. * x1 * x1 + -2907612138424301./562949953421312. * 
+     x1 * x2 + 1409542041811277./562949953421312. * x2 * x2 + -3668555522676813./1125899906842624. * 
+     x1 * x3 + 726903034475363./281474976710656. * x2 * x3 + 4681875744883939./4503599627370496. * 
+     x3 * x3 + 5081513174290049./2251799813685248. * x1 * x4 + -5056645740656145./2251799813685248. * 
+     x2 * x4 + -5081513173034077./4503599627370496. * x3 * x4 + 6119136129884633./9007199254740992. * 
+     x4 * x4 <= 4504625494384113./4503599627370496. and x0 <= 1. and 0. <= 1. and 
+     -x0 <= 1.)
+    -> 2026640445820099./9007199254740992. * x0 * x0 + 2126145./4503599627370496. * 
+       x0 * x1 + 18803980767632465./9007199254740992. * x1 * x1 + -9840929./22517998136852480. * 
+       x0 * x2 + -14533238421213701./4503599627370496. * x1 * x2 + 359518441291214177./225179981368524800. * 
+       x2 * x2 + -3561069./22517998136852480. * x0 * x3 + -2350497594913961./1125899906842624. * 
+       x1 * x3 + 90832740095531231./56294995342131200. * x2 * x3 + 39197730584506643./56294995342131200. * 
+       x3 * x3 + 1405847./5629499534213120. * x0 * x4 + 2076176917316243./1125899906842624. * 
+       x1 * x4 + -51359777327316311./28147497671065600. * x2 * x4 + -12976105727933033./14073748835532800. * 
+       x3 * x4 + 7337111046759473./14073748835532800. * x4 * x4 <= 4504625494384113./4503599627370496.

non-regression/valid/osdp/ex03_0.ae

@@ -0,0 +1,9 @@
+goal g :
+  forall x0, x1, x2 : real.
+    (x1 * x1 <= 4569511492918935./281474976710656. and x2 * x2 <= 3663966569933171./8796093022208.
+     and 5758877526517161./4611686018427387904. * x1 * x1 + 8189182971628365./36893488147419103232. * x1 * x2 + 1609055879090527./1152921504606846976. * x2 * x2 <= 5234633192578273./9007199254740992. and 
+     x0 <= 1. and 0. <= 1. and -x0 <= 1.)
+    -> 5758877526517161./4611686018427387904. * x0 * x0 + 23030385000714648537./18446744073709551616000. * 
+       x0 * x1 + 5758871552841956038519./18446744073709551616000000. * 
+       x1 * x1 + 17910404752073181./184467440737095516160. * x0 * x2 + 28131595653890265613./368934881474191032320000. * 
+       x1 * x2 + 5119550653284578897./3689348814741910323200. * x2 * x2 <= 5234633192578273./9007199254740992.

non-regression/valid/osdp/ex03_1.ae

@@ -0,0 +1,6 @@
+goal g :
+  forall x0, x1, x2 : real.
+    (x1 * x1 <= 4569511492918935./281474976710656. and x2 * x2 <= 3663966569933171./8796093022208.
+     and 5758877526517161./4611686018427387904. * x1 * x1 + 8189182971628365./36893488147419103232. * x1 * x2 + 1609055879090527./1152921504606846976. * x2 * x2 <= 5234633192578273./9007199254740992. and 
+     x0 <= 1. and 0. <= 1. and -x0 <= 1.)
+    -> 1./10000. * x1 * x1 + 1./50. * x1 * x2 + x2 * x2 <= 3663966569933171./8796093022208.

non-regression/valid/osdp/ex03_2.ae

@@ -0,0 +1,6 @@
+goal g :
+  forall x0, x1, x2 : real.
+    (x1 * x1 <= 4569511492918935./281474976710656. and x2 * x2 <= 3663966569933171./8796093022208.
+     and 5758877526517161./4611686018427387904. * x1 * x1 + 8189182971628365./36893488147419103232. * x1 * x2 + 1609055879090527./1152921504606846976. * x2 * x2 <= 5234633192578273./9007199254740992. and 
+     x0 <= 1. and 0. <= 1. and -x0 <= 1.)
+    -> x0 * x0 + 499./500. * x0 * x1 + 249001./1000000. * x1 * x1 + -1./10. * x0 * x2 + -499./10000. * x1 * x2 + 1./400. * x2 * x2 <= 4569511492918935./281474976710656.

non-regression/valid/osdp/ex03_s.ae

@@ -0,0 +1,8 @@
+goal g :
+  forall x0, x1, x2 : real.
+    (5758877526517161./4611686018427387904. * x1 * x1 + 8189182971628365./36893488147419103232. * x1 * x2 + 1609055879090527./1152921504606846976. * x2 * x2 <= 4614627937518555./4503599627370496. and 
+     x0 <= 1. and 0. <= 1. and -x0 <= 1.)
+    -> 5758877526517161./4611686018427387904. * x0 * x0 + 23030385000714648537./18446744073709551616000. * 
+       x0 * x1 + 5758871552841956038519./18446744073709551616000000. * 
+       x1 * x1 + 17910404752073181./184467440737095516160. * x0 * x2 + 28131595653890265613./368934881474191032320000. * 
+       x1 * x2 + 5119550653284578897./3689348814741910323200. * x2 * x2 <= 4614627937518555./4503599627370496.