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