Generated on Wed Nov 5 2014 05:18:16 for Gecode by doxygen 1.7.6.1
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: 2013-08-29 02:46:26 +0200 (Thu, 29 Aug 2013) $ by $Author: tack $
00015  *     $Revision: 13990 $
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<IntVarBranch> bool_varsel0,
00076                    IntValBranch 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<IntVarBranch> bool_varsel;
00124     IntValBranch 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<IntVarBranch> bool_varsel,
00202                      IntValBranch 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(const BrancherHandle& bh,
00250              const string& rel0,
00251              const string& rel1,
00252              const vector<string>& n) {
00253       v.resize(std::max(static_cast<unsigned int>(v.size()),bh.id()+1));
00254       v[bh.id()] = BI(rel0,rel1,n);
00255     }
00257     void print(const BrancherHandle& bh,
00258                int a, int i, int n, ostream& o) const {
00259       const BI& bi = v[bh.id()];
00260       o << bi.n[i] << " " << (a==0 ? bi.r0 : bi.r1) << " " << n;
00261     }
00262 #ifdef GECODE_HAS_FLOAT_VARS
00263     void print(const BrancherHandle& bh,
00264                int a, int i, const FloatNumBranch& nl, ostream& o) const {
00265       const BI& bi = v[bh.id()];
00266       o << bi.n[i] << " "
00267         << (((a == 0) == nl.l) ? "<=" : ">=") << nl.n;
00268     }
00269 #endif
00270   };
00271   
00272   BranchInformation::BranchInformation(void)
00273     : SharedHandle(NULL) {}
00274 
00275   BranchInformation::BranchInformation(const BranchInformation& bi)
00276     : SharedHandle(bi) {}
00277 
00278   void
00279   BranchInformation::init(void) {
00280     assert(object() == 0);
00281     object(new BranchInformationO());
00282   }
00283 
00284   void
00285   BranchInformation::add(const BrancherHandle& bh,
00286                          const std::string& rel0,
00287                          const std::string& rel1,
00288                          const std::vector<std::string>& n) {
00289     static_cast<BranchInformationO*>(object())->add(bh,rel0,rel1,n);
00290   }
00291   void
00292   BranchInformation::print(const BrancherHandle& bh, int a, int i,
00293                            int n, std::ostream& o) const {
00294     static_cast<const BranchInformationO*>(object())->print(bh,a,i,n,o);
00295   }
00296 #ifdef GECODE_HAS_FLOAT_VARS
00297   void
00298   BranchInformation::print(const BrancherHandle& bh, int a, int i,
00299                            const FloatNumBranch& nl, std::ostream& o) const {
00300     static_cast<const BranchInformationO*>(object())->print(bh,a,i,nl,o);
00301   }
00302 #endif
00303   template<class Var>
00304   void varValPrint(const Space &home, const BrancherHandle& bh,
00305                    unsigned int a,
00306                    Var, int i, const int& n,
00307                    std::ostream& o) {
00308     static_cast<const FlatZincSpace&>(home).branchInfo.print(bh,a,i,n,o);
00309   }
00310 
00311 #ifdef GECODE_HAS_FLOAT_VARS
00312   void varValPrintF(const Space &home, const BrancherHandle& bh,
00313                     unsigned int a,
00314                     FloatVar, int i, const FloatNumBranch& nl,
00315                     std::ostream& o) {
00316     static_cast<const FlatZincSpace&>(home).branchInfo.print(bh,a,i,nl,o);
00317   }
00318 #endif
00319 
00320   IntSet vs2is(IntVarSpec* vs) {
00321     if (vs->assigned) {
00322       return IntSet(vs->i,vs->i);
00323     }
00324     if (vs->domain()) {
00325       AST::SetLit* sl = vs->domain.some();
00326       if (sl->interval) {
00327         return IntSet(sl->min, sl->max);
00328       } else {
00329         int* newdom = heap.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
00330         for (int i=sl->s.size(); i--;)
00331           newdom[i] = sl->s[i];
00332         IntSet ret(newdom, sl->s.size());
00333         heap.free(newdom, static_cast<unsigned long int>(sl->s.size()));
00334         return ret;
00335       }
00336     }
00337     return IntSet(Int::Limits::min, Int::Limits::max);
00338   }
00339 
00340   int vs2bsl(BoolVarSpec* bs) {
00341     if (bs->assigned) {
00342       return bs->i;
00343     }
00344     if (bs->domain()) {
00345       AST::SetLit* sl = bs->domain.some();
00346       assert(sl->interval);
00347       return std::min(1, std::max(0, sl->min));
00348     }
00349     return 0;
00350   }
00351 
00352   int vs2bsh(BoolVarSpec* bs) {
00353     if (bs->assigned) {
00354       return bs->i;
00355     }
00356     if (bs->domain()) {
00357       AST::SetLit* sl = bs->domain.some();
00358       assert(sl->interval);
00359       return std::max(0, std::min(1, sl->max));
00360     }
00361     return 1;
00362   }
00363 
00364   TieBreak<IntVarBranch> ann2ivarsel(AST::Node* ann, Rnd rnd, double decay) {
00365     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00366       if (s->id == "input_order")
00367         return TieBreak<IntVarBranch>(INT_VAR_NONE());
00368       if (s->id == "first_fail")
00369         return TieBreak<IntVarBranch>(INT_VAR_SIZE_MIN());
00370       if (s->id == "anti_first_fail")
00371         return TieBreak<IntVarBranch>(INT_VAR_SIZE_MAX());
00372       if (s->id == "smallest")
00373         return TieBreak<IntVarBranch>(INT_VAR_MIN_MIN());
00374       if (s->id == "largest")
00375         return TieBreak<IntVarBranch>(INT_VAR_MAX_MAX());
00376       if (s->id == "occurrence")
00377         return TieBreak<IntVarBranch>(INT_VAR_DEGREE_MAX());
00378       if (s->id == "max_regret")
00379         return TieBreak<IntVarBranch>(INT_VAR_REGRET_MIN_MAX());
00380       if (s->id == "most_constrained")
00381         return TieBreak<IntVarBranch>(INT_VAR_SIZE_MIN(),
00382                                       INT_VAR_DEGREE_MAX());
00383       if (s->id == "random") {
00384         return TieBreak<IntVarBranch>(INT_VAR_RND(rnd));
00385       }
00386       if (s->id == "afc_min")
00387         return TieBreak<IntVarBranch>(INT_VAR_AFC_MIN(decay));
00388       if (s->id == "afc_max")
00389         return TieBreak<IntVarBranch>(INT_VAR_AFC_MAX(decay));
00390       if (s->id == "afc_size_min")
00391         return TieBreak<IntVarBranch>(INT_VAR_AFC_SIZE_MIN(decay));
00392       if (s->id == "afc_size_max") {
00393         return TieBreak<IntVarBranch>(INT_VAR_AFC_SIZE_MAX(decay));
00394       }
00395       if (s->id == "activity_min")
00396         return TieBreak<IntVarBranch>(INT_VAR_ACTIVITY_MIN(decay));
00397       if (s->id == "activity_max")
00398         return TieBreak<IntVarBranch>(INT_VAR_ACTIVITY_MAX(decay));
00399       if (s->id == "activity_size_min")
00400         return TieBreak<IntVarBranch>(INT_VAR_ACTIVITY_SIZE_MIN(decay));
00401       if (s->id == "activity_size_max")
00402         return TieBreak<IntVarBranch>(INT_VAR_ACTIVITY_SIZE_MAX(decay));
00403     }
00404     std::cerr << "Warning, ignored search annotation: ";
00405     ann->print(std::cerr);
00406     std::cerr << std::endl;
00407     return TieBreak<IntVarBranch>(INT_VAR_NONE());
00408   }
00409 
00410   IntValBranch ann2ivalsel(AST::Node* ann, std::string& r0, std::string& r1,
00411                            Rnd rnd) {
00412     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00413       if (s->id == "indomain_min") {
00414         r0 = "="; r1 = "!=";
00415         return INT_VAL_MIN();
00416       }
00417       if (s->id == "indomain_max") {
00418         r0 = "="; r1 = "!=";
00419         return INT_VAL_MAX();
00420       }
00421       if (s->id == "indomain_median") {
00422         r0 = "="; r1 = "!=";
00423         return INT_VAL_MED();
00424       }
00425       if (s->id == "indomain_split") {
00426         r0 = "<="; r1 = ">";
00427         return INT_VAL_SPLIT_MIN();
00428       }
00429       if (s->id == "indomain_reverse_split") {
00430         r0 = ">"; r1 = "<=";
00431         return INT_VAL_SPLIT_MAX();
00432       }
00433       if (s->id == "indomain_random") {
00434         r0 = "="; r1 = "!=";
00435         return INT_VAL_RND(rnd);
00436       }
00437       if (s->id == "indomain") {
00438         r0 = "="; r1 = "=";
00439         return INT_VALUES_MIN();
00440       }
00441       if (s->id == "indomain_middle") {
00442         std::cerr << "Warning, replacing unsupported annotation "
00443                   << "indomain_middle with indomain_median" << std::endl;
00444         r0 = "="; r1 = "!=";
00445         return INT_VAL_MED();
00446       }
00447       if (s->id == "indomain_interval") {
00448         std::cerr << "Warning, replacing unsupported annotation "
00449                   << "indomain_interval with indomain_split" << std::endl;
00450         r0 = "<="; r1 = ">";
00451         return INT_VAL_SPLIT_MIN();
00452       }
00453     }
00454     std::cerr << "Warning, ignored search annotation: ";
00455     ann->print(std::cerr);
00456     std::cerr << std::endl;
00457     r0 = "="; r1 = "!=";
00458     return INT_VAL_MIN();
00459   }
00460 
00461   IntAssign ann2asnivalsel(AST::Node* ann, Rnd rnd) {
00462     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00463       if (s->id == "indomain_min")
00464         return INT_ASSIGN_MIN();
00465       if (s->id == "indomain_max")
00466         return INT_ASSIGN_MAX();
00467       if (s->id == "indomain_median")
00468         return INT_ASSIGN_MED();
00469       if (s->id == "indomain_random") {
00470         return INT_ASSIGN_RND(rnd);
00471       }
00472     }
00473     std::cerr << "Warning, ignored search annotation: ";
00474     ann->print(std::cerr);
00475     std::cerr << std::endl;
00476     return INT_ASSIGN_MIN();
00477   }
00478 
00479 #ifdef GECODE_HAS_SET_VARS
00480   SetVarBranch ann2svarsel(AST::Node* ann, Rnd rnd, double decay) {
00481     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00482       if (s->id == "input_order")
00483         return SET_VAR_NONE();
00484       if (s->id == "first_fail")
00485         return SET_VAR_SIZE_MIN();
00486       if (s->id == "anti_first_fail")
00487         return SET_VAR_SIZE_MAX();
00488       if (s->id == "smallest")
00489         return SET_VAR_MIN_MIN();
00490       if (s->id == "largest")
00491         return SET_VAR_MAX_MAX();
00492       if (s->id == "afc_min")
00493         return SET_VAR_AFC_MIN(decay);
00494       if (s->id == "afc_max")
00495         return SET_VAR_AFC_MAX(decay);
00496       if (s->id == "afc_size_min")
00497         return SET_VAR_AFC_SIZE_MIN(decay);
00498       if (s->id == "afc_size_max")
00499         return SET_VAR_AFC_SIZE_MAX(decay);
00500       if (s->id == "activity_min")
00501         return SET_VAR_ACTIVITY_MIN(decay);
00502       if (s->id == "activity_max")
00503         return SET_VAR_ACTIVITY_MAX(decay);
00504       if (s->id == "activity_size_min")
00505         return SET_VAR_ACTIVITY_SIZE_MIN(decay);
00506       if (s->id == "activity_size_max")
00507         return SET_VAR_ACTIVITY_SIZE_MAX(decay);
00508       if (s->id == "random") {
00509         return SET_VAR_RND(rnd);
00510       }
00511     }
00512     std::cerr << "Warning, ignored search annotation: ";
00513     ann->print(std::cerr);
00514     std::cerr << std::endl;
00515     return SET_VAR_NONE();
00516   }
00517 
00518   SetValBranch ann2svalsel(AST::Node* ann, std::string r0, std::string r1,
00519                            Rnd rnd) {
00520     (void) rnd;
00521     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00522       if (s->id == "indomain_min") {
00523         r0 = "in"; r1 = "not in";
00524         return SET_VAL_MIN_INC();
00525       }
00526       if (s->id == "indomain_max") {
00527         r0 = "in"; r1 = "not in";
00528         return SET_VAL_MAX_INC();
00529       }
00530       if (s->id == "outdomain_min") {
00531         r1 = "in"; r0 = "not in";
00532         return SET_VAL_MIN_EXC();
00533       }
00534       if (s->id == "outdomain_max") {
00535         r1 = "in"; r0 = "not in";
00536         return SET_VAL_MAX_EXC();
00537       }
00538     }
00539     std::cerr << "Warning, ignored search annotation: ";
00540     ann->print(std::cerr);
00541     std::cerr << std::endl;
00542     r0 = "in"; r1 = "not in";
00543     return SET_VAL_MIN_INC();
00544   }
00545 #endif
00546 
00547 #ifdef GECODE_HAS_FLOAT_VARS
00548   TieBreak<FloatVarBranch> ann2fvarsel(AST::Node* ann, Rnd rnd,
00549                                        double decay) {
00550     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00551       if (s->id == "input_order")
00552         return TieBreak<FloatVarBranch>(FLOAT_VAR_NONE());
00553       if (s->id == "first_fail")
00554         return TieBreak<FloatVarBranch>(FLOAT_VAR_SIZE_MIN());
00555       if (s->id == "anti_first_fail")
00556         return TieBreak<FloatVarBranch>(FLOAT_VAR_SIZE_MAX());
00557       if (s->id == "smallest")
00558         return TieBreak<FloatVarBranch>(FLOAT_VAR_MIN_MIN());
00559       if (s->id == "largest")
00560         return TieBreak<FloatVarBranch>(FLOAT_VAR_MAX_MAX());
00561       if (s->id == "occurrence")
00562         return TieBreak<FloatVarBranch>(FLOAT_VAR_DEGREE_MAX());
00563       if (s->id == "most_constrained")
00564         return TieBreak<FloatVarBranch>(FLOAT_VAR_SIZE_MIN(),
00565                                         FLOAT_VAR_DEGREE_MAX());
00566       if (s->id == "random") {
00567         return TieBreak<FloatVarBranch>(FLOAT_VAR_RND(rnd));
00568       }
00569       if (s->id == "afc_min")
00570         return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_MIN(decay));
00571       if (s->id == "afc_max")
00572         return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_MAX(decay));
00573       if (s->id == "afc_size_min")
00574         return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_SIZE_MIN(decay));
00575       if (s->id == "afc_size_max")
00576         return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_SIZE_MAX(decay));
00577       if (s->id == "activity_min")
00578         return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTIVITY_MIN(decay));
00579       if (s->id == "activity_max")
00580         return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTIVITY_MAX(decay));
00581       if (s->id == "activity_size_min")
00582         return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTIVITY_SIZE_MIN(decay));
00583       if (s->id == "activity_size_max")
00584         return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTIVITY_SIZE_MAX(decay));
00585     }
00586     std::cerr << "Warning, ignored search annotation: ";
00587     ann->print(std::cerr);
00588     std::cerr << std::endl;
00589     return TieBreak<FloatVarBranch>(FLOAT_VAR_NONE());
00590   }
00591 
00592   FloatValBranch ann2fvalsel(AST::Node* ann, std::string r0, std::string r1) {
00593     if (AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
00594       if (s->id == "indomain_split") {
00595         r0 = "<="; r1 = ">";
00596         return FLOAT_VAL_SPLIT_MIN();
00597       }
00598       if (s->id == "indomain_reverse_split") {
00599         r1 = "<="; r0 = ">";
00600         return FLOAT_VAL_SPLIT_MAX();
00601       }
00602     }
00603     std::cerr << "Warning, ignored search annotation: ";
00604     ann->print(std::cerr);
00605     std::cerr << std::endl;
00606     r0 = "<="; r1 = ">";
00607     return FLOAT_VAL_SPLIT_MIN();
00608   }
00609 
00610 #endif
00611 
00612   FlatZincSpace::FlatZincSpace(bool share, FlatZincSpace& f)
00613     : Space(share, f), _solveAnnotations(NULL), iv_boolalias(NULL),
00614       needAuxVars(f.needAuxVars) {
00615       _optVar = f._optVar;
00616       _optVarIsInt = f._optVarIsInt;
00617       _method = f._method;
00618       branchInfo.update(*this, share, f.branchInfo);
00619       iv.update(*this, share, f.iv);
00620       intVarCount = f.intVarCount;
00621       
00622       if (needAuxVars) {
00623         IntVarArgs iva;
00624         for (int i=0; i<f.iv_aux.size(); i++) {
00625           if (!f.iv_aux[i].assigned()) {
00626             iva << IntVar();
00627             iva[iva.size()-1].update(*this, share, f.iv_aux[i]);
00628           }
00629         }
00630         iv_aux = IntVarArray(*this, iva);
00631       }
00632       
00633       bv.update(*this, share, f.bv);
00634       boolVarCount = f.boolVarCount;
00635       if (needAuxVars) {
00636         BoolVarArgs bva;
00637         for (int i=0; i<f.bv_aux.size(); i++) {
00638           if (!f.bv_aux[i].assigned()) {
00639             bva << BoolVar();
00640             bva[bva.size()-1].update(*this, share, f.bv_aux[i]);
00641           }
00642         }
00643         bv_aux = BoolVarArray(*this, bva);
00644       }
00645 
00646 #ifdef GECODE_HAS_SET_VARS
00647       sv.update(*this, share, f.sv);
00648       setVarCount = f.setVarCount;
00649       if (needAuxVars) {
00650         SetVarArgs sva;
00651         for (int i=0; i<f.sv_aux.size(); i++) {
00652           if (!f.sv_aux[i].assigned()) {
00653             sva << SetVar();
00654             sva[sva.size()-1].update(*this, share, f.sv_aux[i]);
00655           }
00656         }
00657         sv_aux = SetVarArray(*this, sva);
00658       }
00659 #endif
00660 #ifdef GECODE_HAS_FLOAT_VARS
00661       fv.update(*this, share, f.fv);
00662       floatVarCount = f.floatVarCount;
00663       if (needAuxVars) {
00664         FloatVarArgs fva;
00665         for (int i=0; i<f.fv_aux.size(); i++) {
00666           if (!f.fv_aux[i].assigned()) {
00667             fva << FloatVar();
00668             fva[fva.size()-1].update(*this, share, f.fv_aux[i]);
00669           }
00670         }
00671         fv_aux = FloatVarArray(*this, fva);
00672       }
00673 #endif
00674     }
00675   
00676   FlatZincSpace::FlatZincSpace(void)
00677   : intVarCount(-1), boolVarCount(-1), floatVarCount(-1), setVarCount(-1),
00678     _optVar(-1), _optVarIsInt(true), 
00679     _solveAnnotations(NULL), needAuxVars(true) {
00680     branchInfo.init();
00681   }
00682 
00683   void
00684   FlatZincSpace::init(int intVars, int boolVars,
00685                       int setVars, int floatVars) {
00686     (void) setVars;
00687     (void) floatVars;
00688 
00689     intVarCount = 0;
00690     iv = IntVarArray(*this, intVars);
00691     iv_introduced = std::vector<bool>(2*intVars);
00692     iv_boolalias = alloc<int>(intVars+(intVars==0?1:0));
00693     boolVarCount = 0;
00694     bv = BoolVarArray(*this, boolVars);
00695     bv_introduced = std::vector<bool>(2*boolVars);
00696 #ifdef GECODE_HAS_SET_VARS
00697     setVarCount = 0;
00698     sv = SetVarArray(*this, setVars);
00699     sv_introduced = std::vector<bool>(2*setVars);
00700 #endif
00701 #ifdef GECODE_HAS_FLOAT_VARS
00702     floatVarCount = 0;
00703     fv = FloatVarArray(*this, floatVars);
00704     fv_introduced = std::vector<bool>(2*floatVars);
00705 #endif
00706   }
00707 
00708   void
00709   FlatZincSpace::newIntVar(IntVarSpec* vs) {
00710     if (vs->alias) {
00711       iv[intVarCount++] = iv[vs->i];
00712     } else {
00713       IntSet dom(vs2is(vs));
00714       if (dom.size()==0) {
00715         fail();
00716         return;
00717       } else {
00718         iv[intVarCount++] = IntVar(*this, dom);
00719       }
00720     }
00721     iv_introduced[2*(intVarCount-1)] = vs->introduced;
00722     iv_introduced[2*(intVarCount-1)+1] = vs->funcDep;
00723     iv_boolalias[intVarCount-1] = -1;
00724   }
00725 
00726   void
00727   FlatZincSpace::aliasBool2Int(int iv, int bv) {
00728     iv_boolalias[iv] = bv;
00729   }
00730   int
00731   FlatZincSpace::aliasBool2Int(int iv) {
00732     return iv_boolalias[iv];
00733   }
00734 
00735   void
00736   FlatZincSpace::newBoolVar(BoolVarSpec* vs) {
00737     if (vs->alias) {
00738       bv[boolVarCount++] = bv[vs->i];
00739     } else {
00740       bv[boolVarCount++] = BoolVar(*this, vs2bsl(vs), vs2bsh(vs));
00741     }
00742     bv_introduced[2*(boolVarCount-1)] = vs->introduced;
00743     bv_introduced[2*(boolVarCount-1)+1] = vs->funcDep;
00744   }
00745 
00746 #ifdef GECODE_HAS_SET_VARS
00747   void
00748   FlatZincSpace::newSetVar(SetVarSpec* vs) {
00749     if (vs->alias) {
00750       sv[setVarCount++] = sv[vs->i];
00751     } else if (vs->assigned) {
00752       assert(vs->upperBound());
00753       AST::SetLit* vsv = vs->upperBound.some();
00754       if (vsv->interval) {
00755         IntSet d(vsv->min, vsv->max);
00756         sv[setVarCount++] = SetVar(*this, d, d);
00757       } else {
00758         int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
00759         for (int i=vsv->s.size(); i--; )
00760           is[i] = vsv->s[i];
00761         IntSet d(is, vsv->s.size());
00762         heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
00763         sv[setVarCount++] = SetVar(*this, d, d);
00764       }
00765     } else if (vs->upperBound()) {
00766       AST::SetLit* vsv = vs->upperBound.some();
00767       if (vsv->interval) {
00768         IntSet d(vsv->min, vsv->max);
00769         sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
00770       } else {
00771         int* is = heap.alloc<int>(static_cast<unsigned long int>(vsv->s.size()));
00772         for (int i=vsv->s.size(); i--; )
00773           is[i] = vsv->s[i];
00774         IntSet d(is, vsv->s.size());
00775         heap.free(is,static_cast<unsigned long int>(vsv->s.size()));
00776         sv[setVarCount++] = SetVar(*this, IntSet::empty, d);
00777       }
00778     } else {
00779       sv[setVarCount++] = SetVar(*this, IntSet::empty,
00780                                  IntSet(Set::Limits::min, 
00781                                         Set::Limits::max));
00782     }
00783     sv_introduced[2*(setVarCount-1)] = vs->introduced;
00784     sv_introduced[2*(setVarCount-1)+1] = vs->funcDep;
00785   }
00786 #else
00787   void
00788   FlatZincSpace::newSetVar(SetVarSpec*) {
00789     throw FlatZinc::Error("Gecode", "set variables not supported");
00790   }
00791 #endif
00792 
00793 #ifdef GECODE_HAS_FLOAT_VARS
00794   void
00795   FlatZincSpace::newFloatVar(FloatVarSpec* vs) {
00796     if (vs->alias) {
00797       fv[floatVarCount++] = fv[vs->i];
00798     } else {
00799       double dmin, dmax;
00800       if (vs->domain()) {
00801         dmin = vs->domain.some().first;
00802         dmax = vs->domain.some().second;
00803         if (dmin > dmax) {
00804           fail();
00805           return;
00806         }
00807       } else {
00808         dmin = Float::Limits::min;
00809         dmax = Float::Limits::max;
00810       }
00811       fv[floatVarCount++] = FloatVar(*this, dmin, dmax);
00812     }
00813     fv_introduced[2*(floatVarCount-1)] = vs->introduced;
00814     fv_introduced[2*(floatVarCount-1)+1] = vs->funcDep;
00815   }
00816 #else
00817   void
00818   FlatZincSpace::newFloatVar(FloatVarSpec*) {
00819     throw FlatZinc::Error("Gecode", "float variables not supported");
00820   }
00821 #endif
00822 
00823   void
00824   FlatZincSpace::postConstraint(const ConExpr& ce, AST::Node* ann) {
00825     try {
00826       registry().post(*this, ce, ann);
00827     } catch (Gecode::Exception& e) {
00828       throw FlatZinc::Error("Gecode", e.what());
00829     } catch (AST::TypeError& e) {
00830       throw FlatZinc::Error("Type error", e.what());
00831     }
00832   }
00833 
00834   void flattenAnnotations(AST::Array* ann, std::vector<AST::Node*>& out) {
00835       for (unsigned int i=0; i<ann->a.size(); i++) {
00836         if (ann->a[i]->isCall("seq_search")) {
00837           AST::Call* c = ann->a[i]->getCall();
00838           if (c->args->isArray())
00839             flattenAnnotations(c->args->getArray(), out);
00840           else
00841             out.push_back(c->args);
00842         } else {
00843           out.push_back(ann->a[i]);
00844         }
00845       }
00846   }
00847 
00848   void
00849   FlatZincSpace::createBranchers(AST::Node* ann, int seed, double decay,
00850                                  bool ignoreUnknown,
00851                                  std::ostream& err) {
00852     Rnd rnd(static_cast<unsigned int>(seed));
00853     TieBreak<IntVarBranch> def_int_varsel = INT_VAR_AFC_SIZE_MAX(0.99);
00854     IntValBranch def_int_valsel = INT_VAL_MIN();
00855     TieBreak<IntVarBranch> def_bool_varsel = INT_VAR_AFC_MAX(0.99);
00856     IntValBranch def_bool_valsel = INT_VAL_MIN();
00857 #ifdef GECODE_HAS_SET_VARS
00858     SetVarBranch def_set_varsel = SET_VAR_AFC_SIZE_MAX(0.99);
00859     SetValBranch def_set_valsel = SET_VAL_MIN_INC();
00860 #endif
00861 #ifdef GECODE_HAS_FLOAT_VARS
00862     TieBreak<FloatVarBranch> def_float_varsel = FLOAT_VAR_SIZE_MIN();
00863     FloatValBranch def_float_valsel = FLOAT_VAL_SPLIT_MIN();
00864 #endif
00865 
00866     std::vector<bool> iv_searched(iv.size());
00867     for (unsigned int i=iv.size(); i--;)
00868       iv_searched[i] = false;
00869     std::vector<bool> bv_searched(bv.size());
00870     for (unsigned int i=bv.size(); i--;)
00871       bv_searched[i] = false;
00872 #ifdef GECODE_HAS_SET_VARS
00873     std::vector<bool> sv_searched(sv.size());
00874     for (unsigned int i=sv.size(); i--;)
00875       sv_searched[i] = false;
00876 #endif
00877 #ifdef GECODE_HAS_FLOAT_VARS
00878     std::vector<bool> fv_searched(fv.size());
00879     for (unsigned int i=fv.size(); i--;)
00880       fv_searched[i] = false;
00881 #endif
00882 
00883     if (ann) {
00884       std::vector<AST::Node*> flatAnn;
00885       if (ann->isArray()) {
00886         flattenAnnotations(ann->getArray()  , flatAnn);
00887       } else {
00888         flatAnn.push_back(ann);
00889       }
00890 
00891       for (unsigned int i=0; i<flatAnn.size(); i++) {
00892         if (flatAnn[i]->isCall("gecode_search")) {
00893           AST::Call* c = flatAnn[i]->getCall();
00894           branchWithPlugin(c->args);
00895         } else if (flatAnn[i]->isCall("int_search")) {
00896           AST::Call *call = flatAnn[i]->getCall("int_search");
00897           AST::Array *args = call->getArgs(4);
00898           AST::Array *vars = args->a[0]->getArray();
00899           int k=vars->a.size();
00900           for (int i=vars->a.size(); i--;)
00901             if (vars->a[i]->isInt())
00902               k--;
00903           IntVarArgs va(k);
00904           vector<string> names;
00905           k=0;
00906           for (unsigned int i=0; i<vars->a.size(); i++) {
00907             if (vars->a[i]->isInt())
00908               continue;
00909             va[k++] = iv[vars->a[i]->getIntVar()];
00910             iv_searched[vars->a[i]->getIntVar()] = true;
00911             names.push_back(vars->a[i]->getVarName());
00912           }
00913           std::string r0, r1;
00914           BrancherHandle bh = branch(*this, va, 
00915             ann2ivarsel(args->a[1],rnd,decay), 
00916             ann2ivalsel(args->a[2],r0,r1,rnd),
00917             NULL,
00918             &varValPrint<IntVar>);
00919           branchInfo.add(bh,r0,r1,names);
00920         } else if (flatAnn[i]->isCall("int_assign")) {
00921           AST::Call *call = flatAnn[i]->getCall("int_assign");
00922           AST::Array *args = call->getArgs(2);
00923           AST::Array *vars = args->a[0]->getArray();
00924           int k=vars->a.size();
00925           for (int i=vars->a.size(); i--;)
00926             if (vars->a[i]->isInt())
00927               k--;
00928           IntVarArgs va(k);
00929           k=0;
00930           for (unsigned int i=0; i<vars->a.size(); i++) {
00931             if (vars->a[i]->isInt())
00932               continue;
00933             va[k++] = iv[vars->a[i]->getIntVar()];
00934             iv_searched[vars->a[i]->getIntVar()] = true;
00935           }
00936           assign(*this, va, ann2asnivalsel(args->a[1],rnd), NULL,
00937                 &varValPrint<IntVar>);
00938         } else if (flatAnn[i]->isCall("bool_search")) {
00939           AST::Call *call = flatAnn[i]->getCall("bool_search");
00940           AST::Array *args = call->getArgs(4);
00941           AST::Array *vars = args->a[0]->getArray();
00942           int k=vars->a.size();
00943           for (int i=vars->a.size(); i--;)
00944             if (vars->a[i]->isBool())
00945               k--;
00946           BoolVarArgs va(k);
00947           k=0;
00948           vector<string> names;
00949           for (unsigned int i=0; i<vars->a.size(); i++) {
00950             if (vars->a[i]->isBool())
00951               continue;
00952             va[k++] = bv[vars->a[i]->getBoolVar()];
00953             bv_searched[vars->a[i]->getBoolVar()] = true;
00954             names.push_back(vars->a[i]->getVarName());
00955           }
00956           
00957           std::string r0, r1;
00958           BrancherHandle bh = branch(*this, va, 
00959             ann2ivarsel(args->a[1],rnd,decay), 
00960             ann2ivalsel(args->a[2],r0,r1,rnd), NULL,
00961             &varValPrint<BoolVar>);
00962           branchInfo.add(bh,r0,r1,names);
00963         } else if (flatAnn[i]->isCall("int_default_search")) {
00964           AST::Call *call = flatAnn[i]->getCall("int_default_search");
00965           AST::Array *args = call->getArgs(2);
00966           def_int_varsel = ann2ivarsel(args->a[0],rnd,decay);
00967           std::string r0;
00968           def_int_valsel = ann2ivalsel(args->a[1],r0,r0,rnd);
00969         } else if (flatAnn[i]->isCall("bool_default_search")) {
00970           AST::Call *call = flatAnn[i]->getCall("bool_default_search");
00971           AST::Array *args = call->getArgs(2);
00972           def_bool_varsel = ann2ivarsel(args->a[0],rnd,decay);
00973           std::string r0;
00974           def_bool_valsel = ann2ivalsel(args->a[1],r0,r0,rnd);
00975         } else if (flatAnn[i]->isCall("set_search")) {
00976 #ifdef GECODE_HAS_SET_VARS
00977           AST::Call *call = flatAnn[i]->getCall("set_search");
00978           AST::Array *args = call->getArgs(4);
00979           AST::Array *vars = args->a[0]->getArray();
00980           int k=vars->a.size();
00981           for (int i=vars->a.size(); i--;)
00982             if (vars->a[i]->isSet())
00983               k--;
00984           SetVarArgs va(k);
00985           k=0;
00986           vector<string> names;
00987           for (unsigned int i=0; i<vars->a.size(); i++) {
00988             if (vars->a[i]->isSet())
00989               continue;
00990             va[k++] = sv[vars->a[i]->getSetVar()];
00991             sv_searched[vars->a[i]->getSetVar()] = true;
00992             names.push_back(vars->a[i]->getVarName());
00993           }
00994           std::string r0, r1;
00995           BrancherHandle bh = branch(*this, va, 
00996             ann2svarsel(args->a[1],rnd,decay), 
00997             ann2svalsel(args->a[2],r0,r1,rnd),
00998             NULL,
00999             &varValPrint<SetVar>);
01000           branchInfo.add(bh,r0,r1,names);
01001 #else
01002           if (!ignoreUnknown) {
01003             err << "Warning, ignored search annotation: ";
01004             flatAnn[i]->print(err);
01005             err << std::endl;
01006           }
01007 #endif
01008         } else if (flatAnn[i]->isCall("set_default_search")) {
01009 #ifdef GECODE_HAS_SET_VARS
01010           AST::Call *call = flatAnn[i]->getCall("set_default_search");
01011           AST::Array *args = call->getArgs(2);
01012           def_set_varsel = ann2svarsel(args->a[0],rnd,decay);
01013           std::string r0;
01014           def_set_valsel = ann2svalsel(args->a[1],r0,r0,rnd);
01015 #else
01016           if (!ignoreUnknown) {
01017             err << "Warning, ignored search annotation: ";
01018             flatAnn[i]->print(err);
01019             err << std::endl;
01020           }
01021 #endif
01022         } else if (flatAnn[i]->isCall("float_default_search")) {
01023 #ifdef GECODE_HAS_FLOAT_VARS
01024           AST::Call *call = flatAnn[i]->getCall("float_default_search");
01025           AST::Array *args = call->getArgs(2);
01026           def_float_varsel = ann2fvarsel(args->a[0],rnd,decay);
01027           std::string r0;
01028           def_float_valsel = ann2fvalsel(args->a[1],r0,r0);
01029 #else
01030           if (!ignoreUnknown) {
01031             err << "Warning, ignored search annotation: ";
01032             flatAnn[i]->print(err);
01033             err << std::endl;
01034           }
01035 #endif
01036         } else if (flatAnn[i]->isCall("float_search")) {
01037 #ifdef GECODE_HAS_FLOAT_VARS
01038           AST::Call *call = flatAnn[i]->getCall("float_search");
01039           AST::Array *args = call->getArgs(5);
01040           AST::Array *vars = args->a[0]->getArray();
01041           int k=vars->a.size();
01042           for (int i=vars->a.size(); i--;)
01043             if (vars->a[i]->isFloat())
01044               k--;
01045           FloatVarArgs va(k);
01046           k=0;
01047           vector<string> names;
01048           for (unsigned int i=0; i<vars->a.size(); i++) {
01049             if (vars->a[i]->isFloat())
01050               continue;
01051             va[k++] = fv[vars->a[i]->getFloatVar()];
01052             fv_searched[vars->a[i]->getFloatVar()] = true;
01053             names.push_back(vars->a[i]->getVarName());
01054           }
01055           std::string r0, r1;
01056           BrancherHandle bh = branch(*this, va,
01057             ann2fvarsel(args->a[2],rnd,decay), 
01058             ann2fvalsel(args->a[3],r0,r1),
01059             NULL,
01060             &varValPrintF);
01061           branchInfo.add(bh,r0,r1,names);
01062 #else
01063           if (!ignoreUnknown) {
01064             err << "Warning, ignored search annotation: ";
01065             flatAnn[i]->print(err);
01066             err << std::endl;
01067           }
01068 #endif
01069         } else {
01070           if (!ignoreUnknown) {
01071             err << "Warning, ignored search annotation: ";
01072             flatAnn[i]->print(err);
01073             err << std::endl;
01074           }
01075         }
01076       }
01077     }
01078     int introduced = 0;
01079     int funcdep = 0;
01080     int searched = 0;
01081     for (int i=iv.size(); i--;) {
01082       if (iv_searched[i]) {
01083         searched++;
01084       } else if (iv_introduced[2*i]) {
01085         if (iv_introduced[2*i+1]) {
01086           funcdep++;
01087         } else {
01088           introduced++;
01089         }
01090       }
01091     }
01092     IntVarArgs iv_sol(iv.size()-(introduced+funcdep+searched));
01093     IntVarArgs iv_tmp(introduced);
01094     for (int i=iv.size(), j=0, k=0; i--;) {
01095       if (iv_searched[i])
01096         continue;
01097       if (iv_introduced[2*i]) {
01098         if (!iv_introduced[2*i+1]) {
01099           iv_tmp[j++] = iv[i];
01100         }
01101       } else {
01102         iv_sol[k++] = iv[i];
01103       }
01104     }
01105 
01106     introduced = 0;
01107     funcdep = 0;
01108     searched = 0;
01109     for (int i=bv.size(); i--;) {
01110       if (bv_searched[i]) {
01111         searched++;
01112       } else if (bv_introduced[2*i]) {
01113         if (bv_introduced[2*i+1]) {
01114           funcdep++;
01115         } else {
01116           introduced++;
01117         }
01118       }
01119     }
01120     BoolVarArgs bv_sol(bv.size()-(introduced+funcdep+searched));
01121     BoolVarArgs bv_tmp(introduced);
01122     for (int i=bv.size(), j=0, k=0; i--;) {
01123       if (bv_searched[i])
01124         continue;
01125       if (bv_introduced[2*i]) {
01126         if (!bv_introduced[2*i+1]) {
01127           bv_tmp[j++] = bv[i];
01128         }
01129       } else {
01130         bv_sol[k++] = bv[i];
01131       }
01132     }
01133 
01134     if (iv_sol.size() > 0)
01135       branch(*this, iv_sol, def_int_varsel, def_int_valsel);
01136     if (bv_sol.size() > 0)
01137       branch(*this, bv_sol, def_bool_varsel, def_bool_valsel);
01138 #ifdef GECODE_HAS_FLOAT_VARS
01139     introduced = 0;
01140     funcdep = 0;
01141     searched = 0;
01142     for (int i=fv.size(); i--;) {
01143       if (fv_searched[i]) {
01144         searched++;
01145       } else if (fv_introduced[2*i]) {
01146         if (fv_introduced[2*i+1]) {
01147           funcdep++;
01148         } else {
01149           introduced++;
01150         }
01151       }
01152     }
01153     FloatVarArgs fv_sol(fv.size()-(introduced+funcdep+searched));
01154     FloatVarArgs fv_tmp(introduced);
01155     for (int i=fv.size(), j=0, k=0; i--;) {
01156       if (fv_searched[i])
01157         continue;
01158       if (fv_introduced[2*i]) {
01159         if (!fv_introduced[2*i+1]) {
01160           fv_tmp[j++] = fv[i];
01161         }
01162       } else {
01163         fv_sol[k++] = fv[i];
01164       }
01165     }
01166 
01167     if (fv_sol.size() > 0)
01168       branch(*this, fv_sol, def_float_varsel, def_float_valsel);
01169 #endif
01170 #ifdef GECODE_HAS_SET_VARS
01171     introduced = 0;
01172     funcdep = 0;
01173     searched = 0;
01174     for (int i=sv.size(); i--;) {
01175       if (sv_searched[i]) {
01176         searched++;
01177       } else if (sv_introduced[2*i]) {
01178         if (sv_introduced[2*i+1]) {
01179           funcdep++;
01180         } else {
01181           introduced++;
01182         }
01183       }
01184     }
01185     SetVarArgs sv_sol(sv.size()-(introduced+funcdep+searched));
01186     SetVarArgs sv_tmp(introduced);
01187     for (int i=sv.size(), j=0, k=0; i--;) {
01188       if (sv_searched[i])
01189         continue;
01190       if (sv_introduced[2*i]) {
01191         if (!sv_introduced[2*i+1]) {
01192           sv_tmp[j++] = sv[i];
01193         }
01194       } else {
01195         sv_sol[k++] = sv[i];
01196       }
01197     }
01198 
01199     if (sv_sol.size() > 0)
01200       branch(*this, sv_sol, def_set_varsel, def_set_valsel);
01201 #endif
01202     iv_aux = IntVarArray(*this, iv_tmp);
01203     bv_aux = BoolVarArray(*this, bv_tmp);
01204     int n_aux = iv_aux.size() + bv_aux.size();
01205 #ifdef GECODE_HAS_SET_VARS
01206     sv_aux = SetVarArray(*this, sv_tmp);
01207     n_aux += sv_aux.size();
01208 #endif
01209 #ifdef GECODE_HAS_FLOAT_VARS
01210     fv_aux = FloatVarArray(*this, fv_tmp);
01211     n_aux += fv_aux.size();
01212 #endif
01213     if (n_aux > 0) {
01214       AuxVarBrancher::post(*this, def_int_varsel, def_int_valsel,
01215                            def_bool_varsel, def_bool_valsel
01216 #ifdef GECODE_HAS_SET_VARS
01217                            , def_set_varsel, def_set_valsel
01218 #endif
01219 #ifdef GECODE_HAS_FLOAT_VARS
01220                            , def_float_varsel, def_float_valsel
01221 #endif
01222                            );
01223     }
01224   }
01225 
01226   AST::Array*
01227   FlatZincSpace::solveAnnotations(void) const {
01228     return _solveAnnotations;
01229   }
01230 
01231   void
01232   FlatZincSpace::solve(AST::Array* ann) {
01233     _method = SAT;
01234     _solveAnnotations = ann;
01235   }
01236 
01237   void
01238   FlatZincSpace::minimize(int var, bool isInt, AST::Array* ann) {
01239     _method = MIN;
01240     _optVar = var;
01241     _optVarIsInt = isInt;
01242     // Branch on optimization variable to ensure that it is given a value.
01243     AST::Call* c;
01244     if (isInt) {
01245       AST::Array* args = new AST::Array(4);
01246       args->a[0] = new AST::Array(new AST::IntVar(_optVar));
01247       args->a[1] = new AST::Atom("input_order");
01248       args->a[2] = new AST::Atom("indomain_min");
01249       args->a[3] = new AST::Atom("complete");
01250       c = new AST::Call("int_search", args);
01251     } else {
01252       AST::Array* args = new AST::Array(5);
01253       args->a[0] = new AST::Array(new AST::FloatVar(_optVar));
01254       args->a[1] = new AST::FloatLit(0.0);
01255       args->a[2] = new AST::Atom("input_order");
01256       args->a[3] = new AST::Atom("indomain_split");
01257       args->a[4] = new AST::Atom("complete");
01258       c = new AST::Call("float_search", args);
01259     }
01260     if (!ann)
01261       ann = new AST::Array(c);
01262     else
01263       ann->a.push_back(c);
01264     _solveAnnotations = ann;
01265   }
01266 
01267   void
01268   FlatZincSpace::maximize(int var, bool isInt, AST::Array* ann) {
01269     _method = MAX;
01270     _optVar = var;
01271     _optVarIsInt = isInt;
01272     // Branch on optimization variable to ensure that it is given a value.
01273     AST::Call* c;
01274     if (isInt) {
01275       AST::Array* args = new AST::Array(4);
01276       args->a[0] = new AST::Array(new AST::IntVar(_optVar));
01277       args->a[1] = new AST::Atom("input_order");
01278       args->a[2] = new AST::Atom("indomain_max");
01279       args->a[3] = new AST::Atom("complete");
01280       c = new AST::Call("int_search", args);
01281     } else {
01282       AST::Array* args = new AST::Array(5);
01283       args->a[0] = new AST::Array(new AST::FloatVar(_optVar));
01284       args->a[1] = new AST::FloatLit(0.0);
01285       args->a[2] = new AST::Atom("input_order");
01286       args->a[3] = new AST::Atom("indomain_split_reverse");
01287       args->a[4] = new AST::Atom("complete");
01288       c = new AST::Call("float_search", args);
01289     }
01290     if (!ann)
01291       ann = new AST::Array(c);
01292     else
01293       ann->a.push_back(c);
01294     _solveAnnotations = ann;
01295   }
01296 
01297   FlatZincSpace::~FlatZincSpace(void) {
01298     delete _solveAnnotations;
01299   }
01300 
01301 #ifdef GECODE_HAS_GIST
01302 
01306   template<class Engine>
01307   class GistEngine {
01308   };
01309 
01311   template<typename S>
01312   class GistEngine<DFS<S> > {
01313   public:
01314     static void explore(S* root, const FlatZincOptions& opt,
01315                         Gist::Inspector* i, Gist::Comparator* c) {
01316       Gecode::Gist::Options o;
01317       o.c_d = opt.c_d(); o.a_d = opt.a_d();
01318       o.inspect.click(i);
01319       o.inspect.compare(c);
01320       (void) Gecode::Gist::dfs(root, o);
01321     }
01322   };
01323 
01325   template<typename S>
01326   class GistEngine<BAB<S> > {
01327   public:
01328     static void explore(S* root, const FlatZincOptions& opt,
01329                         Gist::Inspector* i, Gist::Comparator* c) {
01330       Gecode::Gist::Options o;
01331       o.c_d = opt.c_d(); o.a_d = opt.a_d();
01332       o.inspect.click(i);
01333       o.inspect.compare(c);
01334       (void) Gecode::Gist::bab(root, o);
01335     }
01336   };
01337 
01339   template<class S>
01340   class FZPrintingInspector
01341    : public Gecode::Gist::TextOutput, public Gecode::Gist::Inspector {
01342   private:
01343     const Printer& p;
01344   public:
01346     FZPrintingInspector(const Printer& p0);
01348     virtual void inspect(const Space& node);
01350     virtual void finalize(void);
01351   };
01352 
01353   template<class S>
01354   FZPrintingInspector<S>::FZPrintingInspector(const Printer& p0)
01355   : TextOutput("Gecode/FlatZinc"), p(p0) {}
01356 
01357   template<class S>
01358   void
01359   FZPrintingInspector<S>::inspect(const Space& node) {
01360     init();
01361     dynamic_cast<const S&>(node).print(getStream(), p);
01362     getStream() << std::endl;
01363   }
01364 
01365   template<class S>
01366   void
01367   FZPrintingInspector<S>::finalize(void) {
01368     Gecode::Gist::TextOutput::finalize();
01369   }
01370 
01371   template<class S>
01372   class FZPrintingComparator
01373   : public Gecode::Gist::VarComparator<S> {
01374   private:
01375     const Printer& p;
01376   public:
01378     FZPrintingComparator(const Printer& p0);
01379 
01381     virtual void compare(const Space& s0, const Space& s1);
01382   };
01383 
01384   template<class S>
01385   FZPrintingComparator<S>::FZPrintingComparator(const Printer& p0)
01386   : Gecode::Gist::VarComparator<S>("Gecode/FlatZinc"), p(p0) {}
01387 
01388   template<class S>
01389   void
01390   FZPrintingComparator<S>::compare(const Space& s0, const Space& s1) {
01391     this->init();
01392     try {
01393       dynamic_cast<const S&>(s0).compare(dynamic_cast<const S&>(s1),
01394                                          this->getStream(), p);
01395     } catch (Exception& e) {
01396       this->getStream() << "Exception: " << e.what();
01397     }
01398     this->getStream() << std::endl;
01399   }
01400 
01401 #endif
01402 
01403 
01404   template<template<class> class Engine>
01405   void
01406   FlatZincSpace::runEngine(std::ostream& out, const Printer& p,
01407                            const FlatZincOptions& opt, Support::Timer& t_total) {
01408     if (opt.restart()==RM_NONE) {
01409       runMeta<Engine,Driver::EngineToMeta>(out,p,opt,t_total);
01410     } else {
01411       runMeta<Engine,RBS>(out,p,opt,t_total);
01412     }
01413   }
01414 
01415   template<template<class> class Engine,
01416            template<template<class> class,class> class Meta>
01417   void
01418   FlatZincSpace::runMeta(std::ostream& out, const Printer& p,
01419                          const FlatZincOptions& opt, Support::Timer& t_total) {
01420 #ifdef GECODE_HAS_GIST
01421     if (opt.mode() == SM_GIST) {
01422       FZPrintingInspector<FlatZincSpace> pi(p);
01423       FZPrintingComparator<FlatZincSpace> pc(p);
01424       (void) GistEngine<Engine<FlatZincSpace> >::explore(this,opt,&pi,&pc);
01425       return;
01426     }
01427 #endif
01428     StatusStatistics sstat;
01429     unsigned int n_p = 0;
01430     Support::Timer t_solve;
01431     t_solve.start();
01432     if (status(sstat) != SS_FAILED) {
01433       n_p = propagators();
01434     }
01435     Search::Options o;
01436     o.stop = Driver::CombinedStop::create(opt.node(), opt.fail(), opt.time(), 
01437                                           true);
01438     o.c_d = opt.c_d();
01439     o.a_d = opt.a_d();
01440     o.threads = opt.threads();
01441     o.nogoods_limit = opt.nogoods() ? opt.nogoods_limit() : 0;
01442     o.cutoff  = Driver::createCutoff(opt);
01443     if (opt.interrupt())
01444       Driver::CombinedStop::installCtrlHandler(true);
01445     Meta<Engine,FlatZincSpace> se(this,o);
01446     int noOfSolutions = _method == SAT ? opt.solutions() : 0;
01447     bool printAll = _method == SAT || opt.allSolutions();
01448     int findSol = noOfSolutions;
01449     FlatZincSpace* sol = NULL;
01450     while (FlatZincSpace* next_sol = se.next()) {
01451       delete sol;
01452       sol = next_sol;
01453       if (printAll) {
01454         sol->print(out, p);
01455         out << "----------" << std::endl;
01456       }
01457       if (--findSol==0)
01458         goto stopped;
01459     }
01460     if (sol && !printAll) {
01461       sol->print(out, p);
01462       out << "----------" << std::endl;
01463     }
01464     if (!se.stopped()) {
01465       if (sol) {
01466         out << "==========" << endl;
01467       } else {
01468         out << "=====UNSATISFIABLE=====" << endl;
01469       }
01470     } else if (!sol) {
01471         out << "=====UNKNOWN=====" << endl;
01472     }
01473     delete sol;
01474     stopped:
01475     if (opt.interrupt())
01476       Driver::CombinedStop::installCtrlHandler(false);
01477     if (opt.mode() == SM_STAT) {
01478       Gecode::Search::Statistics stat = se.statistics();
01479       out << endl
01480            << "%%  runtime:       ";
01481       Driver::stop(t_total,out);
01482       out << endl
01483            << "%%  solvetime:     ";
01484       Driver::stop(t_solve,out);
01485       out << endl
01486            << "%%  solutions:     " 
01487            << std::abs(noOfSolutions - findSol) << endl
01488            << "%%  variables:     " 
01489            << (intVarCount + boolVarCount + setVarCount) << endl
01490            << "%%  propagators:   " << n_p << endl
01491            << "%%  propagations:  " << sstat.propagate+stat.propagate << endl
01492            << "%%  nodes:         " << stat.node << endl
01493            << "%%  failures:      " << stat.fail << endl
01494            << "%%  restarts:      " << stat.restart << endl
01495            << "%%  peak depth:    " << stat.depth << endl
01496            << endl;
01497     }
01498     delete o.stop;
01499   }
01500 
01501 #ifdef GECODE_HAS_QT
01502   void
01503   FlatZincSpace::branchWithPlugin(AST::Node* ann) {
01504     if (AST::Call* c = dynamic_cast<AST::Call*>(ann)) {
01505       QString pluginName(c->id.c_str());
01506       if (QLibrary::isLibrary(pluginName+".dll")) {
01507         pluginName += ".dll";
01508       } else if (QLibrary::isLibrary(pluginName+".dylib")) {
01509         pluginName = "lib" + pluginName + ".dylib";
01510       } else if (QLibrary::isLibrary(pluginName+".so")) {
01511         // Must check .so after .dylib so that Mac OS uses .dylib
01512         pluginName = "lib" + pluginName + ".so";
01513       }
01514       QPluginLoader pl(pluginName);
01515       QObject* plugin_o = pl.instance();
01516       if (!plugin_o) {
01517         throw FlatZinc::Error("FlatZinc",
01518           "Error loading plugin "+pluginName.toStdString()+
01519           ": "+pl.errorString().toStdString());
01520       }
01521       BranchPlugin* pb = qobject_cast<BranchPlugin*>(plugin_o);
01522       if (!pb) {
01523         throw FlatZinc::Error("FlatZinc",
01524         "Error loading plugin "+pluginName.toStdString()+
01525         ": does not contain valid PluginBrancher");
01526       }
01527       pb->branch(*this, c);
01528     }
01529   }
01530 #else
01531   void
01532   FlatZincSpace::branchWithPlugin(AST::Node*) {
01533     throw FlatZinc::Error("FlatZinc",
01534       "Branching with plugins not supported (requires Qt support)");
01535   }
01536 #endif
01537 
01538   void
01539   FlatZincSpace::run(std::ostream& out, const Printer& p,
01540                       const FlatZincOptions& opt, Support::Timer& t_total) {
01541     switch (_method) {
01542     case MIN:
01543     case MAX:
01544       runEngine<BAB>(out,p,opt,t_total);
01545       break;
01546     case SAT:
01547       runEngine<DFS>(out,p,opt,t_total);
01548       break;
01549     }
01550   }
01551 
01552   void
01553   FlatZincSpace::constrain(const Space& s) {
01554     if (_optVarIsInt) {
01555       if (_method == MIN)
01556         rel(*this, iv[_optVar], IRT_LE, 
01557                    static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
01558       else if (_method == MAX)
01559         rel(*this, iv[_optVar], IRT_GR,
01560                    static_cast<const FlatZincSpace*>(&s)->iv[_optVar].val());
01561     } else {
01562 #ifdef GECODE_HAS_FLOAT_VARS
01563       if (_method == MIN)
01564         rel(*this, fv[_optVar], FRT_LE, 
01565                    static_cast<const FlatZincSpace*>(&s)->fv[_optVar].val());
01566       else if (_method == MAX)
01567         rel(*this, fv[_optVar], FRT_GR,
01568                    static_cast<const FlatZincSpace*>(&s)->fv[_optVar].val());
01569 #endif
01570     }
01571   }
01572 
01573   Space*
01574   FlatZincSpace::copy(bool share) {
01575     return new FlatZincSpace(share, *this);
01576   }
01577 
01578   FlatZincSpace::Meth
01579   FlatZincSpace::method(void) const {
01580     return _method;
01581   }
01582 
01583   int
01584   FlatZincSpace::optVar(void) const {
01585     return _optVar;
01586   }
01587 
01588   bool
01589   FlatZincSpace::optVarIsInt(void) const {
01590     return _optVarIsInt;
01591   }
01592 
01593   void
01594   FlatZincSpace::print(std::ostream& out, const Printer& p) const {
01595     p.print(out, iv, bv
01596 #ifdef GECODE_HAS_SET_VARS
01597     , sv
01598 #endif
01599 #ifdef GECODE_HAS_FLOAT_VARS
01600     , fv
01601 #endif
01602     );
01603   }
01604 
01605   void
01606   FlatZincSpace::compare(const Space& s, std::ostream& out) const {
01607     (void) s; (void) out;
01608 #ifdef GECODE_HAS_GIST
01609     const FlatZincSpace& fs = dynamic_cast<const FlatZincSpace&>(s);
01610     for (int i = 0; i < iv.size(); ++i) {
01611       std::stringstream ss;
01612       ss << "iv[" << i << "]";
01613       std::string result(Gecode::Gist::Comparator::compare(ss.str(), iv[i],
01614                                                            fs.iv[i]));
01615       if (result.length() > 0) out << result << std::endl;
01616     }
01617     for (int i = 0; i < bv.size(); ++i) {
01618       std::stringstream ss;
01619       ss << "bv[" << i << "]";
01620       std::string result(Gecode::Gist::Comparator::compare(ss.str(), bv[i],
01621                                                            fs.bv[i]));
01622       if (result.length() > 0) out << result << std::endl;
01623     }
01624 #ifdef GECODE_HAS_SET_VARS
01625     for (int i = 0; i < sv.size(); ++i) {
01626       std::stringstream ss;
01627       ss << "sv[" << i << "]";
01628       std::string result(Gecode::Gist::Comparator::compare(ss.str(), sv[i],
01629                                                            fs.sv[i]));
01630       if (result.length() > 0) out << result << std::endl;
01631     }
01632 #endif
01633 #ifdef GECODE_HAS_FLOAT_VARS
01634     for (int i = 0; i < fv.size(); ++i) {
01635       std::stringstream ss;
01636       ss << "fv[" << i << "]";
01637       std::string result(Gecode::Gist::Comparator::compare(ss.str(), fv[i],
01638                                                            fs.fv[i]));
01639       if (result.length() > 0) out << result << std::endl;
01640     }
01641 #endif
01642 #endif
01643   }
01644 
01645   void
01646   FlatZincSpace::compare(const FlatZincSpace& s, std::ostream& out,
01647                          const Printer& p) const {
01648     p.printDiff(out, iv, s.iv, bv, s.bv
01649 #ifdef GECODE_HAS_SET_VARS
01650      , sv, s.sv
01651 #endif
01652 #ifdef GECODE_HAS_FLOAT_VARS
01653      , fv, s.fv
01654 #endif
01655     );
01656   }
01657 
01658   void
01659   FlatZincSpace::shrinkArrays(Printer& p) {
01660     p.shrinkArrays(*this, _optVar, _optVarIsInt, iv, bv
01661 #ifdef GECODE_HAS_SET_VARS
01662     , sv
01663 #endif
01664 #ifdef GECODE_HAS_FLOAT_VARS
01665     , fv
01666 #endif
01667     );
01668   }
01669 
01670   IntArgs
01671   FlatZincSpace::arg2intargs(AST::Node* arg, int offset) {
01672     AST::Array* a = arg->getArray();
01673     IntArgs ia(a->a.size()+offset);
01674     for (int i=offset; i--;)
01675       ia[i] = 0;
01676     for (int i=a->a.size(); i--;)
01677       ia[i+offset] = a->a[i]->getInt();
01678     return ia;
01679   }
01680   IntArgs
01681   FlatZincSpace::arg2boolargs(AST::Node* arg, int offset) {
01682     AST::Array* a = arg->getArray();
01683     IntArgs ia(a->a.size()+offset);
01684     for (int i=offset; i--;)
01685       ia[i] = 0;
01686     for (int i=a->a.size(); i--;)
01687       ia[i+offset] = a->a[i]->getBool();
01688     return ia;
01689   }
01690   IntSet
01691   FlatZincSpace::arg2intset(AST::Node* n) {
01692     AST::SetLit* sl = n->getSet();
01693     IntSet d;
01694     if (sl->interval) {
01695       d = IntSet(sl->min, sl->max);
01696     } else {
01697       Region re(*this);
01698       int* is = re.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
01699       for (int i=sl->s.size(); i--; )
01700         is[i] = sl->s[i];
01701       d = IntSet(is, sl->s.size());
01702     }
01703     return d;
01704   }
01705   IntSetArgs
01706   FlatZincSpace::arg2intsetargs(AST::Node* arg, int offset) {
01707     AST::Array* a = arg->getArray();
01708     if (a->a.size() == 0) {
01709       IntSetArgs emptyIa(0);
01710       return emptyIa;
01711     }
01712     IntSetArgs ia(a->a.size()+offset);      
01713     for (int i=offset; i--;)
01714       ia[i] = IntSet::empty;
01715     for (int i=a->a.size(); i--;) {
01716       ia[i+offset] = arg2intset(a->a[i]);
01717     }
01718     return ia;
01719   }
01720   IntVarArgs
01721   FlatZincSpace::arg2intvarargs(AST::Node* arg, int offset) {
01722     AST::Array* a = arg->getArray();
01723     if (a->a.size() == 0) {
01724       IntVarArgs emptyIa(0);
01725       return emptyIa;
01726     }
01727     IntVarArgs ia(a->a.size()+offset);
01728     for (int i=offset; i--;)
01729       ia[i] = IntVar(*this, 0, 0);
01730     for (int i=a->a.size(); i--;) {
01731       if (a->a[i]->isIntVar()) {
01732         ia[i+offset] = iv[a->a[i]->getIntVar()];        
01733       } else {
01734         int value = a->a[i]->getInt();
01735         IntVar iv(*this, value, value);
01736         ia[i+offset] = iv;        
01737       }
01738     }
01739     return ia;
01740   }
01741   BoolVarArgs
01742   FlatZincSpace::arg2boolvarargs(AST::Node* arg, int offset, int siv) {
01743     AST::Array* a = arg->getArray();
01744     if (a->a.size() == 0) {
01745       BoolVarArgs emptyIa(0);
01746       return emptyIa;
01747     }
01748     BoolVarArgs ia(a->a.size()+offset-(siv==-1?0:1));
01749     for (int i=offset; i--;)
01750       ia[i] = BoolVar(*this, 0, 0);
01751     for (int i=0; i<static_cast<int>(a->a.size()); i++) {
01752       if (i==siv)
01753         continue;
01754       if (a->a[i]->isBool()) {
01755         bool value = a->a[i]->getBool();
01756         BoolVar iv(*this, value, value);
01757         ia[offset++] = iv;
01758       } else if (a->a[i]->isIntVar() &&
01759                  aliasBool2Int(a->a[i]->getIntVar()) != -1) {
01760         ia[offset++] = bv[aliasBool2Int(a->a[i]->getIntVar())];
01761       } else {
01762         ia[offset++] = bv[a->a[i]->getBoolVar()];
01763       }
01764     }
01765     return ia;
01766   }
01767   BoolVar
01768   FlatZincSpace::arg2BoolVar(AST::Node* n) {
01769     BoolVar x0;
01770     if (n->isBool()) {
01771       x0 = BoolVar(*this, n->getBool(), n->getBool());
01772     }
01773     else {
01774       x0 = bv[n->getBoolVar()];
01775     }
01776     return x0;
01777   }
01778   IntVar
01779   FlatZincSpace::arg2IntVar(AST::Node* n) {
01780     IntVar x0;
01781     if (n->isIntVar()) {
01782       x0 = iv[n->getIntVar()];
01783     } else {
01784       x0 = IntVar(*this, n->getInt(), n->getInt());            
01785     }
01786     return x0;
01787   }
01788   bool
01789   FlatZincSpace::isBoolArray(AST::Node* b, int& singleInt) {
01790     AST::Array* a = b->getArray();
01791     singleInt = -1;
01792     if (a->a.size() == 0)
01793       return true;
01794     for (int i=a->a.size(); i--;) {
01795       if (a->a[i]->isBoolVar() || a->a[i]->isBool()) {
01796       } else if (a->a[i]->isIntVar()) {
01797         if (aliasBool2Int(a->a[i]->getIntVar()) == -1) {
01798           if (singleInt != -1) {
01799             return false;
01800           }
01801           singleInt = i;
01802         }
01803       } else {
01804         return false;
01805       }
01806     }
01807     return singleInt==-1 || a->a.size() > 1;
01808   }
01809 #ifdef GECODE_HAS_SET_VARS
01810   SetVar
01811   FlatZincSpace::arg2SetVar(AST::Node* n) {
01812     SetVar x0;
01813     if (!n->isSetVar()) {
01814       IntSet d = arg2intset(n);
01815       x0 = SetVar(*this, d, d);
01816     } else {
01817       x0 = sv[n->getSetVar()];
01818     }
01819     return x0;
01820   }
01821   SetVarArgs
01822   FlatZincSpace::arg2setvarargs(AST::Node* arg, int offset, int doffset,
01823                                 const IntSet& od) {
01824     AST::Array* a = arg->getArray();
01825     SetVarArgs ia(a->a.size()+offset);
01826     for (int i=offset; i--;) {
01827       IntSet d = i<doffset ? od : IntSet::empty;
01828       ia[i] = SetVar(*this, d, d);
01829     }
01830     for (int i=a->a.size(); i--;) {
01831       ia[i+offset] = arg2SetVar(a->a[i]);
01832     }
01833     return ia;
01834   }
01835 #endif
01836 #ifdef GECODE_HAS_FLOAT_VARS
01837   FloatValArgs
01838   FlatZincSpace::arg2floatargs(AST::Node* arg, int offset) {
01839     AST::Array* a = arg->getArray();
01840     FloatValArgs fa(a->a.size()+offset);
01841     for (int i=offset; i--;)
01842       fa[i] = 0.0;
01843     for (int i=a->a.size(); i--;)
01844       fa[i+offset] = a->a[i]->getFloat();
01845     return fa;
01846   }
01847   FloatVarArgs
01848   FlatZincSpace::arg2floatvarargs(AST::Node* arg, int offset) {
01849     AST::Array* a = arg->getArray();
01850     if (a->a.size() == 0) {
01851       FloatVarArgs emptyFa(0);
01852       return emptyFa;
01853     }
01854     FloatVarArgs fa(a->a.size()+offset);
01855     for (int i=offset; i--;)
01856       fa[i] = FloatVar(*this, 0.0, 0.0);
01857     for (int i=a->a.size(); i--;) {
01858       if (a->a[i]->isFloatVar()) {
01859         fa[i+offset] = fv[a->a[i]->getFloatVar()];        
01860       } else {
01861         double value = a->a[i]->getFloat();
01862         FloatVar fv(*this, value, value);
01863         fa[i+offset] = fv;
01864       }
01865     }
01866     return fa;
01867   }
01868   FloatVar
01869   FlatZincSpace::arg2FloatVar(AST::Node* n) {
01870     FloatVar x0;
01871     if (n->isFloatVar()) {
01872       x0 = fv[n->getFloatVar()];
01873     } else {
01874       x0 = FloatVar(*this, n->getFloat(), n->getFloat());
01875     }
01876     return x0;
01877   }
01878 #endif
01879   IntConLevel
01880   FlatZincSpace::ann2icl(AST::Node* ann) {
01881     if (ann) {
01882       if (ann->hasAtom("val"))
01883         return ICL_VAL;
01884       if (ann->hasAtom("domain"))
01885         return ICL_DOM;
01886       if (ann->hasAtom("bounds") ||
01887           ann->hasAtom("boundsR") ||
01888           ann->hasAtom("boundsD") ||
01889           ann->hasAtom("boundsZ"))
01890         return ICL_BND;
01891     }
01892     return ICL_DEF;
01893   }
01894 
01895 
01896   void
01897   Printer::init(AST::Array* output) {
01898     _output = output;
01899   }
01900 
01901   void
01902   Printer::printElem(std::ostream& out,
01903                        AST::Node* ai,
01904                        const Gecode::IntVarArray& iv,
01905                        const Gecode::BoolVarArray& bv
01906 #ifdef GECODE_HAS_SET_VARS
01907                        , const Gecode::SetVarArray& sv
01908 #endif
01909 #ifdef GECODE_HAS_FLOAT_VARS
01910                        ,
01911                        const Gecode::FloatVarArray& fv
01912 #endif
01913                        ) const {
01914     int k;
01915     if (ai->isInt(k)) {
01916       out << k;
01917     } else if (ai->isIntVar()) {
01918       out << iv[ai->getIntVar()];
01919     } else if (ai->isBoolVar()) {
01920       if (bv[ai->getBoolVar()].min() == 1) {
01921         out << "true";
01922       } else if (bv[ai->getBoolVar()].max() == 0) {
01923         out << "false";
01924       } else {
01925         out << "false..true";
01926       }
01927 #ifdef GECODE_HAS_SET_VARS
01928     } else if (ai->isSetVar()) {
01929       if (!sv[ai->getSetVar()].assigned()) {
01930         out << sv[ai->getSetVar()];
01931         return;
01932       }
01933       SetVarGlbRanges svr(sv[ai->getSetVar()]);
01934       if (!svr()) {
01935         out << "{}";
01936         return;
01937       }
01938       int min = svr.min();
01939       int max = svr.max();
01940       ++svr;
01941       if (svr()) {
01942         SetVarGlbValues svv(sv[ai->getSetVar()]);
01943         int i = svv.val();
01944         out << "{" << i;
01945         ++svv;
01946         for (; svv(); ++svv)
01947           out << ", " << svv.val();
01948         out << "}";
01949       } else {
01950         out << min << ".." << max;
01951       }
01952 #endif
01953 #ifdef GECODE_HAS_FLOAT_VARS
01954     } else if (ai->isFloatVar()) {
01955       if (fv[ai->getFloatVar()].assigned()) {
01956         FloatVal vv = fv[ai->getFloatVar()].val();
01957         FloatNum v;
01958         if (vv.singleton())
01959           v = vv.min();
01960         else if (vv < 0.0)
01961           v = vv.max();
01962         else
01963           v = vv.min();
01964         std::ostringstream oss;
01965         // oss << std::scientific;
01966         oss << std::setprecision(std::numeric_limits<double>::digits10);
01967         oss << v;
01968         if (oss.str().find(".") == std::string::npos)
01969           oss << ".0";
01970         out << oss.str();
01971       } else {
01972         out << fv[ai->getFloatVar()];
01973       }
01974 #endif
01975     } else if (ai->isBool()) {
01976       out << (ai->getBool() ? "true" : "false");
01977     } else if (ai->isSet()) {
01978       AST::SetLit* s = ai->getSet();
01979       if (s->interval) {
01980         out << s->min << ".." << s->max;
01981       } else {
01982         out << "{";
01983         for (unsigned int i=0; i<s->s.size(); i++) {
01984           out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
01985         }
01986       }
01987     } else if (ai->isString()) {
01988       std::string s = ai->getString();
01989       for (unsigned int i=0; i<s.size(); i++) {
01990         if (s[i] == '\\' && i<s.size()-1) {
01991           switch (s[i+1]) {
01992           case 'n': out << "\n"; break;
01993           case '\\': out << "\\"; break;
01994           case 't': out << "\t"; break;
01995           default: out << "\\" << s[i+1];
01996           }
01997           i++;
01998         } else {
01999           out << s[i];
02000         }
02001       }
02002     }
02003   }
02004 
02005   void
02006   Printer::printElemDiff(std::ostream& out,
02007                        AST::Node* ai,
02008                        const Gecode::IntVarArray& iv1,
02009                        const Gecode::IntVarArray& iv2,
02010                        const Gecode::BoolVarArray& bv1,
02011                        const Gecode::BoolVarArray& bv2
02012 #ifdef GECODE_HAS_SET_VARS
02013                        , const Gecode::SetVarArray& sv1,
02014                        const Gecode::SetVarArray& sv2
02015 #endif
02016 #ifdef GECODE_HAS_FLOAT_VARS
02017                        , const Gecode::FloatVarArray& fv1,
02018                        const Gecode::FloatVarArray& fv2
02019 #endif
02020                        ) const {
02021 #ifdef GECODE_HAS_GIST
02022     using namespace Gecode::Gist;
02023     int k;
02024     if (ai->isInt(k)) {
02025       out << k;
02026     } else if (ai->isIntVar()) {
02027       std::string res(Comparator::compare("",iv1[ai->getIntVar()],
02028                                           iv2[ai->getIntVar()]));
02029       if (res.length() > 0) {
02030         res.erase(0, 1); // Remove '='
02031         out << res;
02032       } else {
02033         out << iv1[ai->getIntVar()];
02034       }
02035     } else if (ai->isBoolVar()) {
02036       std::string res(Comparator::compare("",bv1[ai->getBoolVar()],
02037                                           bv2[ai->getBoolVar()]));
02038       if (res.length() > 0) {
02039         res.erase(0, 1); // Remove '='
02040         out << res;
02041       } else {
02042         out << bv1[ai->getBoolVar()];
02043       }
02044 #ifdef GECODE_HAS_SET_VARS
02045     } else if (ai->isSetVar()) {
02046       std::string res(Comparator::compare("",sv1[ai->getSetVar()],
02047                                           sv2[ai->getSetVar()]));
02048       if (res.length() > 0) {
02049         res.erase(0, 1); // Remove '='
02050         out << res;
02051       } else {
02052         out << sv1[ai->getSetVar()];
02053       }
02054 #endif
02055 #ifdef GECODE_HAS_FLOAT_VARS
02056     } else if (ai->isFloatVar()) {
02057       std::string res(Comparator::compare("",fv1[ai->getFloatVar()],
02058                                           fv2[ai->getFloatVar()]));
02059       if (res.length() > 0) {
02060         res.erase(0, 1); // Remove '='
02061         out << res;
02062       } else {
02063         out << fv1[ai->getFloatVar()];
02064       }
02065 #endif
02066     } else if (ai->isBool()) {
02067       out << (ai->getBool() ? "true" : "false");
02068     } else if (ai->isSet()) {
02069       AST::SetLit* s = ai->getSet();
02070       if (s->interval) {
02071         out << s->min << ".." << s->max;
02072       } else {
02073         out << "{";
02074         for (unsigned int i=0; i<s->s.size(); i++) {
02075           out << s->s[i] << (i < s->s.size()-1 ? ", " : "}");
02076         }
02077       }
02078     } else if (ai->isString()) {
02079       std::string s = ai->getString();
02080       for (unsigned int i=0; i<s.size(); i++) {
02081         if (s[i] == '\\' && i<s.size()-1) {
02082           switch (s[i+1]) {
02083           case 'n': out << "\n"; break;
02084           case '\\': out << "\\"; break;
02085           case 't': out << "\t"; break;
02086           default: out << "\\" << s[i+1];
02087           }
02088           i++;
02089         } else {
02090           out << s[i];
02091         }
02092       }
02093     }
02094 #endif
02095   }
02096 
02097   void
02098   Printer::print(std::ostream& out,
02099                    const Gecode::IntVarArray& iv,
02100                    const Gecode::BoolVarArray& bv
02101 #ifdef GECODE_HAS_SET_VARS
02102                    ,
02103                    const Gecode::SetVarArray& sv
02104 #endif
02105 #ifdef GECODE_HAS_FLOAT_VARS
02106                    ,
02107                    const Gecode::FloatVarArray& fv
02108 #endif
02109                    ) const {
02110     if (_output == NULL)
02111       return;
02112     for (unsigned int i=0; i< _output->a.size(); i++) {
02113       AST::Node* ai = _output->a[i];
02114       if (ai->isArray()) {
02115         AST::Array* aia = ai->getArray();
02116         int size = aia->a.size();
02117         out << "[";
02118         for (int j=0; j<size; j++) {
02119           printElem(out,aia->a[j],iv,bv
02120 #ifdef GECODE_HAS_SET_VARS
02121           ,sv
02122 #endif
02123 #ifdef GECODE_HAS_FLOAT_VARS
02124           ,fv
02125 #endif
02126           );
02127           if (j<size-1)
02128             out << ", ";
02129         }
02130         out << "]";
02131       } else {
02132         printElem(out,ai,iv,bv
02133 #ifdef GECODE_HAS_SET_VARS
02134         ,sv
02135 #endif
02136 #ifdef GECODE_HAS_FLOAT_VARS
02137           ,fv
02138 #endif
02139         );
02140       }
02141     }
02142   }
02143 
02144   void
02145   Printer::printDiff(std::ostream& out,
02146                    const Gecode::IntVarArray& iv1,
02147                    const Gecode::IntVarArray& iv2,
02148                    const Gecode::BoolVarArray& bv1,
02149                    const Gecode::BoolVarArray& bv2
02150 #ifdef GECODE_HAS_SET_VARS
02151                    ,
02152                    const Gecode::SetVarArray& sv1,
02153                    const Gecode::SetVarArray& sv2
02154 #endif
02155 #ifdef GECODE_HAS_FLOAT_VARS
02156                    ,
02157                    const Gecode::FloatVarArray& fv1,
02158                    const Gecode::FloatVarArray& fv2
02159 #endif
02160                    ) const {
02161     if (_output == NULL)
02162       return;
02163     for (unsigned int i=0; i< _output->a.size(); i++) {
02164       AST::Node* ai = _output->a[i];
02165       if (ai->isArray()) {
02166         AST::Array* aia = ai->getArray();
02167         int size = aia->a.size();
02168         out << "[";
02169         for (int j=0; j<size; j++) {
02170           printElemDiff(out,aia->a[j],iv1,iv2,bv1,bv2
02171 #ifdef GECODE_HAS_SET_VARS
02172             ,sv1,sv2
02173 #endif
02174 #ifdef GECODE_HAS_FLOAT_VARS
02175             ,fv1,fv2
02176 #endif
02177           );
02178           if (j<size-1)
02179             out << ", ";
02180         }
02181         out << "]";
02182       } else {
02183         printElemDiff(out,ai,iv1,iv2,bv1,bv2
02184 #ifdef GECODE_HAS_SET_VARS
02185           ,sv1,sv2
02186 #endif
02187 #ifdef GECODE_HAS_FLOAT_VARS
02188             ,fv1,fv2
02189 #endif
02190         );
02191       }
02192     }
02193   }
02194 
02195   void
02196   Printer::shrinkElement(AST::Node* node,
02197                          std::map<int,int>& iv, std::map<int,int>& bv, 
02198                          std::map<int,int>& sv, std::map<int,int>& fv) {
02199     if (node->isIntVar()) {
02200       AST::IntVar* x = static_cast<AST::IntVar*>(node);
02201       if (iv.find(x->i) == iv.end()) {
02202         int newi = iv.size();
02203         iv[x->i] = newi;
02204       }
02205       x->i = iv[x->i];
02206     } else if (node->isBoolVar()) {
02207       AST::BoolVar* x = static_cast<AST::BoolVar*>(node);
02208       if (bv.find(x->i) == bv.end()) {
02209         int newi = bv.size();
02210         bv[x->i] = newi;
02211       }
02212       x->i = bv[x->i];
02213     } else if (node->isSetVar()) {
02214       AST::SetVar* x = static_cast<AST::SetVar*>(node);
02215       if (sv.find(x->i) == sv.end()) {
02216         int newi = sv.size();
02217         sv[x->i] = newi;
02218       }
02219       x->i = sv[x->i];      
02220     } else if (node->isFloatVar()) {
02221       AST::FloatVar* x = static_cast<AST::FloatVar*>(node);
02222       if (fv.find(x->i) == fv.end()) {
02223         int newi = fv.size();
02224         fv[x->i] = newi;
02225       }
02226       x->i = fv[x->i];      
02227     }
02228   }
02229 
02230   void
02231   Printer::shrinkArrays(Space& home,
02232                         int& optVar, bool optVarIsInt,
02233                         Gecode::IntVarArray& iv,
02234                         Gecode::BoolVarArray& bv
02235 #ifdef GECODE_HAS_SET_VARS
02236                         ,
02237                         Gecode::SetVarArray& sv
02238 #endif
02239 #ifdef GECODE_HAS_FLOAT_VARS
02240                         ,
02241                         Gecode::FloatVarArray& fv
02242 #endif
02243                        ) {
02244     if (_output == NULL) {
02245       if (optVarIsInt && optVar != -1) {
02246         IntVar ov = iv[optVar];
02247         iv = IntVarArray(home, 1);
02248         iv[0] = ov;
02249         optVar = 0;
02250       } else {
02251         iv = IntVarArray(home, 0);
02252       }
02253       bv = BoolVarArray(home, 0);
02254 #ifdef GECODE_HAS_SET_VARS
02255       sv = SetVarArray(home, 0);
02256 #endif
02257 #ifdef GECODE_HAS_FLOAT_VARS
02258       if (!optVarIsInt && optVar != -1) {
02259         FloatVar ov = fv[optVar];
02260         fv = FloatVarArray(home, 1);
02261         fv[0] = ov;
02262         optVar = 0;
02263       } else {
02264         fv = FloatVarArray(home,0);
02265       }
02266 #endif
02267       return;
02268     }
02269     std::map<int,int> iv_new;
02270     std::map<int,int> bv_new;
02271     std::map<int,int> sv_new;
02272     std::map<int,int> fv_new;
02273 
02274     if (optVar != -1) {
02275       if (optVarIsInt)
02276         iv_new[optVar] = 0;
02277       else
02278         fv_new[optVar] = 0;
02279       optVar = 0;
02280     }
02281 
02282     for (unsigned int i=0; i< _output->a.size(); i++) {
02283       AST::Node* ai = _output->a[i];
02284       if (ai->isArray()) {
02285         AST::Array* aia = ai->getArray();
02286         for (unsigned int j=0; j<aia->a.size(); j++) {
02287           shrinkElement(aia->a[j],iv_new,bv_new,sv_new,fv_new);
02288         }
02289       } else {
02290         shrinkElement(ai,iv_new,bv_new,sv_new,fv_new);
02291       }
02292     }
02293 
02294     IntVarArgs iva(iv_new.size());
02295     for (map<int,int>::iterator i=iv_new.begin(); i != iv_new.end(); ++i) {
02296       iva[(*i).second] = iv[(*i).first];
02297     }
02298     iv = IntVarArray(home, iva);
02299 
02300     BoolVarArgs bva(bv_new.size());
02301     for (map<int,int>::iterator i=bv_new.begin(); i != bv_new.end(); ++i) {
02302       bva[(*i).second] = bv[(*i).first];
02303     }
02304     bv = BoolVarArray(home, bva);
02305 
02306 #ifdef GECODE_HAS_SET_VARS
02307     SetVarArgs sva(sv_new.size());
02308     for (map<int,int>::iterator i=sv_new.begin(); i != sv_new.end(); ++i) {
02309       sva[(*i).second] = sv[(*i).first];
02310     }
02311     sv = SetVarArray(home, sva);
02312 #endif
02313 
02314 #ifdef GECODE_HAS_FLOAT_VARS
02315     FloatVarArgs fva(fv_new.size());
02316     for (map<int,int>::iterator i=fv_new.begin(); i != fv_new.end(); ++i) {
02317       fva[(*i).second] = fv[(*i).first];
02318     }
02319     fv = FloatVarArray(home, fva);
02320 #endif
02321   }
02322 
02323   Printer::~Printer(void) {
02324     delete _output;
02325   }
02326 
02327 }}
02328 
02329 // STATISTICS: flatzinc-any