Generated on Thu Apr 11 13:58:54 2019 for Gecode by doxygen 1.6.3

flatzinc.cpp

Go to the documentation of this file.
00001 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
00002 /*
00003  *  Main authors:
00004  *     Guido Tack <tack@gecode.org>
00005  *
00006  *  Contributing authors:
00007  *     Gabriel Hjort Blindell <gabriel.hjort.blindell@gmail.com>
00008  *
00009  *  Copyright:
00010  *     Guido Tack, 2007-2012
00011  *     Gabriel Hjort Blindell, 2012
00012  *
00013  *  This file is part of Gecode, the generic constraint
00014  *  development environment:
00015  *     http://www.gecode.org
00016  *
00017  *  Permission is hereby granted, free of charge, to any person obtaining
00018  *  a copy of this software and associated documentation files (the
00019  *  "Software"), to deal in the Software without restriction, including
00020  *  without limitation the rights to use, copy, modify, merge, publish,
00021  *  distribute, sublicense, and/or sell copies of the Software, and to
00022  *  permit persons to whom the Software is furnished to do so, subject to
00023  *  the following conditions:
00024  *
00025  *  The above copyright notice and this permission notice shall be
00026  *  included in all copies or substantial portions of the Software.
00027  *
00028  *  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
00029  *  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
00030  *  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00031  *  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
00032  *  LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
00033  *  OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
00034  *  WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
00035  *
00036  */
00037 
00038 #include <gecode/flatzinc.hh>
00039 #include <gecode/flatzinc/registry.hh>
00040 #include <gecode/flatzinc/plugin.hh>
00041 #include <gecode/flatzinc/branch.hh>
00042 
00043 #include <gecode/search.hh>
00044 
00045 #include <vector>
00046 #include <string>
00047 #include <sstream>
00048 #include <limits>
00049 #include <unordered_set>
00050 
00051 
00052 namespace std {
00053 
00055   template<> struct hash<Gecode::TupleSet> {
00057     forceinline size_t
00058     operator()(const Gecode::TupleSet& x) const {
00059       return x.hash();
00060     }
00061   };
00062 
00064   template<> struct hash<Gecode::SharedArray<int> > {
00066     forceinline size_t
00067     operator()(const Gecode::SharedArray<int>& x) const {
00068       size_t seed = static_cast<size_t>(x.size());
00069       for (int i=x.size(); i--; )
00070         Gecode::cmb_hash(seed, x[i]);
00071       return seed;
00072     }
00073   };
00074 
00076   template<> struct hash<Gecode::DFA> {
00078     forceinline size_t operator()(const Gecode::DFA& d) const {
00079       return d.hash();
00080     }
00081   };
00082 
00083 }
00084 
00085 namespace Gecode { namespace FlatZinc {
00086 
00087   // Default random number generator
00088   Rnd defrnd(0);
00089 
00102   class AuxVarBrancher : public Brancher {
00103   protected:
00105     bool done;
00107     AuxVarBrancher(Home home, TieBreak<IntVarBranch> int_varsel0,
00108                    IntValBranch int_valsel0,
00109                    TieBreak<BoolVarBranch> bool_varsel0,
00110                    BoolValBranch bool_valsel0
00111 #ifdef GECODE_HAS_SET_VARS
00112                    ,
00113                    SetVarBranch set_varsel0,
00114                    SetValBranch set_valsel0
00115 #endif
00116 #ifdef GECODE_HAS_FLOAT_VARS
00117                    ,
00118                    TieBreak<FloatVarBranch> float_varsel0,
00119                    FloatValBranch float_valsel0
00120 #endif
00121                    )
00122       : Brancher(home), done(false),
00123         int_varsel(int_varsel0), int_valsel(int_valsel0),
00124         bool_varsel(bool_varsel0), bool_valsel(bool_valsel0)
00125 #ifdef GECODE_HAS_SET_VARS
00126         , set_varsel(set_varsel0), set_valsel(set_valsel0)
00127 #endif
00128 #ifdef GECODE_HAS_FLOAT_VARS
00129         , float_varsel(float_varsel0), float_valsel(float_valsel0)
00130 #endif
00131         {}
00133     AuxVarBrancher(Space& home, AuxVarBrancher& b)
00134       : Brancher(home, b), done(b.done) {}
00135 
00137     class Choice : public Gecode::Choice {
00138     public:
00140       bool fail;
00142       Choice(const Brancher& b, bool fail0)
00143         : Gecode::Choice(b,1), fail(fail0) {}
00145       virtual size_t size(void) const {
00146         return sizeof(Choice);
00147       }
00149       virtual void archive(Archive& e) const {
00150         Gecode::Choice::archive(e);
00151         e.put(fail);
00152       }
00153     };
00154 
00155     TieBreak<IntVarBranch> int_varsel;
00156     IntValBranch int_valsel;
00157     TieBreak<BoolVarBranch> bool_varsel;
00158     BoolValBranch bool_valsel;
00159 #ifdef GECODE_HAS_SET_VARS
00160     SetVarBranch set_varsel;
00161     SetValBranch set_valsel;
00162 #endif
00163 #ifdef GECODE_HAS_FLOAT_VARS
00164     TieBreak<FloatVarBranch> float_varsel;
00165     FloatValBranch float_valsel;
00166 #endif
00167 
00168   public:
00170     virtual bool status(const Space& _home) const {
00171       if (done) return false;
00172       const FlatZincSpace& home = static_cast<const FlatZincSpace&>(_home);
00173       for (int i=0; i<home.iv_aux.size(); i++)
00174         if (!home.iv_aux[i].assigned()) return true;
00175       for (int i=0; i<home.bv_aux.size(); i++)
00176         if (!home.bv_aux[i].assigned()) return true;
00177 #ifdef GECODE_HAS_SET_VARS
00178       for (int i=0; i<home.sv_aux.size(); i++)
00179         if (!home.sv_aux[i].assigned()) return true;
00180 #endif
00181 #ifdef GECODE_HAS_FLOAT_VARS
00182       for (int i=0; i<home.fv_aux.size(); i++)
00183         if (!home.fv_aux[i].assigned()) return true;
00184 #endif
00185       // No non-assigned variables left
00186       return false;
00187     }
00189     virtual Choice* choice(Space& home) {
00190       done = true;
00191       FlatZincSpace& fzs = static_cast<FlatZincSpace&>(*home.clone());
00192       fzs.needAuxVars = false;
00193       branch(fzs,fzs.iv_aux,int_varsel,int_valsel);
00194       branch(fzs,fzs.bv_aux,bool_varsel,bool_valsel);
00195 #ifdef GECODE_HAS_SET_VARS
00196       branch(fzs,fzs.sv_aux,set_varsel,set_valsel);
00197 #endif
00198 #ifdef GECODE_HAS_FLOAT_VARS
00199       branch(fzs,fzs.fv_aux,float_varsel,float_valsel);
00200 #endif
00201       Search::Options opt; opt.clone = false;
00202       FlatZincSpace* sol = dfs(&fzs, opt);
00203       if (sol) {
00204         delete sol;
00205         return new Choice(*this,false);
00206       } else {
00207         return new Choice(*this,true);
00208       }
00209     }
00211     virtual Choice* choice(const Space&, Archive& e) {
00212       bool fail; e >> fail;
00213       return new Choice(*this, fail);
00214     }
00216     virtual ExecStatus commit(Space&, const Gecode::Choice& c, unsigned int) {
00217       return static_cast<const Choice&>(c).fail ? ES_FAILED : ES_OK;
00218     }
00220     virtual void print(const Space&, const Gecode::Choice& c,
00221                        unsigned int,
00222                        std::ostream& o) const {
00223       o << "FlatZinc("
00224         << (static_cast<const Choice&>(c).fail ? "fail" : "ok")
00225         << ")";
00226     }
00228     virtual Actor* copy(Space& home) {
00229       return new (home) AuxVarBrancher(home, *this);
00230     }
00232     static void post(Home home,
00233                      TieBreak<IntVarBranch> int_varsel,
00234                      IntValBranch int_valsel,
00235                      TieBreak<BoolVarBranch> bool_varsel,
00236                      BoolValBranch bool_valsel
00237 #ifdef GECODE_HAS_SET_VARS
00238                      ,
00239                      SetVarBranch set_varsel,
00240                      SetValBranch set_valsel
00241 #endif
00242 #ifdef GECODE_HAS_FLOAT_VARS
00243                      ,
00244                      TieBreak<FloatVarBranch> float_varsel,
00245                      FloatValBranch float_valsel
00246 #endif
00247                    ) {
00248       (void) new (home) AuxVarBrancher(home, int_varsel, int_valsel,
00249                                        bool_varsel, bool_valsel
00250 #ifdef GECODE_HAS_SET_VARS
00251                                        , set_varsel, set_valsel
00252 #endif
00253 #ifdef GECODE_HAS_FLOAT_VARS
00254                                        , float_varsel, float_valsel
00255 #endif
00256                                        );
00257     }
00259     virtual size_t dispose(Space&) {
00260       return sizeof(*this);
00261     }
00262   };
00263 
00264   class BranchInformationO : public SharedHandle::Object {
00265   private:
00266     struct BI {
00267       std::string r0;
00268       std::string r1;
00269       std::vector<std::string> n;
00270       BI(void) : r0(""), r1(""), n(0) {}
00271       BI(const std::string& r00, const std::string& r10,
00272          const std::vector<std::string>& n0)
00273         : r0(r00), r1(r10), n(n0) {}
00274     };
00275     std::vector<BI> v;
00276     BranchInformationO(std::vector<BI> v0) : v(v0) {}
00277   public:
00278     BranchInformationO(void) {}
00279     virtual ~BranchInformationO(void) {}
00280     virtual SharedHandle::Object* copy(void) const {
00281       return new BranchInformationO(v);
00282     }
00284     void add(BrancherGroup bg,
00285              const std::string& rel0,
00286              const std::string& rel1,
00287              const std::vector<std::string>& n) {
00288       v.resize(std::max(static_cast<unsigned int>(v.size()),bg.id()+1));
00289       v[bg.id()] = BI(rel0,rel1,n);
00290     }
00292     void print(const Brancher& b,
00293                unsigned int a, int i, int n, std::ostream& o) const {
00294       const BI& bi = v[b.group().id()];
00295       o << bi.n[i] << " " << (a==0 ? bi.r0 : bi.r1) << " " << n;
00296     }
00297 #ifdef GECODE_HAS_FLOAT_VARS
00298     void print(const Brancher& b,
00299                unsigned int a, int i, const FloatNumBranch& nl,
00300                std::ostream& o) const {
00301       const BI& bi = v[b.group().id()];
00302       o << bi.n[i] << " "
00303         << (((a == 0) == nl.l) ? "<=" : ">=") << nl.n;
00304     }
00305 #endif
00306   };
00307 
00308   BranchInformation::BranchInformation(void)
00309     : SharedHandle(NULL) {}
00310 
00311   BranchInformation::BranchInformation(const BranchInformation& bi)
00312     : SharedHandle(bi) {}
00313 
00314   void
00315   BranchInformation::init(void) {
00316     assert(object() == NULL);
00317     object(new BranchInformationO());
00318   }
00319 
00320   void
00321   BranchInformation::add(BrancherGroup bg,
00322                          const std::string& rel0,
00323                          const std::string& rel1,
00324                          const std::vector<std::string>& n) {
00325     static_cast<BranchInformationO*>(object())->add(bg,rel0,rel1,n);
00326   }
00327   void
00328   BranchInformation::print(const Brancher& b, unsigned int a, int i,
00329                            int n, std::ostream& o) const {
00330     static_cast<const BranchInformationO*>(object())->print(b,a,i,n,o);
00331   }
00332 #ifdef GECODE_HAS_FLOAT_VARS
00333   void
00334   BranchInformation::print(const Brancher& b, unsigned int a, int i,
00335                            const FloatNumBranch& nl, std::ostream& o) const {
00336     static_cast<const BranchInformationO*>(object())->print(b,a,i,nl,o);
00337   }
00338 #endif
00339   template<class Var>
00340   void varValPrint(const Space &home, const Brancher& b,
00341                    unsigned int a,
00342                    Var, int i, const int& n,
00343                    std::ostream& o) {
00344     static_cast<const FlatZincSpace&>(home).branchInfo.print(b,a,i,n,o);
00345   }
00346 
00347 #ifdef GECODE_HAS_FLOAT_VARS
00348   void varValPrintF(const Space &home, const Brancher& b,
00349                     unsigned int a,
00350                     FloatVar, int i, const FloatNumBranch& nl,
00351                     std::ostream& o) {
00352     static_cast<const FlatZincSpace&>(home).branchInfo.print(b,a,i,nl,o);
00353   }
00354 #endif
00355 
00356   IntSet vs2is(IntVarSpec* vs) {
00357     if (vs->assigned) {
00358       return IntSet(vs->i,vs->i);
00359     }
00360     if (vs->domain()) {
00361       AST::SetLit* sl = vs->domain.some();
00362       if (sl->interval) {
00363         return IntSet(sl->min, sl->max);
00364       } else {
00365         int* newdom = heap.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
00366         for (int i=sl->s.size(); i--;)
00367           newdom[i] = sl->s[i];
00368         IntSet ret(newdom, sl->s.size());
00369         heap.free(newdom, static_cast<unsigned long int>(sl->s.size()));
00370         return ret;
00371       }
00372     }
00373     return IntSet(Int::Limits::min, Int::Limits::max);
00374   }
00375 
00376   int vs2bsl(BoolVarSpec* bs) {
00377     if (bs->assigned) {
00378       return bs->i;
00379     }
00380     if (bs->domain()) {
00381       AST::SetLit* sl = bs->domain.some();
00382       assert(sl->interval);
00383       return std::min(1, std::max(0, sl->min));
00384     }
00385     return 0;
00386   }
00387 
00388   int vs2bsh(BoolVarSpec* bs) {
00389     if (bs->assigned) {
00390       return bs->i;
00391     }
00392     if (bs->domain()) {
00393       AST::SetLit* sl = bs->domain.some();
00394       assert(sl->interval);
00395       return std::max(0, std::min(1, sl->max));
00396     }
00397     return 1;
00398   }
00399 
00400   TieBreak<IntVarBranch> ann2ivarsel(AST::Node* ann, Rnd rnd, double decay) {
00401     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00402       if (s->id == "input_order")
00403         return TieBreak<IntVarBranch>(INT_VAR_NONE());
00404       if (s->id == "first_fail")
00405         return TieBreak<IntVarBranch>(INT_VAR_SIZE_MIN());
00406       if (s->id == "anti_first_fail")
00407         return TieBreak<IntVarBranch>(INT_VAR_SIZE_MAX());
00408       if (s->id == "smallest")
00409         return TieBreak<IntVarBranch>(INT_VAR_MIN_MIN());
00410       if (s->id == "largest")
00411         return TieBreak<IntVarBranch>(INT_VAR_MAX_MAX());
00412       if (s->id == "occurrence")
00413         return TieBreak<IntVarBranch>(INT_VAR_DEGREE_MAX());
00414       if (s->id == "max_regret")
00415         return TieBreak<IntVarBranch>(INT_VAR_REGRET_MIN_MAX());
00416       if (s->id == "most_constrained")
00417         return TieBreak<IntVarBranch>(INT_VAR_SIZE_MIN(),
00418                                       INT_VAR_DEGREE_MAX());
00419       if (s->id == "random") {
00420         return TieBreak<IntVarBranch>(INT_VAR_RND(rnd));
00421       }
00422       if (s->id == "dom_w_deg") {
00423         return TieBreak<IntVarBranch>(INT_VAR_AFC_SIZE_MAX(decay));
00424       }
00425       if (s->id == "afc_min")
00426         return TieBreak<IntVarBranch>(INT_VAR_AFC_MIN(decay));
00427       if (s->id == "afc_max")
00428         return TieBreak<IntVarBranch>(INT_VAR_AFC_MAX(decay));
00429       if (s->id == "afc_size_min")
00430         return TieBreak<IntVarBranch>(INT_VAR_AFC_SIZE_MIN(decay));
00431       if (s->id == "afc_size_max") {
00432         return TieBreak<IntVarBranch>(INT_VAR_AFC_SIZE_MAX(decay));
00433       }
00434       if (s->id == "action_min")
00435         return TieBreak<IntVarBranch>(INT_VAR_ACTION_MIN(decay));
00436       if (s->id == "action_max")
00437         return TieBreak<IntVarBranch>(INT_VAR_ACTION_MAX(decay));
00438       if (s->id == "action_size_min")
00439         return TieBreak<IntVarBranch>(INT_VAR_ACTION_SIZE_MIN(decay));
00440       if (s->id == "action_size_max")
00441         return TieBreak<IntVarBranch>(INT_VAR_ACTION_SIZE_MAX(decay));
00442     }
00443     std::cerr << "Warning, ignored search annotation: ";
00444     ann->print(std::cerr);
00445     std::cerr << std::endl;
00446     return TieBreak<IntVarBranch>(INT_VAR_NONE());
00447   }
00448 
00449   IntValBranch ann2ivalsel(AST::Node* ann, std::string& r0, std::string& r1,
00450                            Rnd rnd) {
00451     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00452       if (s->id == "indomain_min") {
00453         r0 = "="; r1 = "!=";
00454         return INT_VAL_MIN();
00455       }
00456       if (s->id == "indomain_max") {
00457         r0 = "="; r1 = "!=";
00458         return INT_VAL_MAX();
00459       }
00460       if (s->id == "indomain_median") {
00461         r0 = "="; r1 = "!=";
00462         return INT_VAL_MED();
00463       }
00464       if (s->id == "indomain_split") {
00465         r0 = "<="; r1 = ">";
00466         return INT_VAL_SPLIT_MIN();
00467       }
00468       if (s->id == "indomain_reverse_split") {
00469         r0 = ">"; r1 = "<=";
00470         return INT_VAL_SPLIT_MAX();
00471       }
00472       if (s->id == "indomain_random") {
00473         r0 = "="; r1 = "!=";
00474         return INT_VAL_RND(rnd);
00475       }
00476       if (s->id == "indomain") {
00477         r0 = "="; r1 = "=";
00478         return INT_VALUES_MIN();
00479       }
00480       if (s->id == "indomain_middle") {
00481         std::cerr << "Warning, replacing unsupported annotation "
00482                   << "indomain_middle with indomain_median" << std::endl;
00483         r0 = "="; r1 = "!=";
00484         return INT_VAL_MED();
00485       }
00486       if (s->id == "indomain_interval") {
00487         std::cerr << "Warning, replacing unsupported annotation "
00488                   << "indomain_interval with indomain_split" << std::endl;
00489         r0 = "<="; r1 = ">";
00490         return INT_VAL_SPLIT_MIN();
00491       }
00492     }
00493     std::cerr << "Warning, ignored search annotation: ";
00494     ann->print(std::cerr);
00495     std::cerr << std::endl;
00496     r0 = "="; r1 = "!=";
00497     return INT_VAL_MIN();
00498   }
00499 
00500   IntAssign ann2asnivalsel(AST::Node* ann, Rnd rnd) {
00501     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00502       if (s->id == "indomain_min")
00503         return INT_ASSIGN_MIN();
00504       if (s->id == "indomain_max")
00505         return INT_ASSIGN_MAX();
00506       if (s->id == "indomain_median")
00507         return INT_ASSIGN_MED();
00508       if (s->id == "indomain_random") {
00509         return INT_ASSIGN_RND(rnd);
00510       }
00511     }
00512     std::cerr << "Warning, ignored search annotation: ";
00513     ann->print(std::cerr);
00514     std::cerr << std::endl;
00515     return INT_ASSIGN_MIN();
00516   }
00517 
00518   TieBreak<BoolVarBranch> ann2bvarsel(AST::Node* ann, Rnd rnd, double decay) {
00519     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00520       if ((s->id == "input_order") ||
00521           (s->id == "first_fail") ||
00522           (s->id == "anti_first_fail") ||
00523           (s->id == "smallest") ||
00524           (s->id == "largest") ||
00525           (s->id == "max_regret"))
00526        return TieBreak<BoolVarBranch>(BOOL_VAR_NONE());
00527       if ((s->id == "occurrence") ||
00528           (s->id == "most_constrained"))
00529         return TieBreak<BoolVarBranch>(BOOL_VAR_DEGREE_MAX());
00530       if (s->id == "random")
00531         return TieBreak<BoolVarBranch>(BOOL_VAR_RND(rnd));
00532       if ((s->id == "afc_min") ||
00533           (s->id == "afc_size_min"))
00534         return TieBreak<BoolVarBranch>(BOOL_VAR_AFC_MIN(decay));
00535       if ((s->id == "afc_max") ||
00536           (s->id == "afc_size_max") ||
00537           (s->id == "dom_w_deg"))
00538         return TieBreak<BoolVarBranch>(BOOL_VAR_AFC_MAX(decay));
00539       if ((s->id == "action_min") &&
00540           (s->id == "action_size_min"))
00541         return TieBreak<BoolVarBranch>(BOOL_VAR_ACTION_MIN(decay));
00542       if ((s->id == "action_max") ||
00543           (s->id == "action_size_max"))
00544         return TieBreak<BoolVarBranch>(BOOL_VAR_ACTION_MAX(decay));
00545     }
00546     std::cerr << "Warning, ignored search annotation: ";
00547     ann->print(std::cerr);
00548     std::cerr << std::endl;
00549     return TieBreak<BoolVarBranch>(BOOL_VAR_NONE());
00550   }
00551 
00552   BoolValBranch ann2bvalsel(AST::Node* ann, std::string& r0, std::string& r1,
00553                            Rnd rnd) {
00554     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00555       if (s->id == "indomain_min") {
00556         r0 = "="; r1 = "!=";
00557         return BOOL_VAL_MIN();
00558       }
00559       if (s->id == "indomain_max") {
00560         r0 = "="; r1 = "!=";
00561         return BOOL_VAL_MAX();
00562       }
00563       if (s->id == "indomain_median") {
00564         r0 = "="; r1 = "!=";
00565         return BOOL_VAL_MIN();
00566       }
00567       if (s->id == "indomain_split") {
00568         r0 = "<="; r1 = ">";
00569         return BOOL_VAL_MIN();
00570       }
00571       if (s->id == "indomain_reverse_split") {
00572         r0 = ">"; r1 = "<=";
00573         return BOOL_VAL_MAX();
00574       }
00575       if (s->id == "indomain_random") {
00576         r0 = "="; r1 = "!=";
00577         return BOOL_VAL_RND(rnd);
00578       }
00579       if (s->id == "indomain") {
00580         r0 = "="; r1 = "=";
00581         return BOOL_VAL_MIN();
00582       }
00583       if (s->id == "indomain_middle") {
00584         std::cerr << "Warning, replacing unsupported annotation "
00585                   << "indomain_middle with indomain_median" << std::endl;
00586         r0 = "="; r1 = "!=";
00587         return BOOL_VAL_MIN();
00588       }
00589       if (s->id == "indomain_interval") {
00590         std::cerr << "Warning, replacing unsupported annotation "
00591                   << "indomain_interval with indomain_split" << std::endl;
00592         r0 = "<="; r1 = ">";
00593         return BOOL_VAL_MIN();
00594       }
00595     }
00596     std::cerr << "Warning, ignored search annotation: ";
00597     ann->print(std::cerr);
00598     std::cerr << std::endl;
00599     r0 = "="; r1 = "!=";
00600     return BOOL_VAL_MIN();
00601   }
00602 
00603   BoolAssign ann2asnbvalsel(AST::Node* ann, Rnd rnd) {
00604     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00605       if ((s->id == "indomain_min") ||
00606           (s->id == "indomain_median"))
00607         return BOOL_ASSIGN_MIN();
00608       if (s->id == "indomain_max")
00609         return BOOL_ASSIGN_MAX();
00610       if (s->id == "indomain_random") {
00611         return BOOL_ASSIGN_RND(rnd);
00612       }
00613     }
00614     std::cerr << "Warning, ignored search annotation: ";
00615     ann->print(std::cerr);
00616     std::cerr << std::endl;
00617     return BOOL_ASSIGN_MIN();
00618   }
00619 
00620 #ifdef GECODE_HAS_SET_VARS
00621   SetVarBranch ann2svarsel(AST::Node* ann, Rnd rnd, double decay) {
00622     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00623       if (s->id == "input_order")
00624         return SET_VAR_NONE();
00625       if (s->id == "first_fail")
00626         return SET_VAR_SIZE_MIN();
00627       if (s->id == "anti_first_fail")
00628         return SET_VAR_SIZE_MAX();
00629       if (s->id == "smallest")
00630         return SET_VAR_MIN_MIN();
00631       if (s->id == "largest")
00632         return SET_VAR_MAX_MAX();
00633       if (s->id == "afc_min")
00634         return SET_VAR_AFC_MIN(decay);
00635       if (s->id == "afc_max")
00636         return SET_VAR_AFC_MAX(decay);
00637       if (s->id == "afc_size_min")
00638         return SET_VAR_AFC_SIZE_MIN(decay);
00639       if (s->id == "afc_size_max")
00640         return SET_VAR_AFC_SIZE_MAX(decay);
00641       if (s->id == "action_min")
00642         return SET_VAR_ACTION_MIN(decay);
00643       if (s->id == "action_max")
00644         return SET_VAR_ACTION_MAX(decay);
00645       if (s->id == "action_size_min")
00646         return SET_VAR_ACTION_SIZE_MIN(decay);
00647       if (s->id == "action_size_max")
00648         return SET_VAR_ACTION_SIZE_MAX(decay);
00649       if (s->id == "random") {
00650         return SET_VAR_RND(rnd);
00651       }
00652     }
00653     std::cerr << "Warning, ignored search annotation: ";
00654     ann->print(std::cerr);
00655     std::cerr << std::endl;
00656     return SET_VAR_NONE();
00657   }
00658 
00659   SetValBranch ann2svalsel(AST::Node* ann, std::string r0, std::string r1,
00660                            Rnd rnd) {
00661     (void) rnd;
00662     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00663       if (s->id == "indomain_min") {
00664         r0 = "in"; r1 = "not in";
00665         return SET_VAL_MIN_INC();
00666       }
00667       if (s->id == "indomain_max") {
00668         r0 = "in"; r1 = "not in";
00669         return SET_VAL_MAX_INC();
00670       }
00671       if (s->id == "outdomain_min") {
00672         r1 = "in"; r0 = "not in";
00673         return SET_VAL_MIN_EXC();
00674       }
00675       if (s->id == "outdomain_max") {
00676         r1 = "in"; r0 = "not in";
00677         return SET_VAL_MAX_EXC();
00678       }
00679     }
00680     std::cerr << "Warning, ignored search annotation: ";
00681     ann->print(std::cerr);
00682     std::cerr << std::endl;
00683     r0 = "in"; r1 = "not in";
00684     return SET_VAL_MIN_INC();
00685   }
00686 #endif
00687 
00688 #ifdef GECODE_HAS_FLOAT_VARS
00689   TieBreak<FloatVarBranch> ann2fvarsel(AST::Node* ann, Rnd rnd,
00690                                        double decay) {
00691     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00692       if (s->id == "input_order")
00693         return TieBreak<FloatVarBranch>(FLOAT_VAR_NONE());
00694       if (s->id == "first_fail")
00695         return TieBreak<FloatVarBranch>(FLOAT_VAR_SIZE_MIN());
00696       if (s->id == "anti_first_fail")
00697         return TieBreak<FloatVarBranch>(FLOAT_VAR_SIZE_MAX());
00698       if (s->id == "smallest")
00699         return TieBreak<FloatVarBranch>(FLOAT_VAR_MIN_MIN());
00700       if (s->id == "largest")
00701         return TieBreak<FloatVarBranch>(FLOAT_VAR_MAX_MAX());
00702       if (s->id == "occurrence")
00703         return TieBreak<FloatVarBranch>(FLOAT_VAR_DEGREE_MAX());
00704       if (s->id == "most_constrained")
00705         return TieBreak<FloatVarBranch>(FLOAT_VAR_SIZE_MIN(),
00706                                         FLOAT_VAR_DEGREE_MAX());
00707       if (s->id == "random") {
00708         return TieBreak<FloatVarBranch>(FLOAT_VAR_RND(rnd));
00709       }
00710       if (s->id == "afc_min")
00711         return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_MIN(decay));
00712       if (s->id == "afc_max")
00713         return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_MAX(decay));
00714       if (s->id == "afc_size_min")
00715         return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_SIZE_MIN(decay));
00716       if (s->id == "afc_size_max")
00717         return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_SIZE_MAX(decay));
00718       if (s->id == "action_min")
00719         return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTION_MIN(decay));
00720       if (s->id == "action_max")
00721         return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTION_MAX(decay));
00722       if (s->id == "action_size_min")
00723         return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTION_SIZE_MIN(decay));
00724       if (s->id == "action_size_max")
00725         return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTION_SIZE_MAX(decay));
00726     }
00727     std::cerr << "Warning, ignored search annotation: ";
00728     ann->print(std::cerr);
00729     std::cerr << std::endl;
00730     return TieBreak<FloatVarBranch>(FLOAT_VAR_NONE());
00731   }
00732 
00733   FloatValBranch ann2fvalsel(AST::Node* ann, std::string r0, std::string r1) {
00734     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00735       if (s->id == "indomain_split") {
00736         r0 = "<="; r1 = ">";
00737         return FLOAT_VAL_SPLIT_MIN();
00738       }
00739       if (s->id == "indomain_reverse_split") {
00740         r1 = "<="; r0 = ">";
00741         return FLOAT_VAL_SPLIT_MAX();
00742       }
00743     }
00744     std::cerr << "Warning, ignored search annotation: ";
00745     ann->print(std::cerr);
00746     std::cerr << std::endl;
00747     r0 = "<="; r1 = ">";
00748     return FLOAT_VAL_SPLIT_MIN();
00749   }
00750 
00751 #endif
00752 
00753   class FlatZincSpaceInitData {
00754   public:
00756     typedef std::unordered_set<TupleSet> TupleSetSet;
00758     TupleSetSet tupleSetSet;
00759 
00761     typedef std::unordered_set<SharedArray<int> > IntSharedArraySet;
00763     IntSharedArraySet intSharedArraySet;
00764 
00766     typedef std::unordered_set<DFA> DFASet;
00768     DFASet dfaSet;
00769     
00771     FlatZincSpaceInitData(void) {}
00772   };
00773 
00774   FlatZincSpace::FlatZincSpace(FlatZincSpace& f)
00775     : Space(f),
00776       _initData(NULL), _random(f._random),
00777       _solveAnnotations(NULL), iv_boolalias(NULL),
00778 #ifdef GECODE_HAS_FLOAT_VARS
00779       step(f.step),
00780 #endif
00781       needAuxVars(f.needAuxVars) {
00782       _optVar = f._optVar;
00783       _optVarIsInt = f._optVarIsInt;
00784       _method = f._method;
00785       _lns = f._lns;
00786       _lnsInitialSolution = f._lnsInitialSolution;
00787       branchInfo = f.branchInfo;
00788       iv.update(*this, f.iv);
00789       iv_lns.update(*this, f.iv_lns);
00790       intVarCount = f.intVarCount;
00791 
00792       if (needAuxVars) {
00793         IntVarArgs iva;
00794         for (int i=0; i<f.iv_aux.size(); i++) {
00795           if (!f.iv_aux[i].assigned()) {
00796             iva << IntVar();
00797             iva[iva.size()-1].update(*this, f.iv_aux[i]);
00798           }
00799         }
00800         iv_aux = IntVarArray(*this, iva);
00801       }
00802 
00803       bv.update(*this, f.bv);
00804       boolVarCount = f.boolVarCount;
00805       if (needAuxVars) {
00806         BoolVarArgs bva;
00807         for (int i=0; i<f.bv_aux.size(); i++) {
00808           if (!f.bv_aux[i].assigned()) {
00809             bva << BoolVar();
00810             bva[bva.size()-1].update(*this, f.bv_aux[i]);
00811           }
00812         }
00813         bv_aux = BoolVarArray(*this, bva);
00814       }
00815 
00816 #ifdef GECODE_HAS_SET_VARS
00817       sv.update(*this, f.sv);
00818       setVarCount = f.setVarCount;
00819       if (needAuxVars) {
00820         SetVarArgs sva;
00821         for (int i=0; i<f.sv_aux.size(); i++) {
00822           if (!f.sv_aux[i].assigned()) {
00823             sva << SetVar();
00824             sva[sva.size()-1].update(*this, f.sv_aux[i]);
00825           }
00826         }
00827         sv_aux = SetVarArray(*this, sva);
00828       }
00829 #endif
00830 #ifdef GECODE_HAS_FLOAT_VARS
00831       fv.update(*this, f.fv);
00832       floatVarCount = f.floatVarCount;
00833       if (needAuxVars) {
00834         FloatVarArgs fva;
00835         for (int i=0; i<f.fv_aux.size(); i++) {
00836           if (!f.fv_aux[i].assigned()) {
00837             fva << FloatVar();
00838             fva[fva.size()-1].update(*this, f.fv_aux[i]);
00839           }
00840         }
00841         fv_aux = FloatVarArray(*this, fva);
00842       }
00843 #endif
00844     }
00845 
00846   FlatZincSpace::FlatZincSpace(Rnd& random)
00847   :  _initData(new FlatZincSpaceInitData),
00848     intVarCount(-1), boolVarCount(-1), floatVarCount(-1), setVarCount(-1),
00849     _optVar(-1), _optVarIsInt(true), _lns(0), _lnsInitialSolution(0),
00850     _random(random),
00851     _solveAnnotations(NULL), needAuxVars(true) {
00852     branchInfo.init();
00853   }
00854 
00855   void
00856   FlatZincSpace::init(int intVars, int boolVars,
00857                       int setVars, int floatVars) {
00858     (void) setVars;
00859     (void) floatVars;
00860 
00861     intVarCount = 0;
00862     iv = IntVarArray(*this, intVars);
00863     iv_introduced = std::vector<bool>(2*intVars);
00864     iv_boolalias = alloc<int>(intVars+(intVars==0?1:0));
00865     boolVarCount = 0;
00866     bv = BoolVarArray(*this, boolVars);
00867     bv_introduced = std::vector<bool>(2*boolVars);
00868 #ifdef GECODE_HAS_SET_VARS
00869     setVarCount = 0;
00870     sv = SetVarArray(*this, setVars);
00871     sv_introduced = std::vector<bool>(2*setVars);
00872 #endif
00873 #ifdef GECODE_HAS_FLOAT_VARS
00874     floatVarCount = 0;
00875     fv = FloatVarArray(*this, floatVars);
00876     fv_introduced = std::vector<bool>(2*floatVars);
00877 #endif
00878   }
00879 
00880   void
00881   FlatZincSpace::newIntVar(IntVarSpec* vs) {
00882     if (vs->alias) {
00883       iv[intVarCount++] = iv[vs->i];
00884     } else {
00885       IntSet dom(vs2is(vs));
00886       if (dom.size()==0) {
00887         fail();
00888         return;
00889       } else {
00890         iv[intVarCount++] = IntVar(*this, dom);
00891       }
00892     }
00893     iv_introduced[2*(intVarCount-1)] = vs->introduced;
00894     iv_introduced[2*(intVarCount-1)+1] = vs->funcDep;
00895     iv_boolalias[intVarCount-1] = -1;
00896   }
00897 
00898   void
00899   FlatZincSpace::aliasBool2Int(int iv, int bv) {
00900     iv_boolalias[iv] = bv;
00901   }
00902   int
00903   FlatZincSpace::aliasBool2Int(int iv) {
00904     return iv_boolalias[iv];
00905   }
00906 
00907   void
00908   FlatZincSpace::newBoolVar(BoolVarSpec* vs) {
00909     if (vs->alias) {
00910       bv[boolVarCount++] = bv[vs->i];
00911     } else {
00912       bv[boolVarCount++] = BoolVar(*this, vs2bsl(vs), vs2bsh(vs));
00913     }
00914     bv_introduced[2*(boolVarCount-1)] = vs->introduced;
00915     bv_introduced[2*(boolVarCount-1)+1] = vs->funcDep;
00916   }
00917 
00918 #ifdef GECODE_HAS_SET_VARS
00919   void
00920   FlatZincSpace::newSetVar(SetVarSpec* vs) {
00921     if (vs->alias) {
00922       sv[setVarCount++] = sv[vs->i];
00923     } else if (vs->assigned) {
00924       assert(vs->upperBound());
00925       AST::SetLit* vsv = vs->upperBound.some();
00926       if (vsv->interval) {
00927         IntSet d(vsv->min, vsv->max);
00928         sv[setVarCount++] = SetVar(*this, d, d);
00929       } else {
00930         int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
00931         for (int i=vsv->s.size(); i--; )
00932           is[i] = vsv->s[i];
00933         IntSet d(is, vsv->s.size());
00934         heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
00935         sv[setVarCount++] = SetVar(*this, d, d);
00936       }
00937     } else if (vs->upperBound()) {
00938       AST::SetLit* vsv = vs->upperBound.some();
00939       if (vsv->interval) {
00940         IntSet d(vsv->min, vsv->max);
00941         sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
00942       } else {
00943         int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
00944         for (int i=vsv->s.size(); i--; )
00945           is[i] = vsv->s[i];
00946         IntSet d(is, vsv->s.size());
00947         heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
00948         sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
00949       }
00950     } else {
00951       sv[setVarCount++] = SetVar(*this, IntSet::empty,
00952                                  IntSet(Set::Limits::min,
00953                                         Set::Limits::max));
00954     }
00955     sv_introduced[2*(setVarCount-1)] = vs->introduced;
00956     sv_introduced[2*(setVarCount-1)+1] = vs->funcDep;
00957   }
00958 #else
00959   void
00960   FlatZincSpace::newSetVar(SetVarSpec*) {
00961     throw FlatZinc::Error("Gecode", "set variables not supported");
00962   }
00963 #endif
00964 
00965 #ifdef GECODE_HAS_FLOAT_VARS
00966   void
00967   FlatZincSpace::newFloatVar(FloatVarSpec* vs) {
00968     if (vs->alias) {
00969       fv[floatVarCount++] = fv[vs->i];
00970     } else {
00971       double dmin, dmax;
00972       if (vs->domain()) {
00973         dmin = vs->domain.some().first;
00974         dmax = vs->domain.some().second;
00975         if (dmin > dmax) {
00976           fail();
00977           return;
00978         }
00979       } else {
00980         dmin = Float::Limits::min;
00981         dmax = Float::Limits::max;
00982       }
00983       fv[floatVarCount++] = FloatVar(*this, dmin, dmax);
00984     }
00985     fv_introduced[2*(floatVarCount-1)] = vs->introduced;
00986     fv_introduced[2*(floatVarCount-1)+1] = vs->funcDep;
00987   }
00988 #else
00989   void
00990   FlatZincSpace::newFloatVar(FloatVarSpec*) {
00991     throw FlatZinc::Error("Gecode", "float variables not supported");
00992   }
00993 #endif
00994 
00995   namespace {
00996     struct ConExprOrder {
00997       bool operator() (ConExpr* ce0, ConExpr* ce1) {
00998         return ce0->args->a.size() < ce1->args->a.size();
00999       }
01000     };
01001   }
01002 
01003   void
01004   FlatZincSpace::postConstraints(std::vector<ConExpr*>& ces) {
01005     ConExprOrder ceo;
01006     std::sort(ces.begin(), ces.end(), ceo);
01007 
01008     for (unsigned int i=0; i<ces.size(); i++) {
01009       const ConExpr& ce = *ces[i];
01010       try {
01011         registry().post(*this, ce);
01012       } catch (Gecode::Exception& e) {
01013         throw FlatZinc::Error("Gecode", e.what());
01014       } catch (AST::TypeError& e) {
01015         throw FlatZinc::Error("Type error", e.what());
01016       }
01017       delete ces[i];
01018       ces[i] = NULL;
01019     }
01020   }
01021 
01022   void flattenAnnotations(AST::Array* ann, std::vector<AST::Node*>& out) {
01023       for (unsigned int i=0; i<ann->a.size(); i++) {
01024         if (ann->a[i]->isCall("seq_search")) {
01025           AST::Call* c = ann->a[i]->getCall();
01026           if (c->args->isArray())
01027             flattenAnnotations(c->args->getArray(), out);
01028           else
01029             out.push_back(c->args);
01030         } else {
01031           out.push_back(ann->a[i]);
01032         }
01033       }
01034   }
01035 
01036   void
01037   FlatZincSpace::createBranchers(Printer&p, AST::Node* ann, FlatZincOptions& opt,
01038                                  bool ignoreUnknown,
01039                                  std::ostream& err) {
01040     int seed = opt.seed();
01041     double decay = opt.decay();
01042     Rnd rnd(static_cast<unsigned int>(seed));
01043     TieBreak<IntVarBranch> def_int_varsel = INT_VAR_AFC_SIZE_MAX(0.99);
01044     IntBoolVarBranch def_intbool_varsel = INTBOOL_VAR_AFC_SIZE_MAX(0.99);
01045     IntValBranch def_int_valsel = INT_VAL_MIN();
01046     std::string def_int_rel_left = "=";
01047     std::string def_int_rel_right = "!=";
01048     TieBreak<BoolVarBranch> def_bool_varsel = BOOL_VAR_AFC_MAX(0.99);
01049     BoolValBranch def_bool_valsel = BOOL_VAL_MIN();
01050     std::string def_bool_rel_left = "=";
01051     std::string def_bool_rel_right = "!=";
01052 #ifdef GECODE_HAS_SET_VARS
01053     SetVarBranch def_set_varsel = SET_VAR_AFC_SIZE_MAX(0.99);
01054     SetValBranch def_set_valsel = SET_VAL_MIN_INC();
01055     std::string def_set_rel_left = "in";
01056     std::string def_set_rel_right = "not in";
01057 #endif
01058 #ifdef GECODE_HAS_FLOAT_VARS
01059     TieBreak<FloatVarBranch> def_float_varsel = FLOAT_VAR_SIZE_MIN();
01060     FloatValBranch def_float_valsel = FLOAT_VAL_SPLIT_MIN();
01061     std::string def_float_rel_left = "<=";
01062     std::string def_float_rel_right = ">";
01063 #endif
01064 
01065     std::vector<bool> iv_searched(iv.size());
01066     for (unsigned int i=iv.size(); i--;)
01067       iv_searched[i] = false;
01068     std::vector<bool> bv_searched(bv.size());
01069     for (unsigned int i=bv.size(); i--;)
01070       bv_searched[i] = false;
01071 #ifdef GECODE_HAS_SET_VARS
01072     std::vector<bool> sv_searched(sv.size());
01073     for (unsigned int i=sv.size(); i--;)
01074       sv_searched[i] = false;
01075 #endif
01076 #ifdef GECODE_HAS_FLOAT_VARS
01077     std::vector<bool> fv_searched(fv.size());
01078     for (unsigned int i=fv.size(); i--;)
01079       fv_searched[i] = false;
01080 #endif
01081 
01082     _lns = 0;
01083     if (ann) {
01084       std::vector<AST::Node*> flatAnn;
01085       if (ann->isArray()) {
01086         flattenAnnotations(ann->getArray()  , flatAnn);
01087       } else {
01088         flatAnn.push_back(ann);
01089       }
01090 
01091       for (unsigned int i=0; i<flatAnn.size(); i++) {
01092         if (flatAnn[i]->isCall("restart_geometric")) {
01093           AST::Call* call = flatAnn[i]->getCall("restart_geometric");
01094           opt.restart(RM_GEOMETRIC);
01095           AST::Array* args = call->getArgs(2);
01096           opt.restart_base(args->a[0]->getFloat());
01097           opt.restart_scale(args->a[1]->getInt());
01098         } else if (flatAnn[i]->isCall("restart_luby")) {
01099           AST::Call* call = flatAnn[i]->getCall("restart_luby");
01100           opt.restart(RM_LUBY);
01101           opt.restart_scale(call->args->getInt());
01102         } else if (flatAnn[i]->isCall("restart_linear")) {
01103           AST::Call* call = flatAnn[i]->getCall("restart_linear");
01104           opt.restart(RM_LINEAR);
01105           opt.restart_scale(call->args->getInt());
01106         } else if (flatAnn[i]->isCall("restart_constant")) {
01107           AST::Call* call = flatAnn[i]->getCall("restart_constant");
01108           opt.restart(RM_CONSTANT);
01109           opt.restart_scale(call->args->getInt());
01110         } else if (flatAnn[i]->isCall("restart_none")) {
01111           opt.restart(RM_NONE);
01112         } else if (flatAnn[i]->isCall("relax_and_reconstruct")) {
01113           if (_lns != 0)
01114             throw FlatZinc::Error("FlatZinc",
01115             "Only one relax_and_reconstruct annotation allowed");
01116           AST::Call *call = flatAnn[i]->getCall("relax_and_reconstruct");
01117           AST::Array* args;
01118           if (call->args->getArray()->a.size()==2) {
01119             args = call->getArgs(2);
01120           } else {
01121             args = call->getArgs(3);
01122           }
01123           _lns = args->a[1]->getInt();
01124           AST::Array *vars = args->a[0]->getArray();
01125           int k=vars->a.size();
01126           for (int i=vars->a.size(); i--;)
01127             if (vars->a[i]->isInt())
01128               k--;
01129           iv_lns = IntVarArray(*this, k);
01130           k = 0;
01131           for (unsigned int i=0; i<vars->a.size(); i++) {
01132             if (vars->a[i]->isInt())
01133               continue;
01134             iv_lns[k++] = iv[vars->a[i]->getIntVar()];
01135           }
01136           if (args->a.size()==3) {
01137             AST::Array *initial = args->a[2]->getArray();
01138             _lnsInitialSolution = IntSharedArray(initial->a.size());
01139             for (unsigned int i=initial->a.size(); i--;)
01140               _lnsInitialSolution[i] = initial->a[i]->getInt();
01141           }
01142         } else if (flatAnn[i]->isCall("gecode_search")) {
01143           AST::Call* c = flatAnn[i]->getCall();
01144           branchWithPlugin(c->args);
01145         } else if (flatAnn[i]->isCall("int_search")) {
01146           AST::Call *call = flatAnn[i]->getCall("int_search");
01147           AST::Array *args = call->getArgs(4);
01148           AST::Array *vars = args->a[0]->getArray();
01149           int k=vars->a.size();
01150           for (int i=vars->a.size(); i--;)
01151             if (vars->a[i]->isInt())
01152               k--;
01153           IntVarArgs va(k);
01154           std::vector<std::string> names;
01155           k=0;
01156           for (unsigned int i=0; i<vars->a.size(); i++) {
01157             if (vars->a[i]->isInt())
01158               continue;
01159             va[k++] = iv[vars->a[i]->getIntVar()];
01160             iv_searched[vars->a[i]->getIntVar()] = true;
01161             names.push_back(vars->a[i]->getVarName());
01162           }
01163           std::string r0, r1;
01164           {
01165             BrancherGroup bg;
01166             branch(bg(*this), va,
01167                    ann2ivarsel(args->a[1],rnd,decay),
01168                    ann2ivalsel(args->a[2],r0,r1,rnd),
01169                    nullptr,
01170                    &varValPrint<IntVar>);
01171             branchInfo.add(bg,r0,r1,names);
01172           }
01173         } else if (flatAnn[i]->isCall("int_assign")) {
01174           AST::Call *call = flatAnn[i]->getCall("int_assign");
01175           AST::Array *args = call->getArgs(2);
01176           AST::Array *vars = args->a[0]->getArray();
01177           int k=vars->a.size();
01178           for (int i=vars->a.size(); i--;)
01179             if (vars->a[i]->isInt())
01180               k--;
01181           IntVarArgs va(k);
01182           k=0;
01183           for (unsigned int i=0; i<vars->a.size(); i++) {
01184             if (vars->a[i]->isInt())
01185               continue;
01186             va[k++] = iv[vars->a[i]->getIntVar()];
01187             iv_searched[vars->a[i]->getIntVar()] = true;
01188           }
01189           assign(*this, va, ann2asnivalsel(args->a[1],rnd), nullptr,
01190                 &varValPrint<IntVar>);
01191         } else if (flatAnn[i]->isCall("bool_search")) {
01192           AST::Call *call = flatAnn[i]->getCall("bool_search");
01193           AST::Array *args = call->getArgs(4);
01194           AST::Array *vars = args->a[0]->getArray();
01195           int k=vars->a.size();
01196           for (int i=vars->a.size(); i--;)
01197             if (vars->a[i]->isBool())
01198               k--;
01199           BoolVarArgs va(k);
01200           k=0;
01201           std::vector<std::string> names;
01202           for (unsigned int i=0; i<vars->a.size(); i++) {
01203             if (vars->a[i]->isBool())
01204               continue;
01205             va[k++] = bv[vars->a[i]->getBoolVar()];
01206             bv_searched[vars->a[i]->getBoolVar()] = true;
01207             names.push_back(vars->a[i]->getVarName());
01208           }
01209 
01210           std::string r0, r1;
01211           {
01212             BrancherGroup bg;
01213             branch(bg(*this), va,
01214                    ann2bvarsel(args->a[1],rnd,decay),
01215                    ann2bvalsel(args->a[2],r0,r1,rnd),
01216                    nullptr,
01217                    &varValPrint<BoolVar>);
01218             branchInfo.add(bg,r0,r1,names);
01219           }
01220         } else if (flatAnn[i]->isCall("int_default_search")) {
01221           AST::Call *call = flatAnn[i]->getCall("int_default_search");
01222           AST::Array *args = call->getArgs(2);
01223           def_int_varsel = ann2ivarsel(args->a[0],rnd,decay);
01224           def_int_valsel = ann2ivalsel(args->a[1],
01225                                        def_int_rel_left,def_int_rel_right,rnd);
01226         } else if (flatAnn[i]->isCall("bool_default_search")) {
01227           AST::Call *call = flatAnn[i]->getCall("bool_default_search");
01228           AST::Array *args = call->getArgs(2);
01229           def_bool_varsel = ann2bvarsel(args->a[0],rnd,decay);
01230           def_bool_valsel = ann2bvalsel(args->a[1],
01231                                         def_bool_rel_left,def_bool_rel_right,
01232                                         rnd);
01233         } else if (flatAnn[i]->isCall("set_search")) {
01234 #ifdef GECODE_HAS_SET_VARS
01235           AST::Call *call = flatAnn[i]->getCall("set_search");
01236           AST::Array *args = call->getArgs(4);
01237           AST::Array *vars = args->a[0]->getArray();
01238           int k=vars->a.size();
01239           for (int i=vars->a.size(); i--;)
01240             if (vars->a[i]->isSet())
01241               k--;
01242           SetVarArgs va(k);
01243           k=0;
01244           std::vector<std::string> names;
01245           for (unsigned int i=0; i<vars->a.size(); i++) {
01246             if (vars->a[i]->isSet())
01247               continue;
01248             va[k++] = sv[vars->a[i]->getSetVar()];
01249             sv_searched[vars->a[i]->getSetVar()] = true;
01250             names.push_back(vars->a[i]->getVarName());
01251           }
01252           std::string r0, r1;
01253           {
01254             BrancherGroup bg;
01255             branch(bg(*this), va,
01256                    ann2svarsel(args->a[1],rnd,decay),
01257                    ann2svalsel(args->a[2],r0,r1,rnd),
01258                    nullptr,
01259                    &varValPrint<SetVar>);
01260             branchInfo.add(bg,r0,r1,names);
01261           }
01262 #else
01263           if (!ignoreUnknown) {
01264             err << "Warning, ignored search annotation: ";
01265             flatAnn[i]->print(err);
01266             err << std::endl;
01267           }
01268 #endif
01269         } else if (flatAnn[i]->isCall("set_default_search")) {
01270 #ifdef GECODE_HAS_SET_VARS
01271           AST::Call *call = flatAnn[i]->getCall("set_default_search");
01272           AST::Array *args = call->getArgs(2);
01273           def_set_varsel = ann2svarsel(args->a[0],rnd,decay);
01274           def_set_valsel = ann2svalsel(args->a[1],
01275                                        def_set_rel_left,def_set_rel_right,rnd);
01276 #else
01277           if (!ignoreUnknown) {
01278             err << "Warning, ignored search annotation: ";
01279             flatAnn[i]->print(err);
01280             err << std::endl;
01281           }
01282 #endif
01283         } else if (flatAnn[i]->isCall("float_default_search")) {
01284 #ifdef GECODE_HAS_FLOAT_VARS
01285           AST::Call *call = flatAnn[i]->getCall("float_default_search");
01286           AST::Array *args = call->getArgs(2);
01287           def_float_varsel = ann2fvarsel(args->a[0],rnd,decay);
01288           def_float_valsel = ann2fvalsel(args->a[1],
01289                                          def_float_rel_left,def_float_rel_right);
01290 #else
01291           if (!ignoreUnknown) {
01292             err << "Warning, ignored search annotation: ";
01293             flatAnn[i]->print(err);
01294             err << std::endl;
01295           }
01296 #endif
01297         } else if (flatAnn[i]->isCall("float_search")) {
01298 #ifdef GECODE_HAS_FLOAT_VARS
01299           AST::Call *call = flatAnn[i]->getCall("float_search");
01300           AST::Array *args = call->getArgs(5);
01301           AST::Array *vars = args->a[0]->getArray();
01302           int k=vars->a.size();
01303           for (int i=vars->a.size(); i--;)
01304             if (vars->a[i]->isFloat())
01305               k--;
01306           FloatVarArgs va(k);
01307           k=0;
01308           std::vector<std::string> names;
01309           for (unsigned int i=0; i<vars->a.size(); i++) {
01310             if (vars->a[i]->isFloat())
01311               continue;
01312             va[k++] = fv[vars->a[i]->getFloatVar()];
01313             fv_searched[vars->a[i]->getFloatVar()] = true;
01314             names.push_back(vars->a[i]->getVarName());
01315           }
01316           std::string r0, r1;
01317           {
01318             BrancherGroup bg;
01319             branch(bg(*this), va,
01320                    ann2fvarsel(args->a[2],rnd,decay),
01321                    ann2fvalsel(args->a[3],r0,r1),
01322                    nullptr,
01323                    &varValPrintF);
01324             branchInfo.add(bg,r0,r1,names);
01325           }
01326 #else
01327           if (!ignoreUnknown) {
01328             err << "Warning, ignored search annotation: ";
01329             flatAnn[i]->print(err);
01330             err << std::endl;
01331           }
01332 #endif
01333         } else {
01334           if (!ignoreUnknown) {
01335             err << "Warning, ignored search annotation: ";
01336             flatAnn[i]->print(err);
01337             err << std::endl;
01338           }
01339         }
01340       }
01341     }
01342     int introduced = 0;
01343     int funcdep = 0;
01344     int searched = 0;
01345     for (int i=iv.size(); i--;) {
01346       if (iv_searched[i] || (_method != SAT && _optVarIsInt && _optVar==i)) {
01347         searched++;
01348       } else if (iv_introduced[2*i]) {
01349         if (iv_introduced[2*i+1]) {
01350           funcdep++;
01351         } else {
01352           introduced++;
01353         }
01354       }
01355     }
01356     std::vector<std::string> iv_sol_names(iv.size()-(introduced+funcdep+searched));
01357     IntVarArgs iv_sol(iv.size()-(introduced+funcdep+searched));
01358     std::vector<std::string> iv_tmp_names(introduced);
01359     IntVarArgs iv_tmp(introduced);
01360     for (int i=iv.size(), j=0, k=0; i--;) {
01361       if (iv_searched[i] || (_method != SAT && _optVarIsInt && _optVar==i))
01362         continue;
01363       if (iv_introduced[2*i]) {
01364         if (!iv_introduced[2*i+1]) {
01365           iv_tmp_names[j] = p.intVarName(i);
01366           iv_tmp[j++] = iv[i];
01367         }
01368       } else {
01369         iv_sol_names[k] = p.intVarName(i);
01370         iv_sol[k++] = iv[i];
01371       }
01372     }
01373 
01374     introduced = 0;
01375     funcdep = 0;
01376     searched = 0;
01377     for (int i=bv.size(); i--;) {
01378       if (bv_searched[i]) {
01379         searched++;
01380       } else if (bv_introduced[2*i]) {
01381         if (bv_introduced[2*i+1]) {
01382           funcdep++;
01383         } else {
01384           introduced++;
01385         }
01386       }
01387     }
01388     std::vector<std::string> bv_sol_names(bv.size()-(introduced+funcdep+searched));
01389     BoolVarArgs bv_sol(bv.size()-(introduced+funcdep+searched));
01390     BoolVarArgs bv_tmp(introduced);
01391     std::vector<std::string> bv_tmp_names(introduced);
01392     for (int i=bv.size(), j=0, k=0; i--;) {
01393       if (bv_searched[i])
01394         continue;
01395       if (bv_introduced[2*i]) {
01396         if (!bv_introduced[2*i+1]) {
01397           bv_tmp_names[j] = p.boolVarName(i);
01398           bv_tmp[j++] = bv[i];
01399         }
01400       } else {
01401         bv_sol_names[k] = p.boolVarName(i);
01402         bv_sol[k++] = bv[i];
01403       }
01404     }
01405 
01406     if (iv_sol.size() > 0 && bv_sol.size() > 0) {
01407       branch(*this, iv_sol, bv_sol, def_intbool_varsel, def_int_valsel);
01408     } else if (iv_sol.size() > 0) {
01409       BrancherGroup bg;
01410       branch(bg(*this), iv_sol, def_int_varsel, def_int_valsel, nullptr,
01411              &varValPrint<IntVar>);
01412       branchInfo.add(bg,def_int_rel_left,def_int_rel_right,iv_sol_names);
01413     } else if (bv_sol.size() > 0) {
01414       BrancherGroup bg;
01415       branch(bg(*this), bv_sol, def_bool_varsel, def_bool_valsel, nullptr,
01416              &varValPrint<BoolVar>);
01417       branchInfo.add(bg,def_bool_rel_left,def_bool_rel_right,bv_sol_names);
01418     }
01419 #ifdef GECODE_HAS_FLOAT_VARS
01420     introduced = 0;
01421     funcdep = 0;
01422     searched = 0;
01423     for (int i=fv.size(); i--;) {
01424       if (fv_searched[i] || (_method != SAT && !_optVarIsInt && _optVar==i)) {
01425         searched++;
01426       } else if (fv_introduced[2*i]) {
01427         if (fv_introduced[2*i+1]) {
01428           funcdep++;
01429         } else {
01430           introduced++;
01431         }
01432       }
01433     }
01434     std::vector<std::string> fv_sol_names(fv.size()-(introduced+funcdep+searched));
01435     FloatVarArgs fv_sol(fv.size()-(introduced+funcdep+searched));
01436     FloatVarArgs fv_tmp(introduced);
01437     std::vector<std::string> fv_tmp_names(introduced);
01438     for (int i=fv.size(), j=0, k=0; i--;) {
01439       if (fv_searched[i] || (_method != SAT && !_optVarIsInt && _optVar==i))
01440         continue;
01441       if (fv_introduced[2*i]) {
01442         if (!fv_introduced[2*i+1]) {
01443           fv_tmp_names[j] = p.floatVarName(i);
01444           fv_tmp[j++] = fv[i];
01445         }
01446       } else {
01447         fv_sol_names[k] = p.floatVarName(i);
01448         fv_sol[k++] = fv[i];
01449       }
01450     }
01451 
01452     if (fv_sol.size() > 0) {
01453       BrancherGroup bg;
01454       branch(bg(*this), fv_sol, def_float_varsel, def_float_valsel, nullptr,
01455              &varValPrintF);
01456       branchInfo.add(bg,def_float_rel_left,def_float_rel_right,fv_sol_names);
01457     }
01458 #endif
01459 #ifdef GECODE_HAS_SET_VARS
01460     introduced = 0;
01461     funcdep = 0;
01462     searched = 0;
01463     for (int i=sv.size(); i--;) {
01464       if (sv_searched[i]) {
01465         searched++;
01466       } else if (sv_introduced[2*i]) {
01467         if (sv_introduced[2*i+1]) {
01468           funcdep++;
01469         } else {
01470           introduced++;
01471         }
01472       }
01473     }
01474     std::vector<std::string> sv_sol_names(sv.size()-(introduced+funcdep+searched));
01475     SetVarArgs sv_sol(sv.size()-(introduced+funcdep+searched));
01476     SetVarArgs sv_tmp(introduced);
01477     std::vector<std::string> sv_tmp_names(introduced);
01478     for (int i=sv.size(), j=0, k=0; i--;) {
01479       if (sv_searched[i])
01480         continue;
01481       if (sv_introduced[2*i]) {
01482         if (!sv_introduced[2*i+1]) {
01483           sv_tmp_names[j] = p.setVarName(i);
01484           sv_tmp[j++] = sv[i];
01485         }
01486       } else {
01487         sv_sol_names[k] = p.setVarName(i);
01488         sv_sol[k++] = sv[i];
01489       }
01490     }
01491 
01492     if (sv_sol.size() > 0) {
01493       BrancherGroup bg;
01494       branch(bg(*this), sv_sol, def_set_varsel, def_set_valsel, nullptr,
01495              &varValPrint<SetVar>);
01496       branchInfo.add(bg,def_set_rel_left,def_set_rel_right,sv_sol_names);
01497       
01498     }
01499 #endif
01500     iv_aux = IntVarArray(*this, iv_tmp);
01501     bv_aux = BoolVarArray(*this, bv_tmp);
01502     int n_aux = iv_aux.size() + bv_aux.size();
01503 #ifdef GECODE_HAS_SET_VARS
01504     sv_aux = SetVarArray(*this, sv_tmp);
01505     n_aux += sv_aux.size();
01506 #endif
01507 #ifdef GECODE_HAS_FLOAT_VARS
01508     fv_aux = FloatVarArray(*this, fv_tmp);
01509     n_aux += fv_aux.size();
01510 #endif
01511 
01512     if (n_aux > 0) {
01513       if (_method == SAT) {
01514         AuxVarBrancher::post(*this, def_int_varsel, def_int_valsel,
01515                              def_bool_varsel, def_bool_valsel
01516 #ifdef GECODE_HAS_SET_VARS
01517                              , def_set_varsel, def_set_valsel
01518 #endif
01519 #ifdef GECODE_HAS_FLOAT_VARS
01520                              , def_float_varsel, def_float_valsel
01521 #endif
01522                              );
01523       } else {
01524         {
01525           BrancherGroup bg;
01526           branch(bg(*this),iv_aux,def_int_varsel,def_int_valsel, nullptr,
01527                  &varValPrint<IntVar>);
01528           branchInfo.add(bg,def_int_rel_left,def_int_rel_right,iv_tmp_names);
01529         }
01530         {
01531           BrancherGroup bg;
01532           branch(bg(*this),bv_aux,def_bool_varsel,def_bool_valsel, nullptr,
01533                  &varValPrint<BoolVar>);
01534           branchInfo.add(bg,def_bool_rel_left,def_bool_rel_right,bv_tmp_names);
01535         }
01536   #ifdef GECODE_HAS_SET_VARS
01537         {
01538           BrancherGroup bg;
01539           branch(bg(*this),sv_aux,def_set_varsel,def_set_valsel, nullptr,
01540                  &varValPrint<SetVar>);
01541           branchInfo.add(bg,def_set_rel_left,def_set_rel_right,sv_tmp_names);
01542         }
01543   #endif
01544   #ifdef GECODE_HAS_FLOAT_VARS
01545         {
01546           BrancherGroup bg;
01547           branch(bg(*this),fv_aux,def_float_varsel,def_float_valsel, nullptr,
01548                  &varValPrintF);
01549           branchInfo.add(bg,def_float_rel_left,def_float_rel_right,fv_tmp_names);
01550         }
01551   #endif
01552 
01553       }
01554     }
01555 
01556     if (_method == MIN) {
01557       if (_optVarIsInt) {
01558         std::vector<std::string> names(1);
01559         names[0] = p.intVarName(_optVar);
01560         BrancherGroup bg;
01561         branch(bg(*this), iv[_optVar], INT_VAL_MIN(),
01562                &varValPrint<IntVar>);
01563         branchInfo.add(bg,"=","!=",names);
01564       } else {
01565 #ifdef GECODE_HAS_FLOAT_VARS
01566         std::vector<std::string> names(1);
01567         names[0] = p.floatVarName(_optVar);
01568         BrancherGroup bg;
01569         branch(bg(*this), fv[_optVar], FLOAT_VAL_SPLIT_MIN(),
01570                &varValPrintF);
01571         branchInfo.add(bg,"<=",">",names);
01572 #endif
01573       }
01574     } else if (_method == MAX) {
01575       if (_optVarIsInt) {
01576         std::vector<std::string> names(1);
01577         names[0] = p.intVarName(_optVar);
01578         BrancherGroup bg;
01579         branch(bg(*this), iv[_optVar], INT_VAL_MAX(),
01580                &varValPrint<IntVar>);
01581         branchInfo.add(bg,"=","!=",names);
01582       } else {
01583 #ifdef GECODE_HAS_FLOAT_VARS
01584         std::vector<std::string> names(1);
01585         names[0] = p.floatVarName(_optVar);
01586         BrancherGroup bg;
01587         branch(bg(*this), fv[_optVar], FLOAT_VAL_SPLIT_MAX(),
01588                &varValPrintF);
01589         branchInfo.add(bg,"<=",">",names);
01590 #endif
01591       }
01592     }
01593 
01594   }
01595 
01596   AST::Array*
01597   FlatZincSpace::solveAnnotations(void) const {
01598     return _solveAnnotations;
01599   }
01600 
01601   void
01602   FlatZincSpace::solve(AST::Array* ann) {
01603     _method = SAT;
01604     _solveAnnotations = ann;
01605   }
01606 
01607   void
01608   FlatZincSpace::minimize(int var, bool isInt, AST::Array* ann) {
01609     _method = MIN;
01610     _optVar = var;
01611     _optVarIsInt = isInt;
01612     _solveAnnotations = ann;
01613   }
01614 
01615   void
01616   FlatZincSpace::maximize(int var, bool isInt, AST::Array* ann) {
01617     _method = MAX;
01618     _optVar = var;
01619     _optVarIsInt = isInt;
01620     _solveAnnotations = ann;
01621   }
01622 
01623   FlatZincSpace::~FlatZincSpace(void) {
01624     delete _initData;
01625     delete _solveAnnotations;
01626   }
01627 
01628 #ifdef GECODE_HAS_GIST
01629 
01633   template<class Engine>
01634   class GistEngine {
01635   };
01636 
01638   template<typename S>
01639   class GistEngine<DFS<S> > {
01640   public:
01641     static void explore(S* root, const FlatZincOptions& opt,
01642                         Gist::Inspector* i, Gist::Comparator* c) {
01643       Gecode::Gist::Options o;
01644       o.c_d = opt.c_d(); o.a_d = opt.a_d();
01645       o.inspect.click(i);
01646       o.inspect.compare(c);
01647       (void) Gecode::Gist::dfs(root, o);
01648     }
01649   };
01650 
01652   template<typename S>
01653   class GistEngine<BAB<S> > {
01654   public:
01655     static void explore(S* root, const FlatZincOptions& opt,
01656                         Gist::Inspector* i, Gist::Comparator* c) {
01657       Gecode::Gist::Options o;
01658       o.c_d = opt.c_d(); o.a_d = opt.a_d();
01659       o.inspect.click(i);
01660       o.inspect.compare(c);
01661       (void) Gecode::Gist::bab(root, o);
01662     }
01663   };
01664 
01666   template<class S>
01667   class FZPrintingInspector
01668    : public Gecode::Gist::TextOutput, public Gecode::Gist::Inspector {
01669   private:
01670     const Printer& p;
01671   public:
01673     FZPrintingInspector(const Printer& p0);
01675     virtual void inspect(const Space& node);
01677     virtual void finalize(void);
01678   };
01679 
01680   template<class S>
01681   FZPrintingInspector<S>::FZPrintingInspector(const Printer& p0)
01682   : TextOutput("Gecode/FlatZinc"), p(p0) {}
01683 
01684   template<class S>
01685   void
01686   FZPrintingInspector<S>::inspect(const Space& node) {
01687     init();
01688     dynamic_cast<const S&>(node).print(getStream(), p);
01689     getStream() << std::endl;
01690   }
01691 
01692   template<class S>
01693   void
01694   FZPrintingInspector<S>::finalize(void) {
01695     Gecode::Gist::TextOutput::finalize();
01696   }
01697 
01698   template<class S>
01699   class FZPrintingComparator
01700   : public Gecode::Gist::VarComparator<S> {
01701   private:
01702     const Printer& p;
01703   public:
01705     FZPrintingComparator(const Printer& p0);
01706 
01708     virtual void compare(const Space& s0, const Space& s1);
01709   };
01710 
01711   template<class S>
01712   FZPrintingComparator<S>::FZPrintingComparator(const Printer& p0)
01713   : Gecode::Gist::VarComparator<S>("Gecode/FlatZinc"), p(p0) {}
01714 
01715   template<class S>
01716   void
01717   FZPrintingComparator<S>::compare(const Space& s0, const Space& s1) {
01718     this->init();
01719     try {
01720       dynamic_cast<const S&>(s0).compare(dynamic_cast<const S&>(s1),
01721                                          this->getStream(), p);
01722     } catch (Exception& e) {
01723       this->getStream() << "Exception: " << e.what();
01724     }
01725     this->getStream() << std::endl;
01726   }
01727 
01728 #endif
01729 
01730   template<template<class> class Engine>
01731   void
01732   FlatZincSpace::runEngine(std::ostream& out, const Printer& p,
01733                            const FlatZincOptions& opt, Support::Timer& t_total) {
01734     if (opt.restart()==RM_NONE) {
01735       runMeta<Engine,Driver::EngineToMeta>(out,p,opt,t_total);
01736     } else {
01737       runMeta<Engine,RBS>(out,p,opt,t_total);
01738     }
01739   }
01740 
01741 #ifdef GECODE_HAS_CPPROFILER
01742 
01743   class FlatZincGetInfo : public CPProfilerSearchTracer::GetInfo {
01744   public:
01745     const Printer& p;
01746     FlatZincGetInfo(const Printer& printer) : p(printer) {}
01747     virtual std::string
01748     getInfo(const Space& space) const {
01749       std::stringstream ss;
01750       if (const FlatZincSpace* fz_space = dynamic_cast<const FlatZincSpace*>(&space)) {
01751         ss << "{\n\t\"domains\": \"";
01752         ss << fz_space->getDomains(p);
01753         ss << "\"\n}";
01754       }
01755       return ss.str();
01756     }
01757     ~FlatZincGetInfo(void) {};
01758   };
01759 
01760   void printIntVar(std::ostream& os, const std::string name, const Int::IntView& x) {
01761     os << "var ";
01762     if (x.assigned()) {
01763       os << "int: " << name << " = " << x.val() << ";";
01764     } else if (x.range()) {
01765       os << x.min() << ".." << x.max() << ": " << name << ";";
01766     } else {
01767       os << "array_union([";
01768       Gecode::Int::ViewRanges<Int::IntView> r(x);
01769       while (true) {
01770         os << r.min() << ".." << r.max();
01771         ++r;
01772         if (!r()) break;
01773         os << ',';
01774       }
01775       os << "]): " << name << ";";
01776     }
01777     os << "\n";
01778   }
01779   void printBoolVar(std::ostream& os, const std::string name, const BoolVar& b) {
01780     os << "var bool: " << name;
01781     if(b.assigned())
01782       os << " = " << (b.val() ? "true" : "false");
01783     os << ";\n";
01784   }
01785 #ifdef GECODE_HAS_FLOAT_VARS
01786   void printFloatVar(std::ostream& os, const std::string name, const Float::FloatView& f) {
01787     os << "var ";
01788     if(f.assigned())
01789       os << "float: " << name << " = " << f.med() << ";";
01790     else
01791       os << f.min() << ".." << f.max() << ": " << name << ";";
01792     os << "\n";
01793   }
01794 #endif
01795   std::string FlatZincSpace::getDomains(const Printer& p) const {
01796     std::ostringstream oss;
01797 
01798     for (int i = 0; i < iv.size(); i++)
01799       printIntVar(oss, p.intVarName(i), iv[i]);
01800 
01801     for (int i = 0; i < bv.size(); i++)
01802       printBoolVar(oss, p.boolVarName(i), bv[i]);
01803 
01804 #ifdef GECODE_HAS_FLOAT_VARS
01805     for (int i = 0; i < fv.size(); i++)
01806       printFloatVar(oss, p.floatVarName(i), fv[i]);
01807 #endif
01808 #ifdef GECODE_HAS_SET_VARS
01809     for (int i = 0; i < sv.size(); i++)
01810       oss << "var " << sv[i] << ": " << p.setVarName(i) << ";" << std::endl;
01811 #endif
01812 
01813     return oss.str();
01814   }
01815 
01816 #endif
01817 
01818   template<template<class> class Engine,
01819            template<class,template<class> class> class Meta>
01820   void
01821   FlatZincSpace::runMeta(std::ostream& out, const Printer& p,
01822                          const FlatZincOptions& opt, Support::Timer& t_total) {
01823 #ifdef GECODE_HAS_GIST
01824     if (opt.mode() == SM_GIST) {
01825       FZPrintingInspector<FlatZincSpace> pi(p);
01826       FZPrintingComparator<FlatZincSpace> pc(p);
01827       (void) GistEngine<Engine<FlatZincSpace> >::explore(this,opt,&pi,&pc);
01828       return;
01829     }
01830 #endif
01831     StatusStatistics sstat;
01832     unsigned int n_p = 0;
01833     Support::Timer t_solve;
01834     t_solve.start();
01835     if (status(sstat) != SS_FAILED) {
01836       n_p = PropagatorGroup::all.size(*this);
01837     }
01838     Search::Options o;
01839     o.stop = Driver::CombinedStop::create(opt.node(), opt.fail(), opt.time(),
01840                                           true);
01841     o.c_d = opt.c_d();
01842     o.a_d = opt.a_d();
01843 
01844 #ifdef GECODE_HAS_CPPROFILER
01845 
01846     if (opt.mode() == SM_CPPROFILER) {
01847       FlatZincGetInfo* getInfo = nullptr;
01848       if (opt.profiler_info())
01849         getInfo = new FlatZincGetInfo(p);
01850       o.tracer = new CPProfilerSearchTracer(opt.profiler_id(),
01851                                             opt.name(), opt.profiler_port(),
01852                                             getInfo);
01853     }
01854 
01855 #endif
01856 
01857 #ifdef GECODE_HAS_FLOAT_VARS
01858     step = opt.step();
01859 #endif
01860     o.threads = opt.threads();
01861     o.nogoods_limit = opt.nogoods() ? opt.nogoods_limit() : 0;
01862     o.cutoff  = new Search::CutoffAppend(new Search::CutoffConstant(0), 1, Driver::createCutoff(opt));
01863     if (opt.interrupt())
01864       Driver::CombinedStop::installCtrlHandler(true);
01865     {
01866       Meta<FlatZincSpace,Engine> se(this,o);
01867       int noOfSolutions = opt.solutions();
01868       if (noOfSolutions == -1) {
01869         noOfSolutions = (_method == SAT) ? 1 : 0;
01870       }
01871       bool printAll = _method == SAT || opt.allSolutions() || noOfSolutions != 0;
01872       int findSol = noOfSolutions;
01873       FlatZincSpace* sol = NULL;
01874       while (FlatZincSpace* next_sol = se.next()) {
01875         delete sol;
01876         sol = next_sol;
01877         if (printAll) {
01878           sol->print(out, p);
01879           out << "----------" << std::endl;
01880         }
01881         if (--findSol==0)
01882           goto stopped;
01883       }
01884       if (sol && !printAll) {
01885         sol->print(out, p);
01886         out << "----------" << std::endl;
01887       }
01888       if (!se.stopped()) {
01889         if (sol) {
01890           out << "==========" << std::endl;
01891         } else {
01892           out << "=====UNSATISFIABLE=====" << std::endl;
01893         }
01894       } else if (!sol) {
01895           out << "=====UNKNOWN=====" << std::endl;
01896       }
01897       delete sol;
01898       stopped:
01899       if (opt.interrupt())
01900         Driver::CombinedStop::installCtrlHandler(false);
01901       if (opt.mode() == SM_STAT) {
01902         Gecode::Search::Statistics stat = se.statistics();
01903         double totalTime = (t_total.stop() / 1000.0);
01904         double solveTime = (t_solve.stop() / 1000.0);
01905         double initTime = totalTime - solveTime;
01906         out << std::endl
01907             << "%%%mzn-stat: initTime=" << initTime
01908             << std::endl;      
01909         out << "%%%mzn-stat: solveTime=" << solveTime
01910             << std::endl;
01911         out << "%%%mzn-stat: solutions="
01912             << std::abs(noOfSolutions - findSol) << std::endl
01913             << "%%%mzn-stat: variables="
01914             << (intVarCount + boolVarCount + setVarCount) << std::endl
01915             << "%%%mzn-stat: propagators=" << n_p << std::endl
01916             << "%%%mzn-stat: propagations=" << sstat.propagate+stat.propagate << std::endl
01917             << "%%%mzn-stat: nodes=" << stat.node << std::endl
01918             << "%%%mzn-stat: failures=" << stat.fail << std::endl
01919             << "%%%mzn-stat: restarts=" << stat.restart << std::endl
01920             << "%%%mzn-stat: peakDepth=" << stat.depth << std::endl
01921             << "%%%mzn-stat-end" << std::endl
01922             << std::endl;
01923       }
01924     }
01925     delete o.stop;
01926     delete o.tracer;
01927   }
01928 
01929 #ifdef GECODE_HAS_QT
01930   void
01931   FlatZincSpace::branchWithPlugin(AST::Node* ann) {
01932     if (AST::Call* c = dynamic_cast<AST::Call*>(ann)) {
01933       QString pluginName(c->id.c_str());
01934       if (QLibrary::isLibrary(pluginName+".dll")) {
01935         pluginName += ".dll";
01936       } else if (QLibrary::isLibrary(pluginName+".dylib")) {
01937         pluginName = "lib" + pluginName + ".dylib";
01938       } else if (QLibrary::isLibrary(pluginName+".so")) {
01939         // Must check .so after .dylib so that Mac OS uses .dylib
01940         pluginName = "lib" + pluginName + ".so";
01941       }
01942       QPluginLoader pl(pluginName);
01943       QObject* plugin_o = pl.instance();
01944       if (!plugin_o) {
01945         throw FlatZinc::Error("FlatZinc",
01946           "Error loading plugin "+pluginName.toStdString()+
01947           ": "+pl.errorString().toStdString());
01948       }
01949       BranchPlugin* pb = qobject_cast<BranchPlugin*>(plugin_o);
01950       if (!pb) {
01951         throw FlatZinc::Error("FlatZinc",
01952         "Error loading plugin "+pluginName.toStdString()+
01953         ": does not contain valid PluginBrancher");
01954       }
01955       pb->branch(*this, c);
01956     }
01957   }
01958 #else
01959   void
01960   FlatZincSpace::branchWithPlugin(AST::Node*) {
01961     throw FlatZinc::Error("FlatZinc",
01962       "Branching with plugins not supported (requires Qt support)");
01963   }
01964 #endif
01965 
01966   void
01967   FlatZincSpace::run(std::ostream& out, const Printer& p,
01968                       const FlatZincOptions& opt, Support::Timer& t_total) {
01969     switch (_method) {
01970     case MIN:
01971     case MAX:
01972       runEngine<BAB>(out,p,opt,t_total);
01973       break;
01974     case SAT:
01975       runEngine<DFS>(out,p,opt,t_total);
01976       break;
01977     }
01978   }
01979 
01980   void
01981   FlatZincSpace::constrain(const Space& s) {
01982     if (_optVarIsInt) {
01983       if (_method == MIN)
01984         rel(*this, iv[_optVar], IRT_LE,
01985                    static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
01986       else if (_method == MAX)
01987         rel(*this, iv[_optVar], IRT_GR,
01988                    static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
01989     } else {
01990 #ifdef GECODE_HAS_FLOAT_VARS
01991       if (_method == MIN)
01992         rel(*this, fv[_optVar], FRT_LE,
01993                    static_cast<const FlatZincSpace*>(&s)->fv[_optVar].val()-step);
01994       else if (_method == MAX)
01995         rel(*this, fv[_optVar], FRT_GR,
01996                    static_cast<const FlatZincSpace*>(&s)->fv[_optVar].val()+step);
01997 #endif
01998     }
01999   }
02000 
02001   bool
02002   FlatZincSpace::slave(const MetaInfo& mi) {
02003     if ((mi.type() == MetaInfo::RESTART) && (mi.restart() != 0) &&
02004         (_lns > 0) && (mi.last()==NULL) && (_lnsInitialSolution.size()>0)) {
02005       for (unsigned int i=iv_lns.size(); i--;) {
02006         if (_random(99) <= _lns) {
02007           rel(*this, iv_lns[i], IRT_EQ, _lnsInitialSolution[i]);
02008         }
02009       }
02010       return false;
02011     } else if ((mi.type() == MetaInfo::RESTART) && (mi.restart() != 0) &&
02012                (_lns > 0) && mi.last()) {
02013       const FlatZincSpace& last =
02014         static_cast<const FlatZincSpace&>(*mi.last());
02015       for (unsigned int i=iv_lns.size(); i--;) {
02016         if (_random(99) <= _lns) {
02017           rel(*this, iv_lns[i], IRT_EQ, last.iv_lns[i]);
02018         }
02019       }
02020       return false;
02021     }
02022     return true;
02023   }
02024 
02025   Space*
02026   FlatZincSpace::copy(void) {
02027     return new FlatZincSpace(*this);
02028   }
02029 
02030   FlatZincSpace::Meth
02031   FlatZincSpace::method(void) const {
02032     return _method;
02033   }
02034 
02035   int
02036   FlatZincSpace::optVar(void) const {
02037     return _optVar;
02038   }
02039 
02040   bool
02041   FlatZincSpace::optVarIsInt(void) const {
02042     return _optVarIsInt;
02043   }
02044 
02045   void
02046   FlatZincSpace::print(std::ostream& out, const Printer& p) const {
02047     p.print(out, iv, bv
02048 #ifdef GECODE_HAS_SET_VARS
02049     , sv
02050 #endif
02051 #ifdef GECODE_HAS_FLOAT_VARS
02052     , fv
02053 #endif
02054     );
02055   }
02056 
02057   void
02058   FlatZincSpace::compare(const Space& s, std::ostream& out) const {
02059     (void) s; (void) out;
02060 #ifdef GECODE_HAS_GIST
02061     const FlatZincSpace& fs = dynamic_cast<const FlatZincSpace&>(s);
02062     for (int i = 0; i < iv.size(); ++i) {
02063       std::stringstream ss;
02064       ss << "iv[" << i << "]";
02065       std::string result(Gecode::Gist::Comparator::compare(ss.str(), iv[i],
02066                                                            fs.iv[i]));
02067       if (result.length() > 0) out << result << std::endl;
02068     }
02069     for (int i = 0; i < bv.size(); ++i) {
02070       std::stringstream ss;
02071       ss << "bv[" << i << "]";
02072       std::string result(Gecode::Gist::Comparator::compare(ss.str(), bv[i],
02073                                                            fs.bv[i]));
02074       if (result.length() > 0) out << result << std::endl;
02075     }
02076 #ifdef GECODE_HAS_SET_VARS
02077     for (int i = 0; i < sv.size(); ++i) {
02078       std::stringstream ss;
02079       ss << "sv[" << i << "]";
02080       std::string result(Gecode::Gist::Comparator::compare(ss.str(), sv[i],
02081                                                            fs.sv[i]));
02082       if (result.length() > 0) out << result << std::endl;
02083     }
02084 #endif
02085 #ifdef GECODE_HAS_FLOAT_VARS
02086     for (int i = 0; i < fv.size(); ++i) {
02087       std::stringstream ss;
02088       ss << "fv[" << i << "]";
02089       std::string result(Gecode::Gist::Comparator::compare(ss.str(), fv[i],
02090                                                            fs.fv[i]));
02091       if (result.length() > 0) out << result << std::endl;
02092     }
02093 #endif
02094 #endif
02095   }
02096 
02097   void
02098   FlatZincSpace::compare(const FlatZincSpace& s, std::ostream& out,
02099                          const Printer& p) const {
02100     p.printDiff(out, iv, s.iv, bv, s.bv
02101 #ifdef GECODE_HAS_SET_VARS
02102      , sv, s.sv
02103 #endif
02104 #ifdef GECODE_HAS_FLOAT_VARS
02105      , fv, s.fv
02106 #endif
02107     );
02108   }
02109 
02110   void
02111   FlatZincSpace::shrinkArrays(Printer& p) {
02112     p.shrinkArrays(*this, _optVar, _optVarIsInt, iv, bv
02113 #ifdef GECODE_HAS_SET_VARS
02114     , sv
02115 #endif
02116 #ifdef GECODE_HAS_FLOAT_VARS
02117     , fv
02118 #endif
02119     );
02120   }
02121 
02122   IntArgs
02123   FlatZincSpace::arg2intargs(AST::Node* arg, int offset) {
02124     AST::Array* a = arg->getArray();
02125     IntArgs ia(a->a.size()+offset);
02126     for (int i=offset; i--;)
02127       ia[i] = 0;
02128     for (int i=a->a.size(); i--;)
02129       ia[i+offset] = a->a[i]->getInt();
02130     return ia;
02131   }
02132   TupleSet
02133   FlatZincSpace::arg2tupleset(const IntArgs& a, int noOfVars) {
02134     int noOfTuples = a.size() == 0 ? 0 : (a.size()/noOfVars);
02135 
02136     // Build TupleSet
02137     TupleSet ts(noOfVars);
02138     for (int i=0; i<noOfTuples; i++) {
02139       IntArgs t(noOfVars);
02140       for (int j=0; j<noOfVars; j++) {
02141         t[j] = a[i*noOfVars+j];
02142       }
02143       ts.add(t);
02144     }
02145     ts.finalize();
02146 
02147     if (_initData) {
02148       FlatZincSpaceInitData::TupleSetSet::iterator it = _initData->tupleSetSet.find(ts);
02149       if (it != _initData->tupleSetSet.end()) {
02150         return *it;
02151       }
02152       _initData->tupleSetSet.insert(ts);
02153     }
02154     
02155     
02156     return ts;
02157   }
02158   IntSharedArray
02159   FlatZincSpace::arg2intsharedarray(AST::Node* arg, int offset) {
02160     IntArgs ia(arg2intargs(arg,offset));
02161     SharedArray<int> sia(ia);
02162     if (_initData) {
02163       FlatZincSpaceInitData::IntSharedArraySet::iterator it = _initData->intSharedArraySet.find(sia);
02164       if (it != _initData->intSharedArraySet.end()) {
02165         return *it;
02166       }
02167       _initData->intSharedArraySet.insert(sia);
02168     }
02169     
02170     return sia;
02171   }
02172   IntArgs
02173   FlatZincSpace::arg2boolargs(AST::Node* arg, int offset) {
02174     AST::Array* a = arg->getArray();
02175     IntArgs ia(a->a.size()+offset);
02176     for (int i=offset; i--;)
02177       ia[i] = 0;
02178     for (int i=a->a.size(); i--;)
02179       ia[i+offset] = a->a[i]->getBool();
02180     return ia;
02181   }
02182   IntSharedArray
02183   FlatZincSpace::arg2boolsharedarray(AST::Node* arg, int offset) {
02184     IntArgs ia(arg2boolargs(arg,offset));
02185     SharedArray<int> sia(ia);
02186     if (_initData) {
02187       FlatZincSpaceInitData::IntSharedArraySet::iterator it = _initData->intSharedArraySet.find(sia);
02188       if (it != _initData->intSharedArraySet.end()) {
02189         return *it;
02190       }
02191       _initData->intSharedArraySet.insert(sia);
02192     }
02193     
02194     return sia;
02195   }
02196   IntSet
02197   FlatZincSpace::arg2intset(AST::Node* n) {
02198     AST::SetLit* sl = n->getSet();
02199     IntSet d;
02200     if (sl->interval) {
02201       d = IntSet(sl->min, sl->max);
02202     } else {
02203       Region re;
02204       int* is = re.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
02205       for (int i=sl->s.size(); i--; )
02206         is[i] = sl->s[i];
02207       d = IntSet(is, sl->s.size());
02208     }
02209     return d;
02210   }
02211   IntSetArgs
02212   FlatZincSpace::arg2intsetargs(AST::Node* arg, int offset) {
02213     AST::Array* a = arg->getArray();
02214     if (a->a.size() == 0) {
02215       IntSetArgs emptyIa(0);
02216       return emptyIa;
02217     }
02218     IntSetArgs ia(a->a.size()+offset);
02219     for (int i=offset; i--;)
02220       ia[i] = IntSet::empty;
02221     for (int i=a->a.size(); i--;) {
02222       ia[i+offset] = arg2intset(a->a[i]);
02223     }
02224     return ia;
02225   }
02226   IntVarArgs
02227   FlatZincSpace::arg2intvarargs(AST::Node* arg, int offset) {
02228     AST::Array* a = arg->getArray();
02229     if (a->a.size() == 0) {
02230       IntVarArgs emptyIa(0);
02231       return emptyIa;
02232     }
02233     IntVarArgs ia(a->a.size()+offset);
02234     for (int i=offset; i--;)
02235       ia[i] = IntVar(*this, 0, 0);
02236     for (int i=a->a.size(); i--;) {
02237       if (a->a[i]->isIntVar()) {
02238         ia[i+offset] = iv[a->a[i]->getIntVar()];
02239       } else {
02240         int value = a->a[i]->getInt();
02241         IntVar iv(*this, value, value);
02242         ia[i+offset] = iv;
02243       }
02244     }
02245     return ia;
02246   }
02247   BoolVarArgs
02248   FlatZincSpace::arg2boolvarargs(AST::Node* arg, int offset, int siv) {
02249     AST::Array* a = arg->getArray();
02250     if (a->a.size() == 0) {
02251       BoolVarArgs emptyIa(0);
02252       return emptyIa;
02253     }
02254     BoolVarArgs ia(a->a.size()+offset-(siv==-1?0:1));
02255     for (int i=offset; i--;)
02256       ia[i] = BoolVar(*this, 0, 0);
02257     for (int i=0; i<static_cast<int>(a->a.size()); i++) {
02258       if (i==siv)
02259         continue;
02260       if (a->a[i]->isBool()) {
02261         bool value = a->a[i]->getBool();
02262         BoolVar iv(*this, value, value);
02263         ia[offset++] = iv;
02264       } else if (a->a[i]->isIntVar() &&
02265                  aliasBool2Int(a->a[i]->getIntVar()) != -1) {
02266         ia[offset++] = bv[aliasBool2Int(a->a[i]->getIntVar())];
02267       } else {
02268         ia[offset++] = bv[a->a[i]->getBoolVar()];
02269       }
02270     }
02271     return ia;
02272   }
02273   BoolVar
02274   FlatZincSpace::arg2BoolVar(AST::Node* n) {
02275     BoolVar x0;
02276     if (n->isBool()) {
02277       x0 = BoolVar(*this, n->getBool(), n->getBool());
02278     }
02279     else {
02280       x0 = bv[n->getBoolVar()];
02281     }
02282     return x0;
02283   }
02284   IntVar
02285   FlatZincSpace::arg2IntVar(AST::Node* n) {
02286     IntVar x0;
02287     if (n->isIntVar()) {
02288       x0 = iv[n->getIntVar()];
02289     } else {
02290       x0 = IntVar(*this, n->getInt(), n->getInt());
02291     }
02292     return x0;
02293   }
02294   bool
02295   FlatZincSpace::isBoolArray(AST::Node* b, int& singleInt) {
02296     AST::Array* a = b->getArray();
02297     singleInt = -1;
02298     if (a->a.size() == 0)
02299       return true;
02300     for (int i=a->a.size(); i--;) {
02301       if (a->a[i]->isBoolVar() || a->a[i]->isBool()) {
02302       } else if (a->a[i]->isIntVar()) {
02303         if (aliasBool2Int(a->a[i]->getIntVar()) == -1) {
02304           if (singleInt != -1) {
02305             return false;
02306           }
02307           singleInt = i;
02308         }
02309       } else {
02310         return false;
02311       }
02312     }
02313     return singleInt==-1 || a->a.size() > 1;
02314   }
02315 #ifdef GECODE_HAS_SET_VARS
02316   SetVar
02317   FlatZincSpace::arg2SetVar(AST::Node* n) {
02318     SetVar x0;
02319     if (!n->isSetVar()) {
02320       IntSet d = arg2intset(n);
02321       x0 = SetVar(*this, d, d);
02322     } else {
02323       x0 = sv[n->getSetVar()];
02324     }
02325     return x0;
02326   }
02327   SetVarArgs
02328   FlatZincSpace::arg2setvarargs(AST::Node* arg, int offset, int doffset,
02329                                 const IntSet& od) {
02330     AST::Array* a = arg->getArray();
02331     SetVarArgs ia(a->a.size()+offset);
02332     for (int i=offset; i--;) {
02333       IntSet d = i<doffset ? od : IntSet::empty;
02334       ia[i] = SetVar(*this, d, d);
02335     }
02336     for (int i=a->a.size(); i--;) {
02337       ia[i+offset] = arg2SetVar(a->a[i]);
02338     }
02339     return ia;
02340   }
02341 #endif
02342 #ifdef GECODE_HAS_FLOAT_VARS
02343   FloatValArgs
02344   FlatZincSpace::arg2floatargs(AST::Node* arg, int offset) {
02345     AST::Array* a = arg->getArray();
02346     FloatValArgs fa(a->a.size()+offset);
02347     for (int i=offset; i--;)
02348       fa[i] = 0.0;
02349     for (int i=a->a.size(); i--;)
02350       fa[i+offset] = a->a[i]->getFloat();
02351     return fa;
02352   }
02353   FloatVarArgs
02354   FlatZincSpace::arg2floatvarargs(AST::Node* arg, int offset) {
02355     AST::Array* a = arg->getArray();
02356     if (a->a.size() == 0) {
02357       FloatVarArgs emptyFa(0);
02358       return emptyFa;
02359     }
02360     FloatVarArgs fa(a->a.size()+offset);
02361     for (int i=offset; i--;)
02362       fa[i] = FloatVar(*this, 0.0, 0.0);
02363     for (int i=a->a.size(); i--;) {
02364       if (a->a[i]->isFloatVar()) {
02365         fa[i+offset] = fv[a->a[i]->getFloatVar()];
02366       } else {
02367         double value = a->a[i]->getFloat();
02368         FloatVar fv(*this, value, value);
02369         fa[i+offset] = fv;
02370       }
02371     }
02372     return fa;
02373   }
02374   FloatVar
02375   FlatZincSpace::arg2FloatVar(AST::Node* n) {
02376     FloatVar x0;
02377     if (n->isFloatVar()) {
02378       x0 = fv[n->getFloatVar()];
02379     } else {
02380       x0 = FloatVar(*this, n->getFloat(), n->getFloat());
02381     }
02382     return x0;
02383   }
02384 #endif
02385   IntPropLevel
02386   FlatZincSpace::ann2ipl(AST::Node* ann) {
02387     if (ann) {
02388       if (ann->hasAtom("val"))
02389         return IPL_VAL;
02390       if (ann->hasAtom("domain"))
02391         return IPL_DOM;
02392       if (ann->hasAtom("bounds") ||
02393           ann->hasAtom("boundsR") ||
02394           ann->hasAtom("boundsD") ||
02395           ann->hasAtom("boundsZ"))
02396         return IPL_BND;
02397     }
02398     return IPL_DEF;
02399   }
02400 
02401   DFA
02402   FlatZincSpace::getSharedDFA(DFA& a) {
02403     if (_initData) {
02404       FlatZincSpaceInitData::DFASet::iterator it = _initData->dfaSet.find(a);
02405       if (it != _initData->dfaSet.end()) {
02406         return *it;
02407       }
02408       _initData->dfaSet.insert(a);
02409     }
02410     return a;
02411   }
02412 
02413   void
02414   Printer::init(AST::Array* output) {
02415     _output = output;
02416   }
02417 
02418   void
02419   Printer::printElem(std::ostream& out,
02420                        AST::Node* ai,
02421                        const Gecode::IntVarArray& iv,
02422                        const Gecode::BoolVarArray& bv
02423 #ifdef GECODE_HAS_SET_VARS
02424                        , const Gecode::SetVarArray& sv
02425 #endif
02426 #ifdef GECODE_HAS_FLOAT_VARS
02427                        ,
02428                        const Gecode::FloatVarArray& fv
02429 #endif
02430                        ) const {
02431     int k;
02432     if (ai->isInt(k)) {
02433       out << k;
02434     } else if (ai->isIntVar()) {
02435       out << iv[ai->getIntVar()];
02436     } else if (ai->isBoolVar()) {
02437       if (bv[ai->getBoolVar()].min() == 1) {
02438         out << "true";
02439       } else if (bv[ai->getBoolVar()].max() == 0) {
02440         out << "false";
02441       } else {
02442         out << "false..true";
02443       }
02444 #ifdef GECODE_HAS_SET_VARS
02445     } else if (ai->isSetVar()) {
02446       if (!sv[ai->getSetVar()].assigned()) {
02447         out << sv[ai->getSetVar()];
02448         return;
02449       }
02450       SetVarGlbRanges svr(sv[ai->getSetVar()]);
02451       if (!svr()) {
02452         out << "{}";
02453         return;
02454       }
02455       int min = svr.min();
02456       int max = svr.max();
02457       ++svr;
02458       if (svr()) {
02459         SetVarGlbValues svv(sv[ai->getSetVar()]);
02460         int i = svv.val();
02461         out << "{" << i;
02462         ++svv;
02463         for (; svv(); ++svv)
02464           out << ", " << svv.val();
02465         out << "}";
02466       } else {
02467         out << min << ".." << max;
02468       }
02469 #endif
02470 #ifdef GECODE_HAS_FLOAT_VARS
02471     } else if (ai->isFloatVar()) {
02472       if (fv[ai->getFloatVar()].assigned()) {
02473         FloatVal vv = fv[ai->getFloatVar()].val();
02474         FloatNum v;
02475         if (vv.singleton())
02476           v = vv.min();
02477         else if (vv < 0.0)
02478           v = vv.max();
02479         else
02480           v = vv.min();
02481         std::ostringstream oss;
02482         // oss << std::scientific;
02483         oss << std::setprecision(std::numeric_limits<double>::digits10);
02484         oss << v;
02485         if (oss.str().find(".") == std::string::npos)
02486           oss << ".0";
02487         out << oss.str();
02488       } else {
02489         out << fv[ai->getFloatVar()];
02490       }
02491 #endif
02492     } else if (ai->isBool()) {
02493       out << (ai->getBool() ? "true" : "false");
02494     } else if (ai->isSet()) {
02495       AST::SetLit* s = ai->getSet();
02496       if (s->interval) {
02497         out << s->min << ".." << s->max;
02498       } else {
02499         out << "{";
02500         for (unsigned int i=0; i<s->s.size(); i++) {
02501           out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
02502         }
02503       }
02504     } else if (ai->isString()) {
02505       std::string s = ai->getString();
02506       for (unsigned int i=0; i<s.size(); i++) {
02507         if (s[i] == '\\' && i<s.size()-1) {
02508           switch (s[i+1]) {
02509           case 'n': out << "\n"; break;
02510           case '\\': out << "\\"; break;
02511           case 't': out << "\t"; break;
02512           default: out << "\\" << s[i+1];
02513           }
02514           i++;
02515         } else {
02516           out << s[i];
02517         }
02518       }
02519     }
02520   }
02521 
02522   void
02523   Printer::printElemDiff(std::ostream& out,
02524                        AST::Node* ai,
02525                        const Gecode::IntVarArray& iv1,
02526                        const Gecode::IntVarArray& iv2,
02527                        const Gecode::BoolVarArray& bv1,
02528                        const Gecode::BoolVarArray& bv2
02529 #ifdef GECODE_HAS_SET_VARS
02530                        , const Gecode::SetVarArray& sv1,
02531                        const Gecode::SetVarArray& sv2
02532 #endif
02533 #ifdef GECODE_HAS_FLOAT_VARS
02534                        , const Gecode::FloatVarArray& fv1,
02535                        const Gecode::FloatVarArray& fv2
02536 #endif
02537                        ) const {
02538 #ifdef GECODE_HAS_GIST
02539     using namespace Gecode::Gist;
02540     int k;
02541     if (ai->isInt(k)) {
02542       out << k;
02543     } else if (ai->isIntVar()) {
02544       std::string res(Comparator::compare("",iv1[ai->getIntVar()],
02545                                           iv2[ai->getIntVar()]));
02546       if (res.length() > 0) {
02547         res.erase(0, 1); // Remove '='
02548         out << res;
02549       } else {
02550         out << iv1[ai->getIntVar()];
02551       }
02552     } else if (ai->isBoolVar()) {
02553       std::string res(Comparator::compare("",bv1[ai->getBoolVar()],
02554                                           bv2[ai->getBoolVar()]));
02555       if (res.length() > 0) {
02556         res.erase(0, 1); // Remove '='
02557         out << res;
02558       } else {
02559         out << bv1[ai->getBoolVar()];
02560       }
02561 #ifdef GECODE_HAS_SET_VARS
02562     } else if (ai->isSetVar()) {
02563       std::string res(Comparator::compare("",sv1[ai->getSetVar()],
02564                                           sv2[ai->getSetVar()]));
02565       if (res.length() > 0) {
02566         res.erase(0, 1); // Remove '='
02567         out << res;
02568       } else {
02569         out << sv1[ai->getSetVar()];
02570       }
02571 #endif
02572 #ifdef GECODE_HAS_FLOAT_VARS
02573     } else if (ai->isFloatVar()) {
02574       std::string res(Comparator::compare("",fv1[ai->getFloatVar()],
02575                                           fv2[ai->getFloatVar()]));
02576       if (res.length() > 0) {
02577         res.erase(0, 1); // Remove '='
02578         out << res;
02579       } else {
02580         out << fv1[ai->getFloatVar()];
02581       }
02582 #endif
02583     } else if (ai->isBool()) {
02584       out << (ai->getBool() ? "true" : "false");
02585     } else if (ai->isSet()) {
02586       AST::SetLit* s = ai->getSet();
02587       if (s->interval) {
02588         out << s->min << ".." << s->max;
02589       } else {
02590         out << "{";
02591         for (unsigned int i=0; i<s->s.size(); i++) {
02592           out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
02593         }
02594       }
02595     } else if (ai->isString()) {
02596       std::string s = ai->getString();
02597       for (unsigned int i=0; i<s.size(); i++) {
02598         if (s[i] == '\\' && i<s.size()-1) {
02599           switch (s[i+1]) {
02600           case 'n': out << "\n"; break;
02601           case '\\': out << "\\"; break;
02602           case 't': out << "\t"; break;
02603           default: out << "\\" << s[i+1];
02604           }
02605           i++;
02606         } else {
02607           out << s[i];
02608         }
02609       }
02610     }
02611 #else
02612     (void) out;
02613     (void) ai;
02614     (void) iv1;
02615     (void) iv2;
02616     (void) bv1;
02617     (void) bv2;
02618 #ifdef GECODE_HAS_SET_VARS
02619     (void) sv1;
02620     (void) sv2;
02621 #endif
02622 #ifdef GECODE_HAS_FLOAT_VARS
02623     (void) fv1;
02624     (void) fv2;
02625 #endif
02626 
02627 #endif
02628   }
02629 
02630   void
02631   Printer::print(std::ostream& out,
02632                    const Gecode::IntVarArray& iv,
02633                    const Gecode::BoolVarArray& bv
02634 #ifdef GECODE_HAS_SET_VARS
02635                    ,
02636                    const Gecode::SetVarArray& sv
02637 #endif
02638 #ifdef GECODE_HAS_FLOAT_VARS
02639                    ,
02640                    const Gecode::FloatVarArray& fv
02641 #endif
02642                    ) const {
02643     if (_output == NULL)
02644       return;
02645     for (unsigned int i=0; i< _output->a.size(); i++) {
02646       AST::Node* ai = _output->a[i];
02647       if (ai->isArray()) {
02648         AST::Array* aia = ai->getArray();
02649         int size = aia->a.size();
02650         out << "[";
02651         for (int j=0; j<size; j++) {
02652           printElem(out,aia->a[j],iv,bv
02653 #ifdef GECODE_HAS_SET_VARS
02654           ,sv
02655 #endif
02656 #ifdef GECODE_HAS_FLOAT_VARS
02657           ,fv
02658 #endif
02659           );
02660           if (j<size-1)
02661             out << ", ";
02662         }
02663         out << "]";
02664       } else {
02665         printElem(out,ai,iv,bv
02666 #ifdef GECODE_HAS_SET_VARS
02667         ,sv
02668 #endif
02669 #ifdef GECODE_HAS_FLOAT_VARS
02670           ,fv
02671 #endif
02672         );
02673       }
02674     }
02675   }
02676 
02677   void
02678   Printer::printDiff(std::ostream& out,
02679                    const Gecode::IntVarArray& iv1,
02680                    const Gecode::IntVarArray& iv2,
02681                    const Gecode::BoolVarArray& bv1,
02682                    const Gecode::BoolVarArray& bv2
02683 #ifdef GECODE_HAS_SET_VARS
02684                    ,
02685                    const Gecode::SetVarArray& sv1,
02686                    const Gecode::SetVarArray& sv2
02687 #endif
02688 #ifdef GECODE_HAS_FLOAT_VARS
02689                    ,
02690                    const Gecode::FloatVarArray& fv1,
02691                    const Gecode::FloatVarArray& fv2
02692 #endif
02693                    ) const {
02694     if (_output == NULL)
02695       return;
02696     for (unsigned int i=0; i< _output->a.size(); i++) {
02697       AST::Node* ai = _output->a[i];
02698       if (ai->isArray()) {
02699         AST::Array* aia = ai->getArray();
02700         int size = aia->a.size();
02701         out << "[";
02702         for (int j=0; j<size; j++) {
02703           printElemDiff(out,aia->a[j],iv1,iv2,bv1,bv2
02704 #ifdef GECODE_HAS_SET_VARS
02705             ,sv1,sv2
02706 #endif
02707 #ifdef GECODE_HAS_FLOAT_VARS
02708             ,fv1,fv2
02709 #endif
02710           );
02711           if (j<size-1)
02712             out << ", ";
02713         }
02714         out << "]";
02715       } else {
02716         printElemDiff(out,ai,iv1,iv2,bv1,bv2
02717 #ifdef GECODE_HAS_SET_VARS
02718           ,sv1,sv2
02719 #endif
02720 #ifdef GECODE_HAS_FLOAT_VARS
02721             ,fv1,fv2
02722 #endif
02723         );
02724       }
02725     }
02726   }
02727 
02728   void
02729   Printer::addIntVarName(const std::string& n) {
02730     iv_names.push_back(n);
02731   }
02732   void
02733   Printer::addBoolVarName(const std::string& n) {
02734     bv_names.push_back(n);
02735   }
02736 #ifdef GECODE_HAS_FLOAT_VARS
02737   void
02738   Printer::addFloatVarName(const std::string& n) {
02739     fv_names.push_back(n);
02740   }
02741 #endif
02742 #ifdef GECODE_HAS_SET_VARS
02743   void
02744   Printer::addSetVarName(const std::string& n) {
02745     sv_names.push_back(n);
02746   }
02747 #endif
02748 
02749   void
02750   Printer::shrinkElement(AST::Node* node,
02751                          std::map<int,int>& iv, std::map<int,int>& bv,
02752                          std::map<int,int>& sv, std::map<int,int>& fv) {
02753     if (node->isIntVar()) {
02754       AST::IntVar* x = static_cast<AST::IntVar*>(node);
02755       if (iv.find(x->i) == iv.end()) {
02756         int newi = iv.size();
02757         iv[x->i] = newi;
02758       }
02759       x->i = iv[x->i];
02760     } else if (node->isBoolVar()) {
02761       AST::BoolVar* x = static_cast<AST::BoolVar*>(node);
02762       if (bv.find(x->i) == bv.end()) {
02763         int newi = bv.size();
02764         bv[x->i] = newi;
02765       }
02766       x->i = bv[x->i];
02767     } else if (node->isSetVar()) {
02768       AST::SetVar* x = static_cast<AST::SetVar*>(node);
02769       if (sv.find(x->i) == sv.end()) {
02770         int newi = sv.size();
02771         sv[x->i] = newi;
02772       }
02773       x->i = sv[x->i];
02774     } else if (node->isFloatVar()) {
02775       AST::FloatVar* x = static_cast<AST::FloatVar*>(node);
02776       if (fv.find(x->i) == fv.end()) {
02777         int newi = fv.size();
02778         fv[x->i] = newi;
02779       }
02780       x->i = fv[x->i];
02781     }
02782   }
02783 
02784   void
02785   Printer::shrinkArrays(Space& home,
02786                         int& optVar, bool optVarIsInt,
02787                         Gecode::IntVarArray& iv,
02788                         Gecode::BoolVarArray& bv
02789 #ifdef GECODE_HAS_SET_VARS
02790                         ,
02791                         Gecode::SetVarArray& sv
02792 #endif
02793 #ifdef GECODE_HAS_FLOAT_VARS
02794                         ,
02795                         Gecode::FloatVarArray& fv
02796 #endif
02797                        ) {
02798     if (_output == NULL) {
02799       if (optVarIsInt && optVar != -1) {
02800         IntVar ov = iv[optVar];
02801         iv = IntVarArray(home, 1);
02802         iv[0] = ov;
02803         optVar = 0;
02804       } else {
02805         iv = IntVarArray(home, 0);
02806       }
02807       bv = BoolVarArray(home, 0);
02808 #ifdef GECODE_HAS_SET_VARS
02809       sv = SetVarArray(home, 0);
02810 #endif
02811 #ifdef GECODE_HAS_FLOAT_VARS
02812       if (!optVarIsInt && optVar != -1) {
02813         FloatVar ov = fv[optVar];
02814         fv = FloatVarArray(home, 1);
02815         fv[0] = ov;
02816         optVar = 0;
02817       } else {
02818         fv = FloatVarArray(home,0);
02819       }
02820 #endif
02821       return;
02822     }
02823     std::map<int,int> iv_new;
02824     std::map<int,int> bv_new;
02825     std::map<int,int> sv_new;
02826     std::map<int,int> fv_new;
02827 
02828     if (optVar != -1) {
02829       if (optVarIsInt)
02830         iv_new[optVar] = 0;
02831       else
02832         fv_new[optVar] = 0;
02833       optVar = 0;
02834     }
02835 
02836     for (unsigned int i=0; i< _output->a.size(); i++) {
02837       AST::Node* ai = _output->a[i];
02838       if (ai->isArray()) {
02839         AST::Array* aia = ai->getArray();
02840         for (unsigned int j=0; j<aia->a.size(); j++) {
02841           shrinkElement(aia->a[j],iv_new,bv_new,sv_new,fv_new);
02842         }
02843       } else {
02844         shrinkElement(ai,iv_new,bv_new,sv_new,fv_new);
02845       }
02846     }
02847 
02848     IntVarArgs iva(iv_new.size());
02849     for (std::map<int,int>::iterator i=iv_new.begin(); i != iv_new.end(); ++i) {
02850       iva[(*i).second] = iv[(*i).first];
02851     }
02852     iv = IntVarArray(home, iva);
02853 
02854     BoolVarArgs bva(bv_new.size());
02855     for (std::map<int,int>::iterator i=bv_new.begin(); i != bv_new.end(); ++i) {
02856       bva[(*i).second] = bv[(*i).first];
02857     }
02858     bv = BoolVarArray(home, bva);
02859 
02860 #ifdef GECODE_HAS_SET_VARS
02861     SetVarArgs sva(sv_new.size());
02862     for (std::map<int,int>::iterator i=sv_new.begin(); i != sv_new.end(); ++i) {
02863       sva[(*i).second] = sv[(*i).first];
02864     }
02865     sv = SetVarArray(home, sva);
02866 #endif
02867 
02868 #ifdef GECODE_HAS_FLOAT_VARS
02869     FloatVarArgs fva(fv_new.size());
02870     for (std::map<int,int>::iterator i=fv_new.begin(); i != fv_new.end(); ++i) {
02871       fva[(*i).second] = fv[(*i).first];
02872     }
02873     fv = FloatVarArray(home, fva);
02874 #endif
02875   }
02876 
02877   Printer::~Printer(void) {
02878     delete _output;
02879   }
02880 
02881 }}
02882 
02883 // STATISTICS: flatzinc-any