1 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2 /*
3  *  Main authors:
4  *    Vincent Barichard <Vincent.Barichard@univ-angers.fr>
5  *
6  *  Copyright:
7  *    Vincent Barichard, 2013
8  *
9  *  Last modified:
10  *     $Date$ by $Author$
11  *     $Revision$
12  *
13  *  This file is part of Quacode:
14  *     http://quacode.barichard.com
15  *
16  *  Permission is hereby granted, free of charge, to any person obtaining
17  *  a copy of this software and associated documentation files (the
18  *  "Software"), to deal in the Software without restriction, including
19  *  without limitation the rights to use, copy, modify, merge, publish,
20  *  distribute, sublicense, and/or sell copies of the Software, and to
21  *  permit persons to whom the Software is furnished to do so, subject to
22  *  the following conditions:
23  *
24  *  The above copyright notice and this permission notice shall be
25  *  included in all copies or substantial portions of the Software.
26  *
27  *  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
28  *  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
29  *  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
30  *  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
31  *  LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
32  *  OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
33  *  WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
34  *
35  */
36 
37 #ifndef __QCSP_HH__
38 #define __QCSP_HH__
39 
40 #include <gecode/kernel.hh>
41 
42 /*
43  * Configure linking
44  *
45  */
46 #if !defined(QUACODE_STATIC_LIB) && \
47     (defined(__CYGWIN__) || defined(__MINGW32__) || defined(_MSC_VER))
48 
49 #ifdef BUILD_QUACODE_LIB
50 #define QUACODE_EXPORT __declspec( dllexport )
51 #else
52 #define QUACODE_EXPORT __declspec( dllimport )
53 #endif
54 
55 #else
56 
57 #ifdef QUACODE_GCC_HAS_CLASS_VISIBILITY
58 #define QUACODE_EXPORT __attribute__ ((visibility("default")))
59 #else
60 #define QUACODE_EXPORT
61 #endif
62 
63 #endif
64 
65 namespace Gecode {
66   #define EXISTS 0
67   #define FORALL 1
68   typedef unsigned int TQuantifier;
69 }
70 
71 #include <gecode/int.hh>
72 
73 namespace Gecode {
74   /// Quantifier variable
75   template <class VarType>
76   struct QVar {
77     TQuantifier q;
78     VarType     x;
79     int         r;
QVarGecode::QVar80     QVar() : q(EXISTS), r(Int::Limits::max) { }
QVarGecode::QVar81     QVar(VarType& _x) : q(EXISTS), x(_x), r(Int::Limits::max) { }
QVarGecode::QVar82     QVar(TQuantifier _q, VarType& _x, int _r) : q(_q), x(_x), r(_r) { }
varimpGecode::QVar83     void* varimp() const { return x.varimp(); }
84   };
85 
86   typedef QVar<BoolVar> QBoolVar;
87   typedef QVar<IntVar> QIntVar;
88 
89   /** \brief Passing Quantified variables
90    */
91   template <class QVarType>
92   class QVarArgs : public VarArgArray<QVarType> {
93     typedef typename VarArgArray<QVarType>::VarLess VarLess;
94   public:
95     using VarArgArray<QVarType>::n;
96     using VarArgArray<QVarType>::a;
97 
98     /// \name Constructors and initialization
99     //@{
100     /// Allocate empty array
QVarArgs(void)101     QVarArgs(void) {}
102     /// Allocate array with \a n elements
QVarArgs(int n)103     explicit QVarArgs(int n) : VarArgArray<QVarType>(n) {}
104     /// Initialize from variable argument array \a a (copy elements)
QVarArgs(const QVarArgs & a)105     QVarArgs(const QVarArgs& a) : VarArgArray<QVarType>(a) {}
106     /// Initialize from variable array \a a (copy elements)
QVarArgs(const VarArray<QVarType> & a)107     QVarArgs(const VarArray<QVarType>& a)
108      : VarArgArray<QVarType>(a) {}
109     /// Remove all duplicate variables from array (changes element order)
unique(void)110     void unique(void) {
111       if (n < 2)
112         return ;
113       VarLess vl;
114       Support::quicksort<QVarType,VarLess>(a,n,vl);
115       int j = 0;
116       for (int i = 1; i<n; i++)
117         if (a[j].varimp() != a[i].varimp())
118           a[++j] = a[i];
119       n = j+1;
120     }
121     //@}
122   };
123 
124   typedef QVarArgs<QBoolVar> QBoolVarArgs;
125   typedef QVarArgs<QIntVar>  QIntVarArgs;
126 
127   // TRAITS
128   class QuantArgs;
129 
130   /// Traits of %QBoolVarArgs
131   template<>
132   class ArrayTraits<VarArgArray<QBoolVar> > {
133   public:
134     typedef QBoolVarArgs StorageType;
135     typedef QBoolVar     ValueType;
136     typedef QBoolVarArgs ArgsType;
137   };
138 
139   /// Traits of %QIntVarArgs
140   template<>
141   class ArrayTraits<VarArgArray<QIntVar> > {
142   public:
143     typedef QIntVarArgs StorageType;
144     typedef QIntVar     ValueType;
145     typedef QIntVarArgs ArgsType;
146   };
147 
148   /// Traits of %QuantArgs
149   template<>
150   class ArrayTraits<PrimArgArray<TQuantifier> > {
151   public:
152     typedef QuantArgs   StorageType;
153     typedef TQuantifier ValueType;
154     typedef QuantArgs   ArgsType;
155   };
156 
157   /// Passing TQuantifier arguments
158   class QuantArgs : public PrimArgArray<TQuantifier> {
159   public:
160     /// \name Constructors and initialization
161     //@{
162     /// Allocate empty array
QuantArgs(void)163     QuantArgs(void) {}
164     /// Allocate array with \a n elements
QuantArgs(int n)165     explicit QuantArgs(int n) : PrimArgArray<TQuantifier>(n) {}
166     /// Allocate array and copy elements from \a x
QuantArgs(const SharedArray<TQuantifier> & x)167     QuantArgs(const SharedArray<TQuantifier>& x)
168        : PrimArgArray<TQuantifier>(x.size()) {
169        for (int i=x.size(); i--;)
170          a[i] = x[i];
171      }
172     /// Allocate array and copy elements from \a x
QuantArgs(const std::vector<TQuantifier> & x)173     QuantArgs(const std::vector<TQuantifier>& x)
174       : PrimArgArray<TQuantifier>(static_cast<int>(x.size())) {
175       for (std::vector<TQuantifier>::size_type i=x.size(); i--;)
176         a[i] = x[i];
177     }
178     /// Allocate array with \a n elements and initialize with \a e0, ...
179     QUACODE_EXPORT
QuantArgs(int n,TQuantifier e0,...)180     QuantArgs(int n, TQuantifier e0, ...) : PrimArgArray<TQuantifier>(n) {
181       va_list args;
182       va_start(args, e0);
183       a[0] = e0;
184       for (int i = 1; i < n; i++)
185         a[i] = va_arg(args,TQuantifier);
186       va_end(args);
187     }
188     /// Allocate array with \a n elements and initialize with elements from array \a e
QuantArgs(int n,const TQuantifier * e)189     QuantArgs(int n, const TQuantifier* e)  : PrimArgArray<TQuantifier>(n, e) {}
190     /// Initialize from primitive argument array \a a (copy elements)
QuantArgs(const PrimArgArray<TQuantifier> & a)191     QuantArgs(const PrimArgArray<TQuantifier>& a) : PrimArgArray<TQuantifier>(a) {}
192     //@}
193   };
194 
195   /** \brief Post domain consistent propagator for Quantified Boolean operation on \a x0 and \a x1
196    *
197    * Posts propagator for \f$ x_0 \diamond_{\mathit{o}} x_1 = x_2\f$
198    * \ingroup TaskModelIntRelBool
199    */
200   QUACODE_EXPORT void
201   qrel(Home home, QBoolVar qx0, BoolOpType o, QBoolVar qx1, BoolVar x2);
202 
203   /** \brief Post domain consistent propagator for Quantified Boolean clause with positive variables \a x and negative variables \a y
204    *
205    * Posts propagator for \f$ x_0 \diamond_{\mathit{o}} \cdots
206    * \diamond_{\mathit{o}} x_{|x|-1} \diamond_{\mathit{o}} \neg y_0
207    * \diamond_{\mathit{o}} \cdots \diamond_{\mathit{o}} \neg y_{|y|-1}= z\f$
208    *
209    * Throws an exception of type Int::IllegalOperation, if \a o is different
210    * from BOT_AND or BOT_OR.
211    * \ingroup TaskModelIntRelBool
212    */
213   QUACODE_EXPORT void
214   qclause(Home home, BoolOpType o, QBoolVarArgs x, QBoolVarArgs y,
215           BoolVar z);
216   /** \brief Post domain consistent propagator for Quantified Boolean clause with positive variables \a x and negative variables \a y
217    *
218    * Posts propagator for \f$ x_0 \diamond_{\mathit{o}} \cdots
219    * \diamond_{\mathit{o}} x_{|x|-1} \diamond_{\mathit{o}} \neg y_0
220    * \diamond_{\mathit{o}} \cdots \diamond_{\mathit{o}} \neg y_{|y|-1}= n\f$
221    *
222    * Throws an exception of type Int::NotZeroOne, if \a n is neither
223    * 0 or 1.
224    *
225    * Throws an exception of type Int::IllegalOperation, if \a o is different
226    * from BOT_AND or BOT_OR.
227    * \ingroup TaskModelIntRelBool
228    */
229   QUACODE_EXPORT void
230   qclause(Home home, BoolOpType o, QBoolVarArgs x, QBoolVarArgs y,
231           int n);
232 }
233 
234 #include <gecode/search.hh>
235 namespace Gecode {
236   /**
237    * \brief Depth-first search engine for quantified variables
238    *
239    * This class supports depth-first search for quantified variables for subclasses \a T of
240    * Space.
241    * \ingroup TaskModelSearch
242    */
243   template<class T>
244   class QDFS : public Search::Base<T> {
245   private:
246     /// The actual search engine
247     Search::Engine* e;
248   public:
249     /// Initialize search engine for space \a s with options \a o
250     QDFS(T* s, const Search::Options& o=Search::Options::def);
251     /// Whether engine does best solution search
252     static const bool best = false;
253     /// Return next solution (NULL, if none exists or search has been stopped)
254     T* next(void);
255     /// Return statistics
256     Search::Statistics statistics(void) const;
257     /// Check whether engine has been stopped
258     bool stopped(void) const;
259     /// Destructor
260     ~QDFS(void);
261   };
262 }
263 #include <quacode/search/qdfs.hpp>
264 
265 #endif
266