Generated on Sat Feb 7 2015 02:01:11 for Gecode by doxygen 1.8.9.1
colored-matrix.cpp
Go to the documentation of this file.
1 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2 /*
3  * Main authors:
4  * Mikael Lagerkvist <lagerkvist@gecode.org>
5  *
6  * Copyright:
7  * Mikael Lagerkvist, 2012
8  *
9  * Last modified:
10  * $Date: 2013-07-08 14:22:40 +0200 (Mon, 08 Jul 2013) $ by $Author: schulte $
11  * $Revision: 13820 $
12  *
13  * This file is part of Gecode, the generic constraint
14  * development environment:
15  * http://www.gecode.org
16  *
17  * Permission is hereby granted, free of charge, to any person obtaining
18  * a copy of this software and associated documentation files (the
19  * "Software"), to deal in the Software without restriction, including
20  * without limitation the rights to use, copy, modify, merge, publish,
21  * distribute, sublicense, and/or sell copies of the Software, and to
22  * permit persons to whom the Software is furnished to do so, subject to
23  * the following conditions:
24  *
25  * The above copyright notice and this permission notice shall be
26  * included in all copies or substantial portions of the Software.
27  *
28  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
29  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
30  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
31  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
32  * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
33  * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
34  * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
35  *
36  */
37 
38 #include <gecode/driver.hh>
39 #include <gecode/int.hh>
40 #include <gecode/minimodel.hh>
41 
42 #include <fstream>
43 
44 using namespace Gecode;
45 
50 class ColoredMatrixOptions : public Options {
51 private:
61  Driver::StringOption _not_all_equal;
63  Driver::StringOption _same_or_0;
65  Driver::StringOption _distinct_except_0;
67  Driver::StringOption _no_monochrome_rectangle;
68 
69 public:
71  ColoredMatrixOptions(const char* n);
72 
74  void parse(int& argc, char* argv[]) {
75  Options::parse(argc,argv);
76  }
77 
79  unsigned int height(void) const {
80  if (_size.value() == 0)
81  return _height.value();
82  else
83  return _size.value();
84  }
86  unsigned int width(void) const {
87  if (_size.value() == 0)
88  return _width.value();
89  else
90  return _size.value();
91  }
93  unsigned int colors(void) const { return _colors.value(); }
95  int not_all_equal(void) const { return _not_all_equal.value(); }
97  int same_or_0(void) const { return _same_or_0.value(); }
99  int distinct_except_0(void) const { return _distinct_except_0.value(); }
101  int no_monochrome_rectangle(void) const {
102  return _no_monochrome_rectangle.value();
103  }
104 };
105 
106 namespace {
115 
122  DFA same_or_0_dfa(unsigned int colors);
123 
130  TupleSet same_or_0_tuple_set(unsigned int colors);
131 
134  DFA distinct_except_0_dfa(unsigned int colors);
135 
138  DFA no_monochrome_rectangle_dfa(unsigned int colors);
139 
142  IntSetArgs distinct_except_0_counts(unsigned int colors, unsigned int size);
143 
146  DFA not_all_equal_dfa(unsigned int colors);
147 
149 }
150 
169 protected:
174  const unsigned int height;
175  const unsigned int width;
176  const unsigned int colors;
177 
178 
182  IntVarArray x;
187 
190  IntVar same_or_0(const IntVar& a, const IntVar& b)
191  {
192  switch (opt.same_or_0()) {
193  case SAME_OR_0_REIFIED: {
194  IntVar result(*this, 0, colors);
195  BoolVar same = expr(*this, (a == b));
196  rel(*this, result, IRT_EQ, a, same);
197  // Redundant (implied by previous), but improves efficiency
198  rel(*this, result, IRT_NQ, 0, same);
199  return result;
200  }
201  case SAME_OR_0_TUPLE_SET: {
202  static TupleSet table = same_or_0_tuple_set(colors);
203  IntVar result(*this, 0, colors);
204  extensional(*this, IntVarArgs() << a << b << result, table);
205  return result;
206  }
207  case SAME_OR_0_DFA: {
208  static const DFA automaton = same_or_0_dfa(colors);
209  IntVar result(*this, 0, colors);
210  extensional(*this, IntVarArgs() << a << b << result, automaton);
211  return result;
212  }
213  default:
214  GECODE_NEVER;
215  return IntVar(*this, 0, 0);
216  }
217  }
218 
222  {
223  switch (opt.distinct_except_0()) {
224  case DISTINCT_EXCEPT_0_REIFIED:
225  for (int i = v.size(); i--; ) {
226  BoolVar viIsZero = expr(*this, v[i] == 0);
227  for (int j = i; j--; ) {
228  rel(*this, viIsZero || (v[i] != v[j]));
229  }
230  }
231  break;
232  case DISTINCT_EXCEPT_0_DFA: {
233  static const DFA automaton = distinct_except_0_dfa(colors);
234  extensional(*this, v, automaton);
235  break;
236  }
237  case DISTINCT_EXCEPT_0_COUNT: {
238  static const IntSetArgs counts = distinct_except_0_counts(colors, std::max(width, height));
239  count(*this, v, counts, opt.icl());
240  break;
241  }
242  }
243  }
244 
248  {
249  switch (opt.not_all_equal()) {
250  case NOT_ALL_EQUAL_NQ: {
251  rel(*this, v, IRT_NQ);
252  break;
253  }
254  case NOT_ALL_EQUAL_NAIVE: {
255  // At least one pair must be different.
256  // Bad decomposition since too many disjuncts are created.
257  BoolVarArgs disequalities;
258  for (int i = v.size(); i--; )
259  for (int j = i; j--; )
260  disequalities << expr(*this, v[i] != v[j]);
261  rel(*this, BOT_OR, disequalities, 1);
262  break;
263  }
264  case NOT_ALL_EQUAL_REIFIED: {
265  // It must not be the case that all are equal
266  BoolVarArgs equalities;
267  for (int i = 0; i < v.size()-1; ++i)
268  equalities << expr(*this, v[i] == v[i+1]);
269  rel(*this, BOT_AND, equalities, 0);
270  break;
271  }
272  case NOT_ALL_EQUAL_NVALUES:
273  // More than one number
274  nvalues(*this, v, IRT_GR, 1);
275  break;
276  case NOT_ALL_EQUAL_COUNT:
277  // No number in all positions
278  count(*this, v, IntSet(0, v.size()-1), IntArgs::create(colors, 1), opt.icl());
279  break;
280  case NOT_ALL_EQUAL_DFA: {
281  static const DFA automaton = not_all_equal_dfa(colors);
282  extensional(*this, v, automaton);
283  break;
284  }
285  }
286  }
287 
292  const unsigned int length = v1.size();
293  switch (opt.no_monochrome_rectangle()) {
294  case NO_MONOCHROME_DECOMPOSITION: {
295  IntVarArgs z(length);
296  for (unsigned int i = 0; i < length; ++i) {
297  z[i] = same_or_0(v1[i], v2[i]);
298  }
299  distinct_except_0(z);
300  break;
301  }
302  case NO_MONOCHROME_DFA: {
303  static const DFA automaton = no_monochrome_rectangle_dfa(colors);
304  IntVarArgs z(2*length);
305  for (int i = length; i--; ) {
306  z[2*i + 0] = v1[i];
307  z[2*i + 1] = v2[i];
308  }
309  extensional(*this, z, automaton);
310  break;
311  }
312  }
313  }
314 
315 
316 public:
318  enum {
321  };
323  enum {
324  SYMMETRY_NONE = 0,
325  SYMMETRY_MATRIX = 1,
326  SYMMETRY_VALUES = 2,
327  };
329  enum {
330  MODEL_CORNERS = 1,
331  MODEL_ROWS = 2,
332  MODEL_COLUMNS = 4,
333  };
335  enum {
342  };
344  enum {
348  };
350  enum {
354  };
356  enum {
359  };
360 
361 
364  : opt(opt0), height(opt.height()), width(opt.width()), colors(opt.colors()),
365  x(*this, height*width, 1, colors),
366  max_color(*this, 1, colors)
367  {
368 
369  max(*this, x, max_color);
370 
371  Matrix<IntVarArray> m(x, width, height);
372 
373  // For each pair of columns and rows, the intersections may not be equal.
374  if (opt.model() & MODEL_CORNERS) {
375  for (unsigned int c1 = 0; c1 < width; ++c1) {
376  for (unsigned int c2 = c1+1; c2 < width; ++c2) {
377  for (unsigned int r1 = 0; r1 < height; ++r1) {
378  for (unsigned int r2 = r1+1; r2 < height; ++r2) {
379  not_all_equal(IntVarArgs() << m(c1,r1) << m(c1,r2) << m(c2,r1) << m(c2,r2));
380  }
381  }
382  }
383  }
384  }
385  // Given two rows/columns, construct variables representing if
386  // the corresponding places are equal (and if so, what value).
387  // For the new values, no non-zero value may appear more than
388  // once.
389  if (opt.model() & MODEL_ROWS) {
390  for (unsigned int r1 = 0; r1 < height; ++r1) {
391  for (unsigned int r2 = r1+1; r2 < height; ++r2) {
392  no_monochrome_rectangle(m.row(r1), m.row(r2));
393  }
394  }
395  }
396  if (opt.model() & MODEL_COLUMNS) {
397  for (unsigned int c1 = 0; c1 < width; ++c1) {
398  for (unsigned int c2 = c1+1; c2 < width; ++c2) {
399  no_monochrome_rectangle(m.col(c1), m.col(c2));
400  }
401  }
402  }
403 
404  // Symmetry breaking constraints.
405  {
406  // Lexical order for all columns and rows (all are interchangable)
407  if (opt.symmetry() & SYMMETRY_MATRIX) {
408  for (unsigned int r = 0; r < height-1; ++r) {
409  rel(*this, m.row(r), IRT_LE, m.row(r+1));
410  }
411  for (unsigned int c = 0; c < width-1; ++c) {
412  rel(*this, m.col(c), IRT_LE, m.col(c+1));
413  }
414  }
415 
416  // Value precedence. Compatible with row/column ordering
417  if (opt.symmetry() & SYMMETRY_VALUES) {
418  precede(*this, x, IntArgs::create(colors, 1));
419  }
420  }
421 
423  }
424 
426  virtual IntVar cost(void) const {
427  return max_color;
428  }
429 
431  virtual void
432  print(std::ostream& os) const {
433  Matrix<IntVarArray> m(x, width, height);
434  for (unsigned int r = 0; r < height; ++r) {
435  os << "\t";
436  for (unsigned int c = 0; c < width; ++c) {
437  os << m(c, r) << " ";
438  }
439  os << std::endl;
440  }
441  os << std::endl;
442  os << "\tmax color: " << max_color << std::endl;
443  os << std::endl;
444  }
445 
447  ColoredMatrix(bool share, ColoredMatrix& s)
448  : IntMinimizeScript(share,s), opt(s.opt),
449  height(s.height), width(s.width), colors(s.colors) {
450  x.update(*this, share, s.x);
451  max_color.update(*this, share, s.max_color);
452  }
454  virtual Space*
455  copy(bool share) {
456  return new ColoredMatrix(share,*this);
457  }
458 };
459 
461  : Options(n),
462  _height("-height", "Height of matrix", 8),
463  _width("-width", "Width of matrix", 8),
464  _size("-size", "If different from 0, used as both width and height", 0),
465  _colors("-colors", "Maximum number of colors", 4),
466  _not_all_equal("-not-all-equal", "How to implement the not all equals constraint (used in corners model)",
467  ColoredMatrix::NOT_ALL_EQUAL_NQ),
468  _same_or_0("-same-or-0", "How to implement the same or 0 constraint (used in the decomposed no monochrome rectangle constraint)",
469  ColoredMatrix::SAME_OR_0_DFA),
470  _distinct_except_0("-distinct-except-0", "How to implement the distinct except 0 constraint (used in the decomposed no monochrome rectangle constraint)",
471  ColoredMatrix::DISTINCT_EXCEPT_0_DFA),
472  _no_monochrome_rectangle("-no-monochrome-rectangle", "How to implement no monochrome rectangle (used in the rows model)",
473  ColoredMatrix::NO_MONOCHROME_DFA)
474 {
475  add(_height);
476  add(_width);
477  add(_size);
478  add(_colors);
479  add(_not_all_equal);
480  add(_same_or_0);
481  add(_distinct_except_0);
482  add(_no_monochrome_rectangle);
483 
484  // Add search options
485  _search.add(ColoredMatrix::SEARCH_DFS, "dfs", "Find a solution.");
486  _search.add(ColoredMatrix::SEARCH_BAB, "bab", "Find an optimal solution.");
488 
489  // Add symmetry options
490  _symmetry.add(ColoredMatrix::SYMMETRY_NONE, "none", "Don't use symmetry breaking.");
491  _symmetry.add(ColoredMatrix::SYMMETRY_MATRIX, "matrix", "Order matrix rows and columns");
492  _symmetry.add(ColoredMatrix::SYMMETRY_VALUES, "values", "Order values");
494  "both", "Order both rows/columns and values");
496 
497  // Add model options
498  _model.add(ColoredMatrix::MODEL_CORNERS, "corner", "Use direct corners model with not-all-equal constraints.");
499  _model.add(ColoredMatrix::MODEL_ROWS, "rows", "Use model on pairs of rows (same_or_0 and distinct_except_0 constraints).");
501  "both", "Use both rows and corners model");
502  _model.add(ColoredMatrix::MODEL_COLUMNS, "columns", "Use model on pairs of columns (same_or_0 and distinct_except_0 constraints).");
504  "matrix", "Use both rows and columns model");
506 
507  // Add not all equal variants
508  _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_NQ, "nq", "Use nq constraint.");
509  _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_NAIVE, "naive", "Use naive reified decomposition.");
510  _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_REIFIED, "reified", "Use reified decomposition.");
511  _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_NVALUES, "nvalues", "Use nvalues.");
512  _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_COUNT, "count", "Use count.");
513  _not_all_equal.add(ColoredMatrix::NOT_ALL_EQUAL_DFA, "dfa", "Use dfa.");
514 
515  // Add same or 0 variants
516  _same_or_0.add(ColoredMatrix::SAME_OR_0_REIFIED, "reified", "Use reified decomposition.");
517  _same_or_0.add(ColoredMatrix::SAME_OR_0_TUPLE_SET, "tuple-set", "Use tuple set representation.");
518  _same_or_0.add(ColoredMatrix::SAME_OR_0_DFA, "dfa", "Use dfa representation.");
519 
520  // Add distinct except 0 variants
521  _distinct_except_0.add(ColoredMatrix::DISTINCT_EXCEPT_0_REIFIED, "reified", "Use reified decomposition.");
522  _distinct_except_0.add(ColoredMatrix::DISTINCT_EXCEPT_0_DFA, "dfa", "Use dfa decomposition.");
523  _distinct_except_0.add(ColoredMatrix::DISTINCT_EXCEPT_0_COUNT, "count", "Use global cardinality.");
524 
525  // Add no monochrome rectangle variants
526  _no_monochrome_rectangle.add(ColoredMatrix::NO_MONOCHROME_DECOMPOSITION,
527  "decompositions",
528  "Use decompositions into same_or_0 and distinct_except_0.");
529  _no_monochrome_rectangle.add(ColoredMatrix::NO_MONOCHROME_DFA,
530  "dfa",
531  "Use DFA as direct implementation.");
532 }
533 
537 int
538 main(int argc, char* argv[]) {
539  ColoredMatrixOptions opt("Colored matrix");
540  opt.parse(argc,argv);
541  if (opt.search() == ColoredMatrix::SEARCH_DFS) {
542  Script::run<ColoredMatrix,DFS,ColoredMatrixOptions>(opt);
543  } else {
544  Script::run<ColoredMatrix,BAB,ColoredMatrixOptions>(opt);
545  }
546  return 0;
547 }
548 
549 
550 namespace {
551  DFA same_or_0_dfa(unsigned int colors)
552  {
553  /* DFA over variable sequences (x,y,z) where z equals x/y if x and
554  * y are equal, and z equals 0 otherwise.
555  *
556  * DFA is constructed to contain paths
557  * start -- c --> node -- c --> node' -- c --> end
558  * for all colors c representing the case when x and y
559  * are equal.
560  *
561  * For the cases where x and y are non-equal (c and c'), paths
562  * start -- c --> node -- c' --> not-equal -- 0 --> end
563  * are added.
564  */
565 
566  const int start_state = 0;
567  const int not_equal_state = 2*colors+1;
568  const int final_state = 2*colors+2;
569 
570  int n_transitions = colors*colors + 2*colors + 2;
571  DFA::Transition* trans = new DFA::Transition[n_transitions];
572  int current_transition = 0;
573 
574  // From start state
575  for (unsigned int color = 1; color <= colors; ++color) {
576  trans[current_transition++] =
577  DFA::Transition(start_state, color, color);
578  }
579 
580  // From first level states (indices [1..color])
581  // To second-level if same color, otherwise to not_equal_state
582  for (unsigned int state = 1; state <= colors; ++state) {
583  for (unsigned int color = 1; color <= colors; ++color) {
584  if (color == state) {
585  trans[current_transition++] =
586  DFA::Transition(state, color, colors+state);
587  } else {
588  trans[current_transition++] =
589  DFA::Transition(state, color, not_equal_state);
590  }
591  }
592  }
593 
594  // From second level states (indices [colors+1..colors+colors])
595  // To final state with the same color
596  for (unsigned int color = 1; color <= colors; ++color) {
597  trans[current_transition++] =
598  DFA::Transition(colors+color, color, final_state);
599  }
600 
601  // From not equal state to final state
602  trans[current_transition++] =
603  DFA::Transition(not_equal_state, 0, final_state);
604 
605  // End sentinel
606  trans[current_transition++] =
607  DFA::Transition(-1, 0, -1);
608 
609  int final_states[] = {final_state, -1};
610 
611  DFA result(start_state, trans, final_states, true);
612 
613  delete[] trans;
614 
615  return result;
616  }
617 
618  TupleSet same_or_0_tuple_set(unsigned int colors)
619  {
620  TupleSet result;
621  for (unsigned int i = 1; i <= colors; ++i) {
622  for (unsigned int j = 1; j <= colors; ++j) {
623  if (i == j) {
624  result.add(IntArgs(3, i, j, i));
625  } else {
626  result.add(IntArgs(3, i, j, 0));
627  }
628  }
629  }
630  result.finalize();
631  return result;
632  }
633 
634  DFA distinct_except_0_dfa(unsigned int colors)
635  {
636  /* DFA for a sequence that may use each color only once (and all
637  * others are zero).
638  *
639  * For n colors, 2^n nodes are used. For each node, if bit b is one, then
640  * that color has not been used yet. All nodes have self-loops for zero, and
641  * edges for still usable colors to the node with the corresponding bit un-set.
642  * All nodes are final nodes.
643  */
644 
645  const int nstates = 1 << colors;
646  const int start_state = nstates-1;
647 
648  DFA::Transition* trans = new DFA::Transition[nstates*colors + 1];
649  int current_transition = 0;
650 
651  for (int state = nstates; state--; ) {
652  trans[current_transition++] = DFA::Transition(state, 0, state);
653 
654  for (unsigned int color = 1; color <= colors; ++color) {
655  const unsigned int color_bit = (1 << (color-1));
656  if (state & color_bit) {
657  trans[current_transition++] =
658  DFA::Transition(state, color, state & ~color_bit);
659  }
660  }
661  }
662  trans[current_transition++] = DFA::Transition(-1, 0, -1);
663 
664  int* final_states = new int[nstates+1];
665  final_states[nstates] = -1;
666  for (int i = nstates; i--; ) {
667  final_states[i] = i;
668  }
669 
670  DFA result(start_state, trans, final_states);
671 
672  delete[] trans;
673  delete[] final_states;
674 
675  return result;
676  }
677 
678  DFA no_monochrome_rectangle_dfa(unsigned int colors)
679  {
680  /* DFA for a sequence of pairs, where each monochromatic pair may
681  * only appear once.
682  *
683  * For n colors, there are 2^n base states representing which
684  * monochromatic pairs are still available. For each base state s,
685  * the color seen goes to a new intermediate state. A different
686  * color will go back to state s. Seeing the same color will move
687  * to the next base state with that color combination removed (if
688  * it is still allowed).
689  *
690  * In essence, this DFA represents the combination of same_or_0
691  * and distinct_except_0 as a single constraint.
692  */
693 
694  const int base_states = 1 << colors;
695  const int start_state = base_states-1;
696  const int nstates = base_states + colors*base_states;
697 
698  DFA::Transition* trans = new DFA::Transition[nstates*colors + 1];
699  int current_transition = 0;
700 
701  for (int state = base_states; state--; ) {
702  for (unsigned int color = 1; color <= colors; ++color) {
703  const unsigned int color_bit = (1 << (color-1));
704  const int color_remembered_state = state + color*base_states;
705 
706  trans[current_transition++] =
707  DFA::Transition(state, color, color_remembered_state);
708 
709  for (unsigned int next_color = 1; next_color <= colors; ++next_color) {
710  if (next_color == color) {
711  // Two equal adjacent, only transition if color still allowed
712  if (state & color_bit) {
713  trans[current_transition++] =
714  DFA::Transition(color_remembered_state, color, state & ~color_bit);
715  }
716  } else {
717  trans[current_transition++] =
718  DFA::Transition(color_remembered_state, next_color, state);
719  }
720  }
721  }
722  }
723  trans[current_transition++] = DFA::Transition(-1, 0, -1);
724  assert(current_transition <= nstates*colors+1);
725 
726  int* final_states = new int[base_states+1];
727  final_states[base_states] = -1;
728  for (int i = base_states; i--; ) {
729  final_states[i] = i;
730  }
731 
732  DFA result(start_state, trans, final_states);
733 
734  delete[] trans;
735  delete[] final_states;
736 
737  return result;
738  }
739 
740  IntSetArgs distinct_except_0_counts(unsigned int colors, unsigned int size)
741  {
742  IntSetArgs result(colors+1);
743 
744  result[0] = IntSet(0, size);
745 
746  for (unsigned int i = 1; i <= colors; ++i) {
747  result[i] = IntSet(0, 1);
748  }
749 
750  return result;
751  }
752 
753 
754  DFA not_all_equal_dfa(unsigned int colors)
755  {
756  /* DFA for not all equal.
757  *
758  * From the start state, there is a transition for each color to
759  * that colors state. As long as the same color is seen, the
760  * automaton stays in that state. If a different color is seen,
761  * then it goes to the accepting state.
762  */
763 
764  const int nstates = 1 + colors + 1;
765  const int start_state = 0;
766  const int final_state = nstates-1;
767 
768  DFA::Transition* trans = new DFA::Transition[2*colors + colors*colors + 1];
769  int current_transition = 0;
770 
771  // Each color to its own state
772  for (unsigned int color = 1; color <= colors; ++color) {
773  trans[current_transition++] = DFA::Transition(start_state, color, color);
774  }
775 
776  // Each colors state loops on itself, and goes to final on all others
777  for (unsigned int state = 1; state <= colors; ++state) {
778  for (unsigned int color = 1; color <= colors; ++color) {
779  if (state == color) {
780  trans[current_transition++] = DFA::Transition(state, color, state);
781  } else {
782  trans[current_transition++] = DFA::Transition(state, color, final_state);
783  }
784  }
785  }
786 
787  // Loop on all colors in final state
788  for (unsigned int color = 1; color <= colors; ++color) {
789  trans[current_transition++] = DFA::Transition(final_state, color, final_state);
790  }
791 
792  trans[current_transition++] = DFA::Transition(-1, 0, -1);
793 
794  int final_states[] = {final_state, -1};
795 
796  DFA result(start_state, trans, final_states);
797 
798  delete[] trans;
799 
800  return result;
801  }
802 
803 }
804 
805 
806 // STATISTICS: example-any
static IntArgs create(int n, int start, int inc=1)
Allocate array with n elements such that for all .
Definition: array.hpp:72
Use count for implementing not all equals.
Use model on pairs of rows.
void value(int v)
Set default value to v.
Definition: options.hpp:62
virtual void print(std::ostream &os) const
Print solution.
Use nvalues for implementing not all equals.
void finalize(void)
Finalize tuple set.
Definition: tuple-set.hpp:111
Example: Colored matrix example.
virtual Space * copy(bool share)
Copy during cloning.
const FloatNum max
Largest allowed float value.
Definition: float.hh:831
TupleSet same_or_0_tuple_set(unsigned int colors)
int size(void) const
Return size of array (number of elements)
Definition: array.hpp:1662
void update(Space &home, bool share, VarImpVar< VarImp > &y)
Update this variable to be a clone of variable y.
Definition: var.hpp:128
Use dfa for same or 0.
const unsigned int height
Height of matrix.
void max(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:57
unsigned int width(void) const
Return width.
Find optimal solution.
void add(int v, const char *o, const char *h=NULL)
Add option value for value v, string o, and help text h.
Definition: options.cpp:121
IntVar same_or_0(const IntVar &a, const IntVar &b)
unsigned int height(void) const
Return height.
Conjunction.
Definition: int.hh:917
Use direct constraint for implemeting not all equals.
Use dfa for implementing not all equals.
IntVarBranch INT_VAR_SIZE_MIN(BranchTbl tbl)
Select variable with smallest domain size.
Definition: var.hpp:212
IntVarBranch INT_VAR_MIN_MIN(BranchTbl tbl)
Select variable with smallest min.
Definition: var.hpp:192
Integer variable array.
Definition: int.hh:741
Use dfa for distinct except 0.
Greater ( )
Definition: int.hh:909
Use model on pairs of columns.
Use tuple set for same or 0.
Computation spaces.
Definition: core.hpp:1362
Parametric base-class for scripts.
Definition: driver.hh:622
IntSetArgs distinct_except_0_counts(unsigned int colors, unsigned int size)
void add(Driver::BaseOption &o)
Add new option o.
Definition: options.cpp:264
void value(unsigned int v)
Set default value to v.
Definition: options.hpp:95
int no_monochrome_rectangle(void) const
Return how to implement distinct except 0.
int same_or_0(void) const
Return how to implement same or 0.
Driver::StringOption _model
General model options.
Definition: driver.hh:330
void parse(int &argc, char *argv[])
Parse options from arguments argv (number is argc)
void update(Space &, bool share, VarArray< Var > &a)
Update array to be a clone of array a.
Definition: array.hpp:1072
Gecode::FloatVal c(-8, 8)
Deterministic finite automaton (DFA)
Definition: int.hh:1881
bool same(const ConstView< ViewA > &, const ConstView< ViewB > &)
Test whether two views are the same.
Definition: view.hpp:603
const ColoredMatrixOptions & opt
Options for model.
Gecode::IntArgs i(4, 1, 2, 3, 4)
Use dfa for no monochrome rectangle.
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:238
Equality ( )
Definition: int.hh:904
Options opt
The options.
Definition: test.cpp:101
void not_all_equal(const IntVarArgs &v)
unsigned int colors(void) const
Return number of colors.
Use reification for same or 0.
NNF * r
Right subtree.
Definition: bool-expr.cpp:246
int distinct_except_0(void) const
Return how to implement distinct except 0.
virtual IntVar cost(void) const
Return cost.
IntValBranch INT_VAL_MIN(void)
Select smallest value.
Definition: val.hpp:68
Specification of a DFA transition.
Definition: int.hh:1887
unsigned int size(I &i)
Size of all ranges of range iterator i.
Order rows and columns of matrix.
DFA not_all_equal_dfa(unsigned int colors)
Unsigned integer option.
Definition: driver.hh:229
Slice< A > row(int r) const
Access row r.
Definition: matrix.hpp:181
void distinct_except_0(const IntVarArgs &v)
Driver::StringOption _search
Search options.
Definition: driver.hh:340
void precede(Home home, const IntVarArgs &x, int s, int t, IntConLevel)
Post propagator that s precedes t in x.
Definition: precede.cpp:47
ColoredMatrixOptions.
Less ( )
Definition: int.hh:907
Integer sets.
Definition: int.hh:171
Driver::StringOption _symmetry
General symmetry options.
Definition: driver.hh:331
Disjunction.
Definition: int.hh:918
Passing integer variables.
Definition: int.hh:636
DFA no_monochrome_rectangle_dfa(unsigned int colors)
No symmetry breaking.
Passing integer arguments.
Definition: int.hh:607
Passing Boolean variables.
Definition: int.hh:690
void search(int v)
Set default search value.
Definition: options.hpp:230
Boolean integer variables.
Definition: int.hh:491
void parse(int &argc, char *argv[])
Parse options from arguments argv (number is argc)
Definition: options.cpp:331
const int v[7]
Definition: distinct.cpp:207
Class represeting a set of tuples.
Definition: int.hh:2022
const unsigned int width
Width of matrix.
String-valued option (integer value defined by strings)
Definition: driver.hh:174
TieBreak< VarBranch > tiebreak(VarBranch a, VarBranch b)
Combine variable selection criteria a and b for tie-breaking.
void extensional(Home home, const IntVarArgs &x, DFA dfa, IntConLevel)
Post domain consistent propagator for extensional constraint described by a DFA.
Definition: extensional.cpp:45
void no_monochrome_rectangle(IntVarArgs v1, IntVarArgs v2)
Order value occurences.
BoolVar expr(Home home, const BoolExpr &e, IntConLevel icl)
Post Boolean expression and return its value.
Definition: bool-expr.cpp:632
Use model on corner combinations.
Node * x
Pointer to corresponding Boolean expression node.
Definition: bool-expr.cpp:253
void count(Home home, const IntVarArgs &x, int n, IntRelType irt, int m, IntConLevel)
Post propagator for .
Definition: count.cpp:44
Use decomposition for no monochrome rectangle.
ColoredMatrix(const ColoredMatrixOptions &opt0)
Actual model.
IntVarArray x
Array for matrix variables.
Integer variables.
Definition: int.hh:350
DFA distinct_except_0_dfa(unsigned int colors)
int main(int argc, char *argv[])
Main-function.
void symmetry(int v)
Set default symmetry value.
Definition: options.hpp:168
void rel(Home home, FloatVar x0, FloatRelType frt, FloatVal n)
Propagates .
Definition: rel.cpp:47
DFA same_or_0_dfa(unsigned int colors)
int not_all_equal(void) const
Return how to implement not all equals.
ColoredMatrix(bool share, ColoredMatrix &s)
Constructor for cloning s.
Matrix-interface for arrays.
Definition: minimodel.hh:1924
const unsigned int colors
Number of colors to use.
Use reification for distinct except 0.
void model(int v)
Set default model value.
Definition: options.hpp:155
struct Gecode::@518::NNF::@57::@58 b
For binary nodes (and, or, eqv)
Gecode toplevel namespace
Use naive reification for implemeting not all equals.
IntVar max_color
Maximum color used.
Disequality ( )
Definition: int.hh:905
Slice< A > col(int c) const
Access column c.
Definition: matrix.hpp:187
BrancherHandle branch(Home home, const FloatVarArgs &x, FloatVarBranch vars, FloatValBranch vals, FloatBranchFilter bf, FloatVarValPrint vvp)
Branch over x with variable selection vars and value selection vals.
Definition: branch.cpp:43
Use reification for implemeting not all equals.
ColoredMatrixOptions(const char *n)
Initialize options for example with name n.
void add(const IntArgs &tuple)
Add tuple to tuple set.
Definition: tuple-set.hpp:98
#define GECODE_NEVER
Assert that this command is never executed.
Definition: macros.hpp:60
void nvalues(Home home, const IntVarArgs &x, IntRelType irt, int y, IntConLevel)
Post propagator for .
Definition: nvalues.cpp:44
Options for scripts
Definition: driver.hh:326
void icl(IntConLevel i)
Set default integer consistency level.
Definition: options.hpp:194
struct Gecode::@518::NNF::@57::@59 a
For atomic nodes.
Use count for distinct except 0.