48 namespace Gecode {
namespace FlatZinc {
59 int* newdom =
heap.
alloc<
int>(
static_cast<unsigned long int>(sl->
s.size()));
60 for (
int i=sl->
s.size();
i--;)
62 IntSet ret(newdom, sl->
s.size());
63 heap.
free(newdom, static_cast<unsigned long int>(sl->
s.size()));
95 if (
AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
96 if (s->id ==
"input_order")
98 if (s->id ==
"first_fail")
100 if (s->id ==
"anti_first_fail")
102 if (s->id ==
"smallest")
104 if (s->id ==
"largest")
106 if (s->id ==
"occurrence")
108 if (s->id ==
"max_regret")
110 if (s->id ==
"most_constrained")
113 if (s->id ==
"random")
115 if (s->id ==
"afc_min")
117 if (s->id ==
"afc_max")
119 if (s->id ==
"size_afc_min")
121 if (s->id ==
"size_afc_max")
124 std::cerr <<
"Warning, ignored search annotation: ";
125 ann->
print(std::cerr);
126 std::cerr << std::endl;
131 if (
AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
132 if (s->id ==
"indomain_min")
134 if (s->id ==
"indomain_max")
136 if (s->id ==
"indomain_median")
138 if (s->id ==
"indomain_split")
140 if (s->id ==
"indomain_reverse_split")
142 if (s->id ==
"indomain_random")
144 if (s->id ==
"indomain")
146 if (s->id ==
"indomain_middle") {
147 std::cerr <<
"Warning, replacing unsupported annotation "
148 <<
"indomain_middle with indomain_median" << std::endl;
151 if (s->id ==
"indomain_interval") {
152 std::cerr <<
"Warning, replacing unsupported annotation "
153 <<
"indomain_interval with indomain_split" << std::endl;
157 std::cerr <<
"Warning, ignored search annotation: ";
158 ann->
print(std::cerr);
159 std::cerr << std::endl;
164 if (
AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
165 if (s->id ==
"indomain_min")
167 if (s->id ==
"indomain_max")
169 if (s->id ==
"indomain_median")
171 if (s->id ==
"indomain_random")
174 std::cerr <<
"Warning, ignored search annotation: ";
175 ann->
print(std::cerr);
176 std::cerr << std::endl;
180 #ifdef GECODE_HAS_SET_VARS
182 if (
AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
183 if (s->id ==
"input_order")
185 if (s->id ==
"first_fail")
187 if (s->id ==
"anti_first_fail")
189 if (s->id ==
"smallest")
191 if (s->id ==
"largest")
194 std::cerr <<
"Warning, ignored search annotation: ";
195 ann->
print(std::cerr);
196 std::cerr << std::endl;
201 if (
AST::Atom* s = dynamic_cast<AST::Atom*>(ann)) {
202 if (s->id ==
"indomain_min")
204 if (s->id ==
"indomain_max")
206 if (s->id ==
"outdomain_min")
208 if (s->id ==
"outdomain_max")
211 std::cerr <<
"Warning, ignored search annotation: ";
212 ann->
print(std::cerr);
213 std::cerr << std::endl;
219 :
Space(share, f), _solveAnnotations(NULL), iv_boolalias(NULL) {
226 #ifdef GECODE_HAS_SET_VARS
233 : intVarCount(-1), boolVarCount(-1), setVarCount(-1), _optVar(-1),
234 _solveAnnotations(NULL) {}
250 #ifdef GECODE_HAS_SET_VARS
293 #ifdef GECODE_HAS_SET_VARS
305 int* is =
heap.
alloc<
int>(
static_cast<unsigned long int>(vsv->s.size()));
306 for (
int i=vsv->s.
size();
i--; )
309 heap.
free(is,static_cast<unsigned long int>(vsv->s.size()));
318 int* is =
heap.
alloc<
int>(
static_cast<unsigned long int>(vsv->
s.size()));
319 for (
int i=vsv->
s.size();
i--; )
322 heap.
free(is,static_cast<unsigned long int>(vsv->
s.size()));
351 for (
unsigned int i=0;
i<ann->
a.size();
i++) {
352 if (ann->
a[
i]->isCall(
"seq_search")) {
357 out.push_back(c->
args);
359 out.push_back(ann->
a[
i]);
373 std::vector<AST::Node*> flatAnn;
377 flatAnn.push_back(ann);
380 for (
unsigned int i=0;
i<flatAnn.
size();
i++) {
381 if (flatAnn[
i]->isCall(
"gecode_search")) {
383 branchWithPlugin(c->
args);
388 int k=vars->
a.size();
389 for (
int i=vars->
a.size();
i--;)
390 if (vars->
a[
i]->isInt())
394 for (
unsigned int i=0;
i<vars->
a.size();
i++) {
395 if (vars->
a[
i]->isInt())
397 va[k++] =
iv[vars->
a[
i]->getIntVar()];
406 int k=vars->
a.size();
407 for (
int i=vars->
a.size();
i--;)
408 if (vars->
a[
i]->isInt())
412 for (
unsigned int i=0;
i<vars->
a.size();
i++) {
413 if (vars->
a[
i]->isInt())
415 va[k++] =
iv[vars->
a[
i]->getIntVar()];
424 int k=vars->
a.size();
425 for (
int i=vars->
a.size();
i--;)
426 if (vars->
a[
i]->isBool())
430 for (
unsigned int i=0;
i<vars->
a.size();
i++) {
431 if (vars->
a[
i]->isBool())
433 va[k++] =
bv[vars->
a[
i]->getBoolVar()];
439 #ifdef GECODE_HAS_SET_VARS
444 int k=vars->
a.size();
445 for (
int i=vars->
a.size();
i--;)
446 if (vars->
a[
i]->isSet())
450 for (
unsigned int i=0;
i<vars->
a.size();
i++) {
451 if (vars->
a[
i]->isSet())
453 va[k++] =
sv[vars->
a[
i]->getSetVar()];
459 if (!ignoreUnknown) {
460 err <<
"Warning, ignored search annotation: ";
461 flatAnn[
i]->print(err);
466 if (!ignoreUnknown) {
467 err <<
"Warning, ignored search annotation: ";
468 flatAnn[
i]->print(err);
483 for (
int i=
iv.
size(), j=0, k=0; i--;)
490 for (
int i=
bv.
size(); i--;)
495 for (
int i=
bv.
size(), j=0, k=0; i--;)
503 #ifdef GECODE_HAS_SET_VARS
505 for (
int i=
sv.
size(); i--;)
510 for (
int i=
sv.
size(), j=0, k=0; i--;)
519 #ifdef GECODE_HAS_SET_VARS
575 #ifdef GECODE_HAS_GIST
580 template<
class Engine>
586 class GistEngine<
DFS<S> > {
588 static void explore(S* root,
const FlatZincOptions&
opt,
591 o.
c_d = opt.c_d(); o.
a_d = opt.a_d();
599 class GistEngine<BAB<S> > {
601 static void explore(S* root,
const FlatZincOptions& opt,
602 Gist::Inspector* i) {
604 o.
c_d = opt.c_d(); o.
a_d = opt.a_d();
612 class GistEngine<Restart<S> > {
614 static void explore(S* root,
const FlatZincOptions& opt,
615 Gist::Inspector* i) {
617 o.
c_d = opt.c_d(); o.
a_d = opt.a_d();
625 class FZPrintingInspector
631 FZPrintingInspector(
const Printer& p0);
633 virtual void inspect(
const Space& node);
635 virtual void finalize(
void);
639 FZPrintingInspector<S>::FZPrintingInspector(
const Printer& p0)
640 : TextOutput(
"Gecode/FlatZinc"),
p(p0) {}
644 FZPrintingInspector<S>::inspect(
const Space& node) {
646 dynamic_cast<const S&
>(node).
print(getStream(), p);
647 getStream() << std::endl;
652 FZPrintingInspector<S>::finalize(
void) {
658 template<
template<
class>
class Engine>
660 FlatZincSpace::runEngine(std::ostream& out,
const Printer& p,
661 const FlatZincOptions& opt, Support::Timer& t_total) {
662 #ifdef GECODE_HAS_GIST
664 FZPrintingInspector<FlatZincSpace> pi(p);
665 (void) GistEngine<Engine<FlatZincSpace> >::
explore(
this,opt,&pi);
669 StatusStatistics sstat;
670 unsigned int n_p = 0;
671 Support::Timer t_solve;
681 o.threads = opt.threads();
683 Engine<FlatZincSpace> se(
this,o);
684 int noOfSolutions =
_method ==
SAT ? opt.solutions() : 0;
685 bool printAll =
_method ==
SAT || opt.allSolutions();
686 int findSol = noOfSolutions;
693 out <<
"----------" << std::endl;
698 if (sol && !printAll) {
700 out <<
"----------" << std::endl;
704 out <<
"==========" << endl;
706 out <<
"=====UNSATISFIABLE=====" << endl;
709 out <<
"=====UNKNOWN=====" << endl;
724 <<
std::abs(noOfSolutions - findSol) << endl
727 <<
"%% propagators: " << n_p << endl
728 <<
"%% propagations: " << sstat.propagate+stat.
propagate << endl
729 <<
"%% nodes: " << stat.
node << endl
730 <<
"%% failures: " << stat.
fail << endl
731 <<
"%% peak depth: " << stat.
depth << endl
732 <<
"%% peak memory: "
733 << static_cast<int>((stat.
memory+1023) / 1024) <<
" KB"
740 FlatZincSpace::branchWithPlugin(AST::Node* ann) {
741 if (AST::Call*
c = dynamic_cast<AST::Call*>(ann)) {
742 QString pluginName(
c->id.c_str());
743 if (QLibrary::isLibrary(pluginName+
".dll")) {
744 pluginName +=
".dll";
745 }
else if (QLibrary::isLibrary(pluginName+
".dylib")) {
746 pluginName =
"lib" + pluginName +
".dylib";
747 }
else if (QLibrary::isLibrary(pluginName+
".so")) {
749 pluginName =
"lib" + pluginName +
".so";
751 QPluginLoader pl(pluginName);
752 QObject* plugin_o = pl.instance();
754 throw FlatZinc::Error(
"FlatZinc",
755 "Error loading plugin "+pluginName.toStdString()+
756 ": "+pl.errorString().toStdString());
758 BranchPlugin* pb = qobject_cast<BranchPlugin*>(plugin_o);
760 throw FlatZinc::Error(
"FlatZinc",
761 "Error loading plugin "+pluginName.toStdString()+
762 ": does not contain valid PluginBrancher");
764 pb->branch(*
this,
c);
769 FlatZincSpace::branchWithPlugin(AST::Node* ann) {
770 throw FlatZinc::Error(
"FlatZinc",
771 "Branching with plugins not supported (requires Qt support)");
782 runEngine<BAB>(out,p,opt,t_total);
784 runEngine<Restart>(out,
p,
opt,t_total);
787 runEngine<DFS>(out,
p,
opt,t_total);
796 static_cast<const FlatZincSpace*>(&s)->
iv[_optVar].val());
799 static_cast<const FlatZincSpace*>(&s)->
iv[_optVar].val());
841 Printer::printElem(std::ostream& out,
860 out <<
"false..true";
862 #ifdef GECODE_HAS_SET_VARS
868 SetVarGlbRanges svr(sv[ai->
getSetVar()]);
877 SetVarGlbValues svv(sv[ai->
getSetVar()]);
882 out <<
", " << svv.val();
885 out << min <<
".." <<
max;
888 }
else if (ai->
isBool()) {
889 out << (ai->
getBool() ?
"true" :
"false");
890 }
else if (ai->
isSet()) {
891 AST::SetLit* s = ai->
getSet();
893 out << s->
min <<
".." << s->max;
896 for (
unsigned int i=0; i<s->s.size(); i++) {
897 out << s->s[
i] << (i < s->s.size()-1 ?
", " :
"}");
902 for (
unsigned int i=0; i<s.size(); i++) {
903 if (s[i] ==
'\\' && i<s.size()-1) {
905 case 'n': out <<
"\n";
break;
906 case '\\': out <<
"\\";
break;
907 case 't': out <<
"\t";
break;
908 default: out <<
"\\" << s[i+1];
922 #ifdef GECODE_HAS_SET_VARS
929 for (
unsigned int i=0; i< _output->
a.size(); i++) {
933 int size = aia->
a.size();
935 for (
int j=0; j<
size; j++) {
936 printElem(out,aia->
a[j],iv,bv
937 #ifdef GECODE_HAS_SET_VARS
946 printElem(out,ai,iv,bv
947 #ifdef GECODE_HAS_SET_VARS
957 std::map<int,int>& iv, std::map<int,int>& bv,
958 std::map<int,int>& sv) {
961 if (iv.find(x->
i) == iv.end()) {
962 int newi = iv.size();
968 if (bv.find(x->
i) == bv.end()) {
969 int newi = bv.size();
975 if (sv.find(x->
i) == sv.end()) {
976 int newi = sv.size();
988 #ifdef GECODE_HAS_SET_VARS
993 if (_output == NULL) {
1003 #ifdef GECODE_HAS_SET_VARS
1008 std::map<int,int> iv_new;
1009 std::map<int,int> bv_new;
1010 std::map<int,int> sv_new;
1017 for (
unsigned int i=0; i< _output->
a.size(); i++) {
1021 for (
unsigned int j=0; j<aia->
a.size(); j++) {
1030 for (map<int,int>::iterator i=iv_new.begin(); i != iv_new.end(); ++
i) {
1031 iva[(*i).second] = iv[(*i).first];
1036 for (map<int,int>::iterator i=bv_new.begin(); i != bv_new.end(); ++
i) {
1037 bva[(*i).second] = bv[(*i).first];
1041 #ifdef GECODE_HAS_SET_VARS
1043 for (map<int,int>::iterator i=sv_new.begin(); i != sv_new.end(); ++
i) {
1044 sva[(*i).second] = sv[(*i).first];