this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2/*
3 * Main authors:
4 * Guido Tack <tack@gecode.org>
5 *
6 * Contributing authors:
7 * Gabriel Hjort Blindell <gabriel.hjort.blindell@gmail.com>
8 *
9 * Copyright:
10 * Guido Tack, 2007-2012
11 * Gabriel Hjort Blindell, 2012
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/flatzinc.hh>
39#include <gecode/flatzinc/registry.hh>
40#include <gecode/flatzinc/plugin.hh>
41#include <gecode/flatzinc/branch.hh>
42
43#include <gecode/search.hh>
44
45#include <vector>
46#include <string>
47#include <sstream>
48#include <limits>
49#include <unordered_set>
50
51
52namespace std {
53
54 /// Hashing for tuple sets
55 template<> struct hash<Gecode::TupleSet> {
56 /// Return hash key for \a x
57 forceinline size_t
58 operator()(const Gecode::TupleSet& x) const {
59 return x.hash();
60 }
61 };
62
63 /// Hashing for tuple sets
64 template<> struct hash<Gecode::SharedArray<int> > {
65 /// Return hash key for \a x
66 forceinline size_t
67 operator()(const Gecode::SharedArray<int>& x) const {
68 size_t seed = static_cast<size_t>(x.size());
69 for (int i=x.size(); i--; )
70 Gecode::cmb_hash(seed, x[i]);
71 return seed;
72 }
73 };
74
75 /// Hashing for DFAs
76 template<> struct hash<Gecode::DFA> {
77 /// Return hash key for \a d
78 forceinline size_t operator()(const Gecode::DFA& d) const {
79 return d.hash();
80 }
81 };
82
83}
84
85namespace Gecode { namespace FlatZinc {
86
87 // Default random number generator
88 Rnd defrnd(0);
89
90 /**
91 * \brief Branching on the introduced variables
92 *
93 * This brancher makes sure that when a solution is found for the model
94 * variables, all introduced variables are either assigned, or the solution
95 * can be extended to a solution of the introduced variables.
96 *
97 * The advantage over simply branching over the introduced variables is that
98 * only one such extension will be searched for, instead of enumerating all
99 * possible (equivalent) extensions.
100 *
101 */
102 class AuxVarBrancher : public Brancher {
103 protected:
104 /// Flag whether brancher is done
105 bool done;
106 /// Construct brancher
107 AuxVarBrancher(Home home, TieBreak<IntVarBranch> int_varsel0,
108 IntValBranch int_valsel0,
109 TieBreak<BoolVarBranch> bool_varsel0,
110 BoolValBranch bool_valsel0
111#ifdef GECODE_HAS_SET_VARS
112 ,
113 SetVarBranch set_varsel0,
114 SetValBranch set_valsel0
115#endif
116#ifdef GECODE_HAS_FLOAT_VARS
117 ,
118 TieBreak<FloatVarBranch> float_varsel0,
119 FloatValBranch float_valsel0
120#endif
121 )
122 : Brancher(home), done(false),
123 int_varsel(int_varsel0), int_valsel(int_valsel0),
124 bool_varsel(bool_varsel0), bool_valsel(bool_valsel0)
125#ifdef GECODE_HAS_SET_VARS
126 , set_varsel(set_varsel0), set_valsel(set_valsel0)
127#endif
128#ifdef GECODE_HAS_FLOAT_VARS
129 , float_varsel(float_varsel0), float_valsel(float_valsel0)
130#endif
131 {}
132 /// Copy constructor
133 AuxVarBrancher(Space& home, AuxVarBrancher& b)
134 : Brancher(home, b), done(b.done) {}
135
136 /// %Choice that only signals failure or success
137 class Choice : public Gecode::Choice {
138 public:
139 /// Whether brancher should fail
140 bool fail;
141 /// Initialize choice for brancher \a b
142 Choice(const Brancher& b, bool fail0)
143 : Gecode::Choice(b,1), fail(fail0) {}
144 /// Report size occupied
145 virtual size_t size(void) const {
146 return sizeof(Choice);
147 }
148 /// Archive into \a e
149 virtual void archive(Archive& e) const {
150 Gecode::Choice::archive(e);
151 e.put(fail);
152 }
153 };
154
155 TieBreak<IntVarBranch> int_varsel;
156 IntValBranch int_valsel;
157 TieBreak<BoolVarBranch> bool_varsel;
158 BoolValBranch bool_valsel;
159#ifdef GECODE_HAS_SET_VARS
160 SetVarBranch set_varsel;
161 SetValBranch set_valsel;
162#endif
163#ifdef GECODE_HAS_FLOAT_VARS
164 TieBreak<FloatVarBranch> float_varsel;
165 FloatValBranch float_valsel;
166#endif
167
168 public:
169 /// Check status of brancher, return true if alternatives left.
170 virtual bool status(const Space& _home) const {
171 if (done) return false;
172 const FlatZincSpace& home = static_cast<const FlatZincSpace&>(_home);
173 for (int i=0; i<home.iv_aux.size(); i++)
174 if (!home.iv_aux[i].assigned()) return true;
175 for (int i=0; i<home.bv_aux.size(); i++)
176 if (!home.bv_aux[i].assigned()) return true;
177#ifdef GECODE_HAS_SET_VARS
178 for (int i=0; i<home.sv_aux.size(); i++)
179 if (!home.sv_aux[i].assigned()) return true;
180#endif
181#ifdef GECODE_HAS_FLOAT_VARS
182 for (int i=0; i<home.fv_aux.size(); i++)
183 if (!home.fv_aux[i].assigned()) return true;
184#endif
185 // No non-assigned variables left
186 return false;
187 }
188 /// Return choice
189 virtual Choice* choice(Space& home) {
190 done = true;
191 FlatZincSpace& fzs = static_cast<FlatZincSpace&>(*home.clone());
192 fzs.needAuxVars = false;
193 branch(fzs,fzs.iv_aux,int_varsel,int_valsel);
194 branch(fzs,fzs.bv_aux,bool_varsel,bool_valsel);
195#ifdef GECODE_HAS_SET_VARS
196 branch(fzs,fzs.sv_aux,set_varsel,set_valsel);
197#endif
198#ifdef GECODE_HAS_FLOAT_VARS
199 branch(fzs,fzs.fv_aux,float_varsel,float_valsel);
200#endif
201 Search::Options opt; opt.clone = false;
202 FlatZincSpace* sol = dfs(&fzs, opt);
203 if (sol) {
204 delete sol;
205 return new Choice(*this,false);
206 } else {
207 return new Choice(*this,true);
208 }
209 }
210 /// Return choice
211 virtual Choice* choice(const Space&, Archive& e) {
212 bool fail; e >> fail;
213 return new Choice(*this, fail);
214 }
215 /// Perform commit for choice \a c
216 virtual ExecStatus commit(Space&, const Gecode::Choice& c, unsigned int) {
217 return static_cast<const Choice&>(c).fail ? ES_FAILED : ES_OK;
218 }
219 /// Print explanation
220 virtual void print(const Space&, const Gecode::Choice& c,
221 unsigned int,
222 std::ostream& o) const {
223 o << "FlatZinc("
224 << (static_cast<const Choice&>(c).fail ? "fail" : "ok")
225 << ")";
226 }
227 /// Copy brancher
228 virtual Actor* copy(Space& home) {
229 return new (home) AuxVarBrancher(home, *this);
230 }
231 /// Post brancher
232 static void post(Home home,
233 TieBreak<IntVarBranch> int_varsel,
234 IntValBranch int_valsel,
235 TieBreak<BoolVarBranch> bool_varsel,
236 BoolValBranch bool_valsel
237#ifdef GECODE_HAS_SET_VARS
238 ,
239 SetVarBranch set_varsel,
240 SetValBranch set_valsel
241#endif
242#ifdef GECODE_HAS_FLOAT_VARS
243 ,
244 TieBreak<FloatVarBranch> float_varsel,
245 FloatValBranch float_valsel
246#endif
247 ) {
248 (void) new (home) AuxVarBrancher(home, int_varsel, int_valsel,
249 bool_varsel, bool_valsel
250#ifdef GECODE_HAS_SET_VARS
251 , set_varsel, set_valsel
252#endif
253#ifdef GECODE_HAS_FLOAT_VARS
254 , float_varsel, float_valsel
255#endif
256 );
257 }
258 /// Delete brancher and return its size
259 virtual size_t dispose(Space&) {
260 return sizeof(*this);
261 }
262 };
263
264 class BranchInformationO : public SharedHandle::Object {
265 private:
266 struct BI {
267 std::string r0;
268 std::string r1;
269 std::vector<std::string> n;
270 BI(void) : r0(""), r1(""), n(0) {}
271 BI(const std::string& r00, const std::string& r10,
272 const std::vector<std::string>& n0)
273 : r0(r00), r1(r10), n(n0) {}
274 };
275 std::vector<BI> v;
276 BranchInformationO(std::vector<BI> v0) : v(v0) {}
277 public:
278 BranchInformationO(void) {}
279 virtual ~BranchInformationO(void) {}
280 virtual SharedHandle::Object* copy(void) const {
281 return new BranchInformationO(v);
282 }
283 /// Add new brancher information
284 void add(BrancherGroup bg,
285 const std::string& rel0,
286 const std::string& rel1,
287 const std::vector<std::string>& n) {
288 v.resize(std::max(static_cast<unsigned int>(v.size()),bg.id()+1));
289 v[bg.id()] = BI(rel0,rel1,n);
290 }
291 /// Output branch information
292 void print(const Brancher& b,
293 unsigned int a, int i, int n, std::ostream& o) const {
294 const BI& bi = v[b.group().id()];
295 o << bi.n[i] << " " << (a==0 ? bi.r0 : bi.r1) << " " << n;
296 }
297#ifdef GECODE_HAS_FLOAT_VARS
298 void print(const Brancher& b,
299 unsigned int a, int i, const FloatNumBranch& nl,
300 std::ostream& o) const {
301 const BI& bi = v[b.group().id()];
302 o << bi.n[i] << " "
303 << (((a == 0) == nl.l) ? "<=" : ">=") << nl.n;
304 }
305#endif
306 };
307
308 BranchInformation::BranchInformation(void)
309 : SharedHandle(nullptr) {}
310
311 BranchInformation::BranchInformation(const BranchInformation& bi)
312 : SharedHandle(bi) {}
313
314 void
315 BranchInformation::init(void) {
316 assert(object() == nullptr);
317 object(new BranchInformationO());
318 }
319
320 void
321 BranchInformation::add(BrancherGroup bg,
322 const std::string& rel0,
323 const std::string& rel1,
324 const std::vector<std::string>& n) {
325 static_cast<BranchInformationO*>(object())->add(bg,rel0,rel1,n);
326 }
327 void
328 BranchInformation::print(const Brancher& b, unsigned int a, int i,
329 int n, std::ostream& o) const {
330 static_cast<const BranchInformationO*>(object())->print(b,a,i,n,o);
331 }
332#ifdef GECODE_HAS_FLOAT_VARS
333 void
334 BranchInformation::print(const Brancher& b, unsigned int a, int i,
335 const FloatNumBranch& nl, std::ostream& o) const {
336 static_cast<const BranchInformationO*>(object())->print(b,a,i,nl,o);
337 }
338#endif
339 template<class Var>
340 void varValPrint(const Space &home, const Brancher& b,
341 unsigned int a,
342 Var, int i, const int& n,
343 std::ostream& o) {
344 static_cast<const FlatZincSpace&>(home).branchInfo.print(b,a,i,n,o);
345 }
346
347#ifdef GECODE_HAS_FLOAT_VARS
348 void varValPrintF(const Space &home, const Brancher& b,
349 unsigned int a,
350 FloatVar, int i, const FloatNumBranch& nl,
351 std::ostream& o) {
352 static_cast<const FlatZincSpace&>(home).branchInfo.print(b,a,i,nl,o);
353 }
354#endif
355
356 IntSet vs2is(IntVarSpec* vs) {
357 if (vs->assigned) {
358 return IntSet(vs->i,vs->i);
359 }
360 if (vs->domain()) {
361 AST::SetLit* sl = vs->domain.some();
362 if (sl->interval) {
363 return IntSet(sl->min, sl->max);
364 } else {
365 int* newdom = heap.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
366 for (int i=sl->s.size(); i--;)
367 newdom[i] = sl->s[i];
368 IntSet ret(newdom, sl->s.size());
369 heap.free(newdom, static_cast<unsigned long int>(sl->s.size()));
370 return ret;
371 }
372 }
373 return IntSet(Int::Limits::min, Int::Limits::max);
374 }
375
376 int vs2bsl(BoolVarSpec* bs) {
377 if (bs->assigned) {
378 return bs->i;
379 }
380 if (bs->domain()) {
381 AST::SetLit* sl = bs->domain.some();
382 assert(sl->interval);
383 return std::min(1, std::max(0, sl->min));
384 }
385 return 0;
386 }
387
388 int vs2bsh(BoolVarSpec* bs) {
389 if (bs->assigned) {
390 return bs->i;
391 }
392 if (bs->domain()) {
393 AST::SetLit* sl = bs->domain.some();
394 assert(sl->interval);
395 return std::max(0, std::min(1, sl->max));
396 }
397 return 1;
398 }
399
400 TieBreak<IntVarBranch> ann2ivarsel(AST::Node* ann, Rnd rnd, double decay) {
401 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
402 if (s->id == "input_order")
403 return TieBreak<IntVarBranch>(INT_VAR_NONE());
404 if (s->id == "first_fail")
405 return TieBreak<IntVarBranch>(INT_VAR_SIZE_MIN());
406 if (s->id == "anti_first_fail")
407 return TieBreak<IntVarBranch>(INT_VAR_SIZE_MAX());
408 if (s->id == "smallest")
409 return TieBreak<IntVarBranch>(INT_VAR_MIN_MIN());
410 if (s->id == "largest")
411 return TieBreak<IntVarBranch>(INT_VAR_MAX_MAX());
412 if (s->id == "occurrence")
413 return TieBreak<IntVarBranch>(INT_VAR_DEGREE_MAX());
414 if (s->id == "max_regret")
415 return TieBreak<IntVarBranch>(INT_VAR_REGRET_MIN_MAX());
416 if (s->id == "most_constrained")
417 return TieBreak<IntVarBranch>(INT_VAR_SIZE_MIN(),
418 INT_VAR_DEGREE_MAX());
419 if (s->id == "random") {
420 return TieBreak<IntVarBranch>(INT_VAR_RND(rnd));
421 }
422 if (s->id == "dom_w_deg") {
423 return TieBreak<IntVarBranch>(INT_VAR_AFC_SIZE_MAX(decay));
424 }
425 if (s->id == "afc_min")
426 return TieBreak<IntVarBranch>(INT_VAR_AFC_MIN(decay));
427 if (s->id == "afc_max")
428 return TieBreak<IntVarBranch>(INT_VAR_AFC_MAX(decay));
429 if (s->id == "afc_size_min")
430 return TieBreak<IntVarBranch>(INT_VAR_AFC_SIZE_MIN(decay));
431 if (s->id == "afc_size_max") {
432 return TieBreak<IntVarBranch>(INT_VAR_AFC_SIZE_MAX(decay));
433 }
434 if (s->id == "action_min")
435 return TieBreak<IntVarBranch>(INT_VAR_ACTION_MIN(decay));
436 if (s->id == "action_max")
437 return TieBreak<IntVarBranch>(INT_VAR_ACTION_MAX(decay));
438 if (s->id == "action_size_min")
439 return TieBreak<IntVarBranch>(INT_VAR_ACTION_SIZE_MIN(decay));
440 if (s->id == "action_size_max")
441 return TieBreak<IntVarBranch>(INT_VAR_ACTION_SIZE_MAX(decay));
442 }
443 std::cerr << "Warning, ignored search annotation: ";
444 ann->print(std::cerr);
445 std::cerr << std::endl;
446 return TieBreak<IntVarBranch>(INT_VAR_NONE());
447 }
448
449 IntValBranch ann2ivalsel(AST::Node* ann, std::string& r0, std::string& r1,
450 Rnd rnd) {
451 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
452 if (s->id == "indomain_min") {
453 r0 = "="; r1 = "!=";
454 return INT_VAL_MIN();
455 }
456 if (s->id == "indomain_max") {
457 r0 = "="; r1 = "!=";
458 return INT_VAL_MAX();
459 }
460 if (s->id == "indomain_median") {
461 r0 = "="; r1 = "!=";
462 return INT_VAL_MED();
463 }
464 if (s->id == "indomain_split") {
465 r0 = "<="; r1 = ">";
466 return INT_VAL_SPLIT_MIN();
467 }
468 if (s->id == "indomain_reverse_split") {
469 r0 = ">"; r1 = "<=";
470 return INT_VAL_SPLIT_MAX();
471 }
472 if (s->id == "indomain_random") {
473 r0 = "="; r1 = "!=";
474 return INT_VAL_RND(rnd);
475 }
476 if (s->id == "indomain") {
477 r0 = "="; r1 = "=";
478 return INT_VALUES_MIN();
479 }
480 if (s->id == "indomain_middle") {
481 std::cerr << "Warning, replacing unsupported annotation "
482 << "indomain_middle with indomain_median" << std::endl;
483 r0 = "="; r1 = "!=";
484 return INT_VAL_MED();
485 }
486 if (s->id == "indomain_interval") {
487 std::cerr << "Warning, replacing unsupported annotation "
488 << "indomain_interval with indomain_split" << std::endl;
489 r0 = "<="; r1 = ">";
490 return INT_VAL_SPLIT_MIN();
491 }
492 }
493 std::cerr << "Warning, ignored search annotation: ";
494 ann->print(std::cerr);
495 std::cerr << std::endl;
496 r0 = "="; r1 = "!=";
497 return INT_VAL_MIN();
498 }
499
500 IntAssign ann2asnivalsel(AST::Node* ann, Rnd rnd) {
501 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
502 if (s->id == "indomain_min")
503 return INT_ASSIGN_MIN();
504 if (s->id == "indomain_max")
505 return INT_ASSIGN_MAX();
506 if (s->id == "indomain_median")
507 return INT_ASSIGN_MED();
508 if (s->id == "indomain_random") {
509 return INT_ASSIGN_RND(rnd);
510 }
511 }
512 std::cerr << "Warning, ignored search annotation: ";
513 ann->print(std::cerr);
514 std::cerr << std::endl;
515 return INT_ASSIGN_MIN();
516 }
517
518 TieBreak<BoolVarBranch> ann2bvarsel(AST::Node* ann, Rnd rnd, double decay) {
519 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
520 if ((s->id == "input_order") ||
521 (s->id == "first_fail") ||
522 (s->id == "anti_first_fail") ||
523 (s->id == "smallest") ||
524 (s->id == "largest") ||
525 (s->id == "max_regret"))
526 return TieBreak<BoolVarBranch>(BOOL_VAR_NONE());
527 if ((s->id == "occurrence") ||
528 (s->id == "most_constrained"))
529 return TieBreak<BoolVarBranch>(BOOL_VAR_DEGREE_MAX());
530 if (s->id == "random")
531 return TieBreak<BoolVarBranch>(BOOL_VAR_RND(rnd));
532 if ((s->id == "afc_min") ||
533 (s->id == "afc_size_min"))
534 return TieBreak<BoolVarBranch>(BOOL_VAR_AFC_MIN(decay));
535 if ((s->id == "afc_max") ||
536 (s->id == "afc_size_max") ||
537 (s->id == "dom_w_deg"))
538 return TieBreak<BoolVarBranch>(BOOL_VAR_AFC_MAX(decay));
539 if ((s->id == "action_min") &&
540 (s->id == "action_size_min"))
541 return TieBreak<BoolVarBranch>(BOOL_VAR_ACTION_MIN(decay));
542 if ((s->id == "action_max") ||
543 (s->id == "action_size_max"))
544 return TieBreak<BoolVarBranch>(BOOL_VAR_ACTION_MAX(decay));
545 }
546 std::cerr << "Warning, ignored search annotation: ";
547 ann->print(std::cerr);
548 std::cerr << std::endl;
549 return TieBreak<BoolVarBranch>(BOOL_VAR_NONE());
550 }
551
552 BoolValBranch ann2bvalsel(AST::Node* ann, std::string& r0, std::string& r1,
553 Rnd rnd) {
554 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
555 if (s->id == "indomain_min") {
556 r0 = "="; r1 = "!=";
557 return BOOL_VAL_MIN();
558 }
559 if (s->id == "indomain_max") {
560 r0 = "="; r1 = "!=";
561 return BOOL_VAL_MAX();
562 }
563 if (s->id == "indomain_median") {
564 r0 = "="; r1 = "!=";
565 return BOOL_VAL_MIN();
566 }
567 if (s->id == "indomain_split") {
568 r0 = "<="; r1 = ">";
569 return BOOL_VAL_MIN();
570 }
571 if (s->id == "indomain_reverse_split") {
572 r0 = ">"; r1 = "<=";
573 return BOOL_VAL_MAX();
574 }
575 if (s->id == "indomain_random") {
576 r0 = "="; r1 = "!=";
577 return BOOL_VAL_RND(rnd);
578 }
579 if (s->id == "indomain") {
580 r0 = "="; r1 = "=";
581 return BOOL_VAL_MIN();
582 }
583 if (s->id == "indomain_middle") {
584 std::cerr << "Warning, replacing unsupported annotation "
585 << "indomain_middle with indomain_median" << std::endl;
586 r0 = "="; r1 = "!=";
587 return BOOL_VAL_MIN();
588 }
589 if (s->id == "indomain_interval") {
590 std::cerr << "Warning, replacing unsupported annotation "
591 << "indomain_interval with indomain_split" << std::endl;
592 r0 = "<="; r1 = ">";
593 return BOOL_VAL_MIN();
594 }
595 }
596 std::cerr << "Warning, ignored search annotation: ";
597 ann->print(std::cerr);
598 std::cerr << std::endl;
599 r0 = "="; r1 = "!=";
600 return BOOL_VAL_MIN();
601 }
602
603 BoolAssign ann2asnbvalsel(AST::Node* ann, Rnd rnd) {
604 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
605 if ((s->id == "indomain_min") ||
606 (s->id == "indomain_median"))
607 return BOOL_ASSIGN_MIN();
608 if (s->id == "indomain_max")
609 return BOOL_ASSIGN_MAX();
610 if (s->id == "indomain_random") {
611 return BOOL_ASSIGN_RND(rnd);
612 }
613 }
614 std::cerr << "Warning, ignored search annotation: ";
615 ann->print(std::cerr);
616 std::cerr << std::endl;
617 return BOOL_ASSIGN_MIN();
618 }
619
620#ifdef GECODE_HAS_SET_VARS
621 SetVarBranch ann2svarsel(AST::Node* ann, Rnd rnd, double decay) {
622 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
623 if (s->id == "input_order")
624 return SET_VAR_NONE();
625 if (s->id == "first_fail")
626 return SET_VAR_SIZE_MIN();
627 if (s->id == "anti_first_fail")
628 return SET_VAR_SIZE_MAX();
629 if (s->id == "smallest")
630 return SET_VAR_MIN_MIN();
631 if (s->id == "largest")
632 return SET_VAR_MAX_MAX();
633 if (s->id == "afc_min")
634 return SET_VAR_AFC_MIN(decay);
635 if (s->id == "afc_max")
636 return SET_VAR_AFC_MAX(decay);
637 if (s->id == "afc_size_min")
638 return SET_VAR_AFC_SIZE_MIN(decay);
639 if (s->id == "afc_size_max")
640 return SET_VAR_AFC_SIZE_MAX(decay);
641 if (s->id == "action_min")
642 return SET_VAR_ACTION_MIN(decay);
643 if (s->id == "action_max")
644 return SET_VAR_ACTION_MAX(decay);
645 if (s->id == "action_size_min")
646 return SET_VAR_ACTION_SIZE_MIN(decay);
647 if (s->id == "action_size_max")
648 return SET_VAR_ACTION_SIZE_MAX(decay);
649 if (s->id == "random") {
650 return SET_VAR_RND(rnd);
651 }
652 }
653 std::cerr << "Warning, ignored search annotation: ";
654 ann->print(std::cerr);
655 std::cerr << std::endl;
656 return SET_VAR_NONE();
657 }
658
659 SetValBranch ann2svalsel(AST::Node* ann, std::string r0, std::string r1,
660 Rnd rnd) {
661 (void) rnd;
662 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
663 if (s->id == "indomain_min") {
664 r0 = "in"; r1 = "not in";
665 return SET_VAL_MIN_INC();
666 }
667 if (s->id == "indomain_max") {
668 r0 = "in"; r1 = "not in";
669 return SET_VAL_MAX_INC();
670 }
671 if (s->id == "outdomain_min") {
672 r1 = "in"; r0 = "not in";
673 return SET_VAL_MIN_EXC();
674 }
675 if (s->id == "outdomain_max") {
676 r1 = "in"; r0 = "not in";
677 return SET_VAL_MAX_EXC();
678 }
679 }
680 std::cerr << "Warning, ignored search annotation: ";
681 ann->print(std::cerr);
682 std::cerr << std::endl;
683 r0 = "in"; r1 = "not in";
684 return SET_VAL_MIN_INC();
685 }
686#endif
687
688#ifdef GECODE_HAS_FLOAT_VARS
689 TieBreak<FloatVarBranch> ann2fvarsel(AST::Node* ann, Rnd rnd,
690 double decay) {
691 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
692 if (s->id == "input_order")
693 return TieBreak<FloatVarBranch>(FLOAT_VAR_NONE());
694 if (s->id == "first_fail")
695 return TieBreak<FloatVarBranch>(FLOAT_VAR_SIZE_MIN());
696 if (s->id == "anti_first_fail")
697 return TieBreak<FloatVarBranch>(FLOAT_VAR_SIZE_MAX());
698 if (s->id == "smallest")
699 return TieBreak<FloatVarBranch>(FLOAT_VAR_MIN_MIN());
700 if (s->id == "largest")
701 return TieBreak<FloatVarBranch>(FLOAT_VAR_MAX_MAX());
702 if (s->id == "occurrence")
703 return TieBreak<FloatVarBranch>(FLOAT_VAR_DEGREE_MAX());
704 if (s->id == "most_constrained")
705 return TieBreak<FloatVarBranch>(FLOAT_VAR_SIZE_MIN(),
706 FLOAT_VAR_DEGREE_MAX());
707 if (s->id == "random") {
708 return TieBreak<FloatVarBranch>(FLOAT_VAR_RND(rnd));
709 }
710 if (s->id == "afc_min")
711 return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_MIN(decay));
712 if (s->id == "afc_max")
713 return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_MAX(decay));
714 if (s->id == "afc_size_min")
715 return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_SIZE_MIN(decay));
716 if (s->id == "afc_size_max")
717 return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_SIZE_MAX(decay));
718 if (s->id == "action_min")
719 return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTION_MIN(decay));
720 if (s->id == "action_max")
721 return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTION_MAX(decay));
722 if (s->id == "action_size_min")
723 return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTION_SIZE_MIN(decay));
724 if (s->id == "action_size_max")
725 return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTION_SIZE_MAX(decay));
726 }
727 std::cerr << "Warning, ignored search annotation: ";
728 ann->print(std::cerr);
729 std::cerr << std::endl;
730 return TieBreak<FloatVarBranch>(FLOAT_VAR_NONE());
731 }
732
733 FloatValBranch ann2fvalsel(AST::Node* ann, std::string r0, std::string r1) {
734 if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
735 if (s->id == "indomain_split") {
736 r0 = "<="; r1 = ">";
737 return FLOAT_VAL_SPLIT_MIN();
738 }
739 if (s->id == "indomain_reverse_split") {
740 r1 = "<="; r0 = ">";
741 return FLOAT_VAL_SPLIT_MAX();
742 }
743 }
744 std::cerr << "Warning, ignored search annotation: ";
745 ann->print(std::cerr);
746 std::cerr << std::endl;
747 r0 = "<="; r1 = ">";
748 return FLOAT_VAL_SPLIT_MIN();
749 }
750
751#endif
752
753 class FlatZincSpaceInitData {
754 public:
755 /// Hash table of tuple sets
756 typedef std::unordered_set<TupleSet> TupleSetSet;
757 /// Hash table of tuple sets
758 TupleSetSet tupleSetSet;
759
760 /// Hash table of shared integer arrays
761 typedef std::unordered_set<SharedArray<int> > IntSharedArraySet;
762 /// Hash table of shared integer arrays
763 IntSharedArraySet intSharedArraySet;
764
765 /// Hash table of DFAs
766 typedef std::unordered_set<DFA> DFASet;
767 /// Hash table of DFAs
768 DFASet dfaSet;
769
770 /// Initialize
771 FlatZincSpaceInitData(void) {}
772 };
773
774 FlatZincSpace::FlatZincSpace(FlatZincSpace& f)
775 : Space(f),
776 _initData(nullptr), _random(f._random),
777 _solveAnnotations(nullptr), iv_boolalias(nullptr),
778#ifdef GECODE_HAS_FLOAT_VARS
779 step(f.step),
780#endif
781 needAuxVars(f.needAuxVars) {
782 _optVar = f._optVar;
783 _optVarIsInt = f._optVarIsInt;
784 _method = f._method;
785 _lns = f._lns;
786 _lnsInitialSolution = f._lnsInitialSolution;
787 branchInfo = f.branchInfo;
788 iv.update(*this, f.iv);
789 iv_lns.update(*this, f.iv_lns);
790 intVarCount = f.intVarCount;
791
792 if (needAuxVars) {
793 IntVarArgs iva;
794 for (int i=0; i<f.iv_aux.size(); i++) {
795 if (!f.iv_aux[i].assigned()) {
796 iva << IntVar();
797 iva[iva.size()-1].update(*this, f.iv_aux[i]);
798 }
799 }
800 iv_aux = IntVarArray(*this, iva);
801 }
802
803 bv.update(*this, f.bv);
804 boolVarCount = f.boolVarCount;
805 if (needAuxVars) {
806 BoolVarArgs bva;
807 for (int i=0; i<f.bv_aux.size(); i++) {
808 if (!f.bv_aux[i].assigned()) {
809 bva << BoolVar();
810 bva[bva.size()-1].update(*this, f.bv_aux[i]);
811 }
812 }
813 bv_aux = BoolVarArray(*this, bva);
814 }
815
816#ifdef GECODE_HAS_SET_VARS
817 sv.update(*this, f.sv);
818 setVarCount = f.setVarCount;
819 if (needAuxVars) {
820 SetVarArgs sva;
821 for (int i=0; i<f.sv_aux.size(); i++) {
822 if (!f.sv_aux[i].assigned()) {
823 sva << SetVar();
824 sva[sva.size()-1].update(*this, f.sv_aux[i]);
825 }
826 }
827 sv_aux = SetVarArray(*this, sva);
828 }
829#endif
830#ifdef GECODE_HAS_FLOAT_VARS
831 fv.update(*this, f.fv);
832 floatVarCount = f.floatVarCount;
833 if (needAuxVars) {
834 FloatVarArgs fva;
835 for (int i=0; i<f.fv_aux.size(); i++) {
836 if (!f.fv_aux[i].assigned()) {
837 fva << FloatVar();
838 fva[fva.size()-1].update(*this, f.fv_aux[i]);
839 }
840 }
841 fv_aux = FloatVarArray(*this, fva);
842 }
843#endif
844 }
845
846 FlatZincSpace::FlatZincSpace(Rnd& random)
847 : _initData(new FlatZincSpaceInitData),
848 intVarCount(-1), boolVarCount(-1), floatVarCount(-1), setVarCount(-1),
849 _optVar(-1), _optVarIsInt(true), _lns(0), _lnsInitialSolution(0),
850 _random(random),
851 _solveAnnotations(nullptr), needAuxVars(true) {
852 branchInfo.init();
853 }
854
855 void
856 FlatZincSpace::init(int intVars, int boolVars,
857 int setVars, int floatVars) {
858 (void) setVars;
859 (void) floatVars;
860
861 intVarCount = 0;
862 iv = IntVarArray(*this, intVars);
863 iv_introduced = std::vector<bool>(2*intVars);
864 iv_boolalias = alloc<int>(intVars+(intVars==0?1:0));
865 boolVarCount = 0;
866 bv = BoolVarArray(*this, boolVars);
867 bv_introduced = std::vector<bool>(2*boolVars);
868#ifdef GECODE_HAS_SET_VARS
869 setVarCount = 0;
870 sv = SetVarArray(*this, setVars);
871 sv_introduced = std::vector<bool>(2*setVars);
872#endif
873#ifdef GECODE_HAS_FLOAT_VARS
874 floatVarCount = 0;
875 fv = FloatVarArray(*this, floatVars);
876 fv_introduced = std::vector<bool>(2*floatVars);
877#endif
878 }
879
880 void
881 FlatZincSpace::newIntVar(IntVarSpec* vs) {
882 if (vs->alias) {
883 iv[intVarCount++] = iv[vs->i];
884 } else {
885 IntSet dom(vs2is(vs));
886 if (dom.size()==0) {
887 fail();
888 return;
889 } else {
890 iv[intVarCount++] = IntVar(*this, dom);
891 }
892 }
893 iv_introduced[2*(intVarCount-1)] = vs->introduced;
894 iv_introduced[2*(intVarCount-1)+1] = vs->funcDep;
895 iv_boolalias[intVarCount-1] = -1;
896 }
897
898 void
899 FlatZincSpace::aliasBool2Int(int iv, int bv) {
900 iv_boolalias[iv] = bv;
901 }
902 int
903 FlatZincSpace::aliasBool2Int(int iv) {
904 return iv_boolalias[iv];
905 }
906
907 void
908 FlatZincSpace::newBoolVar(BoolVarSpec* vs) {
909 if (vs->alias) {
910 bv[boolVarCount++] = bv[vs->i];
911 } else {
912 bv[boolVarCount++] = BoolVar(*this, vs2bsl(vs), vs2bsh(vs));
913 }
914 bv_introduced[2*(boolVarCount-1)] = vs->introduced;
915 bv_introduced[2*(boolVarCount-1)+1] = vs->funcDep;
916 }
917
918#ifdef GECODE_HAS_SET_VARS
919 void
920 FlatZincSpace::newSetVar(SetVarSpec* vs) {
921 if (vs->alias) {
922 sv[setVarCount++] = sv[vs->i];
923 } else if (vs->assigned) {
924 assert(vs->upperBound());
925 AST::SetLit* vsv = vs->upperBound.some();
926 if (vsv->interval) {
927 IntSet d(vsv->min, vsv->max);
928 sv[setVarCount++] = SetVar(*this, d, d);
929 } else {
930 int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
931 for (int i=vsv->s.size(); i--; )
932 is[i] = vsv->s[i];
933 IntSet d(is, vsv->s.size());
934 heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
935 sv[setVarCount++] = SetVar(*this, d, d);
936 }
937 } else if (vs->upperBound()) {
938 AST::SetLit* vsv = vs->upperBound.some();
939 if (vsv->interval) {
940 IntSet d(vsv->min, vsv->max);
941 sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
942 } else {
943 int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
944 for (int i=vsv->s.size(); i--; )
945 is[i] = vsv->s[i];
946 IntSet d(is, vsv->s.size());
947 heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
948 sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
949 }
950 } else {
951 sv[setVarCount++] = SetVar(*this, IntSet::empty,
952 IntSet(Set::Limits::min,
953 Set::Limits::max));
954 }
955 sv_introduced[2*(setVarCount-1)] = vs->introduced;
956 sv_introduced[2*(setVarCount-1)+1] = vs->funcDep;
957 }
958#else
959 void
960 FlatZincSpace::newSetVar(SetVarSpec*) {
961 throw FlatZinc::Error("Gecode", "set variables not supported");
962 }
963#endif
964
965#ifdef GECODE_HAS_FLOAT_VARS
966 void
967 FlatZincSpace::newFloatVar(FloatVarSpec* vs) {
968 if (vs->alias) {
969 fv[floatVarCount++] = fv[vs->i];
970 } else {
971 double dmin, dmax;
972 if (vs->domain()) {
973 dmin = vs->domain.some().first;
974 dmax = vs->domain.some().second;
975 if (dmin > dmax) {
976 fail();
977 return;
978 }
979 } else {
980 dmin = Float::Limits::min;
981 dmax = Float::Limits::max;
982 }
983 fv[floatVarCount++] = FloatVar(*this, dmin, dmax);
984 }
985 fv_introduced[2*(floatVarCount-1)] = vs->introduced;
986 fv_introduced[2*(floatVarCount-1)+1] = vs->funcDep;
987 }
988#else
989 void
990 FlatZincSpace::newFloatVar(FloatVarSpec*) {
991 throw FlatZinc::Error("Gecode", "float variables not supported");
992 }
993#endif
994
995 namespace {
996 struct ConExprOrder {
997 bool operator() (ConExpr* ce0, ConExpr* ce1) {
998 return ce0->args->a.size() < ce1->args->a.size();
999 }
1000 };
1001 }
1002
1003 void
1004 FlatZincSpace::postConstraints(std::vector<ConExpr*>& ces) {
1005 ConExprOrder ceo;
1006 std::sort(ces.begin(), ces.end(), ceo);
1007
1008 for (unsigned int i=0; i<ces.size(); i++) {
1009 const ConExpr& ce = *ces[i];
1010 try {
1011 registry().post(*this, ce);
1012 } catch (Gecode::Exception& e) {
1013 throw FlatZinc::Error("Gecode", e.what(), ce.ann);
1014 } catch (AST::TypeError& e) {
1015 throw FlatZinc::Error("Type error", e.what(), ce.ann);
1016 }
1017 delete ces[i];
1018 ces[i] = nullptr;
1019 }
1020 }
1021
1022 void flattenAnnotations(AST::Array* ann, std::vector<AST::Node*>& out) {
1023 for (unsigned int i=0; i<ann->a.size(); i++) {
1024 if (ann->a[i]->isCall("seq_search")) {
1025 AST::Call* c = ann->a[i]->getCall();
1026 if (c->args->isArray())
1027 flattenAnnotations(c->args->getArray(), out);
1028 else
1029 out.push_back(c->args);
1030 } else {
1031 out.push_back(ann->a[i]);
1032 }
1033 }
1034 }
1035
1036 void
1037 FlatZincSpace::createBranchers(Printer&p, AST::Node* ann, FlatZincOptions& opt,
1038 bool ignoreUnknown,
1039 std::ostream& err) {
1040 int seed = opt.seed();
1041 double decay = opt.decay();
1042 Rnd rnd(static_cast<unsigned int>(seed));
1043 TieBreak<IntVarBranch> def_int_varsel = INT_VAR_AFC_SIZE_MAX(0.99);
1044 IntBoolVarBranch def_intbool_varsel = INTBOOL_VAR_AFC_SIZE_MAX(0.99);
1045 IntValBranch def_int_valsel = INT_VAL_MIN();
1046 std::string def_int_rel_left = "=";
1047 std::string def_int_rel_right = "!=";
1048 TieBreak<BoolVarBranch> def_bool_varsel = BOOL_VAR_AFC_MAX(0.99);
1049 BoolValBranch def_bool_valsel = BOOL_VAL_MIN();
1050 std::string def_bool_rel_left = "=";
1051 std::string def_bool_rel_right = "!=";
1052#ifdef GECODE_HAS_SET_VARS
1053 SetVarBranch def_set_varsel = SET_VAR_AFC_SIZE_MAX(0.99);
1054 SetValBranch def_set_valsel = SET_VAL_MIN_INC();
1055 std::string def_set_rel_left = "in";
1056 std::string def_set_rel_right = "not in";
1057#endif
1058#ifdef GECODE_HAS_FLOAT_VARS
1059 TieBreak<FloatVarBranch> def_float_varsel = FLOAT_VAR_SIZE_MIN();
1060 FloatValBranch def_float_valsel = FLOAT_VAL_SPLIT_MIN();
1061 std::string def_float_rel_left = "<=";
1062 std::string def_float_rel_right = ">";
1063#endif
1064
1065 std::vector<bool> iv_searched(iv.size());
1066 for (unsigned int i=iv.size(); i--;)
1067 iv_searched[i] = false;
1068 std::vector<bool> bv_searched(bv.size());
1069 for (unsigned int i=bv.size(); i--;)
1070 bv_searched[i] = false;
1071#ifdef GECODE_HAS_SET_VARS
1072 std::vector<bool> sv_searched(sv.size());
1073 for (unsigned int i=sv.size(); i--;)
1074 sv_searched[i] = false;
1075#endif
1076#ifdef GECODE_HAS_FLOAT_VARS
1077 std::vector<bool> fv_searched(fv.size());
1078 for (unsigned int i=fv.size(); i--;)
1079 fv_searched[i] = false;
1080#endif
1081
1082 _lns = 0;
1083 if (ann) {
1084 std::vector<AST::Node*> flatAnn;
1085 if (ann->isArray()) {
1086 flattenAnnotations(ann->getArray() , flatAnn);
1087 } else {
1088 flatAnn.push_back(ann);
1089 }
1090
1091 for (unsigned int i=0; i<flatAnn.size(); i++) {
1092 if (flatAnn[i]->isCall("restart_geometric")) {
1093 AST::Call* call = flatAnn[i]->getCall("restart_geometric");
1094 opt.restart(RM_GEOMETRIC);
1095 AST::Array* args = call->getArgs(2);
1096 opt.restart_base(args->a[0]->getFloat());
1097 opt.restart_scale(args->a[1]->getInt());
1098 } else if (flatAnn[i]->isCall("restart_luby")) {
1099 AST::Call* call = flatAnn[i]->getCall("restart_luby");
1100 opt.restart(RM_LUBY);
1101 opt.restart_scale(call->args->getInt());
1102 } else if (flatAnn[i]->isCall("restart_linear")) {
1103 AST::Call* call = flatAnn[i]->getCall("restart_linear");
1104 opt.restart(RM_LINEAR);
1105 opt.restart_scale(call->args->getInt());
1106 } else if (flatAnn[i]->isCall("restart_constant")) {
1107 AST::Call* call = flatAnn[i]->getCall("restart_constant");
1108 opt.restart(RM_CONSTANT);
1109 opt.restart_scale(call->args->getInt());
1110 } else if (flatAnn[i]->isCall("restart_none")) {
1111 opt.restart(RM_NONE);
1112 } else if (flatAnn[i]->isCall("relax_and_reconstruct")) {
1113 if (_lns != 0)
1114 throw FlatZinc::Error("FlatZinc",
1115 "Only one relax_and_reconstruct annotation allowed");
1116 AST::Call *call = flatAnn[i]->getCall("relax_and_reconstruct");
1117 AST::Array* args;
1118 if (call->args->getArray()->a.size()==2) {
1119 args = call->getArgs(2);
1120 } else {
1121 args = call->getArgs(3);
1122 }
1123 _lns = args->a[1]->getInt();
1124 AST::Array *vars = args->a[0]->getArray();
1125 int k=vars->a.size();
1126 for (int i=vars->a.size(); i--;)
1127 if (vars->a[i]->isInt())
1128 k--;
1129 iv_lns = IntVarArray(*this, k);
1130 k = 0;
1131 for (unsigned int i=0; i<vars->a.size(); i++) {
1132 if (vars->a[i]->isInt())
1133 continue;
1134 iv_lns[k++] = iv[vars->a[i]->getIntVar()];
1135 }
1136 if (args->a.size()==3) {
1137 AST::Array *initial = args->a[2]->getArray();
1138 _lnsInitialSolution = IntSharedArray(initial->a.size());
1139 for (unsigned int i=initial->a.size(); i--;)
1140 _lnsInitialSolution[i] = initial->a[i]->getInt();
1141 }
1142 } else if (flatAnn[i]->isCall("gecode_search")) {
1143 AST::Call* c = flatAnn[i]->getCall();
1144 branchWithPlugin(c->args);
1145 } else if (flatAnn[i]->isCall("int_search")) {
1146 AST::Call *call = flatAnn[i]->getCall("int_search");
1147 AST::Array *args = call->getArgs(4);
1148 AST::Array *vars = args->a[0]->getArray();
1149 int k=vars->a.size();
1150 for (int i=vars->a.size(); i--;)
1151 if (vars->a[i]->isInt())
1152 k--;
1153 IntVarArgs va(k);
1154 std::vector<std::string> names;
1155 k=0;
1156 for (unsigned int i=0; i<vars->a.size(); i++) {
1157 if (vars->a[i]->isInt())
1158 continue;
1159 va[k++] = iv[vars->a[i]->getIntVar()];
1160 iv_searched[vars->a[i]->getIntVar()] = true;
1161 names.push_back(vars->a[i]->getVarName());
1162 }
1163 std::string r0, r1;
1164 {
1165 BrancherGroup bg;
1166 branch(bg(*this), va,
1167 ann2ivarsel(args->a[1],rnd,decay),
1168 ann2ivalsel(args->a[2],r0,r1,rnd),
1169 nullptr,
1170 &varValPrint<IntVar>);
1171 branchInfo.add(bg,r0,r1,names);
1172 }
1173 } else if (flatAnn[i]->isCall("int_assign")) {
1174 AST::Call *call = flatAnn[i]->getCall("int_assign");
1175 AST::Array *args = call->getArgs(2);
1176 AST::Array *vars = args->a[0]->getArray();
1177 int k=vars->a.size();
1178 for (int i=vars->a.size(); i--;)
1179 if (vars->a[i]->isInt())
1180 k--;
1181 IntVarArgs va(k);
1182 k=0;
1183 for (unsigned int i=0; i<vars->a.size(); i++) {
1184 if (vars->a[i]->isInt())
1185 continue;
1186 va[k++] = iv[vars->a[i]->getIntVar()];
1187 iv_searched[vars->a[i]->getIntVar()] = true;
1188 }
1189 assign(*this, va, ann2asnivalsel(args->a[1],rnd), nullptr,
1190 &varValPrint<IntVar>);
1191 } else if (flatAnn[i]->isCall("bool_search")) {
1192 AST::Call *call = flatAnn[i]->getCall("bool_search");
1193 AST::Array *args = call->getArgs(4);
1194 AST::Array *vars = args->a[0]->getArray();
1195 int k=vars->a.size();
1196 for (int i=vars->a.size(); i--;)
1197 if (vars->a[i]->isBool())
1198 k--;
1199 BoolVarArgs va(k);
1200 k=0;
1201 std::vector<std::string> names;
1202 for (unsigned int i=0; i<vars->a.size(); i++) {
1203 if (vars->a[i]->isBool())
1204 continue;
1205 va[k++] = bv[vars->a[i]->getBoolVar()];
1206 bv_searched[vars->a[i]->getBoolVar()] = true;
1207 names.push_back(vars->a[i]->getVarName());
1208 }
1209
1210 std::string r0, r1;
1211 {
1212 BrancherGroup bg;
1213 branch(bg(*this), va,
1214 ann2bvarsel(args->a[1],rnd,decay),
1215 ann2bvalsel(args->a[2],r0,r1,rnd),
1216 nullptr,
1217 &varValPrint<BoolVar>);
1218 branchInfo.add(bg,r0,r1,names);
1219 }
1220 } else if (flatAnn[i]->isCall("int_default_search")) {
1221 AST::Call *call = flatAnn[i]->getCall("int_default_search");
1222 AST::Array *args = call->getArgs(2);
1223 def_int_varsel = ann2ivarsel(args->a[0],rnd,decay);
1224 def_int_valsel = ann2ivalsel(args->a[1],
1225 def_int_rel_left,def_int_rel_right,rnd);
1226 } else if (flatAnn[i]->isCall("bool_default_search")) {
1227 AST::Call *call = flatAnn[i]->getCall("bool_default_search");
1228 AST::Array *args = call->getArgs(2);
1229 def_bool_varsel = ann2bvarsel(args->a[0],rnd,decay);
1230 def_bool_valsel = ann2bvalsel(args->a[1],
1231 def_bool_rel_left,def_bool_rel_right,
1232 rnd);
1233 } else if (flatAnn[i]->isCall("set_search")) {
1234#ifdef GECODE_HAS_SET_VARS
1235 AST::Call *call = flatAnn[i]->getCall("set_search");
1236 AST::Array *args = call->getArgs(4);
1237 AST::Array *vars = args->a[0]->getArray();
1238 int k=vars->a.size();
1239 for (int i=vars->a.size(); i--;)
1240 if (vars->a[i]->isSet())
1241 k--;
1242 SetVarArgs va(k);
1243 k=0;
1244 std::vector<std::string> names;
1245 for (unsigned int i=0; i<vars->a.size(); i++) {
1246 if (vars->a[i]->isSet())
1247 continue;
1248 va[k++] = sv[vars->a[i]->getSetVar()];
1249 sv_searched[vars->a[i]->getSetVar()] = true;
1250 names.push_back(vars->a[i]->getVarName());
1251 }
1252 std::string r0, r1;
1253 {
1254 BrancherGroup bg;
1255 branch(bg(*this), va,
1256 ann2svarsel(args->a[1],rnd,decay),
1257 ann2svalsel(args->a[2],r0,r1,rnd),
1258 nullptr,
1259 &varValPrint<SetVar>);
1260 branchInfo.add(bg,r0,r1,names);
1261 }
1262#else
1263 if (!ignoreUnknown) {
1264 err << "Warning, ignored search annotation: ";
1265 flatAnn[i]->print(err);
1266 err << std::endl;
1267 }
1268#endif
1269 } else if (flatAnn[i]->isCall("set_default_search")) {
1270#ifdef GECODE_HAS_SET_VARS
1271 AST::Call *call = flatAnn[i]->getCall("set_default_search");
1272 AST::Array *args = call->getArgs(2);
1273 def_set_varsel = ann2svarsel(args->a[0],rnd,decay);
1274 def_set_valsel = ann2svalsel(args->a[1],
1275 def_set_rel_left,def_set_rel_right,rnd);
1276#else
1277 if (!ignoreUnknown) {
1278 err << "Warning, ignored search annotation: ";
1279 flatAnn[i]->print(err);
1280 err << std::endl;
1281 }
1282#endif
1283 } else if (flatAnn[i]->isCall("float_default_search")) {
1284#ifdef GECODE_HAS_FLOAT_VARS
1285 AST::Call *call = flatAnn[i]->getCall("float_default_search");
1286 AST::Array *args = call->getArgs(2);
1287 def_float_varsel = ann2fvarsel(args->a[0],rnd,decay);
1288 def_float_valsel = ann2fvalsel(args->a[1],
1289 def_float_rel_left,def_float_rel_right);
1290#else
1291 if (!ignoreUnknown) {
1292 err << "Warning, ignored search annotation: ";
1293 flatAnn[i]->print(err);
1294 err << std::endl;
1295 }
1296#endif
1297 } else if (flatAnn[i]->isCall("float_search")) {
1298#ifdef GECODE_HAS_FLOAT_VARS
1299 AST::Call *call = flatAnn[i]->getCall("float_search");
1300 AST::Array *args = call->getArgs(5);
1301 AST::Array *vars = args->a[0]->getArray();
1302 int k=vars->a.size();
1303 for (int i=vars->a.size(); i--;)
1304 if (vars->a[i]->isFloat())
1305 k--;
1306 FloatVarArgs va(k);
1307 k=0;
1308 std::vector<std::string> names;
1309 for (unsigned int i=0; i<vars->a.size(); i++) {
1310 if (vars->a[i]->isFloat())
1311 continue;
1312 va[k++] = fv[vars->a[i]->getFloatVar()];
1313 fv_searched[vars->a[i]->getFloatVar()] = true;
1314 names.push_back(vars->a[i]->getVarName());
1315 }
1316 std::string r0, r1;
1317 {
1318 BrancherGroup bg;
1319 branch(bg(*this), va,
1320 ann2fvarsel(args->a[2],rnd,decay),
1321 ann2fvalsel(args->a[3],r0,r1),
1322 nullptr,
1323 &varValPrintF);
1324 branchInfo.add(bg,r0,r1,names);
1325 }
1326#else
1327 if (!ignoreUnknown) {
1328 err << "Warning, ignored search annotation: ";
1329 flatAnn[i]->print(err);
1330 err << std::endl;
1331 }
1332#endif
1333 } else {
1334 if (!ignoreUnknown) {
1335 err << "Warning, ignored search annotation: ";
1336 flatAnn[i]->print(err);
1337 err << std::endl;
1338 }
1339 }
1340 }
1341 }
1342 int introduced = 0;
1343 int funcdep = 0;
1344 int searched = 0;
1345 for (int i=iv.size(); i--;) {
1346 if (iv_searched[i] || (_method != SAT && _optVarIsInt && _optVar==i)) {
1347 searched++;
1348 } else if (iv_introduced[2*i]) {
1349 if (iv_introduced[2*i+1]) {
1350 funcdep++;
1351 } else {
1352 introduced++;
1353 }
1354 }
1355 }
1356 std::vector<std::string> iv_sol_names(iv.size()-(introduced+funcdep+searched));
1357 IntVarArgs iv_sol(iv.size()-(introduced+funcdep+searched));
1358 std::vector<std::string> iv_tmp_names(introduced);
1359 IntVarArgs iv_tmp(introduced);
1360 for (int i=iv.size(), j=0, k=0; i--;) {
1361 if (iv_searched[i] || (_method != SAT && _optVarIsInt && _optVar==i))
1362 continue;
1363 if (iv_introduced[2*i]) {
1364 if (!iv_introduced[2*i+1]) {
1365 iv_tmp_names[j] = p.intVarName(i);
1366 iv_tmp[j++] = iv[i];
1367 }
1368 } else {
1369 iv_sol_names[k] = p.intVarName(i);
1370 iv_sol[k++] = iv[i];
1371 }
1372 }
1373
1374 introduced = 0;
1375 funcdep = 0;
1376 searched = 0;
1377 for (int i=bv.size(); i--;) {
1378 if (bv_searched[i]) {
1379 searched++;
1380 } else if (bv_introduced[2*i]) {
1381 if (bv_introduced[2*i+1]) {
1382 funcdep++;
1383 } else {
1384 introduced++;
1385 }
1386 }
1387 }
1388 std::vector<std::string> bv_sol_names(bv.size()-(introduced+funcdep+searched));
1389 BoolVarArgs bv_sol(bv.size()-(introduced+funcdep+searched));
1390 BoolVarArgs bv_tmp(introduced);
1391 std::vector<std::string> bv_tmp_names(introduced);
1392 for (int i=bv.size(), j=0, k=0; i--;) {
1393 if (bv_searched[i])
1394 continue;
1395 if (bv_introduced[2*i]) {
1396 if (!bv_introduced[2*i+1]) {
1397 bv_tmp_names[j] = p.boolVarName(i);
1398 bv_tmp[j++] = bv[i];
1399 }
1400 } else {
1401 bv_sol_names[k] = p.boolVarName(i);
1402 bv_sol[k++] = bv[i];
1403 }
1404 }
1405
1406 if (iv_sol.size() > 0 && bv_sol.size() > 0) {
1407 branch(*this, iv_sol, bv_sol, def_intbool_varsel, def_int_valsel);
1408 } else if (iv_sol.size() > 0) {
1409 BrancherGroup bg;
1410 branch(bg(*this), iv_sol, def_int_varsel, def_int_valsel, nullptr,
1411 &varValPrint<IntVar>);
1412 branchInfo.add(bg,def_int_rel_left,def_int_rel_right,iv_sol_names);
1413 } else if (bv_sol.size() > 0) {
1414 BrancherGroup bg;
1415 branch(bg(*this), bv_sol, def_bool_varsel, def_bool_valsel, nullptr,
1416 &varValPrint<BoolVar>);
1417 branchInfo.add(bg,def_bool_rel_left,def_bool_rel_right,bv_sol_names);
1418 }
1419#ifdef GECODE_HAS_FLOAT_VARS
1420 introduced = 0;
1421 funcdep = 0;
1422 searched = 0;
1423 for (int i=fv.size(); i--;) {
1424 if (fv_searched[i] || (_method != SAT && !_optVarIsInt && _optVar==i)) {
1425 searched++;
1426 } else if (fv_introduced[2*i]) {
1427 if (fv_introduced[2*i+1]) {
1428 funcdep++;
1429 } else {
1430 introduced++;
1431 }
1432 }
1433 }
1434 std::vector<std::string> fv_sol_names(fv.size()-(introduced+funcdep+searched));
1435 FloatVarArgs fv_sol(fv.size()-(introduced+funcdep+searched));
1436 FloatVarArgs fv_tmp(introduced);
1437 std::vector<std::string> fv_tmp_names(introduced);
1438 for (int i=fv.size(), j=0, k=0; i--;) {
1439 if (fv_searched[i] || (_method != SAT && !_optVarIsInt && _optVar==i))
1440 continue;
1441 if (fv_introduced[2*i]) {
1442 if (!fv_introduced[2*i+1]) {
1443 fv_tmp_names[j] = p.floatVarName(i);
1444 fv_tmp[j++] = fv[i];
1445 }
1446 } else {
1447 fv_sol_names[k] = p.floatVarName(i);
1448 fv_sol[k++] = fv[i];
1449 }
1450 }
1451
1452 if (fv_sol.size() > 0) {
1453 BrancherGroup bg;
1454 branch(bg(*this), fv_sol, def_float_varsel, def_float_valsel, nullptr,
1455 &varValPrintF);
1456 branchInfo.add(bg,def_float_rel_left,def_float_rel_right,fv_sol_names);
1457 }
1458#endif
1459#ifdef GECODE_HAS_SET_VARS
1460 introduced = 0;
1461 funcdep = 0;
1462 searched = 0;
1463 for (int i=sv.size(); i--;) {
1464 if (sv_searched[i]) {
1465 searched++;
1466 } else if (sv_introduced[2*i]) {
1467 if (sv_introduced[2*i+1]) {
1468 funcdep++;
1469 } else {
1470 introduced++;
1471 }
1472 }
1473 }
1474 std::vector<std::string> sv_sol_names(sv.size()-(introduced+funcdep+searched));
1475 SetVarArgs sv_sol(sv.size()-(introduced+funcdep+searched));
1476 SetVarArgs sv_tmp(introduced);
1477 std::vector<std::string> sv_tmp_names(introduced);
1478 for (int i=sv.size(), j=0, k=0; i--;) {
1479 if (sv_searched[i])
1480 continue;
1481 if (sv_introduced[2*i]) {
1482 if (!sv_introduced[2*i+1]) {
1483 sv_tmp_names[j] = p.setVarName(i);
1484 sv_tmp[j++] = sv[i];
1485 }
1486 } else {
1487 sv_sol_names[k] = p.setVarName(i);
1488 sv_sol[k++] = sv[i];
1489 }
1490 }
1491
1492 if (sv_sol.size() > 0) {
1493 BrancherGroup bg;
1494 branch(bg(*this), sv_sol, def_set_varsel, def_set_valsel, nullptr,
1495 &varValPrint<SetVar>);
1496 branchInfo.add(bg,def_set_rel_left,def_set_rel_right,sv_sol_names);
1497
1498 }
1499#endif
1500 iv_aux = IntVarArray(*this, iv_tmp);
1501 bv_aux = BoolVarArray(*this, bv_tmp);
1502 int n_aux = iv_aux.size() + bv_aux.size();
1503#ifdef GECODE_HAS_SET_VARS
1504 sv_aux = SetVarArray(*this, sv_tmp);
1505 n_aux += sv_aux.size();
1506#endif
1507#ifdef GECODE_HAS_FLOAT_VARS
1508 fv_aux = FloatVarArray(*this, fv_tmp);
1509 n_aux += fv_aux.size();
1510#endif
1511
1512 if (n_aux > 0) {
1513 if (_method == SAT) {
1514 AuxVarBrancher::post(*this, def_int_varsel, def_int_valsel,
1515 def_bool_varsel, def_bool_valsel
1516#ifdef GECODE_HAS_SET_VARS
1517 , def_set_varsel, def_set_valsel
1518#endif
1519#ifdef GECODE_HAS_FLOAT_VARS
1520 , def_float_varsel, def_float_valsel
1521#endif
1522 );
1523 } else {
1524 {
1525 BrancherGroup bg;
1526 branch(bg(*this),iv_aux,def_int_varsel,def_int_valsel, nullptr,
1527 &varValPrint<IntVar>);
1528 branchInfo.add(bg,def_int_rel_left,def_int_rel_right,iv_tmp_names);
1529 }
1530 {
1531 BrancherGroup bg;
1532 branch(bg(*this),bv_aux,def_bool_varsel,def_bool_valsel, nullptr,
1533 &varValPrint<BoolVar>);
1534 branchInfo.add(bg,def_bool_rel_left,def_bool_rel_right,bv_tmp_names);
1535 }
1536 #ifdef GECODE_HAS_SET_VARS
1537 {
1538 BrancherGroup bg;
1539 branch(bg(*this),sv_aux,def_set_varsel,def_set_valsel, nullptr,
1540 &varValPrint<SetVar>);
1541 branchInfo.add(bg,def_set_rel_left,def_set_rel_right,sv_tmp_names);
1542 }
1543 #endif
1544 #ifdef GECODE_HAS_FLOAT_VARS
1545 {
1546 BrancherGroup bg;
1547 branch(bg(*this),fv_aux,def_float_varsel,def_float_valsel, nullptr,
1548 &varValPrintF);
1549 branchInfo.add(bg,def_float_rel_left,def_float_rel_right,fv_tmp_names);
1550 }
1551 #endif
1552
1553 }
1554 }
1555
1556 if (_method == MIN) {
1557 if (_optVarIsInt) {
1558 std::vector<std::string> names(1);
1559 names[0] = p.intVarName(_optVar);
1560 BrancherGroup bg;
1561 branch(bg(*this), iv[_optVar], INT_VAL_MIN(),
1562 &varValPrint<IntVar>);
1563 branchInfo.add(bg,"=","!=",names);
1564 } else {
1565#ifdef GECODE_HAS_FLOAT_VARS
1566 std::vector<std::string> names(1);
1567 names[0] = p.floatVarName(_optVar);
1568 BrancherGroup bg;
1569 branch(bg(*this), fv[_optVar], FLOAT_VAL_SPLIT_MIN(),
1570 &varValPrintF);
1571 branchInfo.add(bg,"<=",">",names);
1572#endif
1573 }
1574 } else if (_method == MAX) {
1575 if (_optVarIsInt) {
1576 std::vector<std::string> names(1);
1577 names[0] = p.intVarName(_optVar);
1578 BrancherGroup bg;
1579 branch(bg(*this), iv[_optVar], INT_VAL_MAX(),
1580 &varValPrint<IntVar>);
1581 branchInfo.add(bg,"=","!=",names);
1582 } else {
1583#ifdef GECODE_HAS_FLOAT_VARS
1584 std::vector<std::string> names(1);
1585 names[0] = p.floatVarName(_optVar);
1586 BrancherGroup bg;
1587 branch(bg(*this), fv[_optVar], FLOAT_VAL_SPLIT_MAX(),
1588 &varValPrintF);
1589 branchInfo.add(bg,"<=",">",names);
1590#endif
1591 }
1592 }
1593
1594 }
1595
1596 AST::Array*
1597 FlatZincSpace::solveAnnotations(void) const {
1598 return _solveAnnotations;
1599 }
1600
1601 void
1602 FlatZincSpace::solve(AST::Array* ann) {
1603 _method = SAT;
1604 _solveAnnotations = ann;
1605 }
1606
1607 void
1608 FlatZincSpace::minimize(int var, bool isInt, AST::Array* ann) {
1609 _method = MIN;
1610 _optVar = var;
1611 _optVarIsInt = isInt;
1612 _solveAnnotations = ann;
1613 }
1614
1615 void
1616 FlatZincSpace::maximize(int var, bool isInt, AST::Array* ann) {
1617 _method = MAX;
1618 _optVar = var;
1619 _optVarIsInt = isInt;
1620 _solveAnnotations = ann;
1621 }
1622
1623 FlatZincSpace::~FlatZincSpace(void) {
1624 delete _initData;
1625 delete _solveAnnotations;
1626 }
1627
1628#ifdef GECODE_HAS_GIST
1629
1630 /**
1631 * \brief Traits class for search engines
1632 */
1633 template<class Engine>
1634 class GistEngine {
1635 };
1636
1637 /// Specialization for DFS
1638 template<typename S>
1639 class GistEngine<DFS<S> > {
1640 public:
1641 static void explore(S* root, const FlatZincOptions& opt,
1642 Gist::Inspector* i, Gist::Comparator* c) {
1643 Gecode::Gist::Options o;
1644 o.c_d = opt.c_d(); o.a_d = opt.a_d();
1645 o.inspect.click(i);
1646 o.inspect.compare(c);
1647 (void) Gecode::Gist::dfs(root, o);
1648 }
1649 };
1650
1651 /// Specialization for BAB
1652 template<typename S>
1653 class GistEngine<BAB<S> > {
1654 public:
1655 static void explore(S* root, const FlatZincOptions& opt,
1656 Gist::Inspector* i, Gist::Comparator* c) {
1657 Gecode::Gist::Options o;
1658 o.c_d = opt.c_d(); o.a_d = opt.a_d();
1659 o.inspect.click(i);
1660 o.inspect.compare(c);
1661 (void) Gecode::Gist::bab(root, o);
1662 }
1663 };
1664
1665 /// \brief An inspector for printing simple text output
1666 template<class S>
1667 class FZPrintingInspector
1668 : public Gecode::Gist::TextOutput, public Gecode::Gist::Inspector {
1669 private:
1670 const Printer& p;
1671 public:
1672 /// Constructor
1673 FZPrintingInspector(const Printer& p0);
1674 /// Use the print method of the template class S to print a space
1675 virtual void inspect(const Space& node);
1676 /// Finalize when Gist exits
1677 virtual void finalize(void);
1678 };
1679
1680 template<class S>
1681 FZPrintingInspector<S>::FZPrintingInspector(const Printer& p0)
1682 : TextOutput("Gecode/FlatZinc"), p(p0) {}
1683
1684 template<class S>
1685 void
1686 FZPrintingInspector<S>::inspect(const Space& node) {
1687 init();
1688 dynamic_cast<const S&>(node).print(getStream(), p);
1689 getStream() << std::endl;
1690 }
1691
1692 template<class S>
1693 void
1694 FZPrintingInspector<S>::finalize(void) {
1695 Gecode::Gist::TextOutput::finalize();
1696 }
1697
1698 template<class S>
1699 class FZPrintingComparator
1700 : public Gecode::Gist::VarComparator<S> {
1701 private:
1702 const Printer& p;
1703 public:
1704 /// Constructor
1705 FZPrintingComparator(const Printer& p0);
1706
1707 /// Use the compare method of the template class S to compare two spaces
1708 virtual void compare(const Space& s0, const Space& s1);
1709 };
1710
1711 template<class S>
1712 FZPrintingComparator<S>::FZPrintingComparator(const Printer& p0)
1713 : Gecode::Gist::VarComparator<S>("Gecode/FlatZinc"), p(p0) {}
1714
1715 template<class S>
1716 void
1717 FZPrintingComparator<S>::compare(const Space& s0, const Space& s1) {
1718 this->init();
1719 try {
1720 dynamic_cast<const S&>(s0).compare(dynamic_cast<const S&>(s1),
1721 this->getStream(), p);
1722 } catch (Exception& e) {
1723 this->getStream() << "Exception: " << e.what();
1724 }
1725 this->getStream() << std::endl;
1726 }
1727
1728#endif
1729
1730 template<template<class> class Engine>
1731 void
1732 FlatZincSpace::runEngine(std::ostream& out, const Printer& p,
1733 const FlatZincOptions& opt, Support::Timer& t_total) {
1734 if (opt.restart()==RM_NONE) {
1735 runMeta<Engine,Driver::EngineToMeta>(out,p,opt,t_total);
1736 } else {
1737 runMeta<Engine,RBS>(out,p,opt,t_total);
1738 }
1739 }
1740
1741#ifdef GECODE_HAS_CPPROFILER
1742
1743 class FlatZincGetInfo : public CPProfilerSearchTracer::GetInfo {
1744 public:
1745 const Printer& p;
1746 FlatZincGetInfo(const Printer& printer) : p(printer) {}
1747 virtual std::string
1748 getInfo(const Space& space) const {
1749 std::stringstream ss;
1750 if (const FlatZincSpace* fz_space = dynamic_cast<const FlatZincSpace*>(&space)) {
1751 ss << "{\n\t\"domains\": \"";
1752 ss << fz_space->getDomains(p);
1753 ss << "\"\n}";
1754 }
1755 return ss.str();
1756 }
1757 ~FlatZincGetInfo(void) {};
1758 };
1759
1760 void printIntVar(std::ostream& os, const std::string name, const Int::IntView& x) {
1761 os << "var ";
1762 if (x.assigned()) {
1763 os << "int: " << name << " = " << x.val() << ";";
1764 } else if (x.range()) {
1765 os << x.min() << ".." << x.max() << ": " << name << ";";
1766 } else {
1767 os << "array_union([";
1768 Gecode::Int::ViewRanges<Int::IntView> r(x);
1769 while (true) {
1770 os << r.min() << ".." << r.max();
1771 ++r;
1772 if (!r()) break;
1773 os << ',';
1774 }
1775 os << "]): " << name << ";";
1776 }
1777 os << "\n";
1778 }
1779 void printBoolVar(std::ostream& os, const std::string name, const BoolVar& b) {
1780 os << "var bool: " << name;
1781 if(b.assigned())
1782 os << " = " << (b.val() ? "true" : "false");
1783 os << ";\n";
1784 }
1785#ifdef GECODE_HAS_FLOAT_VARS
1786 void printFloatVar(std::ostream& os, const std::string name, const Float::FloatView& f) {
1787 os << "var ";
1788 if(f.assigned())
1789 os << "float: " << name << " = " << f.med() << ";";
1790 else
1791 os << f.min() << ".." << f.max() << ": " << name << ";";
1792 os << "\n";
1793 }
1794#endif
1795 std::string FlatZincSpace::getDomains(const Printer& p) const {
1796 std::ostringstream oss;
1797
1798 for (int i = 0; i < iv.size(); i++)
1799 printIntVar(oss, p.intVarName(i), iv[i]);
1800
1801 for (int i = 0; i < bv.size(); i++)
1802 printBoolVar(oss, p.boolVarName(i), bv[i]);
1803
1804#ifdef GECODE_HAS_FLOAT_VARS
1805 for (int i = 0; i < fv.size(); i++)
1806 printFloatVar(oss, p.floatVarName(i), fv[i]);
1807#endif
1808#ifdef GECODE_HAS_SET_VARS
1809 for (int i = 0; i < sv.size(); i++)
1810 oss << "var " << sv[i] << ": " << p.setVarName(i) << ";" << std::endl;
1811#endif
1812
1813 return oss.str();
1814 }
1815
1816#endif
1817
1818 template<template<class> class Engine,
1819 template<class,template<class> class> class Meta>
1820 void
1821 FlatZincSpace::runMeta(std::ostream& out, const Printer& p,
1822 const FlatZincOptions& opt, Support::Timer& t_total) {
1823#ifdef GECODE_HAS_GIST
1824 if (opt.mode() == SM_GIST) {
1825 FZPrintingInspector<FlatZincSpace> pi(p);
1826 FZPrintingComparator<FlatZincSpace> pc(p);
1827 (void) GistEngine<Engine<FlatZincSpace> >::explore(this,opt,&pi,&pc);
1828 return;
1829 }
1830#endif
1831 StatusStatistics sstat;
1832 unsigned int n_p = 0;
1833 Support::Timer t_solve;
1834 t_solve.start();
1835 if (status(sstat) != SS_FAILED) {
1836 n_p = PropagatorGroup::all.size(*this);
1837 }
1838 Search::Options o;
1839 o.stop = Driver::CombinedStop::create(opt.node(), opt.fail(), opt.time(),
1840 true);
1841 o.c_d = opt.c_d();
1842 o.a_d = opt.a_d();
1843
1844#ifdef GECODE_HAS_CPPROFILER
1845 if (opt.profiler_port()) {
1846 FlatZincGetInfo* getInfo = nullptr;
1847 if (opt.profiler_info())
1848 getInfo = new FlatZincGetInfo(p);
1849 o.tracer = new CPProfilerSearchTracer(opt.profiler_id(),
1850 opt.name(), opt.profiler_port(),
1851 getInfo);
1852 }
1853
1854#endif
1855
1856#ifdef GECODE_HAS_FLOAT_VARS
1857 step = opt.step();
1858#endif
1859 o.threads = opt.threads();
1860 o.nogoods_limit = opt.nogoods() ? opt.nogoods_limit() : 0;
1861 o.cutoff = new Search::CutoffAppend(new Search::CutoffConstant(0), 1, Driver::createCutoff(opt));
1862 if (opt.interrupt())
1863 Driver::CombinedStop::installCtrlHandler(true);
1864 {
1865 Meta<FlatZincSpace,Engine> se(this,o);
1866 int noOfSolutions = opt.solutions();
1867 if (noOfSolutions == -1) {
1868 noOfSolutions = (_method == SAT) ? 1 : 0;
1869 }
1870 bool printAll = _method == SAT || opt.allSolutions() || noOfSolutions != 0;
1871 int findSol = noOfSolutions;
1872 FlatZincSpace* sol = nullptr;
1873 while (FlatZincSpace* next_sol = se.next()) {
1874 delete sol;
1875 sol = next_sol;
1876 if (printAll) {
1877 sol->print(out, p);
1878 out << "----------" << std::endl;
1879 }
1880 if (--findSol==0)
1881 goto stopped;
1882 }
1883 if (sol && !printAll) {
1884 sol->print(out, p);
1885 out << "----------" << std::endl;
1886 }
1887 if (!se.stopped()) {
1888 if (sol) {
1889 out << "==========" << std::endl;
1890 } else {
1891 out << "=====UNSATISFIABLE=====" << std::endl;
1892 }
1893 } else if (!sol) {
1894 out << "=====UNKNOWN=====" << std::endl;
1895 }
1896 delete sol;
1897 stopped:
1898 if (opt.interrupt())
1899 Driver::CombinedStop::installCtrlHandler(false);
1900 if (opt.mode() == SM_STAT) {
1901 Gecode::Search::Statistics stat = se.statistics();
1902 double totalTime = (t_total.stop() / 1000.0);
1903 double solveTime = (t_solve.stop() / 1000.0);
1904 double initTime = totalTime - solveTime;
1905 out << std::endl
1906 << "%%%mzn-stat: initTime=" << initTime
1907 << std::endl;
1908 out << "%%%mzn-stat: solveTime=" << solveTime
1909 << std::endl;
1910 out << "%%%mzn-stat: solutions="
1911 << std::abs(noOfSolutions - findSol) << std::endl
1912 << "%%%mzn-stat: variables="
1913 << (intVarCount + boolVarCount + setVarCount) << std::endl
1914 << "%%%mzn-stat: propagators=" << n_p << std::endl
1915 << "%%%mzn-stat: propagations=" << sstat.propagate+stat.propagate << std::endl
1916 << "%%%mzn-stat: nodes=" << stat.node << std::endl
1917 << "%%%mzn-stat: failures=" << stat.fail << std::endl
1918 << "%%%mzn-stat: restarts=" << stat.restart << std::endl
1919 << "%%%mzn-stat: peakDepth=" << stat.depth << std::endl
1920 << "%%%mzn-stat-end" << std::endl
1921 << std::endl;
1922 }
1923 }
1924 delete o.stop;
1925 delete o.tracer;
1926 }
1927
1928#ifdef GECODE_HAS_QT
1929 void
1930 FlatZincSpace::branchWithPlugin(AST::Node* ann) {
1931 if (AST::Call* c = dynamic_cast<AST::Call*>(ann)) {
1932 QString pluginName(c->id.c_str());
1933 if (QLibrary::isLibrary(pluginName+".dll")) {
1934 pluginName += ".dll";
1935 } else if (QLibrary::isLibrary(pluginName+".dylib")) {
1936 pluginName = "lib" + pluginName + ".dylib";
1937 } else if (QLibrary::isLibrary(pluginName+".so")) {
1938 // Must check .so after .dylib so that Mac OS uses .dylib
1939 pluginName = "lib" + pluginName + ".so";
1940 }
1941 QPluginLoader pl(pluginName);
1942 QObject* plugin_o = pl.instance();
1943 if (!plugin_o) {
1944 throw FlatZinc::Error("FlatZinc",
1945 "Error loading plugin "+pluginName.toStdString()+
1946 ": "+pl.errorString().toStdString());
1947 }
1948 BranchPlugin* pb = qobject_cast<BranchPlugin*>(plugin_o);
1949 if (!pb) {
1950 throw FlatZinc::Error("FlatZinc",
1951 "Error loading plugin "+pluginName.toStdString()+
1952 ": does not contain valid PluginBrancher");
1953 }
1954 pb->branch(*this, c);
1955 }
1956 }
1957#else
1958 void
1959 FlatZincSpace::branchWithPlugin(AST::Node*) {
1960 throw FlatZinc::Error("FlatZinc",
1961 "Branching with plugins not supported (requires Qt support)");
1962 }
1963#endif
1964
1965 void
1966 FlatZincSpace::run(std::ostream& out, const Printer& p,
1967 const FlatZincOptions& opt, Support::Timer& t_total) {
1968 switch (_method) {
1969 case MIN:
1970 case MAX:
1971 runEngine<BAB>(out,p,opt,t_total);
1972 break;
1973 case SAT:
1974 runEngine<DFS>(out,p,opt,t_total);
1975 break;
1976 }
1977 }
1978
1979 void
1980 FlatZincSpace::constrain(const Space& s) {
1981 if (_optVarIsInt) {
1982 if (_method == MIN)
1983 rel(*this, iv[_optVar], IRT_LE,
1984 static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
1985 else if (_method == MAX)
1986 rel(*this, iv[_optVar], IRT_GR,
1987 static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
1988 } else {
1989#ifdef GECODE_HAS_FLOAT_VARS
1990 if (_method == MIN)
1991 rel(*this, fv[_optVar], FRT_LE,
1992 static_cast<const FlatZincSpace*>(&s)->fv[_optVar].val()-step);
1993 else if (_method == MAX)
1994 rel(*this, fv[_optVar], FRT_GR,
1995 static_cast<const FlatZincSpace*>(&s)->fv[_optVar].val()+step);
1996#endif
1997 }
1998 }
1999
2000 bool
2001 FlatZincSpace::slave(const MetaInfo& mi) {
2002 if ((mi.type() == MetaInfo::RESTART) && (mi.restart() != 0) &&
2003 (_lns > 0) && (mi.last()==nullptr) && (_lnsInitialSolution.size()>0)) {
2004 for (unsigned int i=iv_lns.size(); i--;) {
2005 if (_random(99U) <= _lns) {
2006 rel(*this, iv_lns[i], IRT_EQ, _lnsInitialSolution[i]);
2007 }
2008 }
2009 return false;
2010 } else if ((mi.type() == MetaInfo::RESTART) && (mi.restart() != 0) &&
2011 (_lns > 0) && mi.last()) {
2012 const FlatZincSpace& last =
2013 static_cast<const FlatZincSpace&>(*mi.last());
2014 for (unsigned int i=iv_lns.size(); i--;) {
2015 if (_random(99U) <= _lns) {
2016 rel(*this, iv_lns[i], IRT_EQ, last.iv_lns[i]);
2017 }
2018 }
2019 return false;
2020 }
2021 return true;
2022 }
2023
2024 Space*
2025 FlatZincSpace::copy(void) {
2026 return new FlatZincSpace(*this);
2027 }
2028
2029 FlatZincSpace::Meth
2030 FlatZincSpace::method(void) const {
2031 return _method;
2032 }
2033
2034 int
2035 FlatZincSpace::optVar(void) const {
2036 return _optVar;
2037 }
2038
2039 bool
2040 FlatZincSpace::optVarIsInt(void) const {
2041 return _optVarIsInt;
2042 }
2043
2044 void
2045 FlatZincSpace::print(std::ostream& out, const Printer& p) const {
2046 p.print(out, iv, bv
2047#ifdef GECODE_HAS_SET_VARS
2048 , sv
2049#endif
2050#ifdef GECODE_HAS_FLOAT_VARS
2051 , fv
2052#endif
2053 );
2054 }
2055
2056 void
2057 FlatZincSpace::compare(const Space& s, std::ostream& out) const {
2058 (void) s; (void) out;
2059#ifdef GECODE_HAS_GIST
2060 const FlatZincSpace& fs = dynamic_cast<const FlatZincSpace&>(s);
2061 for (int i = 0; i < iv.size(); ++i) {
2062 std::stringstream ss;
2063 ss << "iv[" << i << "]";
2064 std::string result(Gecode::Gist::Comparator::compare(ss.str(), iv[i],
2065 fs.iv[i]));
2066 if (result.length() > 0) out << result << std::endl;
2067 }
2068 for (int i = 0; i < bv.size(); ++i) {
2069 std::stringstream ss;
2070 ss << "bv[" << i << "]";
2071 std::string result(Gecode::Gist::Comparator::compare(ss.str(), bv[i],
2072 fs.bv[i]));
2073 if (result.length() > 0) out << result << std::endl;
2074 }
2075#ifdef GECODE_HAS_SET_VARS
2076 for (int i = 0; i < sv.size(); ++i) {
2077 std::stringstream ss;
2078 ss << "sv[" << i << "]";
2079 std::string result(Gecode::Gist::Comparator::compare(ss.str(), sv[i],
2080 fs.sv[i]));
2081 if (result.length() > 0) out << result << std::endl;
2082 }
2083#endif
2084#ifdef GECODE_HAS_FLOAT_VARS
2085 for (int i = 0; i < fv.size(); ++i) {
2086 std::stringstream ss;
2087 ss << "fv[" << i << "]";
2088 std::string result(Gecode::Gist::Comparator::compare(ss.str(), fv[i],
2089 fs.fv[i]));
2090 if (result.length() > 0) out << result << std::endl;
2091 }
2092#endif
2093#endif
2094 }
2095
2096 void
2097 FlatZincSpace::compare(const FlatZincSpace& s, std::ostream& out,
2098 const Printer& p) const {
2099 p.printDiff(out, iv, s.iv, bv, s.bv
2100#ifdef GECODE_HAS_SET_VARS
2101 , sv, s.sv
2102#endif
2103#ifdef GECODE_HAS_FLOAT_VARS
2104 , fv, s.fv
2105#endif
2106 );
2107 }
2108
2109 void
2110 FlatZincSpace::shrinkArrays(Printer& p) {
2111 p.shrinkArrays(*this, _optVar, _optVarIsInt, iv, bv
2112#ifdef GECODE_HAS_SET_VARS
2113 , sv
2114#endif
2115#ifdef GECODE_HAS_FLOAT_VARS
2116 , fv
2117#endif
2118 );
2119 }
2120
2121 IntArgs
2122 FlatZincSpace::arg2intargs(AST::Node* arg, int offset) {
2123 AST::Array* a = arg->getArray();
2124 IntArgs ia(a->a.size()+offset);
2125 for (int i=offset; i--;)
2126 ia[i] = 0;
2127 for (int i=a->a.size(); i--;)
2128 ia[i+offset] = a->a[i]->getInt();
2129 return ia;
2130 }
2131 TupleSet
2132 FlatZincSpace::arg2tupleset(const IntArgs& a, int noOfVars) {
2133 int noOfTuples = a.size() == 0 ? 0 : (a.size()/noOfVars);
2134
2135 // Build TupleSet
2136 TupleSet ts(noOfVars);
2137 for (int i=0; i<noOfTuples; i++) {
2138 IntArgs t(noOfVars);
2139 for (int j=0; j<noOfVars; j++) {
2140 t[j] = a[i*noOfVars+j];
2141 }
2142 ts.add(t);
2143 }
2144 ts.finalize();
2145
2146 if (_initData) {
2147 FlatZincSpaceInitData::TupleSetSet::iterator it = _initData->tupleSetSet.find(ts);
2148 if (it != _initData->tupleSetSet.end()) {
2149 return *it;
2150 }
2151 _initData->tupleSetSet.insert(ts);
2152 }
2153
2154
2155 return ts;
2156 }
2157 IntSharedArray
2158 FlatZincSpace::arg2intsharedarray(AST::Node* arg, int offset) {
2159 IntArgs ia(arg2intargs(arg,offset));
2160 SharedArray<int> sia(ia);
2161 if (_initData) {
2162 FlatZincSpaceInitData::IntSharedArraySet::iterator it = _initData->intSharedArraySet.find(sia);
2163 if (it != _initData->intSharedArraySet.end()) {
2164 return *it;
2165 }
2166 _initData->intSharedArraySet.insert(sia);
2167 }
2168
2169 return sia;
2170 }
2171 IntArgs
2172 FlatZincSpace::arg2boolargs(AST::Node* arg, int offset) {
2173 AST::Array* a = arg->getArray();
2174 IntArgs ia(a->a.size()+offset);
2175 for (int i=offset; i--;)
2176 ia[i] = 0;
2177 for (int i=a->a.size(); i--;)
2178 ia[i+offset] = a->a[i]->getBool();
2179 return ia;
2180 }
2181 IntSharedArray
2182 FlatZincSpace::arg2boolsharedarray(AST::Node* arg, int offset) {
2183 IntArgs ia(arg2boolargs(arg,offset));
2184 SharedArray<int> sia(ia);
2185 if (_initData) {
2186 FlatZincSpaceInitData::IntSharedArraySet::iterator it = _initData->intSharedArraySet.find(sia);
2187 if (it != _initData->intSharedArraySet.end()) {
2188 return *it;
2189 }
2190 _initData->intSharedArraySet.insert(sia);
2191 }
2192
2193 return sia;
2194 }
2195 IntSet
2196 FlatZincSpace::arg2intset(AST::Node* n) {
2197 AST::SetLit* sl = n->getSet();
2198 IntSet d;
2199 if (sl->interval) {
2200 d = IntSet(sl->min, sl->max);
2201 } else {
2202 Region re;
2203 int* is = re.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
2204 for (int i=sl->s.size(); i--; )
2205 is[i] = sl->s[i];
2206 d = IntSet(is, sl->s.size());
2207 }
2208 return d;
2209 }
2210 IntSetArgs
2211 FlatZincSpace::arg2intsetargs(AST::Node* arg, int offset) {
2212 AST::Array* a = arg->getArray();
2213 if (a->a.size() == 0) {
2214 IntSetArgs emptyIa(0);
2215 return emptyIa;
2216 }
2217 IntSetArgs ia(a->a.size()+offset);
2218 for (int i=offset; i--;)
2219 ia[i] = IntSet::empty;
2220 for (int i=a->a.size(); i--;) {
2221 ia[i+offset] = arg2intset(a->a[i]);
2222 }
2223 return ia;
2224 }
2225 IntVarArgs
2226 FlatZincSpace::arg2intvarargs(AST::Node* arg, int offset) {
2227 AST::Array* a = arg->getArray();
2228 if (a->a.size() == 0) {
2229 IntVarArgs emptyIa(0);
2230 return emptyIa;
2231 }
2232 IntVarArgs ia(a->a.size()+offset);
2233 for (int i=offset; i--;)
2234 ia[i] = IntVar(*this, 0, 0);
2235 for (int i=a->a.size(); i--;) {
2236 if (a->a[i]->isIntVar()) {
2237 ia[i+offset] = iv[a->a[i]->getIntVar()];
2238 } else {
2239 int value = a->a[i]->getInt();
2240 IntVar iv(*this, value, value);
2241 ia[i+offset] = iv;
2242 }
2243 }
2244 return ia;
2245 }
2246 BoolVarArgs
2247 FlatZincSpace::arg2boolvarargs(AST::Node* arg, int offset, int siv) {
2248 AST::Array* a = arg->getArray();
2249 if (a->a.size() == 0) {
2250 BoolVarArgs emptyIa(0);
2251 return emptyIa;
2252 }
2253 BoolVarArgs ia(a->a.size()+offset-(siv==-1?0:1));
2254 for (int i=offset; i--;)
2255 ia[i] = BoolVar(*this, 0, 0);
2256 for (int i=0; i<static_cast<int>(a->a.size()); i++) {
2257 if (i==siv)
2258 continue;
2259 if (a->a[i]->isBool()) {
2260 bool value = a->a[i]->getBool();
2261 BoolVar iv(*this, value, value);
2262 ia[offset++] = iv;
2263 } else if (a->a[i]->isIntVar() &&
2264 aliasBool2Int(a->a[i]->getIntVar()) != -1) {
2265 ia[offset++] = bv[aliasBool2Int(a->a[i]->getIntVar())];
2266 } else {
2267 ia[offset++] = bv[a->a[i]->getBoolVar()];
2268 }
2269 }
2270 return ia;
2271 }
2272 BoolVar
2273 FlatZincSpace::arg2BoolVar(AST::Node* n) {
2274 BoolVar x0;
2275 if (n->isBool()) {
2276 x0 = BoolVar(*this, n->getBool(), n->getBool());
2277 }
2278 else {
2279 x0 = bv[n->getBoolVar()];
2280 }
2281 return x0;
2282 }
2283 IntVar
2284 FlatZincSpace::arg2IntVar(AST::Node* n) {
2285 IntVar x0;
2286 if (n->isIntVar()) {
2287 x0 = iv[n->getIntVar()];
2288 } else {
2289 x0 = IntVar(*this, n->getInt(), n->getInt());
2290 }
2291 return x0;
2292 }
2293 bool
2294 FlatZincSpace::isBoolArray(AST::Node* b, int& singleInt) {
2295 AST::Array* a = b->getArray();
2296 singleInt = -1;
2297 if (a->a.size() == 0)
2298 return true;
2299 for (int i=a->a.size(); i--;) {
2300 if (a->a[i]->isBoolVar() || a->a[i]->isBool()) {
2301 } else if (a->a[i]->isIntVar()) {
2302 if (aliasBool2Int(a->a[i]->getIntVar()) == -1) {
2303 if (singleInt != -1) {
2304 return false;
2305 }
2306 singleInt = i;
2307 }
2308 } else {
2309 return false;
2310 }
2311 }
2312 return singleInt==-1 || a->a.size() > 1;
2313 }
2314#ifdef GECODE_HAS_SET_VARS
2315 SetVar
2316 FlatZincSpace::arg2SetVar(AST::Node* n) {
2317 SetVar x0;
2318 if (!n->isSetVar()) {
2319 IntSet d = arg2intset(n);
2320 x0 = SetVar(*this, d, d);
2321 } else {
2322 x0 = sv[n->getSetVar()];
2323 }
2324 return x0;
2325 }
2326 SetVarArgs
2327 FlatZincSpace::arg2setvarargs(AST::Node* arg, int offset, int doffset,
2328 const IntSet& od) {
2329 AST::Array* a = arg->getArray();
2330 SetVarArgs ia(a->a.size()+offset);
2331 for (int i=offset; i--;) {
2332 IntSet d = i<doffset ? od : IntSet::empty;
2333 ia[i] = SetVar(*this, d, d);
2334 }
2335 for (int i=a->a.size(); i--;) {
2336 ia[i+offset] = arg2SetVar(a->a[i]);
2337 }
2338 return ia;
2339 }
2340#endif
2341#ifdef GECODE_HAS_FLOAT_VARS
2342 FloatValArgs
2343 FlatZincSpace::arg2floatargs(AST::Node* arg, int offset) {
2344 AST::Array* a = arg->getArray();
2345 FloatValArgs fa(a->a.size()+offset);
2346 for (int i=offset; i--;)
2347 fa[i] = 0.0;
2348 for (int i=a->a.size(); i--;)
2349 fa[i+offset] = a->a[i]->getFloat();
2350 return fa;
2351 }
2352 FloatVarArgs
2353 FlatZincSpace::arg2floatvarargs(AST::Node* arg, int offset) {
2354 AST::Array* a = arg->getArray();
2355 if (a->a.size() == 0) {
2356 FloatVarArgs emptyFa(0);
2357 return emptyFa;
2358 }
2359 FloatVarArgs fa(a->a.size()+offset);
2360 for (int i=offset; i--;)
2361 fa[i] = FloatVar(*this, 0.0, 0.0);
2362 for (int i=a->a.size(); i--;) {
2363 if (a->a[i]->isFloatVar()) {
2364 fa[i+offset] = fv[a->a[i]->getFloatVar()];
2365 } else {
2366 double value = a->a[i]->getFloat();
2367 FloatVar fv(*this, value, value);
2368 fa[i+offset] = fv;
2369 }
2370 }
2371 return fa;
2372 }
2373 FloatVar
2374 FlatZincSpace::arg2FloatVar(AST::Node* n) {
2375 FloatVar x0;
2376 if (n->isFloatVar()) {
2377 x0 = fv[n->getFloatVar()];
2378 } else {
2379 x0 = FloatVar(*this, n->getFloat(), n->getFloat());
2380 }
2381 return x0;
2382 }
2383#endif
2384 IntPropLevel
2385 FlatZincSpace::ann2ipl(AST::Node* ann) {
2386 if (ann) {
2387 if (ann->hasAtom("val"))
2388 return IPL_VAL;
2389 if (ann->hasAtom("domain"))
2390 return IPL_DOM;
2391 if (ann->hasAtom("bounds") ||
2392 ann->hasAtom("boundsR") ||
2393 ann->hasAtom("boundsD") ||
2394 ann->hasAtom("boundsZ"))
2395 return IPL_BND;
2396 }
2397 return IPL_DEF;
2398 }
2399
2400 DFA
2401 FlatZincSpace::getSharedDFA(DFA& a) {
2402 if (_initData) {
2403 FlatZincSpaceInitData::DFASet::iterator it = _initData->dfaSet.find(a);
2404 if (it != _initData->dfaSet.end()) {
2405 return *it;
2406 }
2407 _initData->dfaSet.insert(a);
2408 }
2409 return a;
2410 }
2411
2412 void
2413 Printer::init(AST::Array* output) {
2414 _output = output;
2415 }
2416
2417 void
2418 Printer::printElem(std::ostream& out,
2419 AST::Node* ai,
2420 const Gecode::IntVarArray& iv,
2421 const Gecode::BoolVarArray& bv
2422#ifdef GECODE_HAS_SET_VARS
2423 , const Gecode::SetVarArray& sv
2424#endif
2425#ifdef GECODE_HAS_FLOAT_VARS
2426 ,
2427 const Gecode::FloatVarArray& fv
2428#endif
2429 ) const {
2430 int k;
2431 if (ai->isInt(k)) {
2432 out << k;
2433 } else if (ai->isIntVar()) {
2434 out << iv[ai->getIntVar()];
2435 } else if (ai->isBoolVar()) {
2436 if (bv[ai->getBoolVar()].min() == 1) {
2437 out << "true";
2438 } else if (bv[ai->getBoolVar()].max() == 0) {
2439 out << "false";
2440 } else {
2441 out << "false..true";
2442 }
2443#ifdef GECODE_HAS_SET_VARS
2444 } else if (ai->isSetVar()) {
2445 if (!sv[ai->getSetVar()].assigned()) {
2446 out << sv[ai->getSetVar()];
2447 return;
2448 }
2449 SetVarGlbRanges svr(sv[ai->getSetVar()]);
2450 if (!svr()) {
2451 out << "{}";
2452 return;
2453 }
2454 int min = svr.min();
2455 int max = svr.max();
2456 ++svr;
2457 if (svr()) {
2458 SetVarGlbValues svv(sv[ai->getSetVar()]);
2459 int i = svv.val();
2460 out << "{" << i;
2461 ++svv;
2462 for (; svv(); ++svv)
2463 out << ", " << svv.val();
2464 out << "}";
2465 } else {
2466 out << min << ".." << max;
2467 }
2468#endif
2469#ifdef GECODE_HAS_FLOAT_VARS
2470 } else if (ai->isFloatVar()) {
2471 if (fv[ai->getFloatVar()].assigned()) {
2472 FloatVal vv = fv[ai->getFloatVar()].val();
2473 FloatNum v;
2474 if (vv.singleton())
2475 v = vv.min();
2476 else if (vv < 0.0)
2477 v = vv.max();
2478 else
2479 v = vv.min();
2480 std::ostringstream oss;
2481 // oss << std::scientific;
2482 oss << std::setprecision(std::numeric_limits<double>::digits10);
2483 oss << v;
2484 if (oss.str().find(".") == std::string::npos)
2485 oss << ".0";
2486 out << oss.str();
2487 } else {
2488 out << fv[ai->getFloatVar()];
2489 }
2490#endif
2491 } else if (ai->isBool()) {
2492 out << (ai->getBool() ? "true" : "false");
2493 } else if (ai->isSet()) {
2494 AST::SetLit* s = ai->getSet();
2495 if (s->interval) {
2496 out << s->min << ".." << s->max;
2497 } else {
2498 out << "{";
2499 for (unsigned int i=0; i<s->s.size(); i++) {
2500 out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
2501 }
2502 }
2503 } else if (ai->isString()) {
2504 std::string s = ai->getString();
2505 for (unsigned int i=0; i<s.size(); i++) {
2506 if (s[i] == '\\' && i<s.size()-1) {
2507 switch (s[i+1]) {
2508 case 'n': out << "\n"; break;
2509 case '\\': out << "\\"; break;
2510 case 't': out << "\t"; break;
2511 default: out << "\\" << s[i+1];
2512 }
2513 i++;
2514 } else {
2515 out << s[i];
2516 }
2517 }
2518 }
2519 }
2520
2521 void
2522 Printer::printElemDiff(std::ostream& out,
2523 AST::Node* ai,
2524 const Gecode::IntVarArray& iv1,
2525 const Gecode::IntVarArray& iv2,
2526 const Gecode::BoolVarArray& bv1,
2527 const Gecode::BoolVarArray& bv2
2528#ifdef GECODE_HAS_SET_VARS
2529 , const Gecode::SetVarArray& sv1,
2530 const Gecode::SetVarArray& sv2
2531#endif
2532#ifdef GECODE_HAS_FLOAT_VARS
2533 , const Gecode::FloatVarArray& fv1,
2534 const Gecode::FloatVarArray& fv2
2535#endif
2536 ) const {
2537#ifdef GECODE_HAS_GIST
2538 using namespace Gecode::Gist;
2539 int k;
2540 if (ai->isInt(k)) {
2541 out << k;
2542 } else if (ai->isIntVar()) {
2543 std::string res(Comparator::compare("",iv1[ai->getIntVar()],
2544 iv2[ai->getIntVar()]));
2545 if (res.length() > 0) {
2546 res.erase(0, 1); // Remove '='
2547 out << res;
2548 } else {
2549 out << iv1[ai->getIntVar()];
2550 }
2551 } else if (ai->isBoolVar()) {
2552 std::string res(Comparator::compare("",bv1[ai->getBoolVar()],
2553 bv2[ai->getBoolVar()]));
2554 if (res.length() > 0) {
2555 res.erase(0, 1); // Remove '='
2556 out << res;
2557 } else {
2558 out << bv1[ai->getBoolVar()];
2559 }
2560#ifdef GECODE_HAS_SET_VARS
2561 } else if (ai->isSetVar()) {
2562 std::string res(Comparator::compare("",sv1[ai->getSetVar()],
2563 sv2[ai->getSetVar()]));
2564 if (res.length() > 0) {
2565 res.erase(0, 1); // Remove '='
2566 out << res;
2567 } else {
2568 out << sv1[ai->getSetVar()];
2569 }
2570#endif
2571#ifdef GECODE_HAS_FLOAT_VARS
2572 } else if (ai->isFloatVar()) {
2573 std::string res(Comparator::compare("",fv1[ai->getFloatVar()],
2574 fv2[ai->getFloatVar()]));
2575 if (res.length() > 0) {
2576 res.erase(0, 1); // Remove '='
2577 out << res;
2578 } else {
2579 out << fv1[ai->getFloatVar()];
2580 }
2581#endif
2582 } else if (ai->isBool()) {
2583 out << (ai->getBool() ? "true" : "false");
2584 } else if (ai->isSet()) {
2585 AST::SetLit* s = ai->getSet();
2586 if (s->interval) {
2587 out << s->min << ".." << s->max;
2588 } else {
2589 out << "{";
2590 for (unsigned int i=0; i<s->s.size(); i++) {
2591 out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
2592 }
2593 }
2594 } else if (ai->isString()) {
2595 std::string s = ai->getString();
2596 for (unsigned int i=0; i<s.size(); i++) {
2597 if (s[i] == '\\' && i<s.size()-1) {
2598 switch (s[i+1]) {
2599 case 'n': out << "\n"; break;
2600 case '\\': out << "\\"; break;
2601 case 't': out << "\t"; break;
2602 default: out << "\\" << s[i+1];
2603 }
2604 i++;
2605 } else {
2606 out << s[i];
2607 }
2608 }
2609 }
2610#else
2611 (void) out;
2612 (void) ai;
2613 (void) iv1;
2614 (void) iv2;
2615 (void) bv1;
2616 (void) bv2;
2617#ifdef GECODE_HAS_SET_VARS
2618 (void) sv1;
2619 (void) sv2;
2620#endif
2621#ifdef GECODE_HAS_FLOAT_VARS
2622 (void) fv1;
2623 (void) fv2;
2624#endif
2625
2626#endif
2627 }
2628
2629 void
2630 Printer::print(std::ostream& out,
2631 const Gecode::IntVarArray& iv,
2632 const Gecode::BoolVarArray& bv
2633#ifdef GECODE_HAS_SET_VARS
2634 ,
2635 const Gecode::SetVarArray& sv
2636#endif
2637#ifdef GECODE_HAS_FLOAT_VARS
2638 ,
2639 const Gecode::FloatVarArray& fv
2640#endif
2641 ) const {
2642 if (_output == nullptr)
2643 return;
2644 for (unsigned int i=0; i< _output->a.size(); i++) {
2645 AST::Node* ai = _output->a[i];
2646 if (ai->isArray()) {
2647 AST::Array* aia = ai->getArray();
2648 int size = aia->a.size();
2649 out << "[";
2650 for (int j=0; j<size; j++) {
2651 printElem(out,aia->a[j],iv,bv
2652#ifdef GECODE_HAS_SET_VARS
2653 ,sv
2654#endif
2655#ifdef GECODE_HAS_FLOAT_VARS
2656 ,fv
2657#endif
2658 );
2659 if (j<size-1)
2660 out << ", ";
2661 }
2662 out << "]";
2663 } else {
2664 printElem(out,ai,iv,bv
2665#ifdef GECODE_HAS_SET_VARS
2666 ,sv
2667#endif
2668#ifdef GECODE_HAS_FLOAT_VARS
2669 ,fv
2670#endif
2671 );
2672 }
2673 }
2674 }
2675
2676 void
2677 Printer::printDiff(std::ostream& out,
2678 const Gecode::IntVarArray& iv1,
2679 const Gecode::IntVarArray& iv2,
2680 const Gecode::BoolVarArray& bv1,
2681 const Gecode::BoolVarArray& bv2
2682#ifdef GECODE_HAS_SET_VARS
2683 ,
2684 const Gecode::SetVarArray& sv1,
2685 const Gecode::SetVarArray& sv2
2686#endif
2687#ifdef GECODE_HAS_FLOAT_VARS
2688 ,
2689 const Gecode::FloatVarArray& fv1,
2690 const Gecode::FloatVarArray& fv2
2691#endif
2692 ) const {
2693 if (_output == nullptr)
2694 return;
2695 for (unsigned int i=0; i< _output->a.size(); i++) {
2696 AST::Node* ai = _output->a[i];
2697 if (ai->isArray()) {
2698 AST::Array* aia = ai->getArray();
2699 int size = aia->a.size();
2700 out << "[";
2701 for (int j=0; j<size; j++) {
2702 printElemDiff(out,aia->a[j],iv1,iv2,bv1,bv2
2703#ifdef GECODE_HAS_SET_VARS
2704 ,sv1,sv2
2705#endif
2706#ifdef GECODE_HAS_FLOAT_VARS
2707 ,fv1,fv2
2708#endif
2709 );
2710 if (j<size-1)
2711 out << ", ";
2712 }
2713 out << "]";
2714 } else {
2715 printElemDiff(out,ai,iv1,iv2,bv1,bv2
2716#ifdef GECODE_HAS_SET_VARS
2717 ,sv1,sv2
2718#endif
2719#ifdef GECODE_HAS_FLOAT_VARS
2720 ,fv1,fv2
2721#endif
2722 );
2723 }
2724 }
2725 }
2726
2727 void
2728 Printer::addIntVarName(const std::string& n) {
2729 iv_names.push_back(n);
2730 }
2731 void
2732 Printer::addBoolVarName(const std::string& n) {
2733 bv_names.push_back(n);
2734 }
2735#ifdef GECODE_HAS_FLOAT_VARS
2736 void
2737 Printer::addFloatVarName(const std::string& n) {
2738 fv_names.push_back(n);
2739 }
2740#endif
2741#ifdef GECODE_HAS_SET_VARS
2742 void
2743 Printer::addSetVarName(const std::string& n) {
2744 sv_names.push_back(n);
2745 }
2746#endif
2747
2748 void
2749 Printer::shrinkElement(AST::Node* node,
2750 std::map<int,int>& iv, std::map<int,int>& bv,
2751 std::map<int,int>& sv, std::map<int,int>& fv) {
2752 if (node->isIntVar()) {
2753 AST::IntVar* x = static_cast<AST::IntVar*>(node);
2754 if (iv.find(x->i) == iv.end()) {
2755 int newi = iv.size();
2756 iv[x->i] = newi;
2757 }
2758 x->i = iv[x->i];
2759 } else if (node->isBoolVar()) {
2760 AST::BoolVar* x = static_cast<AST::BoolVar*>(node);
2761 if (bv.find(x->i) == bv.end()) {
2762 int newi = bv.size();
2763 bv[x->i] = newi;
2764 }
2765 x->i = bv[x->i];
2766 } else if (node->isSetVar()) {
2767 AST::SetVar* x = static_cast<AST::SetVar*>(node);
2768 if (sv.find(x->i) == sv.end()) {
2769 int newi = sv.size();
2770 sv[x->i] = newi;
2771 }
2772 x->i = sv[x->i];
2773 } else if (node->isFloatVar()) {
2774 AST::FloatVar* x = static_cast<AST::FloatVar*>(node);
2775 if (fv.find(x->i) == fv.end()) {
2776 int newi = fv.size();
2777 fv[x->i] = newi;
2778 }
2779 x->i = fv[x->i];
2780 }
2781 }
2782
2783 void
2784 Printer::shrinkArrays(Space& home,
2785 int& optVar, bool optVarIsInt,
2786 Gecode::IntVarArray& iv,
2787 Gecode::BoolVarArray& bv
2788#ifdef GECODE_HAS_SET_VARS
2789 ,
2790 Gecode::SetVarArray& sv
2791#endif
2792#ifdef GECODE_HAS_FLOAT_VARS
2793 ,
2794 Gecode::FloatVarArray& fv
2795#endif
2796 ) {
2797 if (_output == nullptr) {
2798 if (optVarIsInt && optVar != -1) {
2799 IntVar ov = iv[optVar];
2800 iv = IntVarArray(home, 1);
2801 iv[0] = ov;
2802 optVar = 0;
2803 } else {
2804 iv = IntVarArray(home, 0);
2805 }
2806 bv = BoolVarArray(home, 0);
2807#ifdef GECODE_HAS_SET_VARS
2808 sv = SetVarArray(home, 0);
2809#endif
2810#ifdef GECODE_HAS_FLOAT_VARS
2811 if (!optVarIsInt && optVar != -1) {
2812 FloatVar ov = fv[optVar];
2813 fv = FloatVarArray(home, 1);
2814 fv[0] = ov;
2815 optVar = 0;
2816 } else {
2817 fv = FloatVarArray(home,0);
2818 }
2819#endif
2820 return;
2821 }
2822 std::map<int,int> iv_new;
2823 std::map<int,int> bv_new;
2824 std::map<int,int> sv_new;
2825 std::map<int,int> fv_new;
2826
2827 if (optVar != -1) {
2828 if (optVarIsInt)
2829 iv_new[optVar] = 0;
2830 else
2831 fv_new[optVar] = 0;
2832 optVar = 0;
2833 }
2834
2835 for (unsigned int i=0; i< _output->a.size(); i++) {
2836 AST::Node* ai = _output->a[i];
2837 if (ai->isArray()) {
2838 AST::Array* aia = ai->getArray();
2839 for (unsigned int j=0; j<aia->a.size(); j++) {
2840 shrinkElement(aia->a[j],iv_new,bv_new,sv_new,fv_new);
2841 }
2842 } else {
2843 shrinkElement(ai,iv_new,bv_new,sv_new,fv_new);
2844 }
2845 }
2846
2847 IntVarArgs iva(iv_new.size());
2848 std::vector<std::string> iv_names_new(iv_new.size());
2849 for (std::map<int,int>::iterator i=iv_new.begin(); i != iv_new.end(); ++i) {
2850 iva[(*i).second] = iv[(*i).first];
2851 iv_names_new[(*i).second] = iv_names[(*i).first];
2852 }
2853 iv = IntVarArray(home, iva);
2854 iv_names = iv_names_new;
2855
2856 BoolVarArgs bva(bv_new.size());
2857 std::vector<std::string> bv_names_new(bv_new.size());
2858 for (std::map<int,int>::iterator i=bv_new.begin(); i != bv_new.end(); ++i) {
2859 bva[(*i).second] = bv[(*i).first];
2860 bv_names_new[(*i).second] = bv_names[(*i).first];
2861 }
2862 bv = BoolVarArray(home, bva);
2863 bv_names = bv_names_new;
2864
2865#ifdef GECODE_HAS_SET_VARS
2866 SetVarArgs sva(sv_new.size());
2867 std::vector<std::string> sv_names_new(sv_new.size());
2868 for (std::map<int,int>::iterator i=sv_new.begin(); i != sv_new.end(); ++i) {
2869 sva[(*i).second] = sv[(*i).first];
2870 sv_names_new[(*i).second] = sv_names[(*i).first];
2871 }
2872 sv = SetVarArray(home, sva);
2873 sv_names = sv_names_new;
2874#endif
2875
2876#ifdef GECODE_HAS_FLOAT_VARS
2877 FloatVarArgs fva(fv_new.size());
2878 std::vector<std::string> fv_names_new(fv_new.size());
2879 for (std::map<int,int>::iterator i=fv_new.begin(); i != fv_new.end(); ++i) {
2880 fva[(*i).second] = fv[(*i).first];
2881 fv_names_new[(*i).second] = fv_names[(*i).first];
2882 }
2883 fv = FloatVarArray(home, fva);
2884 fv_names = fv_names_new;
2885#endif
2886 }
2887
2888 Printer::~Printer(void) {
2889 delete _output;
2890 }
2891
2892}}
2893
2894// STATISTICS: flatzinc-any