Index: Makefile.in =================================================================== --- Makefile.in (revision 11521) +++ Makefile.in (working copy) @@ -653,8 +653,13 @@ FLATZINCEXEOBJ = $(FLATZINCEXESRC:%.cpp=%$(OBJSUFFIX)) FLATZINCEXE = tools/flatzinc/fz$(EXESUFFIX) -FLATZINCALLSRC = $(FLATZINCSRC) $(FLATZINCEXESRC) +FLATZINCQXEXESRC0 = fz-qx.cpp +FLATZINCQXEXESRC = $(FLATZINCQXEXESRC0:%=tools/flatzinc/%) +FLATZINCQXEXEOBJ = $(FLATZINCQXEXESRC:%.cpp=%$(OBJSUFFIX)) +FLATZINCQXEXE = tools/flatzinc/fz-qx$(EXESUFFIX) +FLATZINCALLSRC = $(FLATZINCSRC) $(FLATZINCEXESRC) $(FLATZINCQXEXESRC) + FLATZINCBUILDDIRS = gecode/flatzinc tools/flatzinc ifeq "@enable_flatzinc@" "yes" @@ -813,7 +818,7 @@ PDBTARGETS = endif -EXETARGETS = $(FLATZINCEXE) +EXETARGETS = $(FLATZINCEXE) $(FLATZINCQXEXE) # # Testing @@ -1380,7 +1385,7 @@ .PHONY: flatzinc ifeq "@enable_flatzinc@" "yes" -flatzinc: $(FLATZINCEXE) +flatzinc: $(FLATZINCEXE) $(FLATZINCQXEXE) else flatzinc: endif @@ -1390,7 +1395,12 @@ $(LINKALL) $(LINKSTATICQT) $(GLDFLAGS) $(MANIFEST) -manifest $@.manifest -outputresource:$@\;1 +$(FLATZINCQXEXE): $(FLATZINCQXEXEOBJ) $(ALLLIB) + $(CXX) @EXEOUTPUT@$@ $(FLATZINCQXEXEOBJ) $(DLLPATH) $(CXXFLAGS) \ + $(LINKALL) $(LINKSTATICQT) $(GLDFLAGS) + $(MANIFEST) -manifest $@.manifest -outputresource:$@\;1 + # # Autoconf # @@ -1704,6 +1714,8 @@ $(TESTEXE:%=%.manifest) $(RMF) $(FLATZINCEXE) $(FLATZINCEXE:%.exe=%.pdb) \ $(FLATZINCEXE:%.exe=%.ilk) $(FLATZINCEXE:%=%.manifest) + $(RMF) $(FLATZINCQXEXE) $(FLATZINCQXEXE:%.exe=%.pdb) \ + $(FLATZINCQXEXE:%.exe=%.ilk) $(FLATZINCQXEXE:%=%.manifest) $(RMF) doc GecodeReference.chm ChangeLog changelog.hh doxygen.hh $(RMF) $(ALLOBJ:%$(OBJSUFFIX)=%.gcno) $(TESTOBJ:%$(OBJSUFFIX)=%.gcno) $(RMF) $(ALLOBJ:%$(OBJSUFFIX)=%.gcda) $(TESTOBJ:%$(OBJSUFFIX)=%.gcda) Index: gecode/flatzinc.hh =================================================================== --- gecode/flatzinc.hh (revision 11521) +++ gecode/flatzinc.hh (working copy) @@ -47,6 +47,7 @@ #endif #include +#include /* * Support for DLLs under Windows @@ -242,6 +243,62 @@ }; /** + * \brief %Options for running %FlatZinc models with QuickXplain + * + */ + class FlatZincQuickxplainOptions : public Gecode::BaseOptions { + protected: + /// \name Search options + //@{ + Gecode::Driver::DoubleOption _threads; ///< How many threads to use + Gecode::Driver::DoubleOption _parallel; ///< Use all cores + Gecode::Driver::BoolOption _free; ///< Use free search + Gecode::Driver::StringOption _search; ///< Search engine variant + Gecode::Driver::UnsignedIntOption _c_d; ///< Copy recomputation distance + Gecode::Driver::UnsignedIntOption _a_d; ///< Adaptive recomputation distance + //@} + + public: + enum SearchOptions { + FZ_SEARCH_BAB, //< Branch-and-bound search + FZ_SEARCH_RESTART //< Restart search + }; + /// Constructor + FlatZincQuickxplainOptions(const char* s) + : Gecode::BaseOptions(s), + _threads("-threads","number of threads (0 = #processing units)", + Gecode::Search::Config::threads), + _parallel("--parallel", "equivalent to -threads", + Gecode::Search::Config::threads), + _free("--free", "no need to follow search-specification"), + _search("-search","search engine variant", FZ_SEARCH_BAB), + _c_d("-c-d","recomputation commit distance",Gecode::Search::Config::c_d), + _a_d("-a-d","recomputation adaption distance",Gecode::Search::Config::a_d) { + _search.add(FZ_SEARCH_BAB, "bab"); + _search.add(FZ_SEARCH_RESTART, "restart"); + add(_threads); add(_c_d); add(_a_d); + add(_parallel); + add(_free); + add(_search); + } + + void parse(int& argc, char* argv[]) { + Gecode::BaseOptions::parse(argc,argv); + if (_parallel.value() != Gecode::Search::Config::threads && + _threads.value() == Gecode::Search::Config::threads) + _threads.value(_parallel.value()); + } + + double threads(void) const { return _threads.value(); } + bool free(void) const { return _free.value(); } + SearchOptions search(void) const { + return static_cast(_search.value()); + } + unsigned int c_d(void) const { return _c_d.value(); } + unsigned int a_d(void) const { return _a_d.value(); } + }; + + /** * \brief A space that can be initialized with a %FlatZinc model * */ @@ -277,6 +334,11 @@ void runEngine(std::ostream& out, const Printer& p, const FlatZincOptions& opt, Gecode::Support::Timer& t_total); + + template class Engine> + bool + isSatisfiableRunEngine(const FlatZincQuickxplainOptions& opt); + void branchWithPlugin(AST::Node* ann); public: @@ -296,6 +358,17 @@ /// Indicates whether a set variable is introduced by mzn2fzn std::vector sv_introduced; #endif + + /// Indicates whether parse() should post or store constraints + bool postDuringParse; + + /// Maps to store constraints + std::map constraintConExprStore; + std::map constraintASTNodeStore; + + /// Counter to keep track of constraint order + int constraintCount; + /// Construct empty space FlatZincSpace(void); @@ -318,7 +391,22 @@ /// Post a constraint specified by \a ce void postConstraint(const ConExpr& ce, AST::Node* annotation); + + /// Store a constraint specified by \a ce + void storeConstraint(const ConExpr& ce, AST::Node* annotation); + + /// Post all stored constraints + void postStoredConstraints(); + + /// Post a particular constraint + void postStoredConstraint(int i); + + /// Post stored constraints from set + void postStoredConstraints(std::set c); + /// Delete stored constraints from set + void deleteStoredConstraints(std::set c); + /// Post the solve item void solve(AST::Array* annotation); /// Post that integer variable \a var should be minimized @@ -330,6 +418,8 @@ void run(std::ostream& out, const Printer& p, const FlatZincOptions& opt, Gecode::Support::Timer& t_total); + bool isSatisfiable(const FlatZincQuickxplainOptions& opt); + /// Produce output on \a out using \a p void print(std::ostream& out, const Printer& p) const; @@ -385,7 +475,7 @@ GECODE_FLATZINC_EXPORT FlatZincSpace* parse(const std::string& fileName, Printer& p, std::ostream& err = std::cerr, - FlatZincSpace* fzs=NULL); + FlatZincSpace* fzs=NULL, bool post = true); /** * \brief Parse FlatZinc from \a is into \a fzs and return it. @@ -395,7 +485,7 @@ GECODE_FLATZINC_EXPORT FlatZincSpace* parse(std::istream& is, Printer& p, std::ostream& err = std::cerr, - FlatZincSpace* fzs=NULL); + FlatZincSpace* fzs=NULL, bool post = true); }} Index: gecode/flatzinc/parser.yxx =================================================================== --- gecode/flatzinc/parser.yxx (revision 11521) +++ gecode/flatzinc/parser.yxx (working copy) @@ -214,7 +214,11 @@ if (!pp->hadError) { try { assert(pp->domainConstraints[i]->args->a.size() == 2); - pp->fg->postConstraint(*pp->domainConstraints[i], NULL); + if (pp->fg->postDuringParse) { + pp->fg->postConstraint(*pp->domainConstraints[i], NULL); + } else { + pp->fg->storeConstraint(*pp->domainConstraints[i], NULL); + } delete pp->domainConstraints[i]; } catch (Gecode::FlatZinc::Error& e) { yyerror(pp, e.toString().c_str()); @@ -270,8 +274,8 @@ namespace Gecode { namespace FlatZinc { - FlatZincSpace* parse(const std::string& filename, Printer& p, std::ostream& err, - FlatZincSpace* fzs) { + FlatZincSpace* parse(const std::string& filename, Printer& p, + std::ostream& err, FlatZincSpace* fzs, bool post) { #ifdef HAVE_MMAP int fd; char* data; @@ -294,6 +298,7 @@ if (fzs == NULL) { fzs = new FlatZincSpace(); } + fzs->postDuringParse = post; ParserState pp(data, sbuf.st_size, err, fzs); #else std::ifstream file; @@ -307,6 +312,7 @@ if (fzs == NULL) { fzs = new FlatZincSpace(); } + fzs->postDuringParse = post; ParserState pp(s, err, fzs); #endif yylex_init(&pp.yyscanner); @@ -320,14 +326,15 @@ return pp.hadError ? NULL : pp.fg; } - FlatZincSpace* parse(std::istream& is, Printer& p, std::ostream& err, - FlatZincSpace* fzs) { + FlatZincSpace* parse(std::istream& is, Printer& p, std::ostream& err, + FlatZincSpace* fzs, bool post) { std::string s = string(istreambuf_iterator(is), istreambuf_iterator()); if (fzs == NULL) { fzs = new FlatZincSpace(); } + fzs->postDuringParse = post; ParserState pp(s, err, fzs); yylex_init(&pp.yyscanner); yyset_extra(&pp, pp.yyscanner); @@ -1177,7 +1184,11 @@ if (!pp->hadError) { ConExpr c($2, $4); try { - pp->fg->postConstraint(c, $6); + if (pp->fg->postDuringParse) { + pp->fg->postConstraint(c, $6); + } else { + pp->fg->storeConstraint(c, $6); + } } catch (Gecode::FlatZinc::Error& e) { yyerror(pp, e.toString().c_str()); } Index: gecode/flatzinc/ast.hh =================================================================== --- gecode/flatzinc/ast.hh (revision 11521) +++ gecode/flatzinc/ast.hh (working copy) @@ -132,6 +132,9 @@ /// Output string representation virtual void print(std::ostream&) = 0; + + /// Clone + virtual Node* clone() = 0; }; /// Boolean literal node @@ -142,6 +145,9 @@ virtual void print(std::ostream& os) { os << "b(" << (b ? "true" : "false") << ")"; } + virtual BoolLit* clone() { + return new BoolLit(b); + } }; /// Integer literal node class IntLit : public Node { @@ -151,6 +157,9 @@ virtual void print(std::ostream& os) { os << "i("< cloneA(a.size()); + for (unsigned int i = 0; i < a.size(); i++) { + cloneA[i] = a[i]->clone(); + } + + return new Array(cloneA); + } }; /// %Node representing a function call @@ -258,6 +297,10 @@ throw TypeError("arity mismatch"); return a; } + virtual Call* clone() { + Node* cloneArgs = args->clone(); + return new Call(id, cloneArgs); + } }; /// %Node representing an array access @@ -274,6 +317,11 @@ idx->print(os); os << "]"; } + virtual ArrayAccess* clone() { + Node* cloneA = a->clone(); + Node* cloneIdx = idx->clone(); + return new ArrayAccess(cloneA, cloneIdx); + } }; /// %Node representing an atom @@ -284,6 +332,9 @@ virtual void print(std::ostream& os) { os << id; } + virtual Atom* clone () { + return new Atom(id); + } }; /// %String node @@ -294,6 +345,9 @@ virtual void print(std::ostream& os) { os << "s(\"" << s << "\")"; } + virtual String* clone() { + return new String(s); + } }; inline Index: gecode/flatzinc/flatzinc.cpp =================================================================== --- gecode/flatzinc/flatzinc.cpp (revision 11521) +++ gecode/flatzinc/flatzinc.cpp (working copy) @@ -43,6 +43,7 @@ #include #include +#include using namespace std; namespace Gecode { namespace FlatZinc { @@ -206,7 +207,7 @@ #endif FlatZincSpace::FlatZincSpace(bool share, FlatZincSpace& f) - : Space(share, f), _solveAnnotations(NULL), iv_boolalias(NULL) { + : Space(share, f) { _optVar = f._optVar; _method = f._method; iv.update(*this, share, f.iv); @@ -217,11 +218,61 @@ sv.update(*this, share, f.sv); setVarCount = f.setVarCount; #endif + // copy introduced variables + iv_introduced = std::vector(intVarCount); + iv_introduced = f.iv_introduced; + int iv_boolaliasSize = intVarCount+(intVarCount==0?1:0); + iv_boolalias = alloc(iv_boolaliasSize); + iv_boolalias = f.iv_boolalias; + bv_introduced = std::vector(boolVarCount); + bv_introduced = f.bv_introduced; +#ifdef GECODE_HAS_SET_VARS + sv_introduced = std::vector(setVarCount); + sv_introduced = f.sv_introduced; +#endif + + // copy solve annotations + if (f._solveAnnotations) { + if (share) { + _solveAnnotations = f._solveAnnotations; + } else { + _solveAnnotations = f._solveAnnotations->clone(); + } + } else { + _solveAnnotations = NULL; + } + + // copy constraint store + constraintCount = f.constraintCount; + + std::map::iterator cit = f.constraintConExprStore.begin(); + while (cit != f.constraintConExprStore.end()) { + if (share) { + constraintConExprStore[cit->first] = f.constraintConExprStore[cit->first]; + } else { + constraintConExprStore[cit->first] = f.constraintConExprStore[cit->first]->clone(); + } + cit++; + } + + std::map::iterator ait = f.constraintASTNodeStore.begin(); + while (ait != f.constraintASTNodeStore.end()) { + if (f.constraintASTNodeStore[ait->first]) { + if (share) { + constraintASTNodeStore[ait->first] = f.constraintASTNodeStore[ait->first]; + } else { + constraintASTNodeStore[ait->first] = f.constraintASTNodeStore[ait->first]->clone(); + } + } else { + constraintASTNodeStore[ait->first] = NULL; + } + ait++; + } } FlatZincSpace::FlatZincSpace(void) : intVarCount(-1), boolVarCount(-1), setVarCount(-1), _optVar(-1), - _solveAnnotations(NULL) {} + _solveAnnotations(NULL), constraintCount(-1) {} void FlatZincSpace::init(int intVars, int boolVars, @@ -242,6 +293,9 @@ sv = SetVarArray(*this, setVars); sv_introduced = std::vector(setVars); #endif + constraintCount = 0; + std::map constraintConExprStore; + std::map constraintASTNodeStore; } void @@ -331,6 +385,51 @@ } } + void + FlatZincSpace::storeConstraint(const ConExpr& ce, AST::Node* ann) { + constraintConExprStore[constraintCount] = ce.clone(); + if (ann) { + constraintASTNodeStore[constraintCount] = ann->clone(); + } else { + constraintASTNodeStore[constraintCount] = NULL; + } + constraintCount++; + } + + void FlatZincSpace::postStoredConstraints() { + for (int i = 0; i < constraintCount; i++) { + postConstraint(*constraintConExprStore[i], constraintASTNodeStore[i]); + } + } + + void FlatZincSpace::postStoredConstraint(int i) { + if (constraintConExprStore[i]) { + postConstraint(*constraintConExprStore[i], constraintASTNodeStore[i]); + } + } + + void FlatZincSpace::postStoredConstraints(set c) { + set::iterator it = c.begin(); + + while (it != c.end()) { + postStoredConstraint(*it); + it++; + } + } + + void FlatZincSpace::deleteStoredConstraints(set c) { + set::iterator it = c.begin(); + + while (it != c.end()) { + delete constraintConExprStore[*it]; + delete constraintASTNodeStore[*it]; + constraintConExprStore.erase(*it); + constraintASTNodeStore.erase(*it); + it++; + constraintCount--; + } + } + void flattenAnnotations(AST::Array* ann, std::vector& out) { for (unsigned int i=0; ia.size(); i++) { if (ann->a[i]->isCall("seq_search")) { @@ -547,7 +646,6 @@ } FlatZincSpace::~FlatZincSpace(void) { - delete _solveAnnotations; } #ifdef GECODE_HAS_GIST @@ -712,6 +810,31 @@ } } + template class Engine> + bool + FlatZincSpace::isSatisfiableRunEngine(const FlatZincQuickxplainOptions& opt) { + Search::Options o; + o.c_d = opt.c_d(); + o.a_d = opt.a_d(); + o.threads = opt.threads(); + Driver::Cutoff::installCtrlHandler(true); + Engine se(this,o); + + FlatZincSpace* sol = NULL; + if (FlatZincSpace* next_sol = se.next()) { + sol = next_sol; + } + + bool foundSolution = false; + if (sol) { + foundSolution = true; + } + + delete sol; + + return foundSolution; + } + #ifdef GECODE_HAS_QT void FlatZincSpace::branchWithPlugin(AST::Node* ann) { @@ -766,6 +889,23 @@ } } + bool + FlatZincSpace::isSatisfiable(const FlatZincQuickxplainOptions& opt) { + switch (_method) { + case MIN: + case MAX: + if (opt.search() == FlatZincOptions::FZ_SEARCH_BAB) + return isSatisfiableRunEngine(opt); + else + return isSatisfiableRunEngine(opt); + break; + case SAT: + return isSatisfiableRunEngine(opt); + break; + } + return false; + } + void FlatZincSpace::constrain(const Space& s) { if (_method == MIN) Index: gecode/flatzinc/conexpr.hh =================================================================== --- gecode/flatzinc/conexpr.hh (revision 11521) +++ gecode/flatzinc/conexpr.hh (working copy) @@ -50,8 +50,12 @@ std::string id; /// Constraint arguments AST::Array* args; + /// Default constructor + ConExpr(); /// Constructor ConExpr(const std::string& id0, AST::Array* args0); + /// Clone + ConExpr* clone() const; /// Return argument \a i AST::Node* operator[](int i) const; /// Destructor @@ -59,9 +63,24 @@ }; forceinline + ConExpr::ConExpr() {} + + forceinline ConExpr::ConExpr(const std::string& id0, AST::Array* args0) : id(id0), args(args0) {} + forceinline ConExpr* + ConExpr::clone() const { + ConExpr* ceClone = new ConExpr(); + ceClone->id = id; + ceClone->args = new AST::Array(args->a.size()); + for (unsigned int i = 0; i < args->a.size(); i++) { + ceClone->args->a[i] = args->a[i]->clone(); + } + + return ceClone; + } + forceinline AST::Node* ConExpr::operator[](int i) const { return args->a[i]; } Index: tools/flatzinc/fz-qx.cpp =================================================================== --- tools/flatzinc/fz-qx.cpp (revision 0) +++ tools/flatzinc/fz-qx.cpp (revision 0) @@ -0,0 +1,337 @@ +/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */ +/* + * Main authors: + * Guido Tack + * Adriane Boyd + * + * Copyright: + * Guido Tack, Adriane Boyd, 2010 + * + * Permission is hereby granted, free of charge, to any person obtaining + * a copy of this software and associated documentation files (the + * "Software"), to deal in the Software without restriction, including + * without limitation the rights to use, copy, modify, merge, publish, + * distribute, sublicense, and/or sell copies of the Software, and to + * permit persons to whom the Software is furnished to do so, subject to + * the following conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF + * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE + * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION + * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION + * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + */ + +#include +#include +#include +#include + +using namespace std; +using namespace Gecode; + +struct FlatZincSpaceInfo { + FlatZinc::FlatZincSpace* fg; + FlatZinc::Printer& p; + FlatZinc::FlatZincQuickxplainOptions& opt; + Support::Timer& t_total; + bool debug; +}; + +set getConflicts(FlatZincSpaceInfo* s, set fgc); +set quickxplain(FlatZincSpaceInfo* s, set bgc, set fgc); +bool runSpace(FlatZincSpaceInfo* s, set c); +int findFirstFailure(FlatZincSpaceInfo* s, set bgc, + set fgc); +int failureSearch(FlatZincSpaceInfo* s, FlatZinc::FlatZincSpace* fg, + FlatZinc::FlatZincSpace* fg0, set* c, + int lo, int hi); +void printSet(set s); + +int main(int argc, char** argv) { + + Support::Timer t_total; + t_total.start(); + FlatZinc::FlatZincQuickxplainOptions opt("Gecode/FlatZinc QuickXplain"); + opt.parse(argc, argv); + + if (argc!=2) { + cerr << "Usage: " << argv[0] << " [options] " << endl; + cerr << " " << argv[0] << " -help for more information" << endl; + exit(EXIT_FAILURE); + } + + const char* filename = argv[1]; + opt.name(filename); + + FlatZinc::Printer p; + FlatZinc::FlatZincSpace* fg = NULL; + if (!strcmp(filename, "-")) { + fg = FlatZinc::parse(cin, p, std::cerr, NULL, false); + } else { + fg = FlatZinc::parse(filename, p, std::cerr, NULL, false); + } + + if (fg) { + // add all constraints to the foreground + // (if required, you can easily replace this with your + // own method that identifies constraints that are never + // part of a conflict and posts them at this point) + // set bgc, fgc; + // preprocessConstraints(fg, &bgc, &fgc); + // fg->postStoredConstraints(bgc); + // fg->deleteStoredConstraints(bgc); + set fgc; + for (int i = 0; i < fg->constraintCount; i++) { + fgc.insert(i); + } + + fg->createBranchers(fg->solveAnnotations(), false, std::cerr); + + // find and print out conflicts + FlatZincSpaceInfo s = {fg, p, opt, t_total, false}; // change to true + // for debugging info + set conflicts = getConflicts(&s, fgc); + + if (conflicts.size() > 0) { + cout << "Constraints in the input have been numbered sequentially starting at 0." << endl; + cout << "Conflicts found by QuickXplain: "; + printSet(conflicts); + } else { + cout << "No conflicts!" << endl; + } + } else { + exit(EXIT_FAILURE); + } + delete fg; + + return 0; +} + +/** + * Wrapper for quickxplain(). + * + */ +set getConflicts(FlatZincSpaceInfo *s, set fgc) { + set emptySet, conflicts; + + // if no conflicts, return + if (runSpace(s, fgc)) { + return emptySet; + } + conflicts = quickxplain(s, emptySet, fgc); + return conflicts; +} + +/** + * QUICKXPLAIN algorithm from Junker (2004): + * + * Ulrich Junker, 2004. QUICKXPLAIN: Preferred Explanations and + * Relaxations for Over-Constrained Problems. AAAI 2004: 167-172. + * + */ +set quickxplain(FlatZincSpaceInfo* s, set bgc, set fgc) { + set emptySet; + + // check that the background is satisfiable + if (!runSpace(s, bgc)) { + return emptySet; + } + + // check that the current foreground is not empty + // if so, something has gone wrong + if (fgc.empty()) { + exit(EXIT_FAILURE); + } + + // find k where bgc + fgc[1 - (k-1)] is satisfiable and + // bgc + fgc[1 - k] is not + unsigned int k = findFirstFailure(s, bgc, fgc); + + // split the constraints fgc[1 - (k-1)] into two halves, u1 and u2 + unsigned int split = k / 2; + + set::iterator it; + set u1, u2, x; + it = fgc.begin(); + for (unsigned int i = 0; i < k; i++) { + if (i <= split) { + u1.insert(*it); + } else { + u2.insert(*it); + } + + it++; + } + + // add the kth constraint to the current set of conflicts + x.insert(*it); + int k_x = *it; + + set delta1, delta2; + + // check for conflicts in u2 + if (u2.size() > 0) { + // create background for u2 + set bgi; + bgi.insert(bgc.begin(), bgc.end()); + it = fgc.begin(); + for (unsigned int i = 0; i <=split; i++) { + bgi.insert(*it); + it++; + } + bgi.insert(k_x); + + delta2 = quickxplain(s, bgi, u2); + x.insert(delta2.begin(), delta2.end()); + } + + // check for conflicts in u1 + if (u1.size() > 0) { + // create background for u1 + set bg0; + bg0.insert(bgc.begin(), bgc.end()); + bg0.insert(x.begin(), x.end()); + delta1 = quickxplain(s, bg0, u1); + x.insert(delta1.begin(), delta1.end()); + } + + // return the current set of known conflicts + return x; +} + +/** + * Return whether the space is not failed with the given constraints. + * + */ +bool runSpace(FlatZincSpaceInfo* s, set c) { + // create a clone of fg to work on and post constraints + FlatZinc::FlatZincSpace* fg = (FlatZinc::FlatZincSpace*) s->fg->clone(); + fg->postStoredConstraints(c); + + bool ret = false; + + if (s->debug) { + cout << "Running with # constraints: " << c.size() << endl; + } + + ret = fg->isSatisfiable(s->opt); + + if (s->debug) { + cout << "Status: " << fg->status() << endl; + cout << "Satisfiable: " << ret << endl; + cout << endl; + } + + delete fg; + + return ret; +} + +/** + * Wrapper that posts background constraints and sets up variables + * needed for failureSearch(). + * + */ +int findFirstFailure(FlatZincSpaceInfo* s, set bgc, set fgc) { + // create a clone for the search to use as a reference + FlatZinc::FlatZincSpace* fg = (FlatZinc::FlatZincSpace*) s->fg->clone(); + + // post bg constraints to the reference clone + set::iterator it = bgc.begin(); + while (it != bgc.end()) { + fg->postStoredConstraint(*it); + it++; + } + fg->status(); + + // create a clone of the reference clone for the search to modify + FlatZinc::FlatZincSpace* fg2 = (FlatZinc::FlatZincSpace*) fg->clone(); + + int k = failureSearch(s, fg2, fg, &fgc, 0, fgc.size() - 1); + + if (s->debug) { + cout << "Failed at k: " << k << endl; + cout << endl; + } + + delete fg; + delete fg2; + + return k; +} + +/** + * A recursive binary search for the constraint index in c at which + * space fg with constraints c[0..k-1] is satisfiable but with + * constraints c[0..k] is not. + * + */ +int failureSearch(FlatZincSpaceInfo* s, FlatZinc::FlatZincSpace* fg, + FlatZinc::FlatZincSpace* fg0, set* c, + int lo, int hi) { + + if (s->debug) { + cout << "Searching for k between: " << lo << "/" << hi << endl; + } + + if (lo == hi) { + return lo; + } + + // the space should fail at some point, + // so this should never happen + if (hi < lo) { + cerr << "Problem finding failed constraint." << endl; + exit(EXIT_FAILURE); + } + + // at this point c[0..lo-1] are already posted + + // find the midpoint + int mi = lo + ((hi - lo) / 2); + + // post c[lo..mi-1] in fg + set::iterator it = c->begin(); + advance(it, lo); + for (int i = lo; i <= mi; i++) { + fg->postStoredConstraint(*it); + it++; + } + + if (fg->isSatisfiable(s->opt)) { + // continue to use fg since we are only adding constraints + return failureSearch(s, fg, fg0, c, mi + 1, hi); + } + + // clone fg0 in order to create a space with c[0..lo-1] posted + FlatZinc::FlatZincSpace* fg2 = (FlatZinc::FlatZincSpace*) fg0->clone(); + + it = c->begin(); + for (int i = 0; i < lo; i++) { + fg2->postStoredConstraint(*it); + it++; + } + + int ret = failureSearch(s, fg2, fg0, c, lo, mi); + + delete fg2; + + return ret; +} + +void printSet(set s) { + set::iterator it; + for (it = s.begin(); it != s.end(); it++) { + cout << *it << " "; + } + cout << endl; +} + +// STATISTICS: flatzinc-any