1 /* 2 * Regular.java 3 * This file is part of JaCoP. 4 * <p> 5 * JaCoP is a Java Constraint Programming solver. 6 * <p> 7 * Copyright (C) 2008 Polina Maakeva and Radoslaw Szymanek 8 * <p> 9 * This program is free software: you can redistribute it and/or modify 10 * it under the terms of the GNU Affero General Public License as published by 11 * the Free Software Foundation, either version 3 of the License, or 12 * (at your option) any later version. 13 * <p> 14 * This program is distributed in the hope that it will be useful, 15 * but WITHOUT ANY WARRANTY; without even the implied warranty of 16 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 17 * GNU Affero General Public License for more details. 18 * <p> 19 * Notwithstanding any other provision of this License, the copyright 20 * owners of this work supplement the terms of this License with terms 21 * prohibiting misrepresentation of the origin of this work and requiring 22 * that modified versions of this work be marked in reasonable ways as 23 * different from the original version. This supplement of the license 24 * terms is in accordance with Section 7 of GNU Affero General Public 25 * License version 3. 26 * <p> 27 * You should have received a copy of the GNU Affero General Public License 28 * along with this program. If not, see <http://www.gnu.org/licenses/>. 29 */ 30 31 package org.jacop.constraints.regular; 32 33 import org.jacop.api.RemoveLevelLate; 34 import org.jacop.api.Stateful; 35 import org.jacop.api.UsesQueueVariable; 36 import org.jacop.constraints.Constraint; 37 import org.jacop.constraints.ExtensionalSupportSTR; 38 import org.jacop.constraints.In; 39 import org.jacop.constraints.XeqC; 40 import org.jacop.core.*; 41 import org.jacop.util.MDD; 42 import org.jacop.util.fsm.FSM; 43 import org.jacop.util.fsm.FSMState; 44 import org.jacop.util.fsm.FSMTransition; 45 46 import java.io.*; 47 import java.lang.reflect.Array; 48 import java.nio.charset.Charset; 49 import java.util.*; 50 import java.util.concurrent.atomic.AtomicInteger; 51 52 /** 53 * Store all edges removed because of the value removal in one big array. Edges removed due to states being 54 * removed restore in the old fashion way. 55 * <p> 56 * Split pruneArc and reachability analysis so there is only one forward sweep and one backward sweep. 57 * To make it work we need to store number of states for each layer before pruneArc(s) execution. 58 * <p> 59 * Implement predecessors array to simplify UnreachBackwardLoop, update this array and inDegree 60 * as successors array upon removeLevel. Compare two versions. PruneArc will get expensive because 61 * predecessor array has to be updated to upon edges removal due to pruning. 62 * <p> 63 * DONE. Write decomposition of Regular into Table constraints as Slide decomposition of Regular has proposed. 64 * <p> 65 * DONE. Write a translator of Regular (FSM) constraint into one large MDD. 66 * <p> 67 * DONE. Fix the problem if regular is being executed with other constraints (external removal of 68 * values mixing with the removals inferred by a regular). 69 * <p> 70 * DONE. Improve the efficiency of queueVariable(). 71 * <p> 72 * DONE. Move initializeArray from constructor to impose (takes advantage of the fact if imposition is 73 * done much later than creation). 74 * <p> 75 * DONE. Clean initialize array, do not use Stack but HashSet. 76 * <p> 77 * DONE. todo store range, (min, max) per search level in two timestamps so the backtracking can 78 * be done only for layers in between min..max. If not much change happen then backtracking 79 * will be significantly restricted. 80 * <p> 81 * DONE. todo check if possible to remove level attribute from the state. 82 * <p> 83 * todo DONE. CLEAN code (variables, loops, finishing conditions, etc) 84 * 85 * @todo Create toXML() and fromXML() functions. 86 * <p> 87 * todo DONE. Make levelHadChanged a global variable which is allocated only once and is only filled with false 88 * values at the beginning of consistency function. 89 * <p> 90 * DONE. fix a null pointer exception bug after reshuffling impose and consistency. 91 * <p> 92 * DONE. changed indexing in for loop (++ to --) and remove redundant variables after changing 93 * indexing 94 * <p> 95 * DONE. clean consistency function from stuff which can be done at impose function once. 96 * <p> 97 * DONE. efficiency improvements - sweepgraph() only once in consistency function not 98 * multiple times in pruneArc function. 99 * <p> 100 * DONE. If supports are switched off, it seams that constraint does not achieve GAC, 101 * 1% of nodes are wrong decisions. Addded line in pruneArc function. 102 * <p> 103 * DONE. import tests of Regular constraint into Test package. 104 * <p> 105 * DONE. Make the choice of object assigned to an edge within a RegState object 106 * an encapsulated decision so both implementations based on int and domain 107 * can easily coexist. 108 * <p> 109 * DONE. implement one support which does not create new objects and 110 * does not replace RegEdge when new support is found. It only 111 * replaces internal data structure of RegEdge object. 112 * <p> 113 * DONE. use inComplement(a) instead of in(currentdomain.subtract(a). 114 * <p> 115 * DONE. remove store dependent operations from constructor and put in impose. e.g. 116 * initializeArray. 117 * <p> 118 * DONE. remove zeroNode check from consistency and change it to firstTimeConsistencyCalled 119 * as zero node check does not have to be correct (level does not have to be equal to 0). 120 * <p> 121 * DONE. check if union domain function can be changed to addDomain(); (no copying). 122 */ 123 124 125 /** 126 * Regular constraint accepts only the assignment to variables which is accepted by 127 * an automaton. This constraint implements a polynomial algorithm to establish 128 * GAC. There are number of improvements (iterative execution, optimization of computational load upon 129 * backtracking) to improve the constraint further. 130 * 131 * @author Polina Makeeva and Radoslaw Szymanek 132 * @version 4.8 133 */ 134 135 public class Regular extends Constraint implements UsesQueueVariable, Stateful, RemoveLevelLate { 136 137 /** 138 * It specifies if debugging information should be printed out. 139 */ 140 public static final boolean debugAll = false; 141 142 /** 143 * It specifies if constraint description should be saved to latex for later viewing. 144 */ 145 public static final boolean saveAllToLatex = false; 146 147 /** 148 * It specifies if the translation of FSM into optimized MDD should take place so 149 * minimal layered graph can be obtained. This option most of the time causes 150 * out of memory exception as it requires finding and storing all solutions in 151 * mtrie before translation to an optimized MDD can take place. FSM also has to 152 * be a deterministic one. 153 */ 154 public final boolean optimizedMDD = false; 155 156 /** Name of the file to store the latex output after consistency call 157 * The output will be : file_name + "call number" + ".tex" 158 */ 159 public String latexFile = "/home/radek/"; 160 161 /** 162 * This is the counter of save-to-latex calls 163 */ 164 private int calls = 0; 165 166 /** dNames contain a "name" for each value from the union of all variabl's domains. 167 * If Hashmap - dNames - is not null then upon saving the latex graph 168 * the values on the edges will be replaced with their "names". 169 */ 170 public Map<Integer, String> dNames; 171 172 /** 173 * The ith smallest level of Layered Graph which have changed. 174 */ 175 private TimeStamp<Integer> leftChange; 176 177 /** 178 * The ith largest level of Layered Graph which have changed. 179 */ 180 private TimeStamp<Integer> rightChange; 181 182 /** 183 * The position of the currentTouchedIndex 184 */ 185 186 private TimeStamp<Integer> touchedIndex; 187 188 /** 189 * Stores the states of all graph levels 190 */ 191 private RegState[][] stateLevels; 192 193 /** 194 * Time-stamp for the number of active states in each level 195 196 */ 197 private TimeStamp<Integer>[] activeLevels; 198 199 private int activeLevelsTemp[]; 200 201 202 /** 203 * Number of states in the graph 204 * used only during the printing to latex function 205 */ 206 int stateNumber; 207 208 /** 209 * @todo, try to use PriorityQueue based on the number 210 * of states for a given variable or a domain size to 211 * pickup first variables which may result in failure faster. 212 * It does not have to be fully correct ordering. 213 */ 214 LinkedHashSet<IntVar> variableQueue = new LinkedHashSet<IntVar>(); 215 216 Map<IntVar, Integer> mapping; 217 218 static AtomicInteger idNumber = new AtomicInteger(0); 219 220 221 /** 222 * It keeps for each variable value pair a current support. 223 */ 224 public Map<Integer, RegEdge>[] supports; 225 226 227 /** 228 * It specifies if the edges should have a list of values associated with them. 229 */ 230 public boolean listRepresentation = true; 231 232 /** 233 * It specifies if the support functionality should be used. 234 */ 235 public boolean oneSupport = true; 236 237 private Integer leftPosition; 238 239 private Integer rightPosition; 240 241 242 243 /** 244 * Consistency function call the prune arc function for every pruned variable 245 * and collect information about the levels that had some changes in "levelHadChaged" array 246 * Then it collect the values of the edges that are still active on the levels that 247 * had chages and update the domains of the variables. 248 */ 249 250 boolean firstConsistencyCheck = true; 251 252 boolean levelHadChanged[]; 253 254 int firstConsistencyLevel; 255 256 List<Constraint> constraints; 257 258 259 RegState[] touchedStates; 260 261 private int currentTouchedIndex = 0; 262 263 /** 264 * It specifies finite state machine used by this regular. 265 */ 266 public FSM fsm; 267 268 /** 269 * Array of the variables of the graph levels 270 */ 271 public IntVar[] list; 272 273 /** 274 * Constructor need Store to initialize the time-stamps 275 * @param fsm (deterministic) finite automaton 276 * @param list variables which values have to be accepted by the automaton. 277 */ 278 Regular(FSM fsm, IntVar[] list)279 public Regular(FSM fsm, IntVar[] list) { 280 281 checkInputForNullness("list", list); 282 checkInputForDuplicationSkipSingletons("list", list); 283 284 this.queueIndex = 1; 285 this.list = Arrays.copyOf(list, list.length); 286 this.fsm = fsm; 287 numberId = idNumber.incrementAndGet(); 288 leftPosition = 0; 289 rightPosition = list.length - 1; 290 touchedStates = new RegState[fsm.allStates.size() * list.length]; 291 setScope(list); 292 } 293 294 /** 295 * Initialization phase of the algorithm 296 * 297 * Considering that it needs to initialize the array of graph States - stateLevels, 298 * and, thus, it needs to know the actual number of the states on each level I found 299 * nothing better then run the initialization phase with the complete NxN array of states 300 * and then copy the useful ones into a final array (which is ugly) 301 * 302 * 303 * @param dfa 304 */ 305 initializeARRAY(FSM dfa)306 private void initializeARRAY(FSM dfa) { 307 308 int levels = this.list.length; 309 stateNumber = dfa.allStates.size(); 310 311 //The array that keep all possible states with arcs and their domains 312 //If the domain is empty then the arc doesn't exist 313 IntDomain[][][] outarc = new IntervalDomain[levels + 1][stateNumber][stateNumber]; 314 int[][] outdeg = new int[levels + 1][stateNumber]; 315 316 //Reachable region of the graph 317 Set<FSMState> reachable = new HashSet<FSMState>(); 318 //Temporal variable for reachable region 319 Set<FSMState> tmp = new HashSet<FSMState>(); 320 321 //Initialization of the future state array 322 //and the time-stamps with the number of active states 323 this.stateLevels = new RegState[levels + 1][]; 324 325 //The id's of the states are renamed to make the future graph in latex look pretty 326 int level = 0; 327 328 FSMState array[] = new FSMState[stateNumber]; 329 330 dfa.resize(); 331 for (FSMState s : dfa.allStates) 332 array[s.id] = s; 333 334 //----- compute the reachable region of the graph ----- 335 336 //Start with initial state 337 reachable.add(dfa.initState); 338 339 while (level < levels) { 340 //prepare tmp set of reachable states in the next level 341 tmp.clear(); 342 //For each state reached until now 343 for (FSMState s : reachable) 344 //watch it's edges 345 for (FSMTransition t : s.transitions) { 346 //prepare the set of values of this edge 347 IntDomain dom = t.domain.intersect(list[level].dom()); 348 349 if (outarc[level][s.id][t.successor.id] != null) 350 outarc[level][s.id][t.successor.id].addDom(dom); 351 else 352 outarc[level][s.id][t.successor.id] = dom; 353 354 /* If the edge is not empty them add the state to tmp set 355 * check that such states wasn't previously added. 356 * 357 * If the level is the last, then check whether the state 358 * belongs to the set of accepted states 359 */ 360 361 if (dom.getSize() > 0) 362 if (level < levels - 1) 363 tmp.add(t.successor); 364 else if (dfa.finalStates.contains(t.successor)) 365 tmp.add(t.successor); 366 } 367 368 //copy the tmp set of states into reachable region 369 reachable.clear(); 370 reachable.addAll(tmp); 371 //got to next level 372 level++; 373 } 374 375 //initialize the last time-stamp because the counter didn't reach it. 376 /* ----- delete the paths of the graph that doesn't reach the accepted state ----- 377 * 378 * 379 * by calculating the reachable region of the graph starting from the accepted 380 * states and following the edges in the opposite direction. 381 */ 382 383 while (level > 0) { 384 tmp.clear(); 385 386 stateLevels[level] = new RegState[reachable.size()]; 387 388 for (int i = 0; i < stateNumber; i++) 389 for (int j = 0; j < stateNumber; j++) 390 if (outarc[level - 1][j][i] != null && outarc[level - 1][j][i].getSize() > 0) 391 if (!reachable.contains(array[i])) 392 outarc[level - 1][j][i].clear(); 393 else { 394 outdeg[level - 1][j] += outarc[level - 1][j][i].getSize(); 395 tmp.add(array[j]); 396 } 397 398 reachable.clear(); 399 reachable.addAll(tmp); 400 level--; 401 } 402 403 stateLevels[0] = new RegState[1]; 404 this.activeLevelsTemp = new int[this.list.length + 1]; 405 406 // ---- copy the resulting graph into final array ---- 407 int index = 0; 408 int nextLevelIndex = 0; 409 410 for (level = 0; level < levels; level++) { 411 index = nextLevelIndex; 412 nextLevelIndex = 0; 413 414 for (int i = 0; i < stateNumber; i++) { 415 if (outdeg[level][i] > 0) { 416 //If the outdegree of the sate is not 0 then its should be created 417 RegState s = getState(level, i); //Check if it wasn't already created 418 if (s == null) { //If not -> create the state 419 if (listRepresentation) 420 s = new RegStateInt(level, i, outdeg[level][i], index); 421 else 422 s = new RegStateDom(level, i, outdeg[level][i], index); 423 424 stateLevels[level][index++] = s; //Add new state to the list of states of this level 425 426 activeLevelsTemp[level] = index; 427 428 if (debugAll) 429 System.out.println( 430 "Create new state q_" + level + i + " with in degree : " + s.inDegree + " and out degree : " + s.outDegree); 431 432 } 433 434 //For every outgoing arc 435 for (int j = 0; j < stateNumber; j++) 436 //If transition is active 437 if (outarc[level][i][j] != null && outarc[level][i][j].getSize() > 0) { 438 RegState suc = getState(level + 1, j); //See if such state already exists 439 if (suc == null) { 440 if (listRepresentation) 441 suc = new RegStateInt(level + 1, j, outdeg[level + 1][j], nextLevelIndex); 442 else 443 suc = new RegStateDom(level + 1, j, outdeg[level + 1][j], nextLevelIndex); 444 445 stateLevels[level + 1][nextLevelIndex++] = suc; 446 447 activeLevelsTemp[level + 1] = nextLevelIndex; 448 449 if (debugAll) 450 System.out.println( 451 "Create new state q_" + (level + 1) + j + " with in degree : " + suc.inDegree + " and out degree : " 452 + suc.outDegree); 453 } 454 455 s.addTransitions(suc, (IntervalDomain) outarc[level][i][j]); 456 457 if (debugAll) 458 System.out.println( 459 "-- state q_" + level + i + " with in degree : " + s.inDegree + " and out degree : " + s.outDegree); 460 461 if (debugAll) 462 System.out.println( 463 "-- state q_" + (level + 1) + j + " with in degree : " + suc.inDegree + " and out degree : " 464 + suc.outDegree); 465 } 466 467 } 468 } 469 } 470 471 472 } 473 474 /** 475 * Find the state with the corresponding id. 476 * @param level specifies the variable for which the state is seeked for. 477 * @param id specifies the id of the state. 478 * @return the state at given level with a given id. 479 */ getState(int level, int id)480 public RegState getState(int level, int id) { 481 482 for (int i = 0; i < stateLevels[level].length; i++) { 483 if (stateLevels[level][i] != null && stateLevels[level][i].id == id) 484 return stateLevels[level][i]; 485 486 } 487 return null; 488 } 489 490 /** 491 * Collects the damaged states, after pruning the domain of variable "var", 492 * and put these states in two separated sets. 493 * 494 * One with the states with zero incoming degree - these are the candidates 495 * for the forward part. 496 * The other set consists of states with zero out-coming degree - these are 497 * the candidates for backward part. 498 * 499 * @param varIndex the index of the variable which have changed. 500 */ 501 pruneArc(int varIndex)502 public void pruneArc(int varIndex) { 503 504 int state = 0; 505 int preThisLevelStateNb = this.activeLevels[varIndex].value(); 506 RegState s = null; 507 RegState suc = null; 508 int nextVar = varIndex + 1; 509 int preNextLevelStateNb = this.activeLevels[nextVar].value(); 510 511 levelHadChanged[varIndex] = true; 512 513 IntDomain domVar = list[varIndex].domain; 514 515 for (state = preThisLevelStateNb - 1; state >= 0; state--) { 516 517 s = stateLevels[varIndex][state]; 518 if (debugAll) 519 System.out.println(state + ": watch state q_" + varIndex + s.id); 520 521 boolean alreadyTouched = false; 522 523 for (int i = s.outDegree - 1; i >= 0; i--) 524 //If this transition must be removes because it is not in var's domain 525 if (!s.intersects(domVar, i)) { 526 527 if (debugAll) 528 System.out.println( 529 "must remove transition q_" + varIndex + s.id + " -" + s.sucDomToString(i) + "-> q_" + (varIndex + 1) 530 + s.successors[i].id); 531 532 // we remove this transition (we know its index, so its easy) 533 // This will automatically reduce the out-degree of this state 534 // and reduce in-degree of the successor. 535 536 suc = s.successors[i]; 537 s.removeTransition(i); 538 539 if (!alreadyTouched) { 540 addTouchedState(s); 541 alreadyTouched = true; 542 } 543 544 /** 545 * @todo if number of edges at a given layer is relatively close 546 * to the domain size, so the edges are not so often removed it 547 * may be beneficial to check if the removed edge caused loosing 548 * the support and removal of the value from the domain. 549 */ 550 551 if (debugAll) { 552 System.out.println( 553 "-- state q_" + s.level + s.id + " with in degree : " + s.inDegree + " and out degree : " + s.outDegree); 554 System.out.println( 555 "-- state q_" + (suc.level) + suc.id + " with in degree : " + suc.inDegree + " and out degree : " 556 + suc.outDegree); 557 } 558 559 assert (s.outDegree >= 0); 560 561 if (s.outDegree == 0) { 562 if (debugAll) 563 System.out.println("Move OUT state out of scope : q_" + varIndex + s.id); 564 assert (s.level == varIndex); 565 disableState(varIndex, s.pos); 566 } 567 568 assert (suc.inDegree >= 0); 569 570 if (suc.inDegree == 0) { 571 if (debugAll) 572 System.out.println("Move IN state out of scope : q_" + suc.level + suc.id); 573 assert (suc.level == varIndex + 1); 574 disableState(nextVar, suc.pos); 575 levelHadChanged[nextVar] = true; 576 } 577 } 578 579 } 580 581 unreachForwardLoop(preNextLevelStateNb, varIndex + 1); 582 unreachBackwardLoop(preThisLevelStateNb, varIndex - 1); 583 584 } 585 586 587 addTouchedState(RegState s)588 private void addTouchedState(RegState s) { 589 590 if (currentTouchedIndex < touchedStates.length) 591 touchedStates[currentTouchedIndex++] = s; 592 else { 593 594 RegState[] newTouchedStates = new RegState[touchedStates.length * 2]; 595 System.arraycopy(touchedStates, 0, newTouchedStates, 0, touchedStates.length); 596 touchedStates = newTouchedStates; 597 598 } 599 600 } 601 602 /** 603 * It does backward check to remove inactive edges and states. 604 * @param sucPrevLimit previous number of states at a given level. 605 * @param level level for which the backward sweep is computed. 606 * @return level at which the sweep has ended. 607 * 608 * TODO return value is not used. 609 */ unreachBackwardLoop(int sucPrevLimit, int level)610 public int unreachBackwardLoop(int sucPrevLimit, int level) { 611 612 RegState s = null; 613 614 boolean cont = sucPrevLimit != this.activeLevels[level + 1].value(); 615 616 while (level >= 0 && cont) { 617 618 cont = false; 619 620 levelHadChanged[level] = true; 621 622 for (int sPos = this.activeLevels[level].value() - 1; sPos >= 0; sPos--) { 623 624 s = this.stateLevels[level][sPos]; 625 626 boolean alreadyTouched = false; 627 for (int sucIndex = s.outDegree - 1; sucIndex >= 0; sucIndex--) 628 if (!s.successors[sucIndex].isActive(activeLevels)) { 629 s.removeTransition(sucIndex); 630 if (!alreadyTouched) { 631 addTouchedState(s); 632 alreadyTouched = true; 633 } 634 } 635 636 assert (s.outDegree >= 0) : "Negative successor number of q_" + s.level + s.id; 637 638 if (s.outDegree == 0) { 639 assert (s.level == level); 640 disableState(level, sPos); 641 cont = true; 642 } 643 644 } 645 646 level--; 647 } 648 649 return level; 650 } 651 652 653 /** 654 * Forward part deletes the outgoing edges of the damaged state and watch whether 655 * the successors are still active (in-degree {@literal >} 0 ), otherwise we collect it and 656 * continue the loop. 657 * 658 * TODO return value is not used. 659 * 660 * @param end the position of the last active state at a given level. 661 * @param level level being examined. 662 */ unreachForwardLoop(int end, int level)663 public void unreachForwardLoop(int end, int level) { 664 665 int state = 0; 666 RegState s = null; 667 RegState suc = null; 668 669 int preNextLevelStateNb; 670 671 int currentLimit = this.activeLevels[level].value(); 672 673 boolean cont = currentLimit != end; 674 675 while (level < this.list.length && cont) { 676 677 levelHadChanged[level] = true; 678 679 cont = false; 680 681 preNextLevelStateNb = this.activeLevels[level + 1].value(); 682 683 for (state = currentLimit; state < end; state++) { 684 s = stateLevels[level][state]; 685 686 //We are removing a damaged state, thus, all its arcs are removed and 687 //we must remember maximal degree of it 688 // if (s.outDegree > maxDegreePrunned) 689 // maxDegreePrunned = s.outDegree; 690 691 for (int i = s.outDegree - 1; i >= 0; i--) { 692 693 suc = s.successors[i]; 694 suc.inDegree--; 695 696 if (debugAll) 697 System.out 698 .println("watch transition q_" + s.level + s.id + " -" + s.sucDomToString(i) + "-> q_" + (suc.level) + suc.id); 699 700 assert (suc.inDegree >= 0) : "Negative indegree of successor state" + suc.level + suc.id; 701 702 if (suc.inDegree == 0) { 703 if (debugAll) 704 System.out.println("> Move IN state out of scope : q_" + suc.level + suc.id); 705 // changed to directl disableState(int, int). 706 assert (suc.level == level + 1); 707 disableState(level + 1, suc.pos); 708 //@todo levelHasChanged[level+1] = true 709 cont = true; 710 } 711 712 } 713 714 s.outDegree = 0; 715 716 } 717 718 end = preNextLevelStateNb; 719 currentLimit = activeLevels[level + 1].value(); 720 level++; 721 722 } 723 724 // if (maxDegreePrunned > arcsPrunned.value()) 725 // arcsPrunned.update(maxDegreePrunned); 726 727 728 729 } 730 731 732 /** 733 * It marks state as being not active. 734 * 735 * @param level level at which the state is residing. 736 * @param pos position of the state in the array of states. 737 */ 738 disableState(int level, int pos)739 public void disableState(int level, int pos) { 740 741 int lim = activeLevels[level].value(); 742 743 assert (pos < lim); 744 745 RegState s = stateLevels[level][pos]; 746 747 // it must be before the remaining operations 748 lim--; 749 750 stateLevels[level][pos] = stateLevels[level][lim]; 751 stateLevels[level][pos].pos = pos; 752 stateLevels[level][lim] = s; 753 s.pos = lim; 754 activeLevels[level].update(lim); 755 756 } 757 758 int[] lastNumberOfActiveStates; 759 760 @Override public void removeLevel(int level) { 761 762 assert (level > firstConsistencyLevel) : "Constraint has the level at which it has computed its initial state being removed."; 763 764 this.variableQueue.clear(); 765 766 if (leftChange.value() < leftPosition) 767 leftPosition = leftChange.value(); 768 769 if (rightChange.value() > rightPosition) 770 rightPosition = rightChange.value(); 771 772 773 for (int l = leftPosition; l <= rightPosition; l++) 774 lastNumberOfActiveStates[l] = activeLevels[l].value(); 775 776 } 777 778 /** 779 * Sweep the graph upon backtracking. 780 * 781 */ removeLevelLate(int level)782 @Override public void removeLevelLate(int level) { 783 784 RegState curState; 785 int prevVal; 786 787 int checkToIndex = touchedIndex.value(); 788 789 while (currentTouchedIndex > checkToIndex) { 790 791 curState = touchedStates[--currentTouchedIndex]; 792 793 RegState[] successors = curState.successors; 794 prevVal = curState.outDegree; 795 curState.outDegree = successors.length; 796 797 for (int i = prevVal; i < curState.outDegree; i++) 798 if (!(successors[i].isActive(activeLevels) && curState.intersects(list[curState.level].domain, i))) 799 curState.outDegree = i; 800 else 801 successors[i].inDegree++; 802 803 } 804 805 int stateNb = 0; 806 807 //for every level which has been recorded be in between the levels which have changed 808 for (int l = leftPosition; l <= rightPosition; l++) { 809 //for every active state in the level 810 stateNb = this.activeLevels[l].value(); 811 812 //for (int s = 0; s < stateNb; s++) { 813 for (int s = lastNumberOfActiveStates[l]; s < stateNb; s++) { 814 //update its out degree by adding the accumulator 815 //by doing this we add some old, possibly inactive edge 816 curState = stateLevels[l][s]; 817 RegState[] successors = curState.successors; 818 prevVal = curState.outDegree; 819 curState.outDegree = successors.length; 820 //for every new added edge is active 821 //if it is not, then stop 822 for (int i = prevVal; i < curState.outDegree; i++) 823 if (!(successors[i].isActive(activeLevels) && curState.intersects(list[l].domain, i))) 824 curState.outDegree = i; 825 else 826 successors[i].inDegree++; 827 } 828 } 829 830 if (debugAll) 831 System.out.println("..next prunning"); 832 if (saveAllToLatex) 833 saveLatexToFile("After graph sweep"); 834 835 836 leftPosition = list.length; 837 rightPosition = 0; 838 839 840 } 841 queueVariable(int level, Var var)842 @Override public void queueVariable(int level, Var var) { 843 844 variableQueue.add((IntVar) var); 845 846 } 847 consistency(Store store)848 @Override public void consistency(Store store) { 849 850 if (firstConsistencyCheck) { 851 852 RegState state; 853 854 if (oneSupport) { 855 856 for (int level = list.length - 1; level >= 0; level--) { 857 858 // first restrict the domain to the sum of all edges annotations. 859 860 IntervalDomain initial = new IntervalDomain(); 861 862 for (Integer value : supports[level].keySet()) 863 initial.unionAdapt(value, value); 864 865 this.list[level].domain.in(store.level, list[level], initial); 866 867 ValueEnumeration enumer = list[level].domain.valueEnumeration(); 868 869 for (int v; enumer.hasMoreElements(); ) { 870 871 v = enumer.nextElement(); 872 873 874 if (supports[level].get(v) == null) { 875 this.list[level].domain.inComplement(store.level, list[level], v); 876 enumer.domainHasChanged(); 877 continue; 878 } 879 880 RegEdge edge = supports[level].get(v); 881 // function check - checks if there is a support, starting from the 882 // current one. 883 884 if (!edge.check(activeLevels)) { 885 boolean stillSuported = false; 886 for (int st = activeLevels[level].value() - 1; st >= 0; st--) 887 if (stateLevels[level][st].updateSupport(edge, v)) { 888 stillSuported = true; 889 break; 890 } 891 892 if (!stillSuported) { 893 list[level].domain.inComplement(store.level, list[level], v); 894 enumer.domainHasChanged(); 895 } 896 } 897 } 898 899 } 900 } else { 901 902 IntDomain varDom; 903 904 for (int level = this.list.length - 1; level >= 0; level--) { 905 varDom = new IntervalDomain(); 906 for (int s = activeLevels[level].value() - 1; s >= 0; s--) { 907 state = this.stateLevels[level][s]; 908 for (int i = state.outDegree - 1; i >= 0; i--) 909 state.add(varDom, i); 910 } 911 if (debugAll) 912 System.out.println(">>> Variable x_" + level + " had domain " + this.list[level].domain + " and now its " + varDom); 913 this.list[level].domain.in(store.level, list[level], varDom); 914 } 915 } 916 917 if (saveAllToLatex) 918 saveLatexToFile("End of consistency level " + store.level); 919 920 firstConsistencyCheck = false; 921 firstConsistencyLevel = store.level; 922 923 if (variableQueue.isEmpty()) 924 return; 925 926 } 927 928 RegState state; 929 930 Arrays.fill(levelHadChanged, false); 931 932 for (Var var : variableQueue) { 933 pruneArc(mapping.get(var)); 934 } 935 936 // if two consistency functions executed one after the other 937 // then timestamp may be asked to update to the same value. If that 938 // request does not create new level because value at older level 939 // is equal then here the leftChange and rightChange will not be 940 // updated correctly. 941 942 if (leftChange.stamp() < store.level) { 943 for (int i = 0; i < levelHadChanged.length; i++) 944 if (levelHadChanged[i]) { 945 leftChange.update(i); 946 break; 947 } 948 } else { 949 int leftEnd = leftChange.value(); 950 for (int i = 0; i < leftEnd; i++) 951 if (levelHadChanged[i]) { 952 leftChange.update(i); 953 break; 954 } 955 } 956 957 if (rightChange.stamp() < store.level) { 958 for (int i = levelHadChanged.length - 1; i >= 0; i--) 959 if (levelHadChanged[i]) { 960 rightChange.update(i); 961 break; 962 } 963 } else { 964 int rightEnd = rightChange.value(); 965 for (int i = levelHadChanged.length - 1; i > rightEnd; i--) 966 if (levelHadChanged[i]) { 967 rightChange.update(i); 968 break; 969 } 970 } 971 972 /** 973 * @todo implement oneSupport per variable, some variables may be using supports another one just a sweep. 974 * If for example number of states within level is smaller than the domain size then oneSupport is 975 * not worth using. 976 */ 977 if (oneSupport) { 978 979 for (int level = this.list.length - 1; level >= 0; level--) 980 if (levelHadChanged[level]) { 981 982 ValueEnumeration enumer = this.list[level].domain.valueEnumeration(); 983 984 for (int v; enumer.hasMoreElements(); ) { 985 986 v = enumer.nextElement(); 987 RegEdge edge = supports[level].get(v); 988 // function check - checks if there is a support, starting from the 989 // current one. 990 if (!edge.check(activeLevels)) { 991 992 boolean stillSuported = false; 993 994 for (int st = activeLevels[level].value() - 1; st >= 0; st--) 995 if (stateLevels[level][st].updateSupport(edge, v)) { 996 stillSuported = true; 997 break; 998 } 999 1000 if (!stillSuported) { 1001 this.list[level].domain.inComplement(store.level, list[level], v); 1002 enumer.domainHasChanged(); 1003 } 1004 1005 } 1006 } 1007 1008 } 1009 } else { 1010 IntDomain varDom; 1011 /** 1012 * @todo implement possible improvement by checking when varDom.getSize() is equal to vars[level].getSize() 1013 * (no change to the domain of variable discovered early). In addition if there is some state which does 1014 * not cause extension of varDom then move it to the first position of the active states. It will group 1015 * state contributing different supports at the end of the array (beginning of the scan). 1016 */ 1017 for (int level = list.length - 1; level >= 0; level--) 1018 if (levelHadChanged[level]) { 1019 varDom = new IntervalDomain(); 1020 1021 for (int s = activeLevels[level].value() - 1; s >= 0; s--) { 1022 state = stateLevels[level][s]; 1023 for (int i = state.outDegree - 1; i >= 0; i--) 1024 state.add(varDom, i); 1025 } 1026 1027 if (debugAll) 1028 System.out.println(">>> Variable x_" + level + " had domain " + list[level].domain + " and now its " + varDom); 1029 1030 list[level].domain.in(store.level, list[level], varDom); 1031 } 1032 } 1033 1034 if (saveAllToLatex) 1035 saveLatexToFile("End of consistency level " + store.level); 1036 1037 touchedIndex.update(this.currentTouchedIndex); 1038 1039 } 1040 impose(Store store)1041 @Override @SuppressWarnings("unchecked") public void impose(Store store) { 1042 1043 if (optimizedMDD) 1044 initializeARRAY(fsm.transformIntoMDD(list)); 1045 else 1046 initializeARRAY(fsm); 1047 1048 super.impose(store); 1049 1050 store.registerRemoveLevelLateListener(this); 1051 1052 mapping = Var.positionMapping(list, true, this.getClass()); 1053 1054 lastNumberOfActiveStates = new int[list.length + 1]; 1055 activeLevels = new TimeStamp[list.length + 1]; 1056 for (int i = list.length; i >= 0; i--) 1057 activeLevels[i] = new TimeStamp<Integer>(store, activeLevelsTemp[i]); 1058 1059 leftChange = new TimeStamp<Integer>(store, 0); 1060 touchedIndex = new TimeStamp<Integer>(store, 0); 1061 1062 rightChange = new TimeStamp<Integer>(store, list.length - 1); 1063 1064 activeLevelsTemp = null; 1065 1066 if (oneSupport) { 1067 supports = (HashMap<Integer, RegEdge>[]) new HashMap[list.length]; 1068 RegState state; 1069 for (int level = this.list.length - 1; level >= 0; level--) { 1070 supports[level] = new HashMap<Integer, RegEdge>(); 1071 1072 for (int s = this.activeLevels[level].value() - 1; s >= 0; s--) { 1073 state = this.stateLevels[level][s]; 1074 for (int i = state.outDegree - 1; i >= 0; i--) 1075 state.setSupports(supports[level], i); 1076 } 1077 1078 /* 1079 ValueEnumeration enumer = vars[level].domain.valueEnumeration(); 1080 1081 for (int v; enumer.hasMoreElements();) { 1082 1083 v = enumer.nextElement(); 1084 // function check - checks if there is a support, starting from the 1085 // current one. 1086 if (supports[level].get(v) == null) { 1087 this.vars[level].domain.inComplement(store.level, vars[level], v); 1088 enumer.domainHasChanged(); 1089 } 1090 } 1091 */ 1092 1093 } 1094 } 1095 1096 levelHadChanged = new boolean[this.list.length + 1]; 1097 } 1098 getDefaultConsistencyPruningEvent()1099 @Override public int getDefaultConsistencyPruningEvent() { 1100 return IntDomain.ANY; 1101 } 1102 toString()1103 @Override public String toString() { 1104 1105 StringBuffer result = new StringBuffer(id()); 1106 result.append("( [ "); 1107 for (int i = 0; i < list.length; i++) 1108 result.append(list[i].id()).append(" "); 1109 result.append(" ], FSM \n"); 1110 result.append(fsm.toString()); 1111 result.append(")"); 1112 1113 return result.toString(); 1114 } 1115 1116 1117 imposeDecomposition(Store store)1118 @Override public void imposeDecomposition(Store store) { 1119 1120 if (constraints == null) 1121 constraints = decompose(store); 1122 1123 for (Constraint c : constraints) 1124 store.impose(c, queueIndex); 1125 1126 } 1127 1128 decompose(Store store)1129 @Override public List<Constraint> decompose(Store store) { 1130 1131 fsm.resize(); 1132 1133 List<int[]> listOfTuples = new ArrayList<int[]>(); 1134 1135 // tuples for transitions from not-intial states. 1136 1137 for (FSMState state : fsm.allStates) { 1138 1139 for (FSMTransition transition : state.transitions) { 1140 1141 for (ValueEnumeration enumer = transition.domain.valueEnumeration(); enumer.hasMoreElements(); ) { 1142 1143 int[] row = {state.id, enumer.nextElement(), transition.successor.id}; 1144 1145 listOfTuples.add(row); 1146 1147 } 1148 } 1149 } 1150 1151 int[][] tuples = new int[listOfTuples.size()][]; 1152 listOfTuples.toArray(tuples); 1153 1154 IntVar[] q = new IntVar[list.length + 1]; 1155 1156 for (int i = 0; i < q.length; i++) 1157 q[i] = new IntVar(store, "Q" + i, 0, fsm.allStates.size()); 1158 1159 constraints = new ArrayList<Constraint>(); 1160 1161 for (int i = 0; i < q.length - 1; i++) { 1162 IntVar[] scope = {q[i], list[i], q[i + 1]}; 1163 constraints.add(new ExtensionalSupportSTR(scope, tuples)); 1164 } 1165 1166 constraints.add(new XeqC(q[0], fsm.initState.id)); 1167 1168 IntervalDomain finalQ = new IntervalDomain(); 1169 for (FSMState finalState : fsm.finalStates) 1170 finalQ.unionAdapt(finalState.id, finalState.id); 1171 1172 constraints.add(new In(q[q.length - 1], finalQ)); 1173 1174 if (debugAll) { 1175 for (int[] tuple : tuples) { 1176 for (int val : tuple) 1177 System.out.print(val + " "); 1178 System.out.println(""); 1179 1180 System.out.println(fsm); 1181 } 1182 System.out.println(constraints); 1183 } 1184 1185 1186 return constraints; 1187 } 1188 1189 /** 1190 * It creates a latex description of the constraint state. 1191 * @param addDescription added description. 1192 * @return description of the constraint state. 1193 */ toLatex(String addDescription)1194 public String toLatex(String addDescription) { 1195 1196 // todo use StringBuffer in toLatex function. */ 1197 1198 String res = "\\begin{minipage}[b]{.4\\textwidth} \n"; 1199 res += addDescription + "\n"; 1200 res += "\\end{minipage} \n\\begin{minipage}[b]{.55\\textwidth} \n"; 1201 if (list != null) { 1202 String s1 = ""; 1203 String s2 = ""; 1204 String s3 = ""; 1205 for (Var v : list) { 1206 s1 += "c|"; 1207 s2 += "& $" + v.id() + "$ "; 1208 s3 += "& " + v.dom() + " "; 1209 } 1210 res += "\\begin{tabular}{|c|" + s1 + "}" + "\n"; 1211 res += "\\hline " + s2 + " \\\\" + "\n"; 1212 res += "\\hline Domain " + s3 + " \\\\" + "\n"; 1213 res += "\\hline " + "\n"; 1214 res += "\\end{tabular} \\\\ \n\\vspace{10mm} " + "\n"; 1215 } 1216 1217 res += "\\end{minipage}\n\\\\\n\\vspace{.7cm} \n"; 1218 res += "\\resizebox{!}{.17\\textheight}{\n\\resizebox{.17\\textwidth}{!}{ \n"; 1219 res += "\\tikzstyle{stateS}= [circle, fill=black!40, minimum size=25pt]"; 1220 res += "\\tikzstyle{active}= [draw, fill=black!40, minimum size=25pt]"; 1221 res += "\\tikzstyle{ann} = [above, text width=5em, text centered]"; 1222 res += "\\tikzstyle{n}= [circle, fill=black!15, minimum size=15pt]"; 1223 res += "\\begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto]" + "\n"; 1224 RegState init = this.stateLevels[0][0]; 1225 res += "\\node[active,initial] (q_" + init.level + init.id + ") {$q_{" + init.level + init.id + "}$};" + "\n"; 1226 RegState curState; 1227 String style; 1228 for (int l = 1; l < list.length + 1; l++) 1229 for (int i = 0; i < stateNumber; i++) { 1230 curState = getState(l, i); 1231 1232 if (curState == null) 1233 style = "n"; 1234 else if (curState.isActive(activeLevels)) 1235 style = "active"; 1236 else 1237 style = "stateS"; 1238 1239 if (i > 0) 1240 res += "\\node[" + style + "] (q_" + l + i + ") [below of=q_" + l + (i - 1) + "] {$q_{" + l + i + "}$};" + "\n"; 1241 else 1242 res += "\\node[" + style + "] (q_" + l + i + ") [right of=q_" + (l - 1) + i + "] {$q_{" + l + i + "}$};" + "\n"; 1243 } 1244 1245 res += "\\path[ann,->]"; 1246 for (int i = 0; i < stateLevels.length; i++) 1247 for (int r = 0; r < this.activeLevels[i].value(); r++) { 1248 RegState s = stateLevels[i][r]; 1249 for (int j = 0; j < s.outDegree; j++) { 1250 if (dNames != null) 1251 res += " (q_" + s.level + s.id + ") edge node {$" + dNames.get(s.sucDomToString(j)) + "$} (q_" 1252 + s.successors[j].level + s.successors[j].id + ")" + "\n"; 1253 else 1254 res += " (q_" + s.level + s.id + ") edge node {" + s.sucDomToString(j) + "} (q_" + s.successors[j].level 1255 + s.successors[j].id + ")" + "\n"; 1256 } 1257 } 1258 res += ";\n"; 1259 res += "\\end{tikzpicture}\\\\ " + "\n"; 1260 res += "}\n }\n"; 1261 return res; 1262 } 1263 1264 /** 1265 * It saves the constraint latex description into file. 1266 * @param desc description of the constraint 1267 */ saveLatexToFile(String desc)1268 public void saveLatexToFile(String desc) { 1269 String fileName = this.latexFile + (calls++) + ".tex"; 1270 File f = new File(fileName); 1271 try (FileOutputStream fs = new FileOutputStream(f)) { 1272 System.out.println("save latex file " + fileName); 1273 fs.write(this.toLatex(desc).getBytes("UTF-8")); 1274 fs.flush(); 1275 fs.close(); 1276 } catch (FileNotFoundException e) { 1277 e.printStackTrace(); 1278 } catch (NumberFormatException e) { 1279 e.printStackTrace(); 1280 } catch (IOException e) { 1281 e.printStackTrace(); 1282 } 1283 } 1284 1285 /** 1286 * It sets the filename for the file which is used to save latex descriptions. 1287 * @param filename the name of the file 1288 */ setLatexBaseFileName(String filename)1289 public void setLatexBaseFileName(String filename) { 1290 this.latexFile = filename; 1291 } 1292 1293 /** 1294 * It appends latex description of the constraint current state to the specified filename. 1295 * @param desc appended description. 1296 * @param fileName filename where the description is appended. 1297 */ uppendToLatexFile(String desc, String fileName)1298 public void uppendToLatexFile(String desc, String fileName) { 1299 try (OutputStreamWriter char_output = new OutputStreamWriter(new FileOutputStream(fileName), Charset.forName("UTF-8").newEncoder()); 1300 BufferedWriter fs = new BufferedWriter(char_output)) { 1301 1302 System.out.println("save latex file " + fileName); 1303 fs.append(this.toLatex(desc)); 1304 fs.flush(); 1305 fs.close(); 1306 } catch (FileNotFoundException e) { 1307 e.printStackTrace(); 1308 } catch (NumberFormatException e) { 1309 e.printStackTrace(); 1310 } catch (IOException e) { 1311 e.printStackTrace(); 1312 } 1313 } 1314 1315 /** 1316 * Initialization phase of the algorithm 1317 * 1318 * Considering that it needs to initialize the array of graph States - stateLevels, 1319 * and, thus, it needs to know the actual number of the states on each level I found 1320 * nothing better then run the initialization phase with the complete NxN array of states 1321 * and then copy the useful ones into a final array (which is ugly) 1322 * 1323 */ 1324 initializeARRAY(MDD mdd)1325 @SuppressWarnings("unchecked") private void initializeARRAY(MDD mdd) { 1326 1327 int levels = this.list.length; 1328 1329 //Initialization of the future state array 1330 //and the time-stamps with the number of active states 1331 this.stateLevels = new RegState[levels + 1][]; 1332 1333 List<RegState>[] layeredGraph = (ArrayList<RegState>[]) Array.newInstance(new ArrayList<RegState>().getClass(), levels + 1); 1334 for (int i = 0; i < layeredGraph.length; i++) 1335 layeredGraph[i] = new ArrayList<RegState>(); 1336 1337 this.activeLevelsTemp = new int[this.list.length + 1]; 1338 1339 int[] currentPosition = new int[list.length]; 1340 int[] currentOffset = new int[list.length]; 1341 RegState[] currentState = new RegState[list.length + 1]; 1342 1343 int currentLevel = 0; 1344 int noNeighbours = 0; 1345 1346 for (int i = 0; i < list[0].getSize(); i++) 1347 if (mdd.diagram[i] != MDD.NOEDGE) 1348 noNeighbours++; 1349 1350 currentState[0] = new RegStateInt(currentLevel, 0, noNeighbours, activeLevelsTemp[currentLevel]++); 1351 currentState[list.length] = new RegStateInt(list.length, 0, 0, activeLevelsTemp[list.length]++); 1352 1353 layeredGraph[0].add(currentState[currentLevel]); 1354 layeredGraph[list.length].add(currentState[list.length]); 1355 1356 currentPosition[0] = 0; 1357 currentOffset[0] = 0; 1358 currentLevel = 0; 1359 1360 while (currentLevel != -1) { 1361 1362 if (currentOffset[currentLevel] >= list[currentLevel].getSize()) { 1363 currentLevel--; 1364 if (currentLevel >= 0) 1365 currentOffset[currentLevel]++; 1366 continue; 1367 } 1368 1369 int nextNodePosition = mdd.diagram[currentPosition[currentLevel] + currentOffset[currentLevel]]; 1370 1371 // no path with a given value from a current node. 1372 if (nextNodePosition == MDD.NOEDGE) { 1373 currentOffset[currentLevel]++; 1374 continue; 1375 } 1376 1377 if (nextNodePosition == MDD.TERMINAL) { 1378 currentState[currentLevel] 1379 .addTransition(currentState[list.length], mdd.views[currentLevel].indexToValue[currentOffset[currentLevel]]); 1380 currentOffset[currentLevel]++; 1381 continue; 1382 } 1383 1384 boolean visited = false; 1385 1386 RegState s = null; 1387 for (RegState state : layeredGraph[currentLevel + 1]) 1388 if (state.id == nextNodePosition) { 1389 s = state; 1390 visited = true; 1391 } 1392 1393 if (s == null) { 1394 noNeighbours = 0; 1395 1396 if (currentLevel + 1 < list.length) 1397 for (int j = nextNodePosition; j < nextNodePosition + list[currentLevel + 1].getSize(); j++) 1398 if (mdd.diagram[j] != MDD.NOEDGE) 1399 noNeighbours++; 1400 1401 1402 s = new RegStateInt(currentLevel + 1, nextNodePosition, noNeighbours, activeLevelsTemp[currentLevel + 1]++); 1403 layeredGraph[currentLevel + 1].add(s); 1404 } 1405 1406 currentState[currentLevel].addTransition(s, mdd.views[currentLevel].indexToValue[currentOffset[currentLevel]]); 1407 1408 if (visited) { 1409 currentOffset[currentLevel]++; 1410 continue; 1411 } 1412 1413 currentLevel++; 1414 1415 currentState[currentLevel] = s; 1416 currentOffset[currentLevel] = 0; 1417 currentPosition[currentLevel] = nextNodePosition; 1418 1419 } 1420 1421 for (int i = 0; i < layeredGraph.length; i++) { 1422 stateLevels[i] = new RegState[layeredGraph[i].size()]; 1423 int j = 0; 1424 for (RegState state : layeredGraph[i]) { 1425 stateLevels[i][j] = state; 1426 j++; 1427 } 1428 } 1429 1430 } 1431 1432 1433 1434 } 1435