diff --git a/src/flatzinc/parser.cc b/src/flatzinc/parser.cc index bb3f002197..375672cf84 100644 --- a/src/flatzinc/parser.cc +++ b/src/flatzinc/parser.cc @@ -374,11 +374,16 @@ void ParserState::CreateModel() { VLOG(2) << " to_insert " << defines_and_require[i]->DebugString(); } + hash_set forced; while (!to_insert.empty()) { std::vector inserted; for (ConstIter > it(to_insert); !it.at_end(); ++it) { CtSpec* const spec = defines_and_require[*it]; VLOG(2) << "check " << spec->DebugString(); + if (ContainsKey(forced, spec->defines())) { + VLOG(2) << " - cleaning defines"; + spec->RemoveDefines(); + } bool ok = true; hash_set* const required = spec->require_map(); for (ConstIter > def(*required); @@ -397,9 +402,66 @@ void ParserState::CreateModel() { constraints_[index++] = spec; } } - CHECK(!inserted.empty()); - for (int i = 0; i < inserted.size(); ++i) { - to_insert.erase(inserted[i]); + if (inserted.empty()) { + // Recovery mode. We have a dependency!. Let's find the one + // with the smallest number of unsatisfied dependencies. + int to_correct = -1; + int best_unsatisfied = kint32max; + for (ConstIter > it(to_insert); !it.at_end(); ++it) { + CtSpec* const spec = defines_and_require[*it]; + VLOG(2) << "evaluate " << spec->DebugString(); + + int unsatisfied = 0; + hash_set* const required = spec->require_map(); + for (ConstIter > def(*required); + !def.at_end(); + ++def) { + const int dep = *def; + unsatisfied += !ContainsKey(defined, dep); + // Check not alias + if (dep > int_variables_.size()) { + // a bool var. + const int boolvar = dep - int_variables_.size(); + if (bool_variables_[boolvar]->alias) { + VLOG(2) << " - xb(" << boolvar << ") is an alias, disqualified"; + unsatisfied = kint32max; + break; + } + } else { + if (int_variables_[dep]->alias) { + VLOG(2) << " - xi(" << dep << ") is an alias, disqualified"; + unsatisfied = kint32max; + break; + } + } + } + CHECK_GT(unsatisfied, 0); + VLOG(2) << " - unsatisfied = " << unsatisfied; + if (unsatisfied < best_unsatisfied) { + best_unsatisfied = unsatisfied; + to_correct = *it; + } + } + CtSpec* const spec = defines_and_require[to_correct]; + VLOG(2) << "Lifting " << spec->DebugString() + << " with " << best_unsatisfied << " unsatisfied dependencies"; + hash_set* const required = spec->require_map(); + for (ConstIter > def(*required); + !def.at_end(); + ++def) { + const int dep = *def; + if (!ContainsKey(defined, dep)) { + candidates.erase(dep); + defined.insert(dep); + forced.insert(dep); + VLOG(2) << "removing " << dep + << " from set of candidates and forcing as defined"; + } + } + } else { + for (int i = 0; i < inserted.size(); ++i) { + to_insert.erase(inserted[i]); + } } } diff --git a/src/flatzinc/spec.h b/src/flatzinc/spec.h index d27e5df97d..2260cbd969 100644 --- a/src/flatzinc/spec.h +++ b/src/flatzinc/spec.h @@ -537,6 +537,7 @@ class CtSpec { ann_array->a.pop_back(); } } + defines_ = -1; } private: