diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl index 06846a92ff5bb2a1771cfba625a18a0f936ee88d..edb8d1ab39c7e6700661754c58280a5bc1e12abf 100644 --- a/Src/COLIBRI/col_solve.pl +++ b/Src/COLIBRI/col_solve.pl @@ -730,8 +730,8 @@ smt_test :- smt_test(TO,Size) :- %StrDir = "./colibri_tests/colibri/tests/", - %StrDir = "./colibri_tests/colibri/tests/sat/", %0 (sans real/float-> int!) - StrDir = "./colibri_tests/colibri/tests/unsat/", %0 + StrDir = "./colibri_tests/colibri/tests/sat/", %0 (sans real/float-> int!) + %StrDir = "./colibri_tests/colibri/tests/unsat/", %0 %StrDir = "./colibri_tests/colibri/tests/unknown/", %StrDir = "./colibri_tests/colibri/tests/timeout/", diff --git a/Src/COLIBRI/realarith.pl b/Src/COLIBRI/realarith.pl index 98e6cab84d07a908df803b46125089585824062a..a0eaff17ee3115e6328bc4b6fb93487f24c6fce8 100755 --- a/Src/COLIBRI/realarith.pl +++ b/Src/COLIBRI/realarith.pl @@ -12831,10 +12831,18 @@ idiv_mod_real(A,B,Q,R) :- set_priority(1), save_cstr_suspensions((A,B)), get_saved_cstr_suspensions(LSusp), - ((member((_,check_diff_real(BB,AA,QQ,RR)),LSusp), - BB == B, - AA == A) + ((member((Susp,check_divides_real(BB,AA,QQ,RR)),LSusp), + (BB == B -> + (AA == A; + QQ == Q, + RR == R) + ; AA == A, + QQ == Q, + RR == R)) -> + % Fact si arguments égaux ou 3 sur 4 communs + protected_unify(A,AA), + protected_unify(B,BB), protected_unify(Q,QQ), protected_unify(R,RR) ; set_lazy_domain(real,A), @@ -12853,7 +12861,7 @@ idiv_mod_real(A,B,Q,R) :- as(R,real) $>= 0.0, % R est borné par B en valeur absolue as(R,real) $< abs(as(B,real)), - % R = A-BQ, mais de lien direct sur A et B ? + % R = A-BQ, mais pas de lien direct sur A et B ? mult_real(real,B,Q,BQ), minus_real(real,A,BQ,R), % on teste la divisibilite pour forcer R à 0 ou <> 0 diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl index 88c2362605121f20e23ff349143caded563831be..c50d6c6218e5a98824c6a7c541aacf099e041b0e 100644 --- a/Src/COLIBRI/solve.pl +++ b/Src/COLIBRI/solve.pl @@ -9818,8 +9818,6 @@ chk_undef_imod_real(Bool,Type,A,B,R) :- ; true), (nonvar(Bool) -> (Bool == 0 -> - % B <> 0.0 -% imod_real(A,B,R) idiv_mod_real(A,B,_,R) ; protected_unify(B,0.0), undef_imod_real(Type,A,R)) @@ -10459,7 +10457,7 @@ check_exists_cdiv_crem(A,B,Q,R,Suspend) :- -> (RelAX == op -> % A et R de même signe - op(R,RR), + op_real(real,R,RR), (RelBY == eq -> % A // B = Q et -A // B = -Q et R = -RR op_real(real,Q,QQ)