Import from Bin:a1af7a0 Src:7d7d01bcb farith:a93db57

Src/COLIBRI/col_solve.pl

@@ -800,12 +800,10 @@ smt_test(TO,Size) :-
     %StrDir = "./QF_FPLRA/schanda/", % 0 TO (cvc4 0)
 %----------------------------------------------------------------    
     %StrDir = "./QF_FP/20170501-Heizmann-UltimateAutomizer/", % 0
-% A VOIR
     %StrDir = "./QF_FP/20190429-UltimateAutomizerSvcomp2019/",% 0 (bitwuzla 0)
-    %StrDir = "./QF_FP/ramalho/", % 4 (4 min_solve)(cvc4 19)(bitwuzla 17)
-    %StrDir = "./QF_FP/griggio/", % 43 TO (42/41 min_solve)(cast float-double, delta 0) (cvc4 89)(bitwuzla 74) 
-    %StrDir = "./QF_FP/schanda/spark/", % 5 TO (5 min_solve) (avec (X+Y)/2 = X/2+Y/2
-    % quand c'est correcte, pas de inf/0 pour le resultat) (ncvc4 8)(bitwuzla 3)
+    %StrDir = "./QF_FP/ramalho/", % 4 (min_solve)(cvc4 19)(bitwuzla 17)
+    StrDir = "./QF_FP/griggio/", % 43 (min_solve, cast float-double, delta 0) (cvc4 89)(bitwuzla 74) 
+    %StrDir = "./QF_FP/schanda/spark/", % 7 (min_solve avec X =< (X+Y)/2 =< Y) (ncvc4 8)(bitwuzla 3)
     %StrDir = "./QF_FP/wintersteiger/", % tout OK
 
 %-----------------------------------------------------------------
@@ -823,12 +821,12 @@ smt_test(TO,Size) :-
     %StrDir = "./QF_ABV/bmc-arrays/", 
 %-----------------------------------------------------------------
     %StrDir = "QF_AX/",
-    %StrDir = "QF_AX/storeinv/",
-    %StrDir = "QF_AX/swap/",
-    %StrDir = "QF_AX/storecomm/",
-    %StrDir = "QF_AX/cvc/",
+    %StrDir = "QF_AX/storeinv/", % 3
+    %StrDir = "QF_AX/swap/", % 8
+    %StrDir = "QF_AX/storecomm/", % 0
+    %StrDir = "QF_AX/cvc/", % 0
 
-    StrDir = "QF_ALIA/qlock2/", % Des TO et core dump
+    %StrDir = "QF_ALIA/qlock2/", % Des TO et core dump
     %StrDir = "QF_ALIA/cvc/", % TOUT OK
     %StrDir = "QF_ALIA/UltimateAutomizer2/",% des TO
     %StrDir = "QF_ALIA/piVC/", % TOUT OK
@@ -1035,12 +1033,13 @@ smt_unit_test(TO) :-
     %StrDir = "./QF_FP/ramalho/",% 6-2 T0
     %StrDir = "./QF_FP/griggio/", % 59 TO en 24s, 51 en 60s (cvc4 90 en 60s)
     %StrDir = "./QF_FP/schanda/spark/",% 7 TO
-    StrDir = "./QF_FP/wintersteiger/", % 0 TO
+    %StrDir = "./QF_FP/wintersteiger/", % 0 TO
 %------------------------------------------------------------------------
-    %StrDir = "QF_AX/",
+    StrDir = "QF_AX/",
     %StrDir = "QF_AX/storeinv/",
     %StrDir = "QF_AX/swap/",
     %StrDir = "QF_AX/storecomm/",
+    %StrDir = "QF_AX/cvc/",
 %----------------------------------------------------------------------
     %StrDir = "./QF_BV/",
     %StrDir = "./QF_BV/20170501-Heizmann-UltimateAutomizer/",

Src/COLIBRI/realarith.pl

@@ -12792,6 +12792,7 @@ div_real_bis(Type,A,B,C) :-
             true
         ;   div_real_rec(Type,A,B,C),
             div_real_ineqs(Type,A,B,C),
+            average_real_ineqs(Type,A,B,C),
             div_real_inst(Type,A,B,C,Continue3),
             check_div_mult_exact(Type,A,B,C,Continue3,Continue4),
             (var(Continue4) ->
@@ -12800,8 +12801,7 @@ div_real_bis(Type,A,B,C) :-
                 set_prio_inst([A,B,C],4,5,Prio),
                 NewGoal = div_real1(Type,A,B,C),
                 
-                my_suspend(NewGoal,Prio,(A,B,C)->suspend:constrained),
-                saturate_div_real_two(Type,A,B,C)))).
+                my_suspend(NewGoal,Prio,(A,B,C)->suspend:constrained)))).
 check_div_mult_exact(Type,A,B,C,Continue,NContinue) :-
     var(Continue),
