From 967df05283f2748744e477e000ccd089f72f438e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 23 Sep 2021 17:17:06 +0200
Subject: [PATCH 1/2] Regression tests for #44
---
tests/sat/range_mult_fix_44.smt2 | 34 ++++++++++++++++++++++++++++++++
1 file changed, 34 insertions(+)
create mode 100644 tests/sat/range_mult_fix_44.smt2
diff --git a/tests/sat/range_mult_fix_44.smt2 b/tests/sat/range_mult_fix_44.smt2
new file mode 100644
index 000000000..b190d730d
--- /dev/null
+++ b/tests/sat/range_mult_fix_44.smt2
@@ -0,0 +1,34 @@
+;; produced by colibri.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+
+(define-fun fp.isFinite32 ((x Float32)) Bool (not (or (fp.isInfinite x) (fp.isNaN x))))
+
+(declare-const x Float32)
+
+;; Assume
+(assert
+ (and
+ (fp.leq (fp #b0 #b10000001 #b01000000000000000000000) x)
+ (fp.leq x (fp #b0 #b10000010 #b01000000000000000000000))))
+
+;; o
+(define-fun o () Float32
+ (fp.mul RNE x (fp #b0 #b10000000 #b00000000000000000000000)))
+
+;; Ensures
+(assert (fp.isFinite32 o))
+
+;; o
+(define-fun o1 () Float32
+ (fp.sub RNE o (fp #b0 #b10000001 #b01000000000000000000000)))
+
+;; Ensures
+(assert (fp.isFinite32 o1))
+
+;; Goal def'vc
+;; File "range_mult.adb", line 4, characters 0-0
+(assert
+ (not (fp.lt x o1)))
+
+(check-sat)
--
GitLab
From c11623e0c8dc0f154e8fe6747871123b3c5b17f1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 23 Sep 2021 17:17:40 +0200
Subject: [PATCH 2/2] Import from Bin:a1af7a0 Src:b49d22eeb farith:a93db57
---
Src/COLIBRI/check_lin_expr.pl | 1 +
Src/COLIBRI/col_solve.pl | 4 ++--
Src/COLIBRI/realarith.pl | 27 ++++++++-------------------
Src/COLIBRI/solve.pl | 4 ++--
4 files changed, 13 insertions(+), 23 deletions(-)
diff --git a/Src/COLIBRI/check_lin_expr.pl b/Src/COLIBRI/check_lin_expr.pl
index ed5729a71..802dfb94c 100755
--- a/Src/COLIBRI/check_lin_expr.pl
+++ b/Src/COLIBRI/check_lin_expr.pl
@@ -17,6 +17,7 @@ check_exists_lin_expr_giving_diff_args(Type,A,B,Stop) :-
(timeout(try_check_exists_lin_expr_giving_diff_args(Type,A,B,Stop),
0.5,
+ %1.0Inf,
true)
->
true
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 0408fc625..dd4c850a0 100755
--- a/Src/COLIBRI/realarith.pl
+++ b/Src/COLIBRI/realarith.pl
@@ -5443,7 +5443,9 @@ bin_op_real_ineq(Type,Op,A,B,C) :-
% Les arg2 sur les Op non commutatifs sont en relation opposée
Type == real,
occurs(Op,(add_real1,mult_real1,minus_real1,div_real1)),
- !,
+ (occurs(Op,(mult_real1,div_real1)) ->
+ not_zero(C)
+ ; true),!,
(occurs(Op,(minus_real1,div_real1)) ->
Only_arg1 = 1
; true),
@@ -5474,12 +5476,7 @@ bin_op_real_ineq(Type,Op,A,B,C) :-
; op_rel(Rel0,Rel)))
->
(Rel == '=' ->
- Goal1 = protected_unify(O1,O2),
- (Op == mult_real1 ->
- (not_zero(C) ->
- Goal = Goal1
- ; true)
- ; Goal = Goal1)
+ Goal = protected_unify(O1,O2)
; get_rel_between_real_args(O1,O2,Rel12),
(Rel == '<' ->
not occurs(Rel12,('=','>')),
@@ -10407,22 +10404,14 @@ launch_delta_mult_real_pos_pos(Type,A,B,C) :-
mult_float_nearest(Type,A,HB,HC0),
(A < 1.0 ->
% on avance de C vers B
- get_number_of_floats_between(Type,LC0,LB,LD1),
- %get_number_of_floats_between(Type,LC,LB,LD2),
- get_number_of_floats_between(Type,HC0,HB,HD1),
- %get_number_of_floats_between(Type,HC,HB,HD2),
- %LD is min([LD1,LD2,HD1,HD2]),
- %HD is max([LD1,LD2,HD1,HD2]),
+ LD1 is get_number_of_floats_between(Type,LC0,LB) - 1,
+ HD1 is get_number_of_floats_between(Type,HC0,HB) - 1,
LD is min([LD1,HD1]),
HD is max([LD1,HD1]),
launch_delta(C,B,+,LD..HD)
; % on avance de B vers C
- get_number_of_floats_between(Type,LB,LC0,LD1),
- %get_number_of_floats_between(Type,LB,LC,LD2),
- get_number_of_floats_between(Type,HB,HC0,HD1),
- %get_number_of_floats_between(Type,HB,HC,HD2),
- %LD is min([LD1,LD2,HD1,HD2]),
- %HD is max([LD1,LD2,HD1,HD2]),
+ LD1 is get_number_of_floats_between(Type,LB,LC0) - 1,
+ HD1 is get_number_of_floats_between(Type,HB,HC0) - 1,
LD is min([LD1,HD1]),
HD is max([LD1,HD1]),
launch_delta(B,C,+,LD..HD))
diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl
index 4aabed91c..1fdbb2e86 100644
--- a/Src/COLIBRI/solve.pl
+++ b/Src/COLIBRI/solve.pl
@@ -3869,10 +3869,10 @@ diff_reif(Type,Kill,A,B,Bool) :-
!,
diff_reif_array(Type,Kill,A,B,Bool).
diff_reif(Type,Kill,A,A,Bool) ?- !,
- Kill = 0,
+ protected_unify(Kill,0),
protected_unify(Bool,0).
diff_reif(Type,Kill,A,B,0) ?- !,
- Kill = 0,
+ protected_unify(Kill,0),
protected_unify(A,B).
diff_reif(Type,Kill,A,B,Bool) :-
ground(A),
--
GitLab