this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2/*
3 * Main authors:
4 * Linnea Ingmar <linnea.ingmar@hotmail.com>
5 * Mikael Lagerkvist <lagerkvist@gecode.org>
6 * Christian Schulte <schulte@gecode.org>
7 *
8 * Copyright:
9 * Linnea Ingmar, 2017
10 * Mikael Lagerkvist, 2007
11 * Christian Schulte, 2004
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#ifndef GECODE_INT_EXTENSIONAL_HH
39#define GECODE_INT_EXTENSIONAL_HH
40
41#include <gecode/int.hh>
42
43#include <gecode/int/rel.hh>
44
45/**
46 * \namespace Gecode::Int::Extensional
47 * \brief %Extensional propagators
48 */
49
50namespace Gecode { namespace Int { namespace Extensional {
51
52 /**
53 * \brief Domain consistent layered graph (regular) propagator
54 *
55 * The algorithm for the regular propagator is based on:
56 * Gilles Pesant, A Regular Language Membership Constraint
57 * for Finite Sequences of Variables, CP 2004.
58 * Pages 482-495, LNCS 3258, Springer-Verlag, 2004.
59 *
60 * The propagator is not capable of dealing with multiple occurences
61 * of the same view.
62 *
63 * Requires \code #include <gecode/int/extensional.hh> \endcode
64 * \ingroup FuncIntProp
65 */
66 template<class View, class Val, class Degree, class StateIdx>
67 class LayeredGraph : public Propagator {
68 protected:
69 /// States are described by number of incoming and outgoing edges
70 class State {
71 public:
72 Degree i_deg; ///< The in-degree (number of incoming edges)
73 Degree o_deg; ///< The out-degree (number of outgoing edges)
74 /// Initialize with zeroes
75 void init(void);
76 };
77 /// %Edge defined by in-state and out-state
78 class Edge {
79 public:
80 StateIdx i_state; ///< Number of in-state
81 StateIdx o_state; ///< Number of out-state
82 };
83 /// %Support information for a value
84 class Support {
85 public:
86 Val val; ///< Supported value
87 Degree n_edges; ///< Number of supporting edges
88 Edge* edges; ///< Supporting edges in layered graph
89 };
90 /// Type for support size
91 typedef typename Gecode::Support::IntTypeTraits<Val>::utype ValSize;
92 /// %Layer for a view in the layered graph
93 class Layer {
94 public:
95 View x; ///< Integer view
96 StateIdx n_states; ///< Number of states used by outgoing edges
97 ValSize size; ///< Number of supported values
98 State* states; ///< States used by outgoing edges
99 Support* support; ///< Supported values
100 };
101 /// Iterator for telling variable domains by scanning support
102 class LayerValues {
103 private:
104 const Support* s1; ///< Current support
105 const Support* s2; ///< End of support
106 public:
107 /// Default constructor
108 LayerValues(void);
109 /// Initialize for support of layer \a l
110 LayerValues(const Layer& l);
111 /// Initialize for support of layer \a l
112 void init(const Layer& l);
113 /// Test whether more values supported
114 bool operator ()(void) const;
115 /// Move to next supported value
116 void operator ++(void);
117 /// Return supported value
118 int val(void) const;
119 };
120 /// %Advisors for views (by position in array)
121 class Index : public Advisor {
122 public:
123 /// The position of the view in the view array
124 int i;
125 /// Create index advisor
126 Index(Space& home, Propagator& p, Council<Index>& c, int i);
127 /// Clone index advisor \a a
128 Index(Space& home, Index& a);
129 };
130 /// Range approximation of which positions have changed
131 class IndexRange {
132 private:
133 int _fst; ///< First index
134 int _lst; ///< Last index
135 public:
136 /// Initialize range as empty
137 IndexRange(void);
138 /// Reset range to be empty
139 void reset(void);
140 /// Add index \a i to range
141 void add(int i);
142 /// Add index range \a ir to range
143 void add(const IndexRange& ir);
144 /// Shift index range by \a n elements to the left
145 void lshift(int n);
146 /// Test whether range is empty
147 bool empty(void) const;
148 /// Return first position
149 int fst(void) const;
150 /// Return last position
151 int lst(void) const;
152 };
153 /// The advisor council
154 Council<Index> c;
155 /// Number of layers (and views)
156 int n;
157 /// The layers of the graph
158 Layer* layers;
159 /// Maximal number of states per layer
160 StateIdx max_states;
161 /// Total number of states
162 unsigned int n_states;
163 /// Total number of edges
164 unsigned int n_edges;
165 /// Index range with in-degree modifications
166 IndexRange i_ch;
167 /// Index range with out-degree modifications
168 IndexRange o_ch;
169 /// Index range for any change (for compression)
170 IndexRange a_ch;
171 /// Return in state for layer \a i and state index \a is
172 State& i_state(int i, StateIdx is);
173 /// Return in state for layer \a i and in state of edge \a e
174 State& i_state(int i, const Edge& e);
175 /// Decrement out degree for in state of edge \a e for layer \a i
176 bool i_dec(int i, const Edge& e);
177 /// Return out state for layer \a i and state index \a os
178 State& o_state(int i, StateIdx os);
179 /// Return state for layer \a i and out state of edge \a e
180 State& o_state(int i, const Edge& e);
181 /// Decrement in degree for out state of edge \a e for layer \a i
182 bool o_dec(int i, const Edge& e);
183 /// Perform consistency check on data structures
184 void audit(void);
185 /// Initialize layered graph
186 template<class Var>
187 ExecStatus initialize(Space& home,
188 const VarArgArray<Var>& x, const DFA& dfa);
189 /// Constructor for cloning \a p
190 LayeredGraph(Space& home, LayeredGraph<View,Val,Degree,StateIdx>& p);
191 public:
192 /// Constructor for posting
193 template<class Var>
194 LayeredGraph(Home home,
195 const VarArgArray<Var>& x, const DFA& dfa);
196 /// Copy propagator during cloning
197 virtual Actor* copy(Space& home);
198 /// Cost function (defined as high linear)
199 virtual PropCost cost(const Space& home, const ModEventDelta& med) const;
200 /// Schedule function
201 virtual void reschedule(Space& home);
202 /// Give advice to propagator
203 virtual ExecStatus advise(Space& home, Advisor& a, const Delta& d);
204 /// Perform propagation
205 virtual ExecStatus propagate(Space& home, const ModEventDelta& med);
206 /// Delete propagator and return its size
207 virtual size_t dispose(Space& home);
208 /// Post propagator on views \a x and DFA \a dfa
209 template<class Var>
210 static ExecStatus post(Home home,
211 const VarArgArray<Var>& x, const DFA& dfa);
212 };
213
214 /// Select small types for the layered graph propagator
215 template<class Var>
216 ExecStatus post_lgp(Home home,
217 const VarArgArray<Var>& x, const DFA& dfa);
218
219}}}
220
221#include <gecode/int/extensional/layered-graph.hpp>
222
223namespace Gecode { namespace Int { namespace Extensional {
224
225 /// Import type
226 typedef Gecode::Support::BitSetData BitSetData;
227
228 /*
229 * Forward declarations
230 */
231 template<unsigned int size> class TinyBitSet;
232
233 /// Bit-set
234 template<class IndexType>
235 class BitSet {
236 template<class> friend class BitSet;
237 template<unsigned int> friend class TinyBitSet;
238 protected:
239 /// Limit
240 IndexType _limit;
241 /// Indices
242 IndexType* _index;
243 /// Words
244 BitSetData* _bits;
245 /// Replace the \a i th word with \a w, decrease \a limit if \a w is zero
246 void replace_and_decrease(IndexType i, BitSetData w);
247 public:
248 /// Initialize bit set for a number of words \a n
249 BitSet(Space& home, unsigned int n);
250 /// Initialize during cloning
251 template<class OldIndexType>
252 BitSet(Space& home, const BitSet<OldIndexType>& bs);
253 /// Initialize during cloning (unused)
254 BitSet(Space& home, const TinyBitSet<1U>& tbs);
255 /// Initialize during cloning (unused)
256 BitSet(Space& home, const TinyBitSet<2U>& tbs);
257 /// Initialize during cloning (unused)
258 BitSet(Space& home, const TinyBitSet<3U>& tbs);
259 /// Initialize during cloning (unused)
260 BitSet(Space& home, const TinyBitSet<4U>& tbs);
261 /// Get the limit
262 unsigned int limit(void) const;
263 /// Check whether the set is empty
264 bool empty(void) const;
265 /// Make the set empty
266 void flush(void);
267 /// Return the highest active index
268 unsigned int width(void) const;
269 /// Clear the first \a limit words in \a mask
270 void clear_mask(BitSetData* mask) const;
271 /// Add \b to \a mask
272 void add_to_mask(const BitSetData* b, BitSetData* mask) const;
273 /// Intersect with \a mask, sparse mask if \a sparse is true
274 template<bool sparse>
275 void intersect_with_mask(const BitSetData* mask);
276 /// Intersect with the "or" of \a and \a b
277 void intersect_with_masks(const BitSetData* a, const BitSetData* b);
278 /// Check if \a has a non-empty intersection with the set
279 bool intersects(const BitSetData* b) const;
280 /// Perform "nand" with \a b
281 void nand_with_mask(const BitSetData* b);
282 /// Return the number of ones
283 unsigned long long int ones(void) const;
284 /// Return the number of ones after intersection with \a b
285 unsigned long long int ones(const BitSetData* b) const;
286 /// Return an upper bound on the number of bits
287 unsigned long long int bits(void) const;
288 /// Return the number of required bit set words
289 unsigned int words(void) const;
290 /// Return the number of required bit set words
291 unsigned int size(void) const;
292 };
293
294}}}
295
296#include <gecode/int/extensional/bit-set.hpp>
297
298namespace Gecode { namespace Int { namespace Extensional {
299
300 /// Tiny bit-set
301 template<unsigned int _size>
302 class TinyBitSet {
303 template<unsigned int> friend class TinyBitSet;
304 protected:
305 /// Words
306 BitSetData _bits[_size];
307 public:
308 /// Initialize sparse bit set for a number of words \a n
309 TinyBitSet(Space& home, unsigned int n);
310 /// Initialize during cloning
311 template<unsigned int largersize>
312 TinyBitSet(Space& home, const TinyBitSet<largersize>& tbs);
313 /// Initialize during cloning
314 template<class IndexType>
315 TinyBitSet(Space& home, const BitSet<IndexType>& bs);
316 /// Get the limit
317 int limit(void) const;
318 /// Check whether the set is empty
319 bool empty(void) const;
320 /// Make the set empty
321 void flush(void);
322 /// Return the highest active index
323 unsigned int width(void) const;
324 /// Clear the first \a limit words in \a mask
325 void clear_mask(BitSetData* mask);
326 /// Add \b to \a mask
327 void add_to_mask(const BitSetData* b, BitSetData* mask) const;
328 /// Intersect with \a mask, sparse mask if \a sparse is true
329 template<bool sparse>
330 void intersect_with_mask(const BitSetData* mask);
331 /// Intersect with the "or" of \a and \a b
332 void intersect_with_masks(const BitSetData* a, const BitSetData* b);
333 /// Check if \a has a non-empty intersection with the set
334 bool intersects(const BitSetData* b);
335 /// Perform "nand" with \a b
336 void nand_with_mask(const BitSetData* b);
337 /// Perform "nand" with and the "or" of \a a and \a b
338 void nand_with_masks(const BitSetData* a, const BitSetData* b);
339 /// Return the number of ones
340 unsigned long long int ones(void) const;
341 /// Return the number of ones after intersection with \a b
342 unsigned long long int ones(const BitSetData* b) const;
343 /// Return an upper bound on the number of bits
344 unsigned long long int bits(void) const;
345 /// Return the number of required bit set words
346 unsigned int words(void) const;
347 /// Return the total number of words
348 unsigned int size(void) const;
349 };
350
351}}}
352
353#include <gecode/int/extensional/tiny-bit-set.hpp>
354
355namespace Gecode { namespace Int { namespace Extensional {
356
357 /// Tuple type
358 typedef TupleSet::Tuple Tuple;
359
360 /// Base class for compact table propagator
361 template<class View, bool pos>
362 class Compact : public Propagator {
363 protected:
364 /// Range type for supports
365 typedef TupleSet::Range Range;
366 /// Advisor for updating current table
367 class CTAdvisor : public ViewAdvisor<View> {
368 public:
369 using ViewAdvisor<View>::view;
370 protected:
371 /// First range of support data structure
372 const Range* _fst;
373 /// Last range of support data structure
374 const Range* _lst;
375 public:
376 /// \name Constructors
377 //@{
378 /// Initialise from parameters
379 CTAdvisor(Space& home, Propagator& p, Council<CTAdvisor>& c,
380 const TupleSet& ts, View x0, int i);
381 /// Clone advisor \a a
382 CTAdvisor(Space& home, CTAdvisor& a);
383 //@}
384 /// Adjust supports
385 void adjust(void);
386 /// Return first range of support data structure
387 const Range* fst(void) const;
388 /// Return lasst range of support data structure
389 const Range* lst(void) const;
390 /// Dispose advisor
391 void dispose(Space& home, Council<CTAdvisor>& c);
392 };
393 //@}
394 /// \name Support iterators
395 //@{
396 /// Iterator over valid supports
397 class ValidSupports {
398 protected:
399 /// Number of words
400 const unsigned int n_words;
401 /// Maximal value
402 int max;
403 /// Range iterator
404 ViewRanges<View> xr;
405 /// Support iterator
406 const Range* sr;
407 /// The last range
408 const Range* lst;
409 /// The value
410 int n;
411 /// The value's support
412 const BitSetData* s;
413 /// Find a new value (only for negative case)
414 void find(void);
415 public:
416 /// Initialize from initialized propagator
417 ValidSupports(const Compact<View,pos>& p, CTAdvisor& a);
418 /// Initialize during initialization
419 ValidSupports(const TupleSet& ts, int i, View x);
420 /// Move to next supports
421 void operator ++(void);
422 /// Whether there are still supports left
423 bool operator ()(void) const;
424 /// Return supports
425 const BitSetData* supports(void) const;
426 /// Return supported value
427 int val(void) const;
428 };
429 /// Iterator over lost supports
430 class LostSupports {
431 protected:
432 /// Number of words
433 const unsigned int n_words;
434 /// Range information
435 const Range* r;
436 /// Last range
437 const Range* lst;
438 /// Low value
439 int l;
440 /// High value
441 int h;
442 /// The lost value's support
443 const BitSetData* s;
444 public:
445 /// Initialize iterator for values between \a l and \a h
446 LostSupports(const Compact<View,pos>& p, CTAdvisor& a,
447 int l, int h);
448 /// Move iterator to next value
449 void operator ++(void);
450 /// Whether iterator is done
451 bool operator ()(void) const;
452 /// Provide access to corresponding supports
453 const BitSetData* supports(void) const;
454 };
455 //@}
456 /// \name Testing the number of unassigned variables
457 //@{
458 /// Whether all variables are assigned
459 bool all(void) const;
460 /// Whether at most one variable is unassigned
461 bool atmostone(void) const;
462 //@}
463 protected:
464 /// Number of words in supports
465 const unsigned int n_words;
466 /// The tuple set
467 TupleSet ts;
468 /// The advisor council
469 Council<CTAdvisor> c;
470 /// Constructor for cloning \a p
471 Compact(Space& home, Compact& p);
472 /// Constructor for posting
473 Compact(Home home, const TupleSet& ts);
474 /// Setup the actual table
475 template<class Table>
476 void setup(Space& home, Table& table, ViewArray<View>& x);
477 /// Check whether the table covers the whole Cartedion product
478 template<class Table>
479 bool full(const Table& table) const;
480 /// Find range for \a n
481 const Range* range(CTAdvisor& a, int n);
482 /// Return supports for value \a n
483 const BitSetData* supports(CTAdvisor& a, int n);
484 public:
485 /// Cost function
486 virtual PropCost cost(const Space& home, const ModEventDelta& med) const;
487 /// Delete propagator and return its size
488 size_t dispose(Space& home);
489 };
490
491 /**
492 * \brief Domain consistent positive extensional propagator
493 *
494 * This propagator implements the compact-table propagation
495 * algorithm based on:
496 * J. Demeulenaere et. al., Compact-Table: Efficiently
497 * filtering table constraints with reversible sparse
498 * bit-sets, CP 2016.
499 *
500 * Requires \code #include <gecode/int/extensional.hh> \endcode
501 * \ingroup FuncIntProp
502 */
503 template<class View, class Table>
504 class PosCompact : public Compact<View,true> {
505 public:
506 typedef typename Compact<View,true>::ValidSupports ValidSupports;
507 typedef typename Compact<View,true>::Range Range;
508 typedef typename Compact<View,true>::CTAdvisor CTAdvisor;
509 typedef typename Compact<View,true>::LostSupports LostSupports;
510
511 using Compact<View,true>::setup;
512 using Compact<View,true>::supports;
513 using Compact<View,true>::all;
514 using Compact<View,true>::atmostone;
515 using Compact<View,true>::c;
516 using Compact<View,true>::ts;
517
518 /// \name Status management
519 //@{
520 /// Type of status
521 enum StatusType {
522 SINGLE = 0, ///< A single view has been touched
523 MULTIPLE = 1, ///< Multiple view have been touched
524 NONE = 2, ///< No view has been touched
525 PROPAGATING = 3 ///< The propagator is currently running
526 };
527 /// Status management
528 class Status {
529 protected:
530 /// A tagged pointer for storing the status
531 ptrdiff_t s;
532 public:
533 /// Initialize with type \a t (either NONE or SEVERAL)
534 Status(StatusType t);
535 /// Copy constructor
536 Status(const Status& s);
537 /// Return status type
538 StatusType type(void) const;
539 /// Check whether status is single and equal to \a a
540 bool single(CTAdvisor& a) const;
541 /// Set status to SINGLE or MULTIPLE depending on \a a
542 void touched(CTAdvisor& a);
543 /// Set status to NONE
544 void none(void);
545 /// Set status to PROPAGATING
546 void propagating(void);
547 };
548 /// Propagator status
549 Status status;
550 /// Current table
551 Table table;
552 /// Check whether the table is empty
553 bool empty(void) const;
554 /// Constructor for cloning \a p
555 template<class TableProp>
556 PosCompact(Space& home, TableProp& p);
557 /// Constructor for posting
558 PosCompact(Home home, ViewArray<View>& x, const TupleSet& ts);
559 public:
560 /// Schedule function
561 virtual void reschedule(Space& home);
562 /// Perform propagation
563 virtual ExecStatus propagate(Space& home, const ModEventDelta& med);
564 /// Copy propagator during cloning
565 virtual Actor* copy(Space& home);
566 /// Post propagator for views \a x and table \a t
567 static ExecStatus post(Home home, ViewArray<View>& x, const TupleSet& ts);
568 /// Delete propagator and return its size
569 size_t dispose(Space& home);
570 /// Give advice to propagator
571 virtual ExecStatus advise(Space& home, Advisor& a, const Delta& d);
572 };
573
574 /// Post function for positive compact table propagator
575 template<class View>
576 ExecStatus postposcompact(Home home, ViewArray<View>& x, const TupleSet& ts);
577
578 /**
579 * \brief Domain consistent negative extensional propagator
580 *
581 * This propagator implements the compact-table propagation
582 * algorithm based on:
583 * J. Demeulenaere et. al., Compact-Table: Efficiently
584 * filtering table constraints with reversible sparse
585 * bit-sets, CP 2016.
586 * and (negative tables) on:
587 * H. Verhaeghe et al., Extending Compact-Table to
588 * Negative and Short Tables. AAAI 2017.
589 *
590 * Requires \code #include <gecode/int/extensional.hh> \endcode
591 * \ingroup FuncIntProp
592 */
593 template<class View, class Table>
594 class NegCompact : public Compact<View,false> {
595 public:
596 typedef typename Compact<View,false>::ValidSupports ValidSupports;
597 typedef typename Compact<View,false>::Range Range;
598 typedef typename Compact<View,false>::CTAdvisor CTAdvisor;
599
600 using Compact<View,false>::setup;
601 using Compact<View,false>::full;
602 using Compact<View,false>::supports;
603 using Compact<View,false>::atmostone;
604 using Compact<View,false>::c;
605 using Compact<View,false>::ts;
606
607 /// Current table
608 Table table;
609 /// Constructor for cloning \a p
610 template<class TableProp>
611 NegCompact(Space& home, TableProp& p);
612 /// Constructor for posting
613 NegCompact(Home home, ViewArray<View>& x, const TupleSet& ts);
614 public:
615 /// Schedule function
616 virtual void reschedule(Space& home);
617 /// Perform propagation
618 virtual ExecStatus propagate(Space& home, const ModEventDelta& med);
619 /// Copy propagator during cloning
620 virtual Actor* copy(Space& home);
621 /// Post propagator for views \a x and table \a t
622 static ExecStatus post(Home home, ViewArray<View>& x, const TupleSet& ts);
623 /// Delete propagator and return its size
624 size_t dispose(Space& home);
625 /// Give advice to propagator
626 virtual ExecStatus advise(Space& home, Advisor& a, const Delta& d);
627 };
628
629 /// Post function for compact table propagator
630 template<class View>
631 ExecStatus postnegcompact(Home home, ViewArray<View>& x, const TupleSet& ts);
632
633
634 /// Domain consistent reified extensional propagator
635 template<class View, class Table, class CtrlView, ReifyMode rm>
636 class ReCompact : public Compact<View,false> {
637 public:
638 typedef typename Compact<View,false>::ValidSupports ValidSupports;
639 typedef typename Compact<View,false>::Range Range;
640 typedef typename Compact<View,false>::CTAdvisor CTAdvisor;
641
642 using Compact<View,false>::setup;
643 using Compact<View,false>::full;
644 using Compact<View,false>::supports;
645 using Compact<View,false>::c;
646 using Compact<View,false>::ts;
647
648 /// Current table
649 Table table;
650 /// Boolean control view
651 CtrlView b;
652 /// The views (for rewriting)
653 ViewArray<View> y;
654 /// Constructor for cloning \a p
655 template<class TableProp>
656 ReCompact(Space& home, TableProp& p);
657 /// Constructor for posting
658 ReCompact(Home home, ViewArray<View>& x, const TupleSet& ts, CtrlView b);
659 public:
660 /// Schedule function
661 virtual void reschedule(Space& home);
662 /// Perform propagation
663 virtual ExecStatus propagate(Space& home, const ModEventDelta& med);
664 /// Copy propagator during cloning
665 virtual Actor* copy(Space& home);
666 /// Post propagator for views \a x and table \a t
667 static ExecStatus post(Home home, ViewArray<View>& x, const TupleSet& ts,
668 CtrlView b);
669 /// Delete propagator and return its size
670 size_t dispose(Space& home);
671 /// Give advice to propagator
672 virtual ExecStatus advise(Space& home, Advisor& a, const Delta& d);
673 };
674
675 /// Post function for compact table propagator
676 template<class View, class CtrlView, ReifyMode rm>
677 ExecStatus postrecompact(Home home, ViewArray<View>& x, const TupleSet& ts,
678 CtrlView b);
679
680}}}
681
682#include <gecode/int/extensional/compact.hpp>
683
684#endif
685
686// STATISTICS: int-prop