From 950bcb69c23d4d6dda87f3cb60d2b0d2f453a3bd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 10 Sep 2021 10:52:36 +0200
Subject: [PATCH] Import from Bin:a1af7a0 Src:8b49f3e0a farith:a93db57
---
Src/COLIBRI/arith.pl | 23 +++++++++++++++--------
Src/COLIBRI/col_solve.pl | 4 ++--
Src/COLIBRI/lp_arith.pl | 10 ++++++----
Src/COLIBRI/realarith.pl | 3 ++-
Src/COLIBRI/solve.pl | 21 +++++++++++++++------
5 files changed, 40 insertions(+), 21 deletions(-)
diff --git a/Src/COLIBRI/arith.pl b/Src/COLIBRI/arith.pl
index c901f4e57..001fd1373 100755
--- a/Src/COLIBRI/arith.pl
+++ b/Src/COLIBRI/arith.pl
@@ -3380,22 +3380,29 @@ div_mod_int_bis(A, B, Q, BQ, R) :-
check_exists_div_mod_int(A,B,Q,BQ,R) :-
get_saved_cstr_suspensions(LSusp),
((member((Susp,div_mod_int(V1,V2,Quot,V2Quot,RR)),LSusp),
- once (V1 == A; V2 == B),
(V2 == B ->
(V1 == A;
Quot == Q,
RR == R)
; V1 == A,
Quot == Q,
- RR == R))
+ RR == R,
+ (not_unify(Q,0) ->
+ true
+ ; exists_diff_Rel(V2,B),
+ ZQ = 1)))
->
!,
- kill_suspension(Susp),
- protected_unify(A,V1),
- protected_unify(B,V2),
- protected_unify(Quot,Q),
- protected_unify(V2Quot,BQ),
- protected_unify(Rem,R)
+ (nonvar(ZQ) ->
+ protected_unify(Q,0),
+ protected_unify(BQ,0),
+ protected_unify(V2Quot,0)
+ ; kill_suspension(Susp),
+ protected_unify(A,V1),
+ protected_unify(B,V2),
+ protected_unify(Quot,Q),
+ protected_unify(V2Quot,BQ),
+ protected_unify(Rem,R))
; % issue 40: cas diviseur <> 0
% abs(X) = abs(A), abs(Y) = abs(B) =>
% abs(X // Y) = abs(A // B) et abs(X rem Y) = abs(A rem B)
diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index edb8d1ab3..06846a92f 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/lp_arith.pl b/Src/COLIBRI/lp_arith.pl
index cad874d21..a713d7e44 100755
--- a/Src/COLIBRI/lp_arith.pl
+++ b/Src/COLIBRI/lp_arith.pl
@@ -1239,9 +1239,9 @@ lin_mult_int(A,B,C) :-
(Vars = [V,_|_] ->
((get_lin_cstrs(V,Cstrs),
member(mult_int(X,Y,Z),Cstrs),
- (occurs(0,(X,Y,Z)) ->
- match_com_binop(A,B,C,X,Y,Z,U1,U2)
- ; match_inv_com_binop(A,B,C,X,Y,Z,U1,U2)))
+ (not_unify(C,0) ->
+ match_inv_com_binop(A,B,C,X,Y,Z,U1,U2)
+ ; match_com_binop(A,B,C,X,Y,Z,U1,U2)))
->
protected_unify(U1 = U2)
; ls_setup,
@@ -1270,7 +1270,9 @@ lin_mult_real(Type,A,B,C) :-
(Vars = [V,_|_] ->
((get_lin_cstrs(V,Cstrs),
member(mult_real(Type,X,Y,Z),Cstrs),
- (Type == real ->
+ ((Type == real,
+ not_unify(C,0.0))
+ ->
match_inv_com_binop(A,B,C,X,Y,Z,U1,U2)
; match_com_binop(A,B,C,X,Y,Z,U1,U2)))
->
diff --git a/Src/COLIBRI/realarith.pl b/Src/COLIBRI/realarith.pl
index a0eaff17e..4fb7beeef 100755
--- a/Src/COLIBRI/realarith.pl
+++ b/Src/COLIBRI/realarith.pl
@@ -12836,7 +12836,8 @@ idiv_mod_real(A,B,Q,R) :-
(AA == A;
QQ == Q,
RR == R)
- ; AA == A,
+ ; not_zero(Q),
+ AA == A,
QQ == Q,
RR == R))
->
diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl
index c50d6c621..cbd5ae28c 100644
--- a/Src/COLIBRI/solve.pl
+++ b/Src/COLIBRI/solve.pl
@@ -10420,12 +10420,21 @@ check_exists_cdiv_crem(A,B,Q,R,Suspend) :-
R == RR)
; A == AA,
Q == QQ,
- R == RR))
- ->
- protected_unify(A,AA),
- protected_unify(B,BB),
- protected_unify(Q,QQ),
- protected_unify(R,RR)
+ R == RR,
+ (not_zero(Q) ->
+ true
+ ; exists_diff_Rel(B,BB),
+ ZQ = 1)))
+ ->
+ (nonvar(ZQ) ->
+ Suspend = 1,
+ protected_unify(Q,0),
+ protected_unify(QQ,0)
+ ; % Factorisation
+ protected_unify(A,AA),
+ protected_unify(B,BB),
+ protected_unify(Q,QQ),
+ protected_unify(R,RR))
; % issue 40: cas diviseur <> 0
% abs(X) = abs(A), abs(Y) = abs(B) =>
% abs(X // Y) = abs(A // B) et abs(X rem Y) = abs(A rem B)
--
GitLab