Skip to content
Snippets Groups Projects
Commit 10490b7f authored by François Bobot's avatar François Bobot
Browse files

Merge branch 'fix32' into 'master' 

Fix #32

Closes #32

See merge request adacore/colibri!17
parents 810fdd4c e08d7622
No related branches found
No related tags found
1 merge request!17Fix #32
Pipeline #36125 passed
Stage: test
    Hide whitespace changes
    Inline Side-by-side
    Src/COLIBRI/arith.pl
    + 112
    − 105
    View file @ 10490b7f
    ...@@ -4558,128 +4558,135 @@ power_int_body(A,TA,N,Mod2,B,TB,Continue) :- ...@@ -4558,128 +4558,135 @@ power_int_body(A,TA,N,Mod2,B,TB,Continue) :-
    %% plus vite ! %% plus vite !
    check_delta_power(A,N,Mod2,B,TA,TB) :- check_delta_power(A,N,Mod2,B,TA,TB) :-
    (exists_delta_Rel(A,B,Rel,_,_) -> (exists_delta_Rel(A,B,Rel,_,_) ->
    mfd:dvar_domain(A,DomA), mfd:dvar_domain(A,DomA),
    mfd:dvar_domain(B,DomB), mfd:dvar_domain(B,DomB),
    (Mod2 == 0 -> (Mod2 == 0 ->
    Rel \== '>', Rel \== '>',
    (Rel == '>=' -> (Rel == '>=' ->
    %% Donc A = B et A :: [0,1] % Donc A = B et A :: [0,1]
    mfd:quiet_set_intervals(A,[0,1]), mfd:quiet_set_intervals(A,[0,1]),
    protected_unify(A = B) protected_unify(A = B)
    ; (Rel == '=<' -> ; (Rel == '=<' ->
    true true
    ; %% A <> B ; % A <> B
    mfd:dom_difference(DomA,dom([0,1]),NDomA), mfd:dom_difference(DomA,dom([0,1]),NDomA),
    mfd:dvar_set(A,NDomA), mfd:dvar_set(A,NDomA),
    mfd:dvar_remove_element(B,0))) mfd:dvar_remove_element(B,0)))
    ; %% A et B de meme signe ; % A et B de meme signe
    (Rel == '<' -> (Rel == '<' ->
    %% A > 1 % A > 1
    mfd:dvar_remove_smaller(A,2), mfd:dvar_remove_smaller(A,2),
    MinB is pow_int(2,N), MinB is pow_int(2,N),
    mfd:dvar_remove_smaller(B,MinB) mfd:dvar_remove_smaller(B,MinB)
    ; (Rel == '=<' -> ; (Rel == '=<' ->
    %% A >= -1 % A >= -1
    mfd:dvar_remove_smaller(A,-1), mfd:dvar_remove_smaller(A,-1),
    mfd:dvar_remove_smaller(B,-1) mfd:dvar_remove_smaller(B,-1)
    ; (Rel == '>' -> ; (Rel == '>' ->
    %% A < -1 % A < -1
    mfd:dvar_remove_greater(A,-2), mfd:dvar_remove_greater(A,-2),
    MaxB is pow_int(-2,N), MaxB is pow_int(-2,N),
    mfd:dvar_remove_greater(B,MaxB) mfd:dvar_remove_greater(B,MaxB)
    ; (Rel == '>=' -> ; (Rel == '>=' ->
    %% A =< 1 % A =< 1
    mfd:dvar_remove_greater(A,1), mfd:dvar_remove_greater(A,1),
    mfd:dvar_remove_greater(B,1) mfd:dvar_remove_greater(B,1)
    ; %% Rel = '#' ; % Rel = '#'
    mfd:dom_difference(DomA,dom([-1..1]),NDomA), mfd:dom_difference(DomA,dom([-1..1]),NDomA),
    mfd:dom_difference(DomB,dom([-1..1]),NDomB), mfd:dom_difference(DomB,dom([-1..1]),NDomB),
    mfd:dvar_set(A,NDomA), mfd:dvar_set(A,NDomA),
    mfd:dvar_set(B,NDomB)))))), mfd:dvar_set(B,NDomB)))))),
    mfd:dvar_domain(A,NewDomA), mfd:dvar_domain(A,NewDomA),
    mfd:dvar_domain(B,NewDomB), mfd:dvar_domain(B,NewDomB),
    (NewDomA == DomA -> (NewDomA == DomA ->
    true true
    ; TA = 1), ; TA = 1),
    (NewDomB == DomB -> (NewDomB == DomB ->
    true true
    ; TB = 1) ; TB = 1)
    ; true). ; true).
    launch_delta_power(A,Mod2,B) :- launch_delta_power(A,Mod2,B) :-
    var(A), var(A),
    var(B), var(B), % donc N > 0
    A \== B, % donc N > 1
    !, !,
    mfd:dvar_range(A,LA,HA), mfd:dvar_range(A,LA,HA),
    mfd:dvar_range(B,LB,HB), mfd:dvar_range(B,LB,HB),
    (Mod2 == 0 -> (Mod2 == 0 ->
    (LA < 0 -> (HA =< 0 ->
    (abs(LA) =< abs(HA) -> % A neg, B pos: HA -> LB, LA -> HB
    % LA -> LB, HA -> HB D1 is LB - HA,
    MinD is LB - LA, D2 is HB - LA
    MaxD is HB - HA ; (LA < 0 ->
    ; MinD is HB - HA, % A non signé
    MaxD is LB - LA) (not_unify(A,0) ->
    ; MinD is LB - LA, D1 = 1
    MaxD is HB - HA) ; D1 = 0),
    % HA > 0,
    D2 is max(HB-LA,HB-HA)
    ; % A pos, B pos: LA -> LB, HA -> HB
    D1 is LB - LA,
    D2 is HB - HA))
    ; % meme signe pour A et B ; % meme signe pour A et B
    % LA -> LB, HA -> HB % si A et B neg: on recule LA -> LB, HA -> HB
    MinD is LB - LA, % si A et B pos: on avance LA -> LB, HA -> HB
    MaxD is HB - HA), % si A et B non signés: on recule sur LA -> LB,
    % on avance sur HA -> HB
    D1 is LB - LA,
    D2 is HB - HA),
    sort(0,=<,[D1,D2],[MinD,MaxD]),
    launch_delta(A,B,+,MinD..MaxD). launch_delta(A,B,+,MinD..MaxD).
    launch_delta_power(A,Mod2,B). launch_delta_power(A,Mod2,B).
    power_inst(A,N,Mod2,B,Continue) :- power_inst(A,N,Mod2,B,Continue) :-
    (integer(A) -> (integer(A) ->
    B0 is pow_int(A,N), B0 is pow_int(A,N),
    protected_unify(B,B0) protected_unify(B,B0)
    ; (integer(B) -> ; (integer(B) ->
    abs(B,AbsB), abs(B,AbsB),
    int_nroot(AbsB,N,Root), int_nroot(AbsB,N,Root),
    (B >= 0 -> (B >= 0 ->
    (Mod2 == 0 -> (Mod2 == 0 ->
    %% A neg ou pos % A neg ou pos
    OpRoot is -Root, OpRoot is -Root,
    mfd:(A::[OpRoot, Root]) mfd:(A::[OpRoot, Root])
    ; %% A et B du meme signe ; % A et B du meme signe
    A = Root) A = Root)
    ; %% A et B negatifs ; % A et B negatifs
    Mod2 == 1, Mod2 == 1,
    A0 is -Root, A0 is -Root,
    protected_unify(A,A0)) protected_unify(A,A0))
    ; (A == B -> ; (A == B ->
    mfd:(B :: [-1,0,1]) mfd:(B :: [-1,0,1])
    ; mfd:dvar_range(A,MinA,MaxA), ; mfd:dvar_range(A,MinA,MaxA),
    ((MinA >= -1, ((MinA >= -1,
    MaxA =< 1) MaxA =< 1)
    -> ->
    %% A : -1..1 % A : -1..1
    (Mod2 == 1 -> (Mod2 == 1 ->
    protected_unify(A = B) protected_unify(A = B)
    ; abs_val_int_bis(A,B)) ; abs_val_int_bis(A,B))
    ; Continue = 1)))). ; Continue = 1)))).
    power_int_rec(A,TA,N,Mod2,B,TB,Continue) :- power_int_rec(A,TA,N,Mod2,B,TB,Continue) :-
    power_int_ter(A,TA,N,Mod2,B,TB), power_int_ter(A,TA,N,Mod2,B,TB),
    mfd:get_intervals(A,IA), mfd:get_intervals(A,IA),
    mfd:get_intervals(B,IB), mfd:get_intervals(B,IB),
    saturate_power_inequalities(A,B,N,Mod2), saturate_power_inequalities(A,B,N,Mod2),
    power_inst(A,N,Mod2,B,Continue1), power_inst(A,N,Mod2,B,Continue1),
    (var(Continue1) -> (var(Continue1) ->
    true true
    ; mfd:get_intervals(A,NIA), ; mfd:get_intervals(A,NIA),
    mfd:get_intervals(B,NIB), mfd:get_intervals(B,NIB),
    check_reduced(IA,NIA,NTA), check_reduced(IA,NIA,NTA),
    check_reduced(IB,NIB,NTB), check_reduced(IB,NIB,NTB),
    ((var(NTA), ((var(NTA),
    var(NTB)) var(NTB))
    -> ->
    Continue = 1 Continue = 1
    ; power_int_rec(A,NTA,N,Mod2,B,NTB,Continue))). ; power_int_rec(A,NTA,N,Mod2,B,NTB,Continue))).
    power_int_ter(A,TA,N,Mod2,B,TB) :- power_int_ter(A,TA,N,Mod2,B,TB) :-
    (nonvar(A); (nonvar(A);
    ......
    Src/COLIBRI/col_solve.pl
    + 4
    − 4
    View file @ 10490b7f
    ...@@ -735,7 +735,7 @@ smt_test :- ...@@ -735,7 +735,7 @@ smt_test :-
    smt_test(TO,Size) :- smt_test(TO,Size) :-
    %StrDir = "./colibri-master-tests/tests/", %StrDir = "./colibri-master-tests/tests/",
    %StrDir = "./colibri-master-tests/tests/sat/", %0 (sans real/float-> int!) %StrDir = "./colibri-master-tests/tests/sat/", %0 (sans real/float-> int!)
    %StrDir = "./colibri-master-tests/tests/unsat/", %0 StrDir = "./colibri-master-tests/tests/unsat/", %0
    %StrDir = "./colibri-master-tests/tests/unknown/", %StrDir = "./colibri-master-tests/tests/unknown/",
    %StrDir = "./smt/", %StrDir = "./smt/",
    ...@@ -841,7 +841,7 @@ smt_test(TO,Size) :- ...@@ -841,7 +841,7 @@ smt_test(TO,Size) :-
    %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/aachen_real_gmp_gmp_klee_mul.x86_64/", % 3 (bitwuzla 0) %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/aachen_real_gmp_gmp_klee_mul.x86_64/", % 3 (bitwuzla 0)
    %StrDir = "QF_ABVFP/20170428-Liew-KLEE/aachen_real_numerical_recipes_qrdcmp.x86_64/", %StrDir = "QF_ABVFP/20170428-Liew-KLEE/aachen_real_numerical_recipes_qrdcmp.x86_64/",
    %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 100 (177 unsupported) (cvc4 55) %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 106 (177 unsupported) (cvc4 55)
    %StrDir = "./QF_ABVFP/20170501-Heizmann-UltimateAutomizer/", % 0 min_solve (cvc4 0) OK %StrDir = "./QF_ABVFP/20170501-Heizmann-UltimateAutomizer/", % 0 min_solve (cvc4 0) OK
    %---------------------------------------------------------------------- %----------------------------------------------------------------------
    %StrDir = "./QF_ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/",% 0 (cvc4 1|2)! %StrDir = "./QF_ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/",% 0 (cvc4 1|2)!
    ...@@ -851,7 +851,7 @@ smt_test(TO,Size) :- ...@@ -851,7 +851,7 @@ smt_test(TO,Size) :-
    %StrDir = "./QF_BVFP/20170428-Liew-KLEE/imperial_synthetic_sqrt_klee.x86_64/", % 3 (bitwuzla 3) %StrDir = "./QF_BVFP/20170428-Liew-KLEE/imperial_synthetic_sqrt_klee.x86_64/", % 3 (bitwuzla 3)
    %StrDir = "./QF_BVFP/20170428-Liew-KLEE/aachen_syn_halve_longdouble-flow.x86_64/",% 4u %StrDir = "./QF_BVFP/20170428-Liew-KLEE/aachen_syn_halve_longdouble-flow.x86_64/",% 4u
    %StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 16 (cvc4 50)(bitwuzla %StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 17 (cvc4 50)(bitwuzla
    % 15)(89 u)(11 20mn) % 15)(89 u)(11 20mn)
    %StrDir = "./QF_BVFP/20170501-Heizmann-UltimateAutomizer/", % 0 (bitwuzla 0) %StrDir = "./QF_BVFP/20170501-Heizmann-UltimateAutomizer/", % 0 (bitwuzla 0)
    %StrDir = "./QF_BVFP/ramalho/", % 0 TO (bitwuzla 0) %StrDir = "./QF_BVFP/ramalho/", % 0 TO (bitwuzla 0)
    ...@@ -871,7 +871,7 @@ smt_test(TO,Size) :- ...@@ -871,7 +871,7 @@ smt_test(TO,Size) :-
    %StrDir = "./QF_FP/20170501-Heizmann-UltimateAutomizer/", % 0 %StrDir = "./QF_FP/20170501-Heizmann-UltimateAutomizer/", % 0
    %StrDir = "./QF_FP/20190429-UltimateAutomizerSvcomp2019/",% 0 (bitwuzla 0) %StrDir = "./QF_FP/20190429-UltimateAutomizerSvcomp2019/",% 0 (bitwuzla 0)
    %StrDir = "./QF_FP/ramalho/", % 0! (cvc4 19)(bitwuzla 17) %StrDir = "./QF_FP/ramalho/", % 0! (cvc4 19)(bitwuzla 17)
    StrDir = "./QF_FP/griggio/", % 50 (min_solve, sans lin_solve ni ls_reduce..)(39) %StrDir = "./QF_FP/griggio/", % 50 (min_solve, sans lin_solve ni ls_reduce..)(39)
    %(cvc4 89)(bitwuzla 74) LES DD DEMARRENT TROP VITE ? %(cvc4 89)(bitwuzla 74) LES DD DEMARRENT TROP VITE ?
    %StrDir = "./QF_FP/schanda/spark/", % 6 (min_solve avec X =< (X+Y)/2 =< Y) (ncvc4 8)(bitwuzla 3) %StrDir = "./QF_FP/schanda/spark/", % 6 (min_solve avec X =< (X+Y)/2 =< Y) (ncvc4 8)(bitwuzla 3)
    %StrDir = "./QF_FP/wintersteiger/", % tout OK %StrDir = "./QF_FP/wintersteiger/", % tout OK
    ......
    Src/COLIBRI/realarith.pl
    + 10
    − 6
    View file @ 10490b7f
    ...@@ -4471,8 +4471,10 @@ real_inter_dom_if_eq(_,_,DomA,DomB,DomC,DomA,DomB,DomC). ...@@ -4471,8 +4471,10 @@ real_inter_dom_if_eq(_,_,DomA,DomB,DomC,DomA,DomB,DomC).
       
       
       
    % BUG reduce_dom_add_args_from_res(_,Type,FIA,FIB,FIC,RelCA,RelCB,DomA,DomB,DomC,DomA,DomB) :-
    reduce_dom_add_args_from_res(_,Type,FIA,FIB,FIC,RelCA,RelCB,DomA,DomB,DomC,DomA,DomB) :- !. % BUG
    mreal:dom_interval(DomC,[-0.0 .. 0.0]),
    !.
    reduce_dom_add_args_from_res(0,Type,FIA,FIB,FIC,RelCA,RelCB,DomA,DomB,DomC,DomA,DomB) :- !. reduce_dom_add_args_from_res(0,Type,FIA,FIB,FIC,RelCA,RelCB,DomA,DomB,DomC,DomA,DomB) :- !.
    reduce_dom_add_args_from_res(1,Type,FIA,FIB,FIC,RelCA,RelCB,DomA0,DomB0,DomC,DomA,DomB) :- reduce_dom_add_args_from_res(1,Type,FIA,FIB,FIC,RelCA,RelCB,DomA0,DomB0,DomC,DomA,DomB) :-
    mreal:dom_interval(DomA0,IA0), mreal:dom_interval(DomA0,IA0),
    ...@@ -9383,8 +9385,10 @@ minus_float_rec(Cpt,RS,Type,A,B,C) :- ...@@ -9383,8 +9385,10 @@ minus_float_rec(Cpt,RS,Type,A,B,C) :-
    minus_float_rec(NCpt,RS,Type,A,B,C)) minus_float_rec(NCpt,RS,Type,A,B,C))
    ; true). ; true).
       
    % BUG reduce_dom_minus_args_from_res(_,_,FIA,FIB,FIC,RelAC,DomA,DomB,DomC,DomA,DomB) :-
    reduce_dom_minus_args_from_res(_,_,FIA,FIB,FIC,RelAC,DomA,DomB,DomC,DomA,DomB) :- !. % BUG
    mreal:dom_interval(DomC,[-0.0 .. 0.0]),
    !.
    reduce_dom_minus_args_from_res(0,_,FIA,FIB,FIC,RelAC,DomA,DomB,DomC,DomA,DomB) :- !. reduce_dom_minus_args_from_res(0,_,FIA,FIB,FIC,RelAC,DomA,DomB,DomC,DomA,DomB) :- !.
    reduce_dom_minus_args_from_res(1,Type,FIA,FIB,FIC,RelAC,DomA0,DomB0,DomC,DomA,DomB) :- reduce_dom_minus_args_from_res(1,Type,FIA,FIB,FIC,RelAC,DomA0,DomB0,DomC,DomA,DomB) :-
    mreal:dom_interval(DomA0,IA0), mreal:dom_interval(DomA0,IA0),
    ...@@ -15578,8 +15582,8 @@ max_inv2_div_float_nearest0(_,A,C,B) :- ...@@ -15578,8 +15582,8 @@ max_inv2_div_float_nearest0(_,A,C,B) :-
       
    %% ESSAI VARIANTE SIMPLISTE DE power_real AVEC N ENTIER INSTANCIE >= 0 %% ESSAI VARIANTE SIMPLISTE DE power_real AVEC N ENTIER INSTANCIE >= 0
    power_real(A,N,B) :- power_real(A,N,B) :-
    getval(float_eval,Type)@eclipse, getval(float_eval,Type)@eclipse,
    power_real_type(Type,A,N,B). power_real_type(Type,A,N,B).
       
    power_real_type(real,A,N,B) ?- !, power_real_type(real,A,N,B) ?- !,
    power_real(real,A,N,B). power_real(real,A,N,B).
    ......
    tests/sat/mult.smt2 0 → 100644
    + 12
    − 0
    View file @ 10490b7f
    ;; produced by colibri.drv ;;
    (set-logic ALL)
    (set-info :smt-lib-version 2.6)
    (define-fun in_range1 ((x Int)) Bool (and (<= (- 2147483648) x)
    (<= x 2147483647)))
    (declare-const b11 Int)
    (assert (in_range1 b11))
    (assert (not (<= (* b11 b11) 2147483647)))
    (check-sat)
    0% or .
    You are about to add 0 people to the discussion. Proceed with caution.
    Finish editing this message first!
    Please register or to comment