| 169 | } |
| 170 | |
| 171 | void |
| 172 | NNF::post(Home home, SetRelType srt, SetVar s) const { |
| 173 | switch (t) { |
| 174 | case SetExpr::NT_VAR: |
| 175 | if (neg) { |
| 176 | switch (srt) { |
| 177 | case SRT_EQ: |
| 178 | rel(home, u.a.x->x, SRT_CMPL, s); |
| 179 | break; |
| 180 | case SRT_CMPL: |
| 181 | rel(home, u.a.x->x, SRT_EQ, s); |
| 182 | break; |
| 183 | default: |
| 184 | SetVar bc(home,IntSet::empty, |
| 185 | IntSet(Set::Limits::min,Set::Limits::max)); |
| 186 | rel(home, s, SRT_CMPL, bc); |
| 187 | rel(home, u.a.x->x, srt, bc); |
| 188 | break; |
| 189 | } |
| 190 | } else |
| 191 | rel(home, u.a.x->x, srt, s); |
| 192 | break; |
| 193 | case SetExpr::NT_CONST: |
| 194 | { |
| 195 | IntSet ss; |
| 196 | if (neg) { |
| 197 | IntSetRanges sr(u.a.x->s); |
| 198 | Set::RangesCompl<IntSetRanges> src(sr); |
| 199 | ss = IntSet(src); |
| 200 | } else { |
| 201 | ss = u.a.x->s; |
| 202 | } |
| 203 | switch (srt) { |
| 204 | case SRT_SUB: srt = SRT_SUP; break; |
| 205 | case SRT_SUP: srt = SRT_SUB; break; |
| 206 | default: break; |
| 207 | } |
| 208 | dom(home, s, srt, ss); |
| 209 | } |
| 210 | break; |
| 211 | case SetExpr::NT_LEXP: |
| 212 | { |
| 213 | IntVar iv = u.a.x->e.post(home,IntPropLevels::def); |
| 214 | if (neg) { |
| 215 | SetVar ic(home,IntSet::empty, |
| 216 | IntSet(Set::Limits::min,Set::Limits::max)); |
| 217 | rel(home, iv, SRT_CMPL, ic); |
| 218 | rel(home,ic,srt,s); |
| 219 | } else { |
| 220 | rel(home,iv,srt,s); |
| 221 | } |
| 222 | } |
| 223 | break; |
| 224 | case SetExpr::NT_INTER: |
| 225 | { |
| 226 | SetVarArgs bs(p+n); |
| 227 | int i=0; |
| 228 | post(home, SetExpr::NT_INTER, bs, i); |