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