lex.hpp
Go to the documentation of this file.
00001 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */ 00002 /* 00003 * Main authors: 00004 * Christian Schulte <schulte@gecode.org> 00005 * 00006 * Copyright: 00007 * Christian Schulte, 2003 00008 * 00009 * Last modified: 00010 * $Date: 2010-03-03 17:32:21 +0100 (Wed, 03 Mar 2010) $ by $Author: schulte $ 00011 * $Revision: 10364 $ 00012 * 00013 * This file is part of Gecode, the generic constraint 00014 * development environment: 00015 * http://www.gecode.org 00016 * 00017 * Permission is hereby granted, free of charge, to any person obtaining 00018 * a copy of this software and associated documentation files (the 00019 * "Software"), to deal in the Software without restriction, including 00020 * without limitation the rights to use, copy, modify, merge, publish, 00021 * distribute, sublicense, and/or sell copies of the Software, and to 00022 * permit persons to whom the Software is furnished to do so, subject to 00023 * the following conditions: 00024 * 00025 * The above copyright notice and this permission notice shall be 00026 * included in all copies or substantial portions of the Software. 00027 * 00028 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, 00029 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 00030 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND 00031 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE 00032 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION 00033 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION 00034 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 00035 * 00036 */ 00037 00038 namespace Gecode { namespace Int { namespace Rel { 00039 00040 template<class View> 00041 inline 00042 Lex<View>::Lex(Home home, 00043 ViewArray<View>& x0, ViewArray<View>& y0, bool s) 00044 : Propagator(home), x(x0), y(y0), strict(s) { 00045 x.subscribe(home, *this, PC_INT_BND); 00046 y.subscribe(home, *this, PC_INT_BND); 00047 } 00048 00049 template<class View> 00050 forceinline 00051 Lex<View>::Lex(Space& home, bool share, Lex<View>& p) 00052 : Propagator(home,share,p), strict(p.strict) { 00053 x.update(home,share,p.x); 00054 y.update(home,share,p.y); 00055 } 00056 00057 template<class View> 00058 Actor* 00059 Lex<View>::copy(Space& home, bool share) { 00060 return new (home) Lex<View>(home,share,*this); 00061 } 00062 00063 template<class View> 00064 PropCost 00065 Lex<View>::cost(const Space&, const ModEventDelta&) const { 00066 return PropCost::linear(PropCost::LO, x.size()); 00067 } 00068 00069 template<class View> 00070 forceinline size_t 00071 Lex<View>::dispose(Space& home) { 00072 assert(!home.failed()); 00073 x.cancel(home,*this,PC_INT_BND); 00074 y.cancel(home,*this,PC_INT_BND); 00075 (void) Propagator::dispose(home); 00076 return sizeof(*this); 00077 } 00078 00079 template<class View> 00080 ExecStatus 00081 Lex<View>::propagate(Space& home, const ModEventDelta&) { 00082 /* 00083 * State 1 00084 * 00085 */ 00086 { 00087 int i = 0; 00088 int n = x.size(); 00089 00090 while ((i < n) && (x[i].min() == y[i].max())) { 00091 // case: =, >= 00092 GECODE_ME_CHECK(x[i].lq(home,y[i].max())); 00093 GECODE_ME_CHECK(y[i].gq(home,x[i].min())); 00094 i++; 00095 } 00096 00097 if (i == n) // case: $ 00098 return strict ? ES_FAILED : home.ES_SUBSUMED(*this); 00099 00100 // Possible cases left: <, <=, > (yields failure), ? 00101 GECODE_ME_CHECK(x[i].lq(home,y[i].max())); 00102 GECODE_ME_CHECK(y[i].gq(home,x[i].min())); 00103 00104 if (x[i].max() < y[i].min()) // case: < (after tell) 00105 return home.ES_SUBSUMED(*this); 00106 00107 // x[i] can never be equal to y[i] (otherwise: >=) 00108 assert(!(x[i].assigned() && y[i].assigned() && 00109 x[i].val() == y[i].val())); 00110 // Remove all elements between 0...i-1 as they are assigned and equal 00111 x.drop_fst(i); y.drop_fst(i); 00112 // After this, execution continues at [1] 00113 } 00114 00115 /* 00116 * State 2 00117 * prefix: (?|<=) 00118 * 00119 */ 00120 { 00121 int i = 1; 00122 int n = x.size(); 00123 00124 while ((i < n) && 00125 (x[i].min() == y[i].max()) && 00126 (x[i].max() == y[i].min())) { // case: = 00127 assert(x[i].assigned() && y[i].assigned() && 00128 (x[i].val() == y[i].val())); 00129 i++; 00130 } 00131 00132 if (i == n) { // case: $ 00133 if (strict) 00134 goto rewrite_le; 00135 else 00136 goto rewrite_lq; 00137 } 00138 00139 if (x[i].max() < y[i].min()) // case: < 00140 goto rewrite_lq; 00141 00142 if (x[i].min() > y[i].max()) // case: > 00143 goto rewrite_le; 00144 00145 if (i > 1) { 00146 // Remove equal elements [1...i-1], keep element [0] 00147 x[i-1]=x[0]; x.drop_fst(i-1); 00148 y[i-1]=y[0]; y.drop_fst(i-1); 00149 } 00150 } 00151 00152 if (x[1].max() <= y[1].min()) { 00153 // case: <= (invariant: not =, <) 00154 /* 00155 * State 3 00156 * prefix: (?|<=),<= 00157 * 00158 */ 00159 int i = 2; 00160 int n = x.size(); 00161 00162 while ((i < n) && (x[i].max() == y[i].min())) // case: <=, = 00163 i++; 00164 00165 if (i == n) { // case: $ 00166 if (strict) 00167 return ES_FIX; 00168 else 00169 goto rewrite_lq; 00170 } 00171 00172 if (x[i].max() < y[i].min()) // case: < 00173 goto rewrite_lq; 00174 00175 if (x[i].min() > y[i].max()) { // case: > 00176 // Eliminate [i]...[n-1] 00177 for (int j=i; j<n; j++) { 00178 x[j].cancel(home,*this,PC_INT_BND); 00179 y[j].cancel(home,*this,PC_INT_BND); 00180 } 00181 x.size(i); y.size(i); 00182 strict = true; 00183 } 00184 00185 return ES_FIX; 00186 } 00187 00188 if (x[1].min() >= y[1].max()) { 00189 // case: >= (invariant: not =, >) 00190 /* 00191 * State 4 00192 * prefix: (?|<=) >= 00193 * 00194 */ 00195 int i = 2; 00196 int n = x.size(); 00197 00198 while ((i < n) && (x[i].min() == y[i].max())) 00199 // case: >=, = 00200 i++; 00201 00202 if (i == n) { // case: $ 00203 if (strict) 00204 goto rewrite_le; 00205 else 00206 return ES_FIX; 00207 } 00208 00209 if (x[i].min() > y[i].max()) // case: > 00210 goto rewrite_le; 00211 00212 if (x[i].max() < y[i].min()) { // case: < 00213 // Eliminate [i]...[n-1] 00214 for (int j=i; j<n; j++) { 00215 x[j].cancel(home,*this,PC_INT_BND); 00216 y[j].cancel(home,*this,PC_INT_BND); 00217 } 00218 x.size(i); y.size(i); 00219 strict = false; 00220 } 00221 00222 return ES_FIX; 00223 } 00224 00225 return ES_FIX; 00226 00227 rewrite_le: 00228 GECODE_REWRITE(*this,Le<View>::post(home(*this),x[0],y[0])); 00229 rewrite_lq: 00230 GECODE_REWRITE(*this,Lq<View>::post(home(*this),x[0],y[0])); 00231 } 00232 00233 template<class View> 00234 ExecStatus 00235 Lex<View>::post(Home home, 00236 ViewArray<View>& x, ViewArray<View>& y, bool strict){ 00237 if (x.size() == 0) 00238 return strict ? ES_FAILED : ES_OK; 00239 if (x.size() == 1) { 00240 if (strict) 00241 return Le<View>::post(home,x[0],y[0]); 00242 else 00243 return Lq<View>::post(home,x[0],y[0]); 00244 } 00245 (void) new (home) Lex<View>(home,x,y,strict); 00246 return ES_OK; 00247 } 00248 00249 }}} 00250 00251 // STATISTICS: int-prop