text: //
  // Copyright (c) 2010-2017 Benjamin Kaufmann
  //
  // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/
  //
  // 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 <clasp/minimize_constraint.h>
  #include <clasp/solver.h>
  #include <clasp/weight_constraint.h>
  #include <clasp/clause.h>
  #include <cmath>
  namespace Clasp {
  /////////////////////////////////////////////////////////////////////////////////////////
  // SharedMinimizeData
  /////////////////////////////////////////////////////////////////////////////////////////
  SharedMinimizeData::SharedMinimizeData(const SumVec& lhsAdjust, MinimizeMode m) : mode_(m) {
  	adjust_ = lhsAdjust;
  	lower_  = new LowerType[adjust_.size()];
  	count_  = 1;
  	resetBounds();
  	setMode(MinimizeMode_t::optimize);
  }
  SharedMinimizeData::~SharedMinimizeData() {
  	delete[] lower_;
  }
  
  void SharedMinimizeData::destroy() const {
  	this->~SharedMinimizeData();
  	::operator delete(const_cast<SharedMinimizeData*>(this));
  }
  
  void SharedMinimizeData::resetBounds() {
  	gCount_  = 0;
  	optGen_  = 0;
  	std::fill_n(lower_, numRules(), wsum_t(0));
  	up_[0].assign(numRules(), maxBound());
  	up_[1].assign(numRules(), maxBound());
  	const WeightLiteral* lit = lits;
  	for (weight_t wPos = 0, end = (weight_t)weights.size(), x; wPos != end; wPos = x+1) {
  		assert(weights[wPos].weight >= 0);
  		for (x = wPos; weights[x].next; ) { // compound weight - check for negative
  			if (weights[++x].weight < 0) {
  				while (lit->second != wPos) { ++lit; }
  				for (const WeightLiteral* t = lit; t->second == wPos; ++t) {
  					lower_[weights[x].level] += weights[x].weight;
  				}
  			}
  		}
  	}
  }
  
  bool SharedMinimizeData::setMode(MinimizeMode m, const wsum_t* bound, uint32 boundSize)  {
  	mode_ = m;
  	if (boundSize && bound) {
  		SumVec& opt = up_[0];
  		bool    ok  = false;
  		gCount_     = 0;
  		optGen_     = 0;
  		boundSize   = std::min(boundSize, numRules());
  		for (uint32 i = 0, end = boundSize; i != end; ++i) {
  			wsum_t B = bound[i], a = adjust(i);
  			B        = a >= 0 || (maxBound() + a) >= B ? B - a : maxBound();
  			wsum_t d = B - lower_[i];
  			if (d < 0 && !ok) { return false; }
  			opt[i]   = B;
  			ok       = ok || d > 0;
  		}
  		for (uint32 i = boundSize, end = (uint32)opt.size(); i != end; ++i) { opt[i] = maxBound(); }
  	}
  	return true;
  }
  
  MinimizeConstraint* SharedMinimizeData::attach(Solver& s, const OptParams& params, bool addRef) {
  	if (addRef) this->share();
  	MinimizeConstraint* ret;
  	if (params.type == OptParams::type_bb || mode() == MinimizeMode_t::enumerate) {
  		ret = new DefaultMinimize(this, params);
  	}
  	else {
  		ret = new UncoreMinimize(this, params);
  	}
  	ret->attach(s);
  	return ret;
  }
  
  const SumVec* SharedMinimizeData::setOptimum(const wsum_t* newOpt) {
  	if (optGen_) { return up_ + (optGen_&1u); }
  	uint32  g = gCount_;
  	uint32  n = 1u - (g & 1u);
  	SumVec& U = up_[n];
  	U.assign(newOpt, newOpt + numRules());
  	assert(mode() != MinimizeMode_t::enumerate || n == 1);
  	if (mode() != MinimizeMode_t::enumerate) {
  		if (++g == 0) { g = 2; }
  		gCount_  = g;
  	}
  	return &U;
  }
  void SharedMinimizeData::setLower(uint32 lev, wsum_t low) {
  	lower_[lev] = low;
  }
  wsum_t SharedMinimizeData::incLower(uint32 at, wsum_t low){
  	for (wsum_t stored;;) {
  		if ((stored = lower(at)) >= low) {
  			return stored;
  		}
  		if (compare_and_swap(lower_[at], stored, low) == stored) {
  			return low;
  		}
  	}
  }
  wsum_t SharedMinimizeData::lower(uint32 lev) const {
  	return lower_[lev];
  }
  wsum_t SharedMinimizeData::optimum(uint32 lev) const {
  	wsum_t o = sum(lev);
  	return o + (o != maxBound() ? adjust(lev) : 0);
  }
  void SharedMinimizeData::markOptimal() {
  	optGen_ = generation();
  }
  void SharedMinimizeData::sub(wsum_t* lhs, const LevelWeight* w, uint32& aLev) const {
  	if (w->level < aLev) { aLev = w->level; }
  	do { lhs[w->level] -= w->weight; } while (w++->next);
  }
  bool SharedMinimizeData::imp(wsum_t* lhs, const LevelWeight* w, const wsum_t* rhs, uint32& lev) const {
  	assert(lev <= w->level && std::equal(lhs, lhs+lev, rhs));
  	while (lev != w->level && lhs[lev] == rhs[lev]) { ++lev; }
  	for (uint32 i = lev, end = numRules(); i != end; ++i) {
  		wsum_t temp = lhs[i];
  		if (i == w->level) { temp += w->weight; if (w->next) ++w; }
  		if (temp != rhs[i]){ return temp > rhs[i]; }
  	}
  	return false;
  }
  /////////////////////////////////////////////////////////////////////////////////////////
  // MinimizeConstraint
  /////////////////////////////////////////////////////////////////////////////////////////
  MinimizeConstraint::MinimizeConstraint(SharedData* d) : shared_(d) {}
  
  MinimizeConstraint::~MinimizeConstraint() {
  	assert(shared_ == 0 && "MinimizeConstraint not destroyed!");
  }
  bool MinimizeConstraint::prepare(Solver& s, bool useTag) {
  	POTASSCO_REQUIRE(!s.isFalse(tag_), "Tag literal must not be false!");
  	if (useTag && tag_ == lit_true())      { tag_ = posLit(s.pushTagVar(false)); }
  	if (s.isTrue(tag_) || s.hasConflict()){ return !s.hasConflict(); }
  	return useTag ? s.pushRoot(tag_) : s.force(tag_, 0);
  }
  void MinimizeConstraint::destroy(Solver* s, bool d) {
  	shared_->release();
  	shared_ = 0;
  	Constraint::destroy(s, d);
  }
  void MinimizeConstraint::reportLower(Solver& s, uint32 lev, wsum_t low) const {
  	s.lower.level = lev;
  	s.lower.bound = low + shared_->adjust(lev);
  }
  /////////////////////////////////////////////////////////////////////////////////////////
  // DefaultMinimize
  /////////////////////////////////////////////////////////////////////////////////////////
  union DefaultMinimize::UndoInfo {
  	UndoInfo() : rep(0) {}
  	struct {
  		uint32 idx    : 30; // index of literal on stack
  		uint32 newDL  :  1; // first literal of new DL?
  		uint32 idxSeen:  1; // literal with idx already propagated?
  	}      data;
  	uint32 rep;
  	uint32 index() const { return data.idx; }
  	bool   newDL() const { return data.newDL != 0u; }
  };
  DefaultMinimize::DefaultMinimize(SharedData* d, const OptParams& params)
  	: MinimizeConstraint(d)
  	, bounds_(0)
  	, pos_(d->lits)
  	, undo_(0)
  	, undoTop_(0)
  	, size_(d->numRules()) {
  	step_.type = params.algo;
  	if (step_.type == OptParams::bb_hier && d->numRules() == 1) {
  		step_.type = 0;
  	}
  }
  
  DefaultMinimize::~DefaultMinimize() {
  	delete [] bounds_;
  	delete [] undo_;
  }
  
  void DefaultMinimize::destroy(Solver* s, bool detach) {
  	if (s && detach) {
  		for (const WeightLiteral* it = shared_->lits; !isSentinel(it->first); ++it) {
  			s->removeWatch(it->first, this);
  		}
  		for (uint32 dl = 0; (dl = lastUndoLevel(*s)) != 0; ) {
  			s->removeUndoWatch(dl, this);
  			DefaultMinimize::undoLevel(*s);
  		}
  	}
  	MinimizeConstraint::destroy(s, detach);
  }
  
  bool DefaultMinimize::attach(Solver& s) {
  	assert(s.decisionLevel() == 0 && !bounds_);
  	uint32 numL = 0;
  	VarVec up;
  	for (const WeightLiteral* it = shared_->lits; !isSentinel(it->first); ++it, ++numL) {
  		if (s.value(it->first.var()) == value_free) {
  			s.addWatch(it->first, this, numL);
  		}
  		else if (s.isTrue(it->first)) {
  			up.push_back(numL);
  		}
  	}
  	bounds_ = new wsum_t[(numRules() * (3 + uint32(step_.type != 0)))]; // upper, sum, temp, lower
  	std::fill(this->opt(), this->sum(), SharedData::maxBound());
  	std::fill(this->sum(), this->end(), wsum_t(0));
  	stepInit(0);
  	// [0,numL+1)      : undo stack
  	// [numL+1, numL*2): pos  stack
  	undo_    = new UndoInfo[(numL*2)+1];
  	undoTop_ = 0;
  	posTop_  = numL+1;
  	actLev_  = 0;
  	for (WeightVec::size_type i = 0; i != up.size(); ++i) {
  		DefaultMinimize::propagate(s, shared_->lits[up[i]].first, up[i]);
  	}
  	return true;
  }
  
  // Returns the numerical highest decision level watched by this constraint.
  uint32 DefaultMinimize::lastUndoLevel(const Solver& s) const {
  	return undoTop_ != 0
  		? s.level(shared_->lits[undo_[undoTop_-1].index()].first.var())
  		: 0;
  }
  bool DefaultMinimize::litSeen(uint32 i) const { return undo_[i].data.idxSeen != 0; }
  
  // Pushes the literal at index idx onto the undo stack
  // and marks it as seen; if literal is first in current level
  // adds a new undo watch.
  void DefaultMinimize::pushUndo(Solver& s, uint32 idx) {
  	assert(idx >= static_cast<uint32>(pos_ - shared_->lits));
  	undo_[undoTop_].data.idx  = idx;
  	undo_[undoTop_].data.newDL= 0;
  	if (lastUndoLevel(s) != s.decisionLevel()) {
  		// remember current "look at" position and start
  		// a new decision level on the undo stack
  		undo_[posTop_++].data.idx = static_cast<uint32>(pos_-shared_->lits);
  		s.addUndoWatch(s.decisionLevel(), this);
  		undo_[undoTop_].data.newDL = 1;
  	}
  	undo_[idx].data.idxSeen   = 1;
  	++undoTop_;
  }
  /////////////////////////////////////////////////////////////////////////////////////////
  // MinimizeConstraint - arithmetic strategy implementation
  //
  // For now we use a simple "switch-on-type" approach.
  // In the future, if new strategies emerge, we may want to use a strategy hierarchy.
  /////////////////////////////////////////////////////////////////////////////////////////
  #define STRATEGY(x) shared_->x
  // set *lhs = *rhs, where lhs != rhs
  void DefaultMinimize::assign(wsum_t* lhs, wsum_t* rhs) const {
  	std::memcpy(lhs, rhs, size_*sizeof(wsum_t));
  }
  // returns lhs > rhs
  bool DefaultMinimize::greater(wsum_t* lhs, wsum_t* rhs, uint32 len, uint32& aLev) const {
  	while (*lhs == *rhs && --len) { ++lhs, ++rhs; ++aLev; }
  	return *lhs > *rhs;
  }
  /////////////////////////////////////////////////////////////////////////////////////////
  Constraint::PropResult DefaultMinimize::propagate(Solver& s, Literal, uint32& data) {
  	pushUndo(s, data);
  	STRATEGY(add(sum(), shared_->lits[data]));
  	return PropResult(propagateImpl(s, propagate_new_sum), true);
  }
  
  // Computes the set of literals implying p and returns
  // the highest decision level of that set.
  // PRE: p is implied on highest undo level
  uint32 DefaultMinimize::computeImplicationSet(const Solver& s, const WeightLiteral& p, uint32& undoPos) {
  	wsum_t* temp    = this->temp(), *opt = this->opt();
  	uint32 up       = undoTop_, lev = actLev_;
  	uint32 minLevel = std::max(s.level(tag_.var()), s.level(s.sharedContext()->stepLiteral().var()));
  	// start from current sum
  	assign(temp, sum());
  	// start with full set
  	for (UndoInfo u; up != 0; --up) {
  		u = undo_[up-1];
  		// subtract last element from set
  		STRATEGY(sub(temp, shared_->lits[u.index()], lev));
  		if (!STRATEGY(imp(temp, p, opt, lev))) {
  			// p is no longer implied after we removed last literal,
  			// hence [0, up) implies p @ level of last literal
  			undoPos = up;
  			return std::max(s.level(shared_->lits[u.index()].first.var()), minLevel);
  		}
  	}
  	undoPos = 0;
  	return minLevel;
  }
  
  bool DefaultMinimize::propagateImpl(Solver& s, PropMode m) {
  	Iter it    = pos_;
  	uint32 idx = static_cast<uint32>(it - shared_->lits);
  	uint32 DL  = s.decisionLevel();
  	// current implication level or "unknown" if
  	// we propagate a new optimum
  	uint32 impLevel = DL + (m == propagate_new_opt);
  	weight_t lastW  = -1;
  	uint32 undoPos  = undoTop_;
  	bool ok         = true;
  	actLev_         = std::min(actLev_, shared_->level(idx));
  	for (wsum_t* sum= this->sum(), *opt = this->opt(); ok && !isSentinel(it->first); ++it, ++idx) {
  		// skip propagated/false literals
  		if (litSeen(idx) || (m == propagate_new_sum && s.isFalse(it->first))) {
  			continue;
  		}
  		if (lastW != it->second) {
  			// check if the current weight is implied
  			if (!STRATEGY(imp(sum, *it, opt, actLev_))) {
  				// all good - current optimum is safe
  				pos_    = it;
  				return true;
  			}
  			// compute implication set and level of current weight
  			if (m == propagate_new_opt) {
  				impLevel = computeImplicationSet(s, *it, undoPos);
  			}
  			lastW = it->second;
  		}
  		assert(active());
  		// force implied literals
  		if (!s.isFalse(it->first) || (impLevel < DL && s.level(it->first.var()) > impLevel)) {
  			if (impLevel != DL) { DL = s.undoUntil(impLevel, Solver::undo_pop_bt_level); }
  			ok = s.force(~it->first, impLevel, this, undoPos);
  		}
  	}
  	return ok;
  }
  
  // pops free literals from the undo stack and decreases current sum
  void DefaultMinimize::undoLevel(Solver&) {
  	assert(undoTop_ != 0 && posTop_ > undoTop_);
  	uint32 up  = undoTop_;
  	uint32 idx = undo_[--posTop_].index();
  	for (wsum_t* sum = this->sum();;) {
  		UndoInfo& u = undo_[--up];
  		undo_[u.index()].data.idxSeen = 0;
  		STRATEGY(sub(sum, shared_->lits[u.index()], actLev_));
  		if (u.newDL()) { break; }
  	}
  	undoTop_ = up;
  	Iter temp= shared_->lits + idx;
  	if (temp < pos_) {
  		pos_    = temp;
  		actLev_ = std::min(actLev_, shared_->level(idx));
  	}
  }
  
  // computes the reason for p -
  // all literals that were propagated before p
  void DefaultMinimize::reason(Solver& s, Literal p, LitVec& lits) {
  	assert(s.isTrue(tag_));
  	uint32 stop = s.reasonData(p);
  	Literal   x = s.sharedContext()->stepLiteral();
  	assert(stop <= undoTop_);
  	if (!isSentinel(x) && s.isTrue(x)) { lits.push_back(x); }
  	if (s.level(tag_.var()))           { lits.push_back(tag_); }
  	for (uint32 i = 0; i != stop; ++i) {
  		UndoInfo u = undo_[i];
  		x = shared_->lits[u.index()].first;
  		lits.push_back(x);
  	}
  }
  
  bool DefaultMinimize::minimize(Solver& s, Literal p, CCMinRecursive* rec) {
  	assert(s.isTrue(tag_));
  	uint32 stop = s.reasonData(p);
  	Literal   x = s.sharedContext()->stepLiteral();
  	assert(stop <= undoTop_);
  	if (!s.ccMinimize(x, rec) || !s.ccMinimize(tag_, rec)) { return false; }
  	for (uint32 i = 0; i != stop; ++i) {
  		UndoInfo u = undo_[i];
  		x = shared_->lits[u.index()].first;
  		if (!s.ccMinimize(x, rec)) {
  			return false;
  		}
  	}
  	return true;
  }
  /////////////////////////////////////////////////////////////////////////////////////////
  // DefaultMinimize - bound management
  /////////////////////////////////////////////////////////////////////////////////////////
  // Stores the current sum as the shared optimum.
  void DefaultMinimize::commitUpperBound(const Solver&)  {
  	shared_->setOptimum(sum());
  	if (step_.type == OptParams::bb_inc) { step_.size *= 2; }
  }
  bool DefaultMinimize::commitLowerBound(Solver& s, bool upShared) {
  	bool act  = active() && shared_->checkNext();
  	bool more = step_.lev < size_ && (step_.size > 1 || step_.lev != size_-1);
  	if (act && step_.type && step_.lev < size_) {
  		uint32 x = step_.lev;
  		wsum_t L = opt()[x] + 1;
  		if (upShared) {
  			wsum_t sv = shared_->incLower(x, L);
  			if (sv == L) { reportLower(s, x, sv); }
  			else         { L = sv; }
  		}
  		stepLow()= L;
  		if (step_.type == OptParams::bb_inc){ step_.size = 1; }
  	}
  	return more;
  }
  bool DefaultMinimize::handleUnsat(Solver& s, bool up, LitVec& out) {
  	bool more = shared_->optimize() && commitLowerBound(s, up);
  	uint32 dl = s.isTrue(tag_) ? s.level(tag_.var()) : 0;
  	relaxBound(false);
  	if (more && dl && dl <= s.rootLevel()) {
  		s.popRootLevel(s.rootLevel()-dl, &out); // pop and remember new path
  		return s.popRootLevel(1);               // pop tag - disable constraint
  	}
  	return false;
  }
  
  // Disables the minimize constraint by clearing its upper bound.
  bool DefaultMinimize::relaxBound(bool full) {
  	if (active()) { std::fill(opt(), opt()+size_, SharedData::maxBound()); }
  	pos_       = shared_->lits;
  	actLev_    = 0;
  	if (full || !shared_->optimize()) { stepInit(0); }
  	return true;
  }
  
  void DefaultMinimize::stepInit(uint32 n) {
  	step_.size = uint32(step_.type != OptParams::bb_dec);
  	if (step_.type) { step_.lev = n; if (n != size_) stepLow() = 0-shared_->maxBound(); }
  	else            { step_.lev = shared_->maxLevel(); }
  }
  
  // Integrates new (tentative) bounds from the ones stored in the shared data object.
  bool DefaultMinimize::integrateBound(Solver& s) {
  	bool useTag = shared_->optimize() && (step_.type != 0 || shared_->mode() == MinimizeMode_t::enumOpt);
  	if (!prepare(s, useTag)) { return false; }
  	if (useTag && s.level(tag_.var()) == 0) {
  		step_.type = 0;
  		stepInit(0);
  	}
  	if ((active() && !shared_->checkNext())) { return !s.hasConflict(); }
  	WeightLiteral min(lit_true(), shared_->weights.empty() ? uint32(0) : (uint32)shared_->weights.size()-1);
  	while (!s.hasConflict() && updateBounds(shared_->checkNext())) {
  		uint32 x = 0;
  		uint32 dl= s.decisionLevel() + 1;
  		if (!STRATEGY(imp(sum(), min, opt(), actLev_)) || (dl = computeImplicationSet(s, min, x)) > s.rootLevel()) {
  			for (--dl; !s.hasConflict() || s.resolveConflict(); ) {
  				if      (s.undoUntil(dl, Solver::undo_pop_bt_level) > dl){ s.backtrack(); }
  				else if (propagateImpl(s, propagate_new_opt))            { return true;   }
  			}
  		}
  		if (!shared_->checkNext()) {
  			break;
  		}
  		if (!step_.type) { ++step_.lev; }
  		else             { stepLow() = ++opt()[step_.lev]; }
  	}
  	relaxBound(false);
  	if (!s.hasConflict()) {
  		s.undoUntil(0);
  		s.setStopConflict();
  	}
  	return false;
  }
  
  // Loads bounds from the shared data object and (optionally) applies
  // the current step to get the next tentative bound to check.
  bool DefaultMinimize::updateBounds(bool applyStep) {
  	for (;;) {
  		const uint32  seq   = shared_->generation();
  		const wsum_t* upper = shared_->upper();
  		wsum_t*       myLow = step_.type ? end() : 0;
  		wsum_t*       bound = opt();
  		uint32        appLev= applyStep ? step_.lev : size_;
  		for (uint32 i = 0; i != size_; ++i) {
  			wsum_t U = upper[i], B = bound[i];
  			if (i != appLev) {
  				wsum_t L = shared_->lower(i);
  				if (myLow) {
  					if (i > step_.lev || L > myLow[i]) { myLow[i] = L; }
  					else                               { L = myLow[i]; }
  				}
  				if      (i > appLev) { bound[i] = SharedData::maxBound(); }
  				else if (U >= L)     { bound[i] = U; }
  				else                 { stepInit(size_); return false; }
  				continue;
  			}
  			if (step_.type) {
  				wsum_t L = (stepLow() = std::max(myLow[i], shared_->lower(i)));
  				if (U < L) { // path exhausted?
  					stepInit(size_);
  					return false;
  				}
  				if (B < L) { // tentative bound too strong?
  					return false;
  				}
  				if (B < U) { // existing step?
  					assert(std::count(bound+i+1, bound+size_, SharedData::maxBound()) == int(size_ - (i+1)));
  					return true;
  				}
  				if (U == L) {// done with current level?
  					bound[i] = U;
  					stepInit(++appLev);
  					continue;
  				}
  				assert(U > L && B > L);
  				wsum_t diff = U - L;
  				uint32 half = static_cast<uint32>( (diff>>1) | (diff&1) );
  				if (step_.type == OptParams::bb_inc) {
  					step_.size = std::min(step_.size, half);
  				}
  				else if (step_.type == OptParams::bb_dec) {
  					if (!step_.size) { step_.size = static_cast<uint32>(diff); }
  					else             { step_.size = half; }
  				}
  			}
  			assert(step_.size != 0);
  			bound[i] = U - step_.size;
  			actLev_  = 0;
  			pos_     = shared_->lits;
  		}
  		if (seq == shared_->generation()) { break; }
  	}
  	return step_.lev != size_ || !applyStep;
  }
  #undef STRATEGY
  /////////////////////////////////////////////////////////////////////////////////////////
  // MinimizeBuilder
  /////////////////////////////////////////////////////////////////////////////////////////
  MinimizeBuilder::MinimizeBuilder() { }
  void MinimizeBuilder::clear() {
  	LitVec().swap(lits_);
  }
  bool MinimizeBuilder::empty() const {
  	return lits_.empty();
  }
  MinimizeBuilder& MinimizeBuilder::add(weight_t prio, const WeightLitVec& lits) {
  	for (WeightLitVec::const_iterator it = lits.begin(), end = lits.end(); it != end; ++it) {
  		add(prio, *it);
  	}
  	return *this;
  }
  MinimizeBuilder& MinimizeBuilder::add(weight_t prio, WeightLiteral lit) {
  	lits_.push_back(MLit(lit, prio));
  	return *this;
  }
  MinimizeBuilder& MinimizeBuilder::add(weight_t prio, weight_t w) {
  	lits_.push_back(MLit(WeightLiteral(lit_true(), w), prio));
  	return *this;
  }
  MinimizeBuilder& MinimizeBuilder::add(const SharedData& con) {
  	if (con.numRules() == 1) {
  		const weight_t P = !con.prios.empty() ? con.prios[0] : 0;
  		for (const WeightLiteral* it = con.lits; !isSentinel(it->first); ++it) { add(P, *it); }
  	}
  	else {
  		for (const WeightLiteral* it = con.lits; !isSentinel(it->first); ++it) {
  			const SharedData::LevelWeight* w = &con.weights[it->second];
  			do {
  				add( w->level < con.prios.size() ? con.prios[w->level] : -static_cast<weight_t>(w->level), WeightLiteral(it->first, w->weight) );
  			} while (w++->next);
  		}
  	}
  	for (uint32 i = 0; i != con.numRules(); ++i) {
  		if (wsum_t w = con.adjust(i)) {
  			const weight_t P = i < con.prios.size() ? con.prios[i] : -static_cast<weight_t>(i);
  			while (w < CLASP_WEIGHT_T_MIN) { add(P, CLASP_WEIGHT_T_MIN); w -= CLASP_WEIGHT_T_MIN; }
  			while (w > CLASP_WEIGHT_T_MAX) { add(P, CLASP_WEIGHT_T_MAX); w -= CLASP_WEIGHT_T_MAX; }
  			add(P, static_cast<weight_t>(w));
  		}
  	}
  	return *this;
  }
  // Comparator for preparing levels: compare (prio, var, weight)
  bool MinimizeBuilder::CmpPrio::operator()(const MLit& lhs, const MLit& rhs) const {
  	if (lhs.prio != rhs.prio)           { return lhs.prio > rhs.prio; }
  	if (lhs.lit.var() != rhs.lit.var()) { return lhs.lit  < rhs.lit; }
  	return lhs.weight > rhs.weight;
  }
  // Comparator for merging levels: compare (var, level, weight)
  bool MinimizeBuilder::CmpLit::operator()(const MLit& lhs, const MLit& rhs) const {
  	if (lhs.lit.var() != rhs.lit.var()) { return lhs.lit  < rhs.lit; }
  	if (lhs.prio != rhs.prio)           { return lhs.prio < rhs.prio; }
  	return lhs.weight > rhs.weight;
  }
  // Comparator for sorting literals by final weight
  bool MinimizeBuilder::CmpWeight::operator()(const MLit& lhs, const MLit& rhs) const {
  	if (!weights) { return lhs.weight > rhs.weight; }
  	const SharedData::LevelWeight* wLhs = &(*weights)[lhs.weight];
  	const SharedData::LevelWeight* wRhs = &(*weights)[rhs.weight];
  	for (;; ++wLhs, ++wRhs) {
  		if (wLhs->level != wRhs->level)  { return wLhs->level < wRhs->level; }
  		if (wLhs->weight != wRhs->weight){ return wLhs->weight > wRhs->weight; }
  		if (!wLhs->next) { return wRhs->next && (++wRhs)->weight < 0; }
  		if (!wRhs->next) { ++wLhs; break; }
  	}
  	return wLhs->weight > 0;
  }
  
  // Replaces integer priorities with increasing levels and merges duplicate/complementary literals.
  void MinimizeBuilder::prepareLevels(const Solver& s, SumVec& adjust, WeightVec& prios) {
  	// group first by decreasing priorities and then by variables
  	std::stable_sort(lits_.begin(), lits_.end(), CmpPrio());
  	prios.clear(); adjust.clear();
  	// assign levels and simplify lits
  	LitVec::iterator j = lits_.begin();
  	for (LitVec::const_iterator it = lits_.begin(), end = lits_.end(); it != end;) {
  		const weight_t P = it->prio, L = static_cast<weight_t>(prios.size());
  		wsum_t R = 0;
  		for (LitVec::const_iterator k; it != end && it->prio == P; it = k) {
  			Literal x(it->lit); // make literal unique wrt this level
  			wsum_t  w = it->weight;
  			for (k = it + 1; k != end && k->lit.var() == x.var() && k->prio == P; ++k) {
  				if (k->lit == x){ w += k->weight; }
  				else            { w -= k->weight; R += k->weight; }
  			}
  			if (w < 0){
  				R += w;
  				x  = ~x;
  				w  = -w;
  			}
  			if (w && s.value(x.var()) == value_free) {
  				POTASSCO_CHECK(static_cast<weight_t>(w) == w, EOVERFLOW, "MinimizeBuilder: weight too large");
  				*j++ = MLit(WeightLiteral(x, static_cast<weight_t>(w)), L);
  			}
  			else if (s.isTrue(x)) { R += w; }
  		}
  		prios.push_back(P);
  		adjust.push_back(R);
  	}
  	lits_.erase(j, lits_.end());
  }
  
  void MinimizeBuilder::mergeLevels(SumVec& adjust, SharedData::WeightVec& weights) {
  	// group first by variables and then by increasing levels
  	std::stable_sort(lits_.begin(), lits_.end(), CmpLit());
  	LitVec::iterator j = lits_.begin();
  	weights.clear(); weights.reserve(lits_.size());
  	for (LitVec::const_iterator it = lits_.begin(), end = lits_.end(), k; it != end; it = k) {
  		// handle first occurrence of var
  		assert(it->weight > 0 && "most important occurrence of lit must have positive weight");
  		weight_t wpos = (weight_t)weights.size();
  		weights.push_back(SharedData::LevelWeight(it->prio, it->weight));
  		// handle remaining occurrences with lower prios
  		for (k = it + 1; k != end && k->lit.var() == it->lit.var(); ++k) {
  			assert(k->prio > it->prio && "levels not prepared!");
  			weights.back().next = 1;
  			weights.push_back(SharedData::LevelWeight(k->prio, k->weight));
  			if (k->lit.sign() != it->lit.sign()) {
  				adjust[k->prio] += k->weight;
  				weights.back().weight = -k->weight;
  			}
  		}
  		(*j = *it).weight = wpos;
  		++j;
  	}
  	lits_.erase(j, lits_.end());
  }
  
  MinimizeBuilder::SharedData* MinimizeBuilder::createShared(SharedContext& ctx, const SumVec& adjust, const CmpWeight& cmp) {
  	const uint32 nLits = static_cast<uint32>(lits_.size());
  	SharedData*  ret   = new (::operator new(sizeof(SharedData) + ((nLits + 1)*sizeof(WeightLiteral)))) SharedData(adjust);
  	// sort literals by decreasing weight
  	std::stable_sort(lits_.begin(), lits_.end(), cmp);
  	uint32   last = 0;
  	weight_t wIdx = 0;
  	for (uint32 i = 0; i != nLits; ++i) {
  		WeightLiteral x(lits_[i].lit, lits_[i].weight);
  		ctx.setFrozen(x.first.var(), true);
  		ret->lits[i] = x;
  		if (!cmp.weights) { continue; }
  		if (!i || cmp(lits_[last], lits_[i])) {
  			last = i;
  			wIdx = (weight_t)ret->weights.size();
  			for (const SharedData::LevelWeight* w = &(*cmp.weights)[x.second];; ++w) {
  				ret->weights.push_back(*w);
  				if (!w->next) { break; }
  			}
  		}
  		ret->lits[i].second = wIdx;
  	}
  	ret->lits[nLits] = WeightLiteral(lit_true(), (weight_t)ret->weights.size());
  	if (cmp.weights) {
  		ret->weights.push_back(SharedData::LevelWeight((uint32)adjust.size()-1, 0));
  	}
  	ret->resetBounds();
  	return ret;
  }
  
  MinimizeBuilder::SharedData* MinimizeBuilder::build(SharedContext& ctx) {
  	POTASSCO_REQUIRE(!ctx.frozen());
  	if ((!ctx.ok() || !ctx.master()->propagate()) || empty()) {
  		clear();
  		return 0;
  	}
  	typedef SharedData::WeightVec FlatVec;
  	WeightVec prios;
  	SumVec    adjust;
  	FlatVec   weights;
  	CmpWeight cmp(0);
  	prepareLevels(*ctx.master(), adjust, prios);
  	if (prios.size() > 1) {
  		mergeLevels(adjust, weights);
  		cmp.weights = &weights;
  	}
  	else if (prios.empty()) {
  		prios.assign(1, 0);
  		adjust.assign(1, 0);
  	}
  	SharedData* ret = createShared(ctx, adjust, cmp);
  	ret->prios.swap(prios);
  	clear();
  	return ret;
  }
  /////////////////////////////////////////////////////////////////////////////////////////
  // UncoreMinimize
  /////////////////////////////////////////////////////////////////////////////////////////
  UncoreMinimize::UncoreMinimize(SharedMinimizeData* d, const OptParams& params)
  	: MinimizeConstraint(d)
  	, enum_(0)
  	, sum_(new wsum_t[d->numRules()])
  	, auxInit_(UINT32_MAX)
  	, auxAdd_(0)
  	, freeOpen_(0)
  	, options_(params) {
  }
  void UncoreMinimize::init() {
  	releaseLits();
  	fix_.clear();
  	eRoot_ = 0;
  	aTop_  = 0;
  	upper_ = shared_->upper(0);
  	lower_ = 0;
  	gen_   = 0;
  	level_ = 0;
  	next_  = 0;
  	disj_  = 0;
  	path_  = 1;
  	init_  = 1;
  	actW_  = 1;
  	nextW_ = 0;
  }
  bool UncoreMinimize::attach(Solver& s) {
  	init();
  	initRoot(s);
  	auxInit_ = UINT32_MAX;
  	auxAdd_  = 0;
  	if (s.sharedContext()->concurrency() > 1 && shared_->mode() == MinimizeMode_t::enumOpt) {
  		enum_ = new DefaultMinimize(shared_->share(), OptParams());
  		enum_->attach(s);
  		enum_->relaxBound(true);
  	}
  	return true;
  }
  // Detaches the constraint and all cores from s and removes
  // any introduced aux vars.
  void UncoreMinimize::detach(Solver* s, bool b) {
  	releaseLits();
  	if (s && auxAdd_ && s->numAuxVars() == (auxInit_ + auxAdd_)) {
  		s->popAuxVar(auxAdd_, &closed_);
  		auxInit_ = UINT32_MAX;
  		auxAdd_  = 0;
  	}
  	Clasp::destroyDB(closed_, s, b);
  	fix_.clear();
  }
  // Destroys this object and optionally detaches it from the given solver.
  void UncoreMinimize::destroy(Solver* s, bool b) {
  	detach(s, b);
  	delete [] sum_;
  	if (enum_) { enum_->destroy(s, b); enum_ = 0; }
  	MinimizeConstraint::destroy(s, b);
  }
  Constraint::PropResult UncoreMinimize::propagate(Solver& s, Literal p, uint32& other) {
  	return PropResult(s.force(Literal::fromId(other), Antecedent(p)), true);
  }
  bool UncoreMinimize::simplify(Solver& s, bool) {
  	if (s.decisionLevel() == 0) { simplifyDB(s, closed_, false); }
  	return false;
  }
  void UncoreMinimize::reason(Solver& s, Literal, LitVec& out) {
  	uint32 r = initRoot(s);
  	for (uint32 i = 1; i <= r; ++i) {
  		out.push_back(s.decision(i));
  	}
  }
  
  // Integrates any new information from this constraint into s.
  bool UncoreMinimize::integrate(Solver& s) {
  	assert(!s.isFalse(tag_));
  	bool useTag = (shared_->mode() == MinimizeMode_t::enumOpt) || s.sharedContext()->concurrency() > 1;
  	if (!prepare(s, useTag)) {
  		return false;
  	}
  	if (enum_ && !shared_->optimize() && !enum_->integrateBound(s)) {
  		return false;
  	}
  	for (uint32 gGen = shared_->generation(); gGen != gen_; ) {
  		gen_   = gGen;
  		upper_ = shared_->upper(level_);
  		gGen   = shared_->generation();
  	}
  	if (init_ && !initLevel(s)) {
  		return false;
  	}
  	if (next_ && !addNext(s)) {
  		return false;
  	}
  	if (path_ && !pushPath(s)) {
  		return false;
  	}
  	if (!validLowerBound()) {
  		next_ = 1;
  		s.setStopConflict();
  		return false;
  	}
  	return true;
  }
  
  // Initializes the next optimization level to look at.
  bool UncoreMinimize::initLevel(Solver& s) {
  	initRoot(s);
  	next_  = 0;
  	disj_  = 0;
  	actW_  = 1;
  	nextW_ = 0;
  	*sum_  = -1;
  	if (!fixLevel(s)) {
  		return false;
  	}
  	for (LitVec::const_iterator it = fix_.begin(), end = fix_.end(); it != end; ++it) {
  		if (!s.force(*it, eRoot_, this)) { return false; }
  	}
  	if (!shared_->optimize()) {
  		level_ = shared_->maxLevel();
  		lower_ = shared_->lower(level_);
  		upper_ = shared_->upper(level_);
  		path_  = 0;
  		init_  = 0;
  		return true;
  	}
  	weight_t maxW = 1;
  	uint32_t next = 1 - init_;
  	for (uint32 level = (level_ + next), n = 1; level <= shared_->maxLevel() && assume_.empty(); ++level) {
  		level_ = level;
  		lower_ = 0;
  		upper_ = shared_->upper(level_);
  		for (const WeightLiteral* it = shared_->lits; !isSentinel(it->first); ++it) {
  			if (weight_t w = shared_->weight(*it, level_)){
  				Literal x = it->first;
  				if (w < 0) {
  					lower_ += w;
  					w       = -w;
  					x       = ~x;
  				}
  				if (s.value(x.var()) == value_free || s.level(x.var()) > eRoot_) {
  					newAssumption(~x, w);
  					if (w > maxW){ maxW = w; }
  				}
  				else if (s.isTrue(x)) {
  					lower_ += w;
  				}
  			}
  		}
  		if (n == 1) {
  			if      (lower_ > upper_){ next = 1; break; }
  			else if (lower_ < upper_){ next = (n = 0);  }
  			else                     {
  				n    = shared_->checkNext() || level != shared_->maxLevel();
  				next = n;
  				while (!assume_.empty()) {
  					fixLit(s, assume_.back().lit);
  					assume_.pop_back();
  				}
  				litData_.clear();
  				assume_.clear();
  				maxW = 1;
  			}
  		}
  	}
  	init_ = 0;
  	path_ = 1;
  	disj_ = options_.hasOption(OptParams::usc_disjoint);
  	actW_ = options_.hasOption(OptParams::usc_stratify) ? maxW : 1;
  	if (next && !s.hasConflict()) {
  		s.force(~tag_, Antecedent(0));
  		disj_ = 0;
  	}
  	if (auxInit_ == UINT32_MAX) {
  		auxInit_ = s.numAuxVars();
  	}
  	return !s.hasConflict();
  }
  
  Literal UncoreMinimize::newLit(Solver& s) {
  	++auxAdd_;
  	return posLit(s.pushAuxVar());
  }
  UncoreMinimize::LitPair UncoreMinimize::newAssumption(Literal p, weight_t w) {
  	assert(w > 0);
  	if (nextW_ && w > nextW_) {
  		nextW_ = w;
  	}
  	litData_.push_back(LitData(w, true, 0));
  	assume_.push_back(LitPair(p, sizeVec(litData_)));
  	return assume_.back();
  }
  bool UncoreMinimize::push(Solver& s, Literal p, uint32 id) {
  	assert(conflict_.empty());
  	if (s.pushRoot(p)) {
  		return true;
  	}
  	else if (!s.hasConflict()) {
  		conflict_.assign(1, ~p);
  		conflict_.push_back(Literal::fromRep(id));
  		if (s.level(p.var()) > eRoot_) { s.force(p, Antecedent(0)); }
  		else                           { s.setStopConflict(); }
  	}
  	return false;
  }
  // Pushes the active assumptions from the active optimization level to
  // the root path.
  bool UncoreMinimize::pushPath(Solver& s) {
  	assert(!next_);
  	for (bool push = path_ != 0; !s.hasConflict() && push; ) {
  		path_ = 0;
  		if (!s.propagate() || !s.simplify()) { path_ = 1;  return false; }
  		initRoot(s);
  		if (todo_.shrink()) {
  			return pushTrim(s);
  		}
  		wsum_t   fixW = upper_ - lower_, low = 0;
  		weight_t maxW = 0;
  		uint32 j = 0, i = 0, end = sizeVec(assume_);
  		bool  ok = true;
  		nextW_ = 0;
  		for (uint32 dl; i != end && ok; ++i) {
  			LitData& x = getData(assume_[i].id);
  			if (x.assume) {
  				Literal  p = assume_[i].lit;
  				weight_t w = x.weight;
  				assume_[j++] = assume_[i];
  				if (w < actW_) {
  					nextW_ = std::max(nextW_, w);
  				}
  				else if (w > fixW) {
  					--j;
  					ok = fixLit(s, p);
  					push = false;
  					x.assume = 0;
  					x.weight = 0;
  					if (hasCore(x)) { closeCore(s, x, false); }
  				}
  				else if (!s.isFalse(p) || s.level(p.var()) > eRoot_) {
  					maxW = std::max(maxW, w);
  					ok   = !push || this->push(s, p, assume_[i].id);
  				}
  				else {
  					LitPair core(~p, assume_[i].id);
  					--j;
  					dl   = s.decisionLevel();
  					ok   = addCore(s, &core, 1, w, true);
  					low += w;
  					fixW = fixW - w;
  					end  = sizeVec(assume_);
  					push = push && s.decisionLevel() == dl;
  				}
  			}
  		}
  		if (i != j) { moveDown(assume_, i, j); }
  		if (low) {
  			shared_->incLower(level_, lower_);
  		}
  		push  = !push || maxW > fixW;
  		aTop_ = s.rootLevel();
  		POTASSCO_REQUIRE(s.decisionLevel() == s.rootLevel(), "pushPath must be called on root level (%u:%u)", s.rootLevel(), s.decisionLevel());
  	}
  	return !s.hasConflict();
  }
  
  // Removes invalid assumptions from the root path.
  bool UncoreMinimize::popPath(Solver& s, uint32 dl) {
  	POTASSCO_REQUIRE(dl <= aTop_ && eRoot_ <= aTop_ && s.rootLevel() <= aTop_, "You must not mess with my root level!");
  	if (dl < eRoot_) { dl = eRoot_; }
  	sum_[0] = -1;
  	path_   = 1;
  	return s.popRootLevel(s.rootLevel() - (aTop_ = dl));
  }
  
  bool UncoreMinimize::relax(Solver& s, bool reset) {
  	if (next_ && !reset) {
  		// commit cores of last model
  		if (todo_.shrink()) {
  			resetTrim(s);
  		}
  		addNext(s);
  	}
  	if ((reset && shared_->optimize()) || !assume_.empty() || level_ != shared_->maxLevel()) {
  		detach(&s, true);
  		init();
  	}
  	else {
  		releaseLits();
  	}
  	if (!shared_->optimize()) {
  		gen_ = shared_->generation();
  	}
  	init_ = 1;
  	next_ = 0;
  	assert(assume_.empty());
  	return !enum_ || enum_->relax(s, reset);
  }
  
  // Computes the costs of the current assignment.
  wsum_t* UncoreMinimize::computeSum(const Solver& s) const {
  	std::fill_n(sum_, shared_->numRules(), wsum_t(0));
  	for (const WeightLiteral* it = shared_->lits; !isSentinel(it->first); ++it) {
  		if (s.isTrue(it->first)) { shared_->add(sum_, *it); }
  	}
  	return sum_;
  }
  // Checks whether the current assignment in s is valid w.r.t the
  // bound stored in the shared data object.
  bool UncoreMinimize::valid(Solver& s) {
  	if (shared_->upper(level_) == SharedData::maxBound()){ return true; }
  	if (sum_[0] < 0) { computeSum(s); }
  	const wsum_t* rhs;
  	uint32 end = shared_->numRules();
  	wsum_t cmp = 0;
  	do {
  		gen_  = shared_->generation();
  		rhs   = shared_->upper();
  		upper_= rhs[level_];
  		for (uint32 i = level_; i != end && (cmp = sum_[i]-rhs[i]) == 0; ++i) { ; }
  	} while (gen_ != shared_->generation());
  	if (s.numFreeVars() != 0) { sum_[0] = -1; }
  	if (cmp < wsum_t(!shared_->checkNext())) {
  		return true;
  	}
  	next_ = 1;
  	s.setStopConflict();
   	return false;
  }
  // Sets the current sum as the current shared optimum.
  bool UncoreMinimize::handleModel(Solver& s) {
  	if (!valid(s))  { return false; }
  	if (sum_[0] < 0){ computeSum(s);}
  	shared_->setOptimum(sum_);
  	next_ = shared_->checkNext();
  	gen_  = shared_->generation();
  	upper_= shared_->upper(level_);
  	POTASSCO_ASSERT(!next_ || disj_ || todo_.shrink() || nextW_ || lower_ == sum_[level_], "Unexpected lower bound on model!");
  	return true;
  }
  
  // Tries to recover from either a model or a root-level conflict.
  bool UncoreMinimize::handleUnsat(Solver& s, bool up, LitVec&) {
  	assert(s.hasConflict());
  	if (enum_) { enum_->relaxBound(true); }
  	bool trimCore = options_.trim != 0u;
  	do {
  		if (next_ == 0) {
  			if (s.hasStopConflict()) { return false; }
  			if (todo_.shrink()) {
  				lower_ -= todo_.weight();
  				todo_.clear(false);
  			}
  			uint32 cs = analyze(s);
  			if (!cs) {
  				todo_.clear();
  				return false;
  			}
  			lower_ += todo_.weight();
  			if (disj_) { // preprocessing: remove assumptions and remember core
  				todo_.terminate(); // null-terminate core
  				for (Todo::const_iterator it = todo_.end() - (cs + 1); it->id; ++it) {
  					getData(it->id).assume = 0;
  				}
  			}
  			else if (trimCore && validLowerBound() && todo_.shrinkNext(*this, value_false)) {
  				popPath(s, 0);
  			}
  			else {
  				resetTrim(s);
  			}
  			next_ = !validLowerBound();
  			if (up && shared_->incLower(level_, lower_) == lower_) {
  				reportLower(s, level_, lower_);
  			}
  		}
  		else {
  			s.clearStopConflict();
  			addNext(s);
  		}
  	} while (next_ || s.hasConflict());
  	return true;
  }
  
  bool UncoreMinimize::addNext(Solver& s) {
  	popPath(s, 0);
  	const wsum_t cmp = (lower_ - upper_);
  	if (disj_) {
  		for (Todo::const_iterator it = todo_.begin(), end = todo_.end(), cs; (cs = it) != end; ++it) {
  			weight_t w = std::numeric_limits<weight_t>::max();
  			while (it->id) { w = std::min(w, getData(it->id).weight); ++it; }
  			if (!addCore(s, &*cs, uint32(it - cs), w, false)) { break; }
  		}
  		todo_.clear(false);
  	}
  	else if (todo_.shrink() && (!todo_.shrinkNext(*this, value_true) || cmp >= 0)) {
  		resetTrim(s);
  	}
  	next_ = 0;
  	disj_ = 0;
  	if (cmp >= 0) {
  		fixLevel(s);
  		if (cmp > 0) { s.hasConflict() || s.force(~tag_, Antecedent(0)); }
  		else if (level_ != shared_->maxLevel() || shared_->checkNext()) {
  			initLevel(s);
  		}
  	}
  	else if (!todo_.shrink() && nextW_) {
  		actW_ = nextW_;
  		disj_ = options_.hasOption(OptParams::usc_disjoint);
  	}
  	return !s.hasConflict();
  }
  
  // Analyzes the current root level conflict and stores the set of our assumptions
  // that caused the conflict in todo_.
  uint32 UncoreMinimize::analyze(Solver& s) {
  	uint32 cs    = 0;
  	uint32 minDL = s.decisionLevel();
  	if (!conflict_.empty()) {
  		LitPair p(conflict_[0], conflict_[1].rep());
  		assert(s.isTrue(p.lit));
  		todo_.add(p, getData(p.id).weight);
  		minDL = s.level(p.lit.var());
  		cs = 1;
  	}
  	conflict_.clear();
  	if (s.decisionLevel() <= eRoot_) {
  		return cs;
  	}
  	s.resolveToCore(conflict_);
  	for (LitVec::const_iterator it = conflict_.begin(), end = conflict_.end(); it != end; ++it) {
  		s.markSeen(*it);
  	}
  	// map marked root decisions back to our assumptions
  	uint32 roots = sizeVec(conflict_), dl;
  	cs += roots;
  	for (LitSet::iterator it = assume_.begin(), end = assume_.end(); it != end && roots; ++it) {
  		Literal p = it->lit;
  		if (s.seen(p) && (dl = s.level(p.var())) > eRoot_ && dl <= aTop_) {
  			assert(p == s.decision(dl) && getData(it->id).assume);
  			if (dl < minDL) { minDL = dl; }
  			todo_.add(LitPair(~p, it->id), getData(it->id).weight);
  			assert(s.isFalse(~p));
  			s.clearSeen(p.var());
  			--roots;
  		}
  	}
  	popPath(s, minDL - (minDL != 0));
  	if (roots) { // clear remaining levels - can only happen if someone messed with our assumptions
  		cs -= roots;
  		for (LitVec::const_iterator it = conflict_.begin(), end = conflict_.end(); it != end; ++it) { s.clearSeen(it->var()); }
  	}
  	conflict_.clear();
  	return cs;
  }
  
  // Eliminates the given core by adding suitable constraints to the solver.
  bool UncoreMinimize::addCore(Solver& s, const LitPair* lits, uint32 cs, weight_t w, bool updateLower) {
  	assert(s.decisionLevel() == s.rootLevel());
  	assert(w && cs);
  	// apply weight and check for subcores
  	if (updateLower) { lower_ += w; }
  	for (uint32 i = 0; i != cs; ++i) {
  		LitData& x = getData(lits[i].id);
  		if ( (x.weight -= w) <= 0) {
  			x.assume = 0;
  			x.weight = 0;
  		}
  		else if (disj_ && !x.assume) {
  			x.assume = 1;
  			assume_.push_back(LitPair(~lits[i].lit, lits[i].id));
  		}
  		if (x.weight == 0 && hasCore(x)) {
  			Core& core = getCore(x);
  			temp_.start(core.bound + 1);
  			for (uint32 k = 0, end = core.size(); k != end; ++k) {
  				Literal p = core.at(k);
  				while (s.topValue(p.var()) != s.value(p.var()) && s.rootLevel() > eRoot_) {
  					s.popRootLevel(s.rootLevel() - std::max(s.level(p.var())-1, eRoot_));
  					aTop_ = std::min(aTop_, s.rootLevel());
  				}
  				temp_.add(s, p);
  			}
  			weight_t cw = core.weight;
  			if (!closeCore(s, x, temp_.bound <= 1) || !addOllCon(s, temp_, cw)) {
  				return false;
  			}
  		}
  	}
  	if (cs == 1) {
  		return fixLit(s, lits[0].lit);
  	}
  	// add new core
  	switch (options_.algo) {
  		default:
  		case OptParams::usc_oll: return addOll(s, lits, cs, w);
  		case OptParams::usc_one: return addK(s, cs, lits, cs, w);
  		case OptParams::usc_k:   return addK(s, options_.kLim, lits, cs, w);
  		case OptParams::usc_pmr: return addPmr(s, lits, cs, w);
  	}
  }
  bool UncoreMinimize::addOll(Solver& s, const LitPair* lits, uint32 size, weight_t w) {
  	temp_.start(2);
  	for (uint32 i = 0; i != size; ++i) { temp_.add(s, lits[i].lit); }
  	if (!temp_.unsat()) {
  		return addOllCon(s, temp_, w);
  	}
  	Literal fix = !temp_.lits.empty() ? temp_.lits[0].first : lits[0].lit;
  	return temp_.bound < 2 || fixLit(s, fix);
  }
  bool UncoreMinimize::addK(Solver& s, uint32 k, const LitPair* lits, uint32 size, weight_t w) {
  	const bool concise = options_.hasOption(OptParams::usc_succinct);
  	const int x = k ? (size + (k-1)) / k
  	            : size <= 8 ? 1
  	            : (int)std::ceil(size / (((std::log10(size)*16)-2)/2.0));
  	k = (size + (x-1)) / x;
  	uint32 idx = 1;
  	Literal cp = ~lits[0].lit, bin[2];
  	do {
  		uint32 n = k, connect = uint32((idx + k) < size);
  		if (!connect) {
  			n = size - idx;
  		}
  		weight_t B = static_cast<weight_t>(n + connect);
  		temp_.start(B);
  		temp_.add(s, cp);
  		for (uint32 i = 0; i != n; ++i) {
  			temp_.add(s, ~lits[idx++].lit);
  		}
  		if (connect) {
  			bin[0] = newLit(s);
  			temp_.add(s, ~bin[0]);
  			cp = bin[0];
  		}
  		for (uint32 i = 0, b = connect; i != n; ++i, b = 1) {
  			Literal ri = newAssumption(newLit(s), w).lit;
  			bin[b] = ri;
  			temp_.add(s, ~ri);
  			if (b) { // bin[0] -> bin[1];
  				addImplication(s, bin[0], bin[1], concise);
  				bin[0] = bin[1];
  			}
  		}
  		if (!addConstraint(s, temp_.begin(), temp_.size(), temp_.bound)) {
  			return false;
  		}
  	} while (idx != size);
  	if (!concise && !s.hasConflict()) {
  		typedef ClauseCreator::Result Result;
  		const uint32 flags = ClauseCreator::clause_explicit | ClauseCreator::clause_not_root_sat | ClauseCreator::clause_no_add;
  		for (uint32 i = 0; i != size; ++i)   { conflict_.push_back(lits[i].lit); }
  		for (uint32 i = 1; i <= eRoot_; ++i) { conflict_.push_back(~s.decision(i)); }
  		Result res = ClauseCreator::create(s, conflict_, flags, Constraint_t::Other);
  		if (res.local) { closed_.push_back(res.local); }
  		conflict_.clear();
  	}
  	return !s.hasConflict();
  }
  bool UncoreMinimize::addPmr(Solver& s, const LitPair* lits, uint32 size, weight_t w) {
  	assert(size > 1);
  	uint32 i   = size - 1;
  	Literal bp = lits[i].lit;
  	while (--i != 0) {
  		Literal an = lits[i].lit;
  		Literal bn = newLit(s);
  		Literal cn = newLit(s);
  		newAssumption(~cn, w);
  		if (!addPmrCon(comp_disj, s, bn, an, bp)) { return false; }
  		if (!addPmrCon(comp_conj, s, cn, an, bp)) { return false; }
  		bp = bn;
  	}
  	Literal an = lits[i].lit;
  	Literal cn = newLit(s);
  	newAssumption(~cn, w);
  	return addPmrCon(comp_conj, s, cn, an, bp);
  }
  bool UncoreMinimize::addPmrCon(CompType c, Solver& s, Literal head, Literal body1, Literal body2) {
  	typedef ClauseCreator::Result Result;
  	const uint32 flags = ClauseCreator::clause_explicit | ClauseCreator::clause_not_root_sat | ClauseCreator::clause_no_add;
  	const bool    sign = c == comp_conj;
  	uint32       first = 0, last = 3;
  	if (options_.hasOption(OptParams::usc_succinct)) {
  		first = c == comp_disj;
  		last  = first + (1 + (c == comp_disj));
  	}
  	Literal temp[3][3] = {
  		{ (~head)^ sign,   body1 ^ sign, body2 ^ sign },
  		{   head ^ sign, (~body1)^ sign, lit_false() },
  		{   head ^ sign, (~body2)^ sign, lit_false() }
  	};
  	for (uint32 i = first, sz = 3; i != last; ++i) {
  		Result res = ClauseCreator::create(s, ClauseRep::create(temp[i], sz, Constraint_t::Other), flags);
  		if (res.local) { closed_.push_back(res.local); }
  		if (!res.ok()) { return false; }
  		sz = 2;
  	}
  	return true;
  }
  bool UncoreMinimize::addOllCon(Solver& s, const WCTemp& wc, weight_t weight) {
  	typedef WeightConstraint::CPair ResPair;
  	weight_t B = wc.bound;
  	if (B <= 0) {
  		// constraint is sat and hence conflicting w.r.t new assumption -
  		// relax core
  		lower_ += ((1-B)*weight);
  		B       = 1;
  	}
  	if (static_cast<uint32>(B) > static_cast<uint32>(wc.lits.size())) {
  		// constraint is unsat and hence the new assumption is trivially satisfied
  		return true;
  	}
  	// create new var for this core
  	LitPair aux = newAssumption(newLit(s), weight);
  	WeightLitsRep rep = {const_cast<WCTemp&>(wc).begin(), wc.size(), B, (weight_t)wc.size()};
  	uint32       fset = WeightConstraint::create_explicit | WeightConstraint::create_no_add | WeightConstraint::create_no_freeze | WeightConstraint::create_no_share;
  	if (options_.hasOption(OptParams::usc_succinct)) { fset |= WeightConstraint::create_only_bfb; }
  	ResPair       res = WeightConstraint::create(s, ~aux.lit, rep, fset);
  	if (res.ok() && res.first()) {
  		getData(aux.id).coreId = allocCore(res.first(), B, weight, rep.bound != rep.reach);
  	}
  	return !s.hasConflict();
  }
  // Adds implication: a -> b either via a single watch on a or as a clause -a v b.
  bool UncoreMinimize::addImplication(Solver& s, Literal a, Literal b, bool concise) {
  	if (concise) {
  		POTASSCO_ASSERT(s.auxVar(a.var()));
  		s.addWatch(a, this, b.id());
  	}
  	else {
  		typedef ClauseCreator::Result Result;
  		const uint32 flags = ClauseCreator::clause_explicit | ClauseCreator::clause_not_root_sat | ClauseCreator::clause_no_add;
  		Literal clause[] = {~a, b};
  		Result res = ClauseCreator::create(s, ClauseRep::create(clause, 2, Constraint_t::Other), flags);
  		if (res.local) { closed_.push_back(res.local); }
  		if (!res.ok()) { return false; }
  	}
  	return true;
  }
  // Adds the cardinality constraint lits[0] + ... + lits[size-1] >= bound.
  bool UncoreMinimize::addConstraint(Solver& s, WeightLiteral* lits, uint32 size, weight_t bound) {
  	typedef WeightConstraint::CPair ResPair;
  	WeightLitsRep rep = {lits, size, bound, static_cast<weight_t>(size)};
  	const uint32 fset = WeightConstraint::create_explicit | WeightConstraint::create_no_add | WeightConstraint::create_no_freeze | WeightConstraint::create_no_share;
  	ResPair       res = WeightConstraint::create(s, lit_true(), rep, fset);
  	if (res.first()) {
  		closed_.push_back(res.first());
  	}
  	return res.ok();
  }
  
  // Computes the solver's initial root level, i.e. all assumptions that are not from us.
  uint32 UncoreMinimize::initRoot(Solver& s) {
  	if (eRoot_ == aTop_ && !s.hasStopConflict()) {
  		eRoot_ = s.rootLevel();
  		aTop_  = eRoot_;
  	}
  	return eRoot_;
  }
  
  // Assigns p at the solver's initial root level.
  bool UncoreMinimize::fixLit(Solver& s, Literal p) {
  	assert(s.decisionLevel() >= eRoot_);
  	if (s.decisionLevel() > eRoot_ && (!s.isTrue(p) || s.level(p.var()) > eRoot_)) {
  		// go back to root level
  		s.popRootLevel(s.rootLevel() - eRoot_);
  		aTop_ = s.rootLevel();
  	}
  	if (eRoot_ && s.topValue(p.var()) != trueValue(p)) { fix_.push_back(p); }
  	return !s.hasConflict() && s.force(p, this);
  }
  // Fixes any remaining assumptions of the active optimization level.
  bool UncoreMinimize::fixLevel(Solver& s) {
  	for (LitSet::iterator it = assume_.begin(), end = assume_.end(); it != end; ++it) {
  		if (getData(it->id).assume) { fixLit(s, it->lit); }
  	}
  	releaseLits();
  	return !s.hasConflict();
  }
  void UncoreMinimize::releaseLits() {
  	// remaining cores are no longer open - move to closed list
  	for (CoreTable::iterator it = open_.begin(), end = open_.end(); it != end; ++it) {
  		if (it->con) { closed_.push_back(it->con); }
  	}
  	open_.clear();
  	litData_.clear();
  	assume_.clear();
  	todo_.clear();
  	freeOpen_ = 0;
  }
  
  uint32 UncoreMinimize::allocCore(WeightConstraint* con, weight_t bound, weight_t weight, bool open) {
  	if (!open) {
  		closed_.push_back(con);
  		return 0;
  	}
  	if (freeOpen_) { // pop next slot from free list
  		uint32 fp = freeOpen_ - 1;
  		assert(open_[fp].con == 0 && open_[fp].bound == static_cast<weight_t>(0xDEADC0DE));
  		freeOpen_ = static_cast<uint32>(open_[fp].weight);
  		open_[fp] = Core(con, bound, weight);
  		return fp + 1;
  	}
  	open_.push_back(Core(con, bound, weight));
  	return static_cast<uint32>(open_.size());
  }
  bool UncoreMinimize::closeCore(Solver& s, LitData& x, bool sat) {
  	if (uint32 coreId = x.coreId) {
  		Core& core = open_[coreId-1];
  		x.coreId = 0;
  		// close by moving to closed list
  		if (!sat) { closed_.push_back(core.con); }
  		else { fixLit(s, core.tag()); core.con->destroy(&s, true); }
  		// link slot to free list
  		core      = Core(0, static_cast<weight_t>(0xDEADC0DE), static_cast<weight_t>(freeOpen_));
  		freeOpen_ = coreId;
  	}
  	return !s.hasConflict();
  }
  bool UncoreMinimize::pushTrim(Solver& s) {
  	assert(!s.hasConflict() && s.rootLevel() == aTop_ && conflict_.empty());
  	uint32 top = aTop_;
  	todo_.shrinkPush(*this, s);
  	if ((aTop_ = s.rootLevel()) != top && !s.hasConflict() && options_.tLim) {
  		struct Limit : public PostPropagator {
  			Limit(UncoreMinimize& s, uint64 lim) : self(&s), limit(lim) {}
  			uint32 priority() const { return priority_reserved_ufs + 2; }
  			bool propagateFixpoint(Clasp::Solver& s, Clasp::PostPropagator* ctx) {
  				if (ctx || s.stats.conflicts < limit) { return true; }
  				s.setStopConflict();
  				self->next_ = 1;
  				self = 0;
  				s.removePost(this);
  				return false;
  			}
  			void undoLevel(Solver& s) {
  				if (self) { s.removePost(this); }
  				this->destroy();
  			}
  			UncoreMinimize* self;
  			uint64 limit;
  		}*limit = new Limit(*this, s.stats.conflicts + (uint64(1) << options_.tLim));
  		s.addPost(limit);
  		s.addUndoWatch(aTop_, limit);
  	}
  	else if (s.hasStopConflict() && conflict_.size() == 2) {
  		assert(getData(conflict_[1].rep()).assume);
  		lower_ -= todo_.weight();
  		todo_.clear(true);
  		s.clearStopConflict();
  		conflict_.clear();
  		popPath(s, 0);
  		pushPath(s);
  	}
  	return !s.hasConflict();
  }
  void UncoreMinimize::resetTrim(Solver& s) {
  	if (todo_.size()) {
  		addCore(s, &*todo_.begin(), todo_.size(), todo_.weight(), false);
  		todo_.clear();
  	}
  }
  uint32  UncoreMinimize::Core::size()       const { return con->size() - 1; }
  Literal UncoreMinimize::Core::at(uint32 i) const { return con->lit(i+1, WeightConstraint::FFB_BTB); }
  Literal UncoreMinimize::Core::tag()        const { return con->lit(0, WeightConstraint::FTB_BFB); }
  void    UncoreMinimize::WCTemp::add(Solver& s, Literal p) {
  	if (s.topValue(p.var()) == value_free) { lits.push_back(WeightLiteral(p, 1)); }
  	else if (s.isTrue(p)) { --bound; }
  }
  void UncoreMinimize::Todo::clear(bool withShrink) {
  	lits_.clear();
  	minW_ = CLASP_WEIGHT_T_MAX;
  	if (withShrink) { shrinkReset(); }
  }
  void UncoreMinimize::Todo::shrinkReset() {
  	core_.clear();
  	last_ = next_ = step_ = 0;
  }
  void UncoreMinimize::Todo::terminate() {
  	lits_.push_back(LitPair(lit_true(), 0));
  	minW_ = CLASP_WEIGHT_T_MAX;
  }
  void UncoreMinimize::Todo::add(const LitPair& x, weight_t w) {
  	lits_.push_back(x);
  	if (w < minW_) { minW_ = w; }
  }
  void UncoreMinimize::Todo::shrinkPush(UncoreMinimize& self, Solver& s) {
  	const uint32 skip = step_ < sizeVec(core_) ? core_[step_].id : 0u;
  	uint32 n = next_;
  	for (Todo::const_iterator it = lits_.end(); n--;) {
  		const LitPair& x = *--it;
  		if (x.id != skip && !self.push(s, ~x.lit, x.id)) {
  			break;
  		}
  	}
  }
  bool UncoreMinimize::Todo::shrinkNext(UncoreMinimize& self, ValueRep result) {
  	if (self.options_.trim == OptParams::usc_trim_min) {
  		return subsetNext(self, result);
  	}
  	if (result == value_false) {
  		next_ = last_;
  		step_ = 0u;
  	}
  	else {
  		last_ = next_;
  	}
  	const uint32 t  = self.options_.trim;
  	const uint32 mx = size();
  	uint32 s = step_;
  	switch (t) {
  		default:
  		case OptParams::usc_trim_lin: step_ = s = 1;                break;
  		case OptParams::usc_trim_inv: step_ = s = (mx - next_) - 1; break;
  		case OptParams::usc_trim_rgs:
  			if      (s == 0u)          { step_ = s = uint32(last_ == 0u); }
  			else if ((next_ + s) > mx) { step_ = 2; s = 1; }
  			else                       { step_ = s * 2; }
  			break;
  		case OptParams::usc_trim_exp:
  			if      (s == 0u)          { s = step_ = uint32(last_ == 0u); }
  			else if ((next_ + s) < mx) { step_ = s * 2; }
  			else                       { s = (mx - next_) / 2; }
  			break;
  		case OptParams::usc_trim_bin: step_ = s = (mx - next_) / 2; break;
  	}
  	return s && (next_ += s) < mx;
  }
  bool UncoreMinimize::Todo::subsetNext(UncoreMinimize& self, ValueRep result) {
  	if      (result == value_true) { ++step_; }
  	else if (!core_.empty()) {
  		for (Todo::const_iterator it = lits_.begin(), end = lits_.end(); it != end; ++it) {
  			self.setFlag(it->id, true);
  		}
  		LitSet::iterator j = core_.begin();
  		uint32 marked = 0u;
  		for (LitSet::const_iterator it = j, s = j + step_, end = core_.end(); it != end; ++it) {
  			if (self.flagged(it->id)) {
  				self.setFlag(it->id, false);
  				++marked;
  				*j++ = *it;
  			}
  			else if (j < s) {
  				--s, --step_;
  			}
  		}
  		assert(marked == size());
  		core_.erase(j, core_.end());
  		next_ = marked;
  	}
  	else {
  		for (Todo::const_iterator it = lits_.end(), end = lits_.begin(); it != end;) { core_.push_back(*--it); }
  		step_ = 0;
  		next_ = size();
  	}
  	return step_ < size() && size() > 1;
  }
  } // end namespaces Clasp
  