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