From fdb87cd437edaf9a53fa8b5de96d5ae8e4fd9644 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 9 Sep 2021 11:43:14 +0200
Subject: [PATCH] Import from Bin:a1af7a0 Src:c996ce084 farith:a93db57
---
Src/COLIBRI/col_solve.pl | 4 ++--
Src/COLIBRI/realarith.pl | 16 ++++++++++++----
Src/COLIBRI/solve.pl | 4 +---
3 files changed, 15 insertions(+), 9 deletions(-)
diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index 06846a92f..edb8d1ab3 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 98e6cab84..a0eaff17e 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 88c236260..c50d6c621 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)
--
GitLab