@@ -12828,52 +12828,31 @@ check_div_mult_exact(Type,A,B,C,_,Continue) :-
 % permet de capturer certains calculs de moyenne
 % Ex A =< (A+B)/2 =< B et A < B
 % pour les average_(1,2,3) de schanda
-%saturate_div_real_two(Type,A,B,C) :- !.
+% average_real_ineqs(Type,A,B,C) :- !.
 % Bizarre !!
-saturate_div_real_two(Type,A,B,C) :-
+average_real_ineqs(Type,A,B,C) :-
     ((B == 2.0,
-      not_inf_bounds(A),
-      not_zero(C),
       get_saved_cstr_suspensions(LSusp),
       member((S,add_real1(Type,X,Y,AA)),LSusp),
-      % (X+Y)/2 = C
-      % dans ce cas (X+Y)/2 = X/2 + Y/2
+      AA == A,
       var(X),
-      var(Y))
+      var(Y),
+      get_rel_between_real_args(X,Y,Rel),
+      occurs(Rel,(<,=<,>,>=)))
     ->
-        % on sature en creant X/2 + Y/2 = C
-        get_cstr_suspensions(X,LSX),
-        ((member(SX,LSX),
-          get_suspension_data(SX,goal,div_real1(Type,XX,X2,Xd2)),
-          X2 == 2.0,
-          XX == X)
-        ->
-            Goals1 = []
-        ;   Goals1 = [div_real(Type,X,2.0,Xd2)]),
-        get_cstr_suspensions(Y,LSY),
-        ((member(SY,LSY),
-          get_suspension_data(SY,goal,div_real1(Type,YY,Y2,Yd2)),
-          Y2 == 2.0,
-          YY == Y)
-        ->
-            Goals2 = Goals1
-        ;   append(Goals1,[div_real(Type,Y,2.0,Yd2)],Goals2)),
-        (Goals2 == [] ->
-            ((member((_,add_real1(Type,Ud2,Vd2,CC)),LSusp),
-              CC == C,
-              (Ud2 == Xd2 ->
-                  Vd2 == Yd2
-              ;   Ud2 == Yd2,
-                  Vd2 == Xd2))
-            ->
-                Goals = []
-            ;   Goals = [add_real(Type,Xd2,Yd2,C)])
-        ;   append(Goals2,[add_real(Type,Xd2,Yd2,C)],Goals)),
-        (foreach(G,Goals) do
-            call_priority(G,2))
+        (getval(use_delta,1)@eclipse ->
+            (occurs(Rel,(=<,<)) ->
+                launch_real_ineq(=<,Type,X,C),
+                launch_real_ineq(=<,Type,C,Y)
+            ;   launch_real_ineq(=<,Type,Y,C),
+                launch_real_ineq(=<,Type,C,X))
+        ;   (occurs(Rel,(=<,<)) ->
+                launch_geq_real(Type,Y,C),
+                launch_geq_real(Type,C,X)
+            ;   launch_geq_real(Type,X,C),
+                launch_geq_real(Type,C,Y)))
     ;   true).
-
 %% PMO si les 3 args sont des float_int entre -2^53 et 2^53 on peut
 %% deleguer le calcul de mult_real aux entiers
 check_launch_div_int(Type,A,B,C,Continue,_) :-