diff: clpr division and \==
Fergus Henderson
fjh at kryten.cs.mu.OZ.AU
Sat Sep 6 21:25:12 AEST 1997
clpr/cfloat.m:
clpr/cfloat_float.m:
clpr/float_cfloat.m:
Add disequality constraints (\==).
Fix division so that it handles division by zero properly;
in particular, define `X/Y=Z' as if by `X=Y*Z, Y\==Z'
rather than just `X=Y*Z', since the latter breaks referential
transparency.
clpr/cfloat.m:
Remove the calls to save_transient_registers() and
restore_transient_registers() from MR_cfloat_maybe_trail_solver(),
because they are not needed.
cvs diff: Diffing .
Index: Mmakefile
===================================================================
RCS file: /home/mercury1/repository/clpr/Mmakefile,v
retrieving revision 1.3
diff -u -u -r1.3 Mmakefile
--- 1.3 1997/09/04 02:57:26
+++ Mmakefile 1997/09/06 09:50:04
@@ -25,6 +25,9 @@
MLFLAGS = -g
RM_C = :
+# The CLP(R) headers are missing lots of prototypes, so disable that warning...
+MGNUCFLAGS += -Wno-strict-prototypes -Wno-traditional
+
# Link in the CLP(R) library
MLLIBS = -Lclpr -lclpr $(EXTRA_MLLIBS)
Index: cfloat.m
===================================================================
RCS file: /home/mercury1/repository/clpr/cfloat.m,v
retrieving revision 1.8
diff -u -u -r1.8 cfloat.m
--- 1.8 1997/09/04 21:37:14
+++ cfloat.m 1997/09/06 09:59:27
@@ -70,6 +70,13 @@
:- mode '=='(ca, co) is det.
:- mode '=='(co, co) is det.
+ % disequality
+:- pred \==(cfloat, cfloat).
+:- mode \==(ca, ca) is semidet.
+:- mode \==(co, ca) is det.
+:- mode \==(ca, co) is det.
+:- mode \==(co, co) is det.
+
% addition
:- func '+'(cfloat, cfloat) = cfloat.
:- mode '+'(ca, ca) = ca is semidet.
@@ -104,24 +111,14 @@
:- mode '*'(co, co) = co is det.
% division
- %
- % BEWARE:
- % The semantics OUGHT to be X / Y = Z <=> Y \= 0, X = Y * Z.
- % But that turns ought to be difficult to implement, because
- % the underlying CLP(R) constraint solver doesn't support
- % disequality constraints (\=).
- % Hence the current implementation of division is BROKEN.
- % Currently we use X / Y = Z <=> X = Y * Z, but that
- % breaks referential transparency, because the term X/X
- % has an infinite set of values for X == 0.0.
- %
+ % X / Y = Z :- X = Y * Z, Y \== 0.
:- func '/'(cfloat, cfloat) = cfloat.
:- mode '/'(ca, ca) = ca is semidet.
:- mode '/'(ca, co) = ca is semidet. % semidet since eg. 0/X=1 fails
:- mode '/'(co, ca) = ca is semidet. % semidet since eg. X/0=1 fails
:- mode '/'(ca, ca) = co is semidet. % semidet since eg. 1/0=Y fails
:- mode '/'(co, co) = ca is det.
-:- mode '/'(ca, co) = co is det.
+:- mode '/'(ca, co) = co is semidet. % XXX really det
:- mode '/'(co, ca) = co is semidet. % semidet since eg. X/0=Y fails
:- mode '/'(co, co) = co is det.
@@ -242,6 +239,13 @@
:- mode cfloat__eq(ca, co) is det.
:- mode cfloat__eq(co, co) is det.
+ % X \= Y
+:- pred cfloat__diseq(cfloat, cfloat).
+:- mode cfloat__diseq(ca, ca) is semidet.
+:- mode cfloat__diseq(co, ca) is det.
+:- mode cfloat__diseq(ca, co) is det.
+:- mode cfloat__diseq(co, co) is det.
+
% cfloat__plus(X, Y, Z) is true iff X+Y=Z
:- pred cfloat__plus(cfloat, cfloat, cfloat).
:- mode cfloat__plus(ca, ca, ca) is semidet.
@@ -275,17 +279,6 @@
:- mode cfloat__mult(co, ca, co) is det.
:- mode cfloat__mult(co, co, co) is det.
- % X/Y = Z
-:- pred cfloat__div(cfloat, cfloat, cfloat).
-:- mode cfloat__div(ca, ca, ca) is semidet.
-:- mode cfloat__div(ca, co, ca) is semidet. % semidet since eg. 0/X=1 fails
-:- mode cfloat__div(co, ca, ca) is semidet. % semidet since eg. X/0=1 fails
-:- mode cfloat__div(ca, ca, co) is semidet. % semidet since eg. 1/0=Y fails
-:- mode cfloat__div(co, co, ca) is det.
-:- mode cfloat__div(ca, co, co) is det.
-:- mode cfloat__div(co, ca, co) is semidet. % semidet since eg. X/0=Y fails
-:- mode cfloat__div(co, co, co) is det.
-
%-----------------------------------------------------------------------------%
% The following predicates are used to implement the operators
@@ -296,6 +289,11 @@
:- mode cfloat__eq_float(ca, in) is semidet.
:- mode cfloat__eq_float(co, in) is det.
+ % X \= Y
+:- pred cfloat__diseq_float(cfloat, float).
+:- mode cfloat__diseq_float(ca, in) is semidet.
+:- mode cfloat__diseq_float(co, in) is det.
+
% X+Y=Z
:- pred cfloat__plus_float(cfloat, float, cfloat).
:- mode cfloat__plus_float(ca, in, ca) is semidet.
@@ -318,11 +316,12 @@
:- mode cfloat__mult_float(co, in, co) is det.
% X/Y = Z
+ % reports a runtime error if Y = 0.
:- pred cfloat__div_float(cfloat, float, cfloat).
:- mode cfloat__div_float(ca, in, ca) is semidet.
-:- mode cfloat__div_float(co, in, ca) is semidet. % since eg. X/0=1 fails
-:- mode cfloat__div_float(ca, in, co) is semidet. % since eg. 1/0=Y fails
-:- mode cfloat__div_float(co, in, co) is semidet. % since eg. X/0=Y fails
+:- mode cfloat__div_float(co, in, ca) is det.
+:- mode cfloat__div_float(ca, in, co) is det.
+:- mode cfloat__div_float(co, in, co) is det.
% X > Y
:- pred cfloat__gt_float(cfloat, float).
@@ -353,11 +352,12 @@
%----------------------------------------------------------------------------%
X == Y :- cfloat__eq(X, Y).
+X \== Y :- cfloat__diseq(X, Y).
- X = 0.0 - X.
X + Y = Z :- cfloat__plus(X, Y, Z).
X - Y = Z :- cfloat__minus(X, Y, Z).
X * Y = Z :- cfloat__mult(X, Y, Z).
-X / Y = Z :- cfloat__div(X, Y, Z).
+X / Y = Z :- Y \== 0.0, X = Y * Z.
%----------------------------------------------------------------------------%
@@ -397,9 +397,7 @@
#define ML_cfloat_maybe_trail_solver() \\
( stamp != MR_current_choicepoint_id() ? ( \\
- save_transient_registers(), \\
ML_cfloat_trail_solver(), \\
- restore_transient_registers(), \\
(void)0 \\
) : ( \\
(void)0 \\
@@ -478,6 +476,8 @@
bool ML_cfloat_eq(ML_svar, ML_svar);
bool ML_cfloat_eq_float(ML_svar, Float);
+/* bool ML_cfloat_diseq(ML_svar, ML_svar, bool&); */
+/* bool ML_cfloat_diseq_float(ML_svar, Float, bool&); */
bool ML_cfloat_gt(ML_svar, ML_svar);
bool ML_cfloat_gt_float(ML_svar, Float);
bool ML_cfloat_lt(ML_svar, ML_svar);
@@ -492,7 +492,6 @@
bool ML_cfloat_minus_float(ML_svar, Float, ML_svar);
bool ML_cfloat_mult(ML_svar, ML_svar, ML_svar);
bool ML_cfloat_mult_float(ML_svar, Float, ML_svar);
-bool ML_cfloat_div(ML_svar, ML_svar, ML_svar);
bool ML_cfloat_div_float(ML_svar, Float, ML_svar);
bool ML_cfloat_min(ML_svar, ML_svar, ML_svar);
bool ML_cfloat_max(ML_svar, ML_svar, ML_svar);
@@ -535,6 +534,40 @@
)
/*
+** Svar1 \\= Svar2 :-
+** Svar1 - Svar2 = Diff,
+** abs(Diff) = AbsDiff,
+** AbsDiff > 0.
+*/
+#define ML_cfloat_diseq(Svar1, Svar2, result) \\
+ do { \\
+ Word Diff, AbsDiff; \\
+ \\
+ ML_cfloat_init_solver_var(Diff); \\
+ ML_cfloat_init_solver_var(AbsDiff); \\
+ (void) ML_cfloat_minus((Svar1), (Svar2), Diff); \\
+ (void) ML_cfloat_abs(Diff, AbsDiff); \\
+ (result) = ML_cfloat_gt_float(AbsDiff, 0.0); \\
+ } while(0)
+
+/*
+** Svar \\= Val :-
+** Svar - Val = Diff,
+** abs(Diff) = AbsDiff,
+** AbsDiff > 0.
+*/
+#define ML_cfloat_diseq_float(Svar, Val, result) \\
+ do { \\
+ Word Diff, AbsDiff; \\
+ \\
+ ML_cfloat_init_solver_var(Diff); \\
+ ML_cfloat_init_solver_var(AbsDiff); \\
+ (void) ML_cfloat_minus_float((Svar), (Val), Diff); \\
+ (void) ML_cfloat_abs(Diff, AbsDiff); \\
+ (result) = ML_cfloat_gt_float(AbsDiff, 0.0); \\
+ } while(0)
+
+/*
** Svar1 + Svar2 = Svar3 :-
** 1.0*Svar1 + 1.0*Svar2 + -1.0*Svar3 = 0.0.
*/
@@ -615,24 +648,27 @@
)
/*
-** Svar1 / Svar2 = Svar3 :-
-** Svar3 * Svar2 = Svar1.
-*/
-#define ML_cfloat_div(Svar1, Svar2, Svar3) \\
- ML_cfloat_mult(Svar3, Svar2, Svar1)
-
-/*
** Svar1 / Val = Svar2 :-
-** (1.0/Val)*Svar1 + -1.0*Svar2 = 0.0.
+** ( Val = 0 ->
+** error(""division by zero"")
+** ;
+** (1.0/Val)*Svar1 + -1.0*Svar2 = 0.0
+** ).
+** Note that we need to explicitly check for division by zero,
+** because on some platforms the call to 1.0/Val will just return
+** infinity, rather than a run-time error (floating point exception).
*/
#define ML_cfloat_div_float(Svar1, Val, Svar2) \\
- ( \\
+ ( Val == 0 ? ( \\
+ fatal_error(""division by zero""), \\
+ FALSE \\
+ ) : ( \\
ML_cfloat_maybe_trail_solver(), \\
init_eqn(), \\
s_evar(1.0 / (double) Val, Svar1), \\
s_evar(-1.0, Svar2), \\
/* return */ s_econ(0.0) \\
- )
+ ) )
/*
** Svar1 > Svar2 :-
@@ -690,7 +726,7 @@
** Svar1 > Val :-
** 1.0*Svar1 > Val.
*/
-#define ML_cfloat_gt_float(Svar1, Val) \\
+#define ML_cfloat_gt_float(Svar, Val) \\
( \\
ML_cfloat_maybe_trail_solver(), \\
init_eqn(), \\
@@ -702,7 +738,7 @@
** Svar >= Val :-
** 1.0*Svar >= Val.
*/
-#define ML_cfloat_ge_float(Svar1, Val) \\
+#define ML_cfloat_ge_float(Svar, Val) \\
( \\
ML_cfloat_maybe_trail_solver(), \\
init_eqn(), \\
@@ -1062,52 +1098,6 @@
").
-:- pragma c_code(cfloat__div(Svar1::ca, Svar2::ca, Svar3::ca),
- "
- SUCCESS_INDICATOR = ML_cfloat_div(Svar1, Svar2, Svar3);
- ").
-:- pragma c_code(cfloat__div(Svar1::co, Svar2::ca, Svar3::ca),
- "
- ML_cfloat_init_solver_var(Svar1);
- SUCCESS_INDICATOR = ML_cfloat_div(Svar1, Svar2, Svar3);
- ").
-:- pragma c_code(cfloat__div(Svar1::ca, Svar2::co, Svar3::ca),
- "
- ML_cfloat_init_solver_var(Svar2);
- SUCCESS_INDICATOR = ML_cfloat_div(Svar1, Svar2, Svar3);
- ").
-:- pragma c_code(cfloat__div(Svar1::ca, Svar2::ca, Svar3::co),
- "
- ML_cfloat_init_solver_var(Svar3);
- SUCCESS_INDICATOR = ML_cfloat_div(Svar1, Svar2, Svar3);
- ").
-:- pragma c_code(cfloat__div(Svar1::co, Svar2::co, Svar3::ca),
- "
- ML_cfloat_init_solver_var(Svar1);
- ML_cfloat_init_solver_var(Svar2);
- (void) ML_cfloat_div(Svar1, Svar2, Svar3);
- ").
-:- pragma c_code(cfloat__div(Svar1::co, Svar2::ca, Svar3::co),
- "
- ML_cfloat_init_solver_var(Svar1);
- ML_cfloat_init_solver_var(Svar3);
- SUCCESS_INDICATOR = ML_cfloat_div(Svar1, Svar2, Svar3);
- ").
-:- pragma c_code(cfloat__div(Svar1::ca, Svar2::co, Svar3::co),
- "
- ML_cfloat_init_solver_var(Svar2);
- ML_cfloat_init_solver_var(Svar3);
- (void) ML_cfloat_div(Svar1, Svar2, Svar3);
- ").
-:- pragma c_code(cfloat__div(Svar1::co, Svar2::co, Svar3::co),
- "
- ML_cfloat_init_solver_var(Svar1);
- ML_cfloat_init_solver_var(Svar2);
- ML_cfloat_init_solver_var(Svar3);
- (void) ML_cfloat_div(Svar1, Svar2, Svar3);
- ").
-
-
:- pragma c_code(cfloat__div_float(Svar1::ca, Val::in, Svar2::ca),
"
SUCCESS_INDICATOR = ML_cfloat_div_float(Svar1, Val, Svar2);
@@ -1115,18 +1105,18 @@
:- pragma c_code(cfloat__div_float(Svar1::co, Val::in, Svar2::ca),
"
ML_cfloat_init_solver_var(Svar1);
- SUCCESS_INDICATOR = ML_cfloat_div_float(Svar1, Val, Svar2);
+ (void) ML_cfloat_div_float(Svar1, Val, Svar2);
").
:- pragma c_code(cfloat__div_float(Svar1::ca, Val::in, Svar2::co),
"
ML_cfloat_init_solver_var(Svar2);
- SUCCESS_INDICATOR = ML_cfloat_div_float(Svar1, Val, Svar2);
+ (void) ML_cfloat_div_float(Svar1, Val, Svar2);
").
:- pragma c_code(cfloat__div_float(Svar1::co, Val::in, Svar2::co),
"
ML_cfloat_init_solver_var(Svar1);
ML_cfloat_init_solver_var(Svar2);
- SUCCESS_INDICATOR = ML_cfloat_div_float(Svar1, Val, Svar2);
+ (void) ML_cfloat_div_float(Svar1, Val, Svar2);
").
%-----------------------------------------------------------------------------%
@@ -1158,6 +1148,46 @@
ML_cfloat_init_solver_var(Svar);
SUCCESS_INDICATOR = ML_cfloat_eq_float(Svar, Val);
").
+
+
+:- pragma c_code(cfloat__diseq(Svar1::ca, Svar2::ca),
+ "{
+ ML_cfloat_diseq(Svar1, Svar2, SUCCESS_INDICATOR);
+ }").
+:- pragma c_code(cfloat__diseq(Svar1::co, Svar2::ca),
+ "{
+ bool result;
+ ML_cfloat_init_solver_var(Svar1);
+ ML_cfloat_diseq(Svar1, Svar2, result);
+ (void) result; /* result not used */
+ }").
+:- pragma c_code(cfloat__diseq(Svar1::ca, Svar2::co),
+ "{
+ bool result;
+ ML_cfloat_init_solver_var(Svar2);
+ ML_cfloat_diseq(Svar1, Svar2, result);
+ (void) result; /* result not used */
+ }").
+:- pragma c_code(cfloat__diseq(Svar1::co, Svar2::co),
+ "{
+ bool result;
+ ML_cfloat_init_solver_var(Svar1);
+ ML_cfloat_init_solver_var(Svar2);
+ ML_cfloat_diseq(Svar1, Svar2, result);
+ (void) result; /* result not used */
+ }").
+
+:- pragma c_code(cfloat__diseq_float(Svar::ca, Val::in),
+ "{
+ ML_cfloat_diseq_float(Svar, Val, SUCCESS_INDICATOR);
+ }").
+:- pragma c_code(cfloat__diseq_float(Svar::co, Val::in),
+ "{
+ bool result;
+ ML_cfloat_init_solver_var(Svar);
+ ML_cfloat_diseq_float(Svar, Val, result);
+ (void) result; /* result not used */
+ }").
%-----------------------------------------------------------------------------%
Index: cfloat_float.m
===================================================================
RCS file: /home/mercury1/repository/clpr/cfloat_float.m,v
retrieving revision 1.1
diff -u -u -r1.1 cfloat_float.m
--- 1.1 1997/08/27 17:11:09
+++ cfloat_float.m 1997/09/06 09:13:53
@@ -26,6 +26,11 @@
:- mode ==(ca, in) is semidet.
:- mode ==(co, in) is det.
+ % cfloat-float disequality
+:- pred \==(cfloat, float).
+:- mode \==(ca, in) is semidet.
+:- mode \==(co, in) is det.
+
% addition
:- func '+'(cfloat, float) = cfloat.
:- mode '+'(ca, in) = ca is semidet.
@@ -48,11 +53,13 @@
:- mode '*'(co, in) = co is det.
% division
+ % note that division by a zero float results in a runtime error
+ % (whereas division by a zero cfloat just fails)
:- func '/'(cfloat, float) = cfloat.
:- mode '/'(ca, in) = ca is semidet.
-:- mode '/'(co, in) = ca is semidet. % semidet since eg. X/0=1 fails
-:- mode '/'(ca, in) = co is semidet. % semidet since eg. 1/0=Y fails
-:- mode '/'(co, in) = co is semidet. % semidet since eg. X/0=Y fails
+:- mode '/'(co, in) = ca is det.
+:- mode '/'(ca, in) = co is det.
+:- mode '/'(co, in) = co is det.
% X > Y
:- pred '>'(cfloat, float).
@@ -77,6 +84,7 @@
:- implementation.
X == Y :- cfloat__eq_float(X, Y).
+X \== Y :- cfloat__diseq_float(X, Y).
X + Y = Z :- cfloat__plus_float(X, Y, Z).
X - Y = Z :- cfloat__minus_float(X, Y, Z).
Index: float_cfloat.m
===================================================================
RCS file: /home/mercury1/repository/clpr/float_cfloat.m,v
retrieving revision 1.2
diff -u -u -r1.2 float_cfloat.m
--- 1.2 1997/09/04 21:37:16
+++ float_cfloat.m 1997/09/06 09:40:10
@@ -26,6 +26,11 @@
:- mode ==(in, ca) is semidet.
:- mode ==(in, co) is det.
+ % cfloat-float disequality
+:- pred \==(float, cfloat).
+:- mode \==(in, ca) is semidet.
+:- mode \==(in, co) is det.
+
% addition
:- func '+'(float, cfloat) = cfloat.
:- mode '+'(in, ca) = ca is semidet.
@@ -52,7 +57,7 @@
:- mode '/'(in, ca) = ca is semidet.
:- mode '/'(in, co) = ca is semidet. % semidet since eg. X/0=1 fails
:- mode '/'(in, ca) = co is semidet. % semidet since eg. 1/0=Y fails
-:- mode '/'(in, co) = co is det.
+:- mode '/'(in, co) = co is semidet. % XXX really det
% X > Y
:- pred '>'(float, cfloat).
@@ -77,11 +82,12 @@
:- implementation.
X == Y :- cfloat__eq_float(Y, X).
+X \== Y :- cfloat__diseq_float(Y, X).
X + Y = Z :- cfloat__plus_float(Y, X, Z).
-X - Y = Z :- X == Cfloat_X, Cfloat_X - Y = Z.
+X - Y = Z :- X == Cfloat_X, Cfloat_X - Y = Z. % not maximally efficient
X * Y = Z :- cfloat__mult_float(Y, X, Z).
-X / Y = Z :- X == Cfloat_X, Cfloat_X / Y = Z.
+X / Y = Z :- X == Cfloat_X, Cfloat_X / Y = Z. % not maximally efficient
X > Y :- cfloat__gt_float(Y, X).
X >= Y :- cfloat__ge_float(Y, X).
--
Fergus Henderson <fjh at cs.mu.oz.au> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3 | -- the last words of T. S. Garp.
More information about the developers
mailing list