Skip to content

Commit 4357d15

Browse files
author
Christian Schulte
committed
Now all float constraints restrict their variable domains when being posted
1 parent 5b76309 commit 4357d15

File tree

11 files changed

+132
-64
lines changed

11 files changed

+132
-64
lines changed

‎changelog.in‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,15 @@ Date: TBD
6868
[DESCRIPTION]
6969
Changes
7070

71+
[ENTRY]
72+
Module: float
73+
What: change
74+
Rank: major
75+
Thanks: Kurt Van Den Branden
76+
[DESCRIPTION]
77+
All constraints over float variables now constrain their
78+
variables when being posted to avoid overflow.
79+
7180
[ENTRY]
7281
Module: float
7382
What: change

‎gecode/float/arithmetic/abs.hpp‎

100644100755
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,13 @@ namespace Gecode { namespace Float { namespace Arithmetic {
4545
template<class A, class B>
4646
ExecStatus
4747
Abs<A,B>::post(Home home, A x0, B x1) {
48+
GECODE_ME_CHECK(x1.eq(home,abs(x0.val())));
49+
if (x0.min() >= 0)
50+
GECODE_ME_CHECK(x0.eq(home,FloatVal(x1.min(), x1.max())));
51+
else if (x0.max() <= 0)
52+
GECODE_ME_CHECK(x0.eq(home,FloatVal(-x1.max(), -x1.min())));
53+
else
54+
GECODE_ME_CHECK(x0.eq(home,FloatVal(-x1.max(), x1.max())));
4855
(void) new (home) Abs<A,B>(home,x0,x1);
4956
return ES_OK;
5057
}

‎gecode/float/arithmetic/div.hpp‎

100644100755
Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,8 @@ namespace Gecode { namespace Float { namespace Arithmetic {
5858
template<class A, class B, class C>
5959
ExecStatus
6060
Div<A,B,C>::post(Home home, A x0, B x1, C x2) {
61+
GECODE_ME_CHECK(x2.eq(home,x0.domain() / x1.domain()));
62+
GECODE_ME_CHECK(x0.eq(home,x2.domain() * x1.domain()));
6163
(void) new (home) Div<A,B,C>(home,x0,x1,x2);
6264
return ES_OK;
6365
}

‎gecode/float/arithmetic/min-max.hpp‎

100644100755
Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,9 @@ namespace Gecode { namespace Float { namespace Arithmetic {
6666
template<class A, class B, class C>
6767
ExecStatus
6868
Min<A,B,C>::post(Home home, A x0, B x1, C x2) {
69+
GECODE_ME_CHECK(x2.eq(home,min(x0.domain(),x1.domain())));
70+
GECODE_ME_CHECK(x0.gq(home,x2.min()));
71+
GECODE_ME_CHECK(x1.gq(home,x2.min()));
6972
(void) new (home) Min<A,B,C>(home,x0,x1,x2);
7073
return ES_OK;
7174
}
@@ -115,6 +118,9 @@ namespace Gecode { namespace Float { namespace Arithmetic {
115118
template<class A, class B, class C>
116119
ExecStatus
117120
Max<A,B,C>::post(Home home, A x0, B x1, C x2) {
121+
GECODE_ME_CHECK(x2.eq(home,max(x0.domain(),x1.domain())));
122+
GECODE_ME_CHECK(x0.lq(home,x2.max()));
123+
GECODE_ME_CHECK(x1.lq(home,x2.max()));
118124
(void) new (home) Max<A,B,C>(home,x0,x1,x2);
119125
return ES_OK;
120126
}

‎gecode/float/arithmetic/pow-nroot.hpp‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -134,6 +134,8 @@ namespace Gecode { namespace Float { namespace Arithmetic {
134134
NthRoot<A,B>::post(Home home, A x0, B x1, int n) {
135135
if (n == 0) return ES_FAILED;
136136
GECODE_ME_CHECK(x0.gq(home,0.0));
137+
GECODE_ME_CHECK(x1.eq(home,nroot(x0.domain(),n)));
138+
GECODE_ME_CHECK(x0.eq(home,pow(x1.domain(),n)));
137139
(void) new (home) NthRoot<A,B>(home,x0,x1,n);
138140
return ES_OK;
139141
}

‎gecode/float/channel/channel.hpp‎

100644100755
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,9 @@ namespace Gecode { namespace Float { namespace Channel {
5656
Channel<A,B>::post(Home home, A x0, B x1) {
5757
GECODE_ME_CHECK(x0.eq(home,FloatVal(Int::Limits::min,
5858
Int::Limits::max)));
59+
GECODE_ME_CHECK(x1.gq(home,static_cast<int>(std::ceil(x0.min()))));
60+
GECODE_ME_CHECK(x1.lq(home,static_cast<int>(std::floor(x0.max()))));
61+
GECODE_ME_CHECK(x0.eq(home,FloatVal(x1.min(),x1.max())));
5962
(void) new (home) Channel<A,B>(home,x0,x1);
6063
return ES_OK;
6164
}

‎gecode/float/transcendental/exp-log.hpp‎

100644100755
Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,10 @@ namespace Gecode { namespace Float { namespace Transcendental {
5151
} else {
5252
GECODE_ME_CHECK(x1.gq(home,0.0));
5353
}
54-
54+
GECODE_ME_CHECK(x1.eq(home,exp(x0.domain())));
55+
if (x1.max() == 0.0)
56+
return ES_FAILED;
57+
GECODE_ME_CHECK(x0.eq(home,log(x1.domain())));
5558
(void) new (home) Exp<A,B>(home,x0,x1);
5659
return ES_OK;
5760
}
@@ -98,6 +101,10 @@ namespace Gecode { namespace Float { namespace Transcendental {
98101
GECODE_ME_CHECK(x0.eq(home,0.0));
99102
} else {
100103
GECODE_ME_CHECK(x1.gq(home,0.0));
104+
if (x1.max() == 0.0)
105+
return ES_FAILED;
106+
GECODE_ME_CHECK(x0.eq(home,log(x1.domain())/log(base)));
107+
GECODE_ME_CHECK(x1.eq(home,exp(x0.domain()*log(base))));
101108
(void) new (home) Pow<A,B>(home,base,x0,x1);
102109
}
103110
return ES_OK;

‎gecode/float/trigonometric.hh‎

100644100755
Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,8 @@ namespace Gecode { namespace Float { namespace Trigonometric {
5555
protected:
5656
using MixBinaryPropagator<A,PC_FLOAT_BND,B,PC_FLOAT_BND>::x0;
5757
using MixBinaryPropagator<A,PC_FLOAT_BND,B,PC_FLOAT_BND>::x1;
58-
58+
/// Perform actual propagation
59+
static ExecStatus dopropagate(Space& home, A x0, B x1);
5960
/// Constructor for cloning \a p
6061
Sin(Space& home, Sin& p);
6162
/// Constructor for creation
@@ -83,7 +84,8 @@ namespace Gecode { namespace Float { namespace Trigonometric {
8384
protected:
8485
using MixBinaryPropagator<A,PC_FLOAT_BND,B,PC_FLOAT_BND>::x0;
8586
using MixBinaryPropagator<A,PC_FLOAT_BND,B,PC_FLOAT_BND>::x1;
86-
87+
/// Perform actual propagation
88+
static ExecStatus dopropagate(Space& home, A x0, B x1);
8789
/// Constructor for cloning \a p
8890
Cos(Space& home, Cos& p);
8991
/// Constructor for creation
@@ -165,7 +167,8 @@ namespace Gecode { namespace Float { namespace Trigonometric {
165167
protected:
166168
using MixBinaryPropagator<A,PC_FLOAT_BND,B,PC_FLOAT_BND>::x0;
167169
using MixBinaryPropagator<A,PC_FLOAT_BND,B,PC_FLOAT_BND>::x1;
168-
170+
/// Perform actual propagation
171+
static ExecStatus dopropagate(Space& home, A x0, B x1);
169172
/// Constructor for cloning \a p
170173
Tan(Space& home, Tan& p);
171174
/// Constructor for creation

‎gecode/float/trigonometric/asinacos.hpp‎

100644100755
Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,8 @@ namespace Gecode { namespace Float { namespace Trigonometric {
5151
} else {
5252
GECODE_ME_CHECK(x0.gq(home,-1.0));
5353
GECODE_ME_CHECK(x0.lq(home,1.0));
54+
GECODE_ME_CHECK(x1.eq(home,asin(x0.domain())));
55+
GECODE_ME_CHECK(x0.eq(home,sin(x1.domain())));
5456
(void) new (home) ASin<A,B>(home,x0,x1);
5557
}
5658
return ES_OK;
@@ -102,6 +104,8 @@ namespace Gecode { namespace Float { namespace Trigonometric {
102104
} else {
103105
GECODE_ME_CHECK(x0.gq(home,-1.0));
104106
GECODE_ME_CHECK(x0.lq(home,1.0));
107+
GECODE_ME_CHECK(x1.eq(home,acos(x0.domain())));
108+
GECODE_ME_CHECK(x0.eq(home,cos(x1.domain())));
105109
(void) new (home) ACos<A,B>(home,x0,x1);
106110
}
107111
return ES_OK;

‎gecode/float/trigonometric/sincos.hpp‎

100644100755
Lines changed: 45 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -115,6 +115,26 @@ void aSinProject(Rounding& r, const V& aSinIv, FloatNum& iv_min, FloatNum& iv_ma
115115
*
116116
*/
117117

118+
template<class A, class B>
119+
ExecStatus
120+
Sin<A,B>::dopropagate(Space& home, A x0, B x1) {
121+
GECODE_ME_CHECK(x1.eq(home,sin(x0.val())));
122+
Rounding r;
123+
int n_min = 2*static_cast<int>(r.div_up(x0.min(), pi_twice_upper()));
124+
int n_max = 2*static_cast<int>(r.div_up(x0.max(), pi_twice_upper()));
125+
if (x0.min() < 0) n_min-=2;
126+
if (x0.max() < 0) n_max-=2;
127+
FloatNum iv_min = r.sub_down(x0.min(),r.mul_down(n_min, pi_upper()));
128+
FloatNum iv_max = r.sub_up (x0.max(),r.mul_down(n_max, pi_upper()));
129+
aSinProject(r,x1,iv_min,iv_max,n_min,n_max);
130+
FloatNum n_iv_min = r.add_down(iv_min,r.mul_down(n_min, pi_upper()));
131+
FloatNum n_iv_max = r.add_up (iv_max,r.mul_down(n_max, pi_upper()));
132+
if (n_iv_min > n_iv_max) return ES_FAILED;
133+
GECODE_ME_CHECK(x0.eq(home,FloatVal(n_iv_min,n_iv_max)));
134+
GECODE_ME_CHECK(x1.eq(home,sin(x0.val()))); // Redo sin because with x0 reduction, sin may be more accurate
135+
return ES_OK;
136+
}
137+
118138
template<class A, class B>
119139
forceinline
120140
Sin<A,B>::Sin(Home home, A x0, B x1)
@@ -128,6 +148,7 @@ void aSinProject(Rounding& r, const V& aSinIv, FloatNum& iv_min, FloatNum& iv_ma
128148
} else {
129149
GECODE_ME_CHECK(x1.gq(home,-1.0));
130150
GECODE_ME_CHECK(x1.lq(home,1.0));
151+
GECODE_ES_CHECK(dopropagate(home,x0,x1));
131152
(void) new (home) Sin<A,B>(home,x0,x1);
132153
}
133154

@@ -149,20 +170,7 @@ void aSinProject(Rounding& r, const V& aSinIv, FloatNum& iv_min, FloatNum& iv_ma
149170
template<class A, class B>
150171
ExecStatus
151172
Sin<A,B>::propagate(Space& home, const ModEventDelta&) {
152-
GECODE_ME_CHECK(x1.eq(home,sin(x0.val())));
153-
Rounding r;
154-
int n_min = 2*static_cast<int>(r.div_up(x0.min(), pi_twice_upper()));
155-
int n_max = 2*static_cast<int>(r.div_up(x0.max(), pi_twice_upper()));
156-
if (x0.min() < 0) n_min-=2;
157-
if (x0.max() < 0) n_max-=2;
158-
FloatNum iv_min = r.sub_down(x0.min(),r.mul_down(n_min, pi_upper()));
159-
FloatNum iv_max = r.sub_up (x0.max(),r.mul_down(n_max, pi_upper()));
160-
aSinProject(r,x1,iv_min,iv_max,n_min,n_max);
161-
FloatNum n_iv_min = r.add_down(iv_min,r.mul_down(n_min, pi_upper()));
162-
FloatNum n_iv_max = r.add_up (iv_max,r.mul_down(n_max, pi_upper()));
163-
if (n_iv_min > n_iv_max) return ES_FAILED;
164-
GECODE_ME_CHECK(x0.eq(home,FloatVal(n_iv_min,n_iv_max)));
165-
GECODE_ME_CHECK(x1.eq(home,sin(x0.val()))); // Redo sin because with x0 reduction, sin may be more accurate
173+
GECODE_ES_CHECK(dopropagate(home,x0,x1));
166174
return (x0.assigned()) ? home.ES_SUBSUMED(*this) : ES_FIX;
167175
}
168176

@@ -171,6 +179,27 @@ void aSinProject(Rounding& r, const V& aSinIv, FloatNum& iv_min, FloatNum& iv_ma
171179
*
172180
*/
173181

182+
template<class A, class B>
183+
ExecStatus
184+
Cos<A,B>::dopropagate(Space& home, A x0, B x1) {
185+
GECODE_ME_CHECK(x1.eq(home,cos(x0.val())));
186+
Rounding r;
187+
FloatVal x0Trans = x0.val() + FloatVal::pi_half();
188+
int n_min = 2*static_cast<int>(r.div_up(x0Trans.min(), pi_twice_upper()));
189+
int n_max = 2*static_cast<int>(r.div_up(x0Trans.max(), pi_twice_upper()));
190+
if (x0Trans.min() < 0) n_min-=2;
191+
if (x0Trans.max() < 0) n_max-=2;
192+
FloatNum iv_min = r.sub_down(x0Trans.min(),r.mul_down(n_min, pi_upper()));
193+
FloatNum iv_max = r.sub_up (x0Trans.max(),r.mul_down(n_max, pi_upper()));
194+
aSinProject(r,x1,iv_min,iv_max,n_min,n_max);
195+
FloatNum n_iv_min = r.add_down(iv_min,r.mul_down(n_min, pi_upper()));
196+
FloatNum n_iv_max = r.add_up (iv_max,r.mul_down(n_max, pi_upper()));
197+
if (n_iv_min > n_iv_max) return ES_FAILED;
198+
GECODE_ME_CHECK(x0.eq(home,FloatVal(n_iv_min,n_iv_max) - FloatVal::pi_half()));
199+
GECODE_ME_CHECK(x1.eq(home,cos(x0.val()))); // Redo sin because with x0 reduction, sin may be more accurate
200+
return ES_OK;
201+
}
202+
174203
template<class A, class B>
175204
forceinline
176205
Cos<A,B>::Cos(Home home, A x0, B x1)
@@ -190,6 +219,7 @@ void aSinProject(Rounding& r, const V& aSinIv, FloatNum& iv_min, FloatNum& iv_ma
190219
} else {
191220
GECODE_ME_CHECK(x1.gq(home,-1.0));
192221
GECODE_ME_CHECK(x1.lq(home,1.0));
222+
GECODE_ES_CHECK(dopropagate(home,x0,x1));
193223
(void) new (home) Cos<A,B>(home,x0,x1);
194224
}
195225
return ES_OK;
@@ -210,21 +240,7 @@ void aSinProject(Rounding& r, const V& aSinIv, FloatNum& iv_min, FloatNum& iv_ma
210240
template<class A, class B>
211241
ExecStatus
212242
Cos<A,B>::propagate(Space& home, const ModEventDelta&) {
213-
GECODE_ME_CHECK(x1.eq(home,cos(x0.val())));
214-
Rounding r;
215-
FloatVal x0Trans = x0.val() + FloatVal::pi_half();
216-
int n_min = 2*static_cast<int>(r.div_up(x0Trans.min(), pi_twice_upper()));
217-
int n_max = 2*static_cast<int>(r.div_up(x0Trans.max(), pi_twice_upper()));
218-
if (x0Trans.min() < 0) n_min-=2;
219-
if (x0Trans.max() < 0) n_max-=2;
220-
FloatNum iv_min = r.sub_down(x0Trans.min(),r.mul_down(n_min, pi_upper()));
221-
FloatNum iv_max = r.sub_up (x0Trans.max(),r.mul_down(n_max, pi_upper()));
222-
aSinProject(r,x1,iv_min,iv_max,n_min,n_max);
223-
FloatNum n_iv_min = r.add_down(iv_min,r.mul_down(n_min, pi_upper()));
224-
FloatNum n_iv_max = r.add_up (iv_max,r.mul_down(n_max, pi_upper()));
225-
if (n_iv_min > n_iv_max) return ES_FAILED;
226-
GECODE_ME_CHECK(x0.eq(home,FloatVal(n_iv_min,n_iv_max) - FloatVal::pi_half()));
227-
GECODE_ME_CHECK(x1.eq(home,cos(x0.val()))); // Redo sin because with x0 reduction, sin may be more accurate
243+
GECODE_ES_CHECK(dopropagate(home,x0,x1));
228244
return (x0.assigned()) ? home.ES_SUBSUMED(*this) : ES_FIX;
229245
}
230246

0 commit comments

Comments
 (0